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