Theory Derivations

(*
  Title:  Derivations and Maximal Consistent Sets
  Author: Asta Halkjær From
*)

chapter ‹Derivations›

theory Derivations imports Maximal_Consistent_Sets begin

section ‹Rearranging Assumptions›

locale Derivations =
  fixes derive :: 'a list  'a  bool
  assumes derive_struct: A B p. derive A p  set A  set B  derive B p
begin

theorem derive_split:
  assumes set A  set B  X derive A p
  shows C. set C  X  derive (B @ C) p
  using struct_split[where P=λA. derive A p] derive_struct assms by blast

corollary derive_split1:
  assumes set A  {q}  X derive A p
  shows C. set C  X  derive (q # C) p
  using assms derive_split[where B=[q]] by simp

end

section ‹MCSs and Deriving Falsity›

locale Derivations_MCS = Derivations + MCS_Base +
  fixes fls
  assumes consistent_derive_fls: S. consistent S = (S'. set S'  S  derive S' fls)
begin

theorem MCS_derive_fls:
  assumes consistent S maximal S
  shows p  S  (S'. set S'  S  derive (p # S') fls)
proof
  assume p  S
  then show S'. set S'  S  derive (p # S') fls
    using assms derive_split1 consistent_derive_fls unfolding maximal_def by metis
next
  assume S'. set S'  S  derive (p # S') fls
  then show p  S
    using assms consistent_derive_fls by fastforce
qed

end

section ‹MCSs and Derivability›

locale Derivations_MCS_Cut = Derivations_MCS +
  assumes derive_assm: A p. p  set A  derive A p
    and derive_cut: A B p q. derive A p  derive (p # B) q  derive (A @ B) q
begin

theorem MCS_derive:
  assumes consistent S maximal S
  shows p  S  (S'. set S'  S  derive S' p)
proof
  assume p  S
  then show S'. set S'  S  derive S' p
    using derive_assm by (metis List.set_insert empty_set empty_subsetI insert_subset singletonI)
next
  assume A. set A  S  derive A p
  then obtain A where A: set A  S derive A p
    by blast
  have consistent ({p}  S)
    unfolding consistent_derive_fls
  proof safe
    fix B
    assume B: set B  {p}  S derive B fls
    then obtain C where C: derive (p # C) fls set C  S
      using derive_split1 by blast
    then have derive (A @ C) fls
      using A derive_cut by blast
    then show False
      using A(1) B(1) C assms(1) consistent_derive_fls by simp
  qed
  then show p  S
    using assms unfolding maximal_def by auto
qed

end

end