Theory Derivations

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

chapter ‹Derivations›

theory Derivations imports Maximal_Consistent_Sets begin

lemma split_finite_sets:
  assumes ‹finite A› ‹finite B›
    and ‹A ⊆ B ∪ S›
  shows ‹∃B' C. finite C ∧ A = B' ∪ C ∧ B' = A ∩ B ∧ C ⊆ S›
  using assms subset_UnE by auto

lemma split_list:
  assumes ‹set A ⊆ set B ∪ S›
  shows ‹∃B' C. set (B' @ C) = set A ∧ set B' = set A ∩ set B ∧ set C ⊆ S›
  using assms split_finite_sets[where A=‹set A› and B=‹set B› and S=S]
  by (metis List.finite_set finite_Un finite_list set_append)

section ‹Derivations›

locale Derivations =
  fixes derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)
  assumes derive_assm [simp]: ‹⋀A p. p ∈ set A ⟹ A ⊢ p›
    and derive_set: ‹⋀A B r. A ⊢ r ⟹ set A = set B ⟹ B ⊢ r›
begin

theorem derive_split:
  assumes ‹set A ⊆ set B ∪ X› ‹A ⊢ p›
  shows ‹∃B' C. set B' = set A ∩ set B ∧ set C ⊆ X ∧ B' @ C ⊢ p›
  using assms derive_set split_list[where A=A and B=B] by metis

corollary derive_split1:
  assumes ‹set A ⊆ {q} ∪ X› ‹A ⊢ p› ‹q ∈ set A›
  shows ‹∃C. set C ⊆ X ∧ q # C ⊢ p›
  using assms derive_split[where A=A and X=X and B=‹[q]› and p=p] derive_set[where B=‹q # _›]
  by auto

end

section ‹MCSs and Explosion›

locale Derivations_MCS = MCS_Base consistent + Derivations derive
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50) +
  assumes consistent_underivable: ‹⋀S. consistent S ⟷ (∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢ q))›
begin

theorem MCS_explode:
  assumes ‹consistent S› ‹maximal S›
  shows ‹p ∉ S ⟷ (∃A. set A ⊆ S ∧ (∀q. p # A ⊢ q))›
proof safe
  assume ‹p ∉ S›
  then obtain B where B: ‹set B ⊆ {p} ∪ S› ‹p ∈ set B› ‹∀q. B ⊢ q›
    using assms unfolding consistent_underivable maximal_def by blast
  moreover have ‹set (p # removeAll p B) = set B›
    using B(2) by auto
  ultimately have ‹∀q. p # removeAll p B ⊢ q›
    using derive_set by metis
  then show ‹∃A. set A ⊆ S ∧ (∀q. p # A ⊢ q)›
    using B(1) by (metis Diff_subset_conv set_removeAll)
next
  fix A
  assume ‹set A ⊆ S› ‹∀q. p # A ⊢ q› ‹p ∈ S›
  then show False
    using assms unfolding consistent_underivable
    by (metis (no_types, lifting) insert_subsetI list.simps(15))
qed

end

section ‹MCSs and Derivability›

locale Derivations_Cut_MCS = Derivations_MCS consistent derive
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50) +
  assumes derive_cut: ‹⋀A B p q. A ⊢ p ⟹ p # B ⊢ q ⟹ A @ B ⊢ q›
begin

theorem MCS_derive:
  assumes ‹consistent S› ‹maximal S›
  shows ‹p ∈ S ⟷ (∃A. set A ⊆ S ∧ A ⊢ p)›
proof safe
  assume ‹p ∈ S›
  then show ‹∃A. set A ⊆ S ∧ A ⊢ p›
    using derive_assm by (metis List.set_insert empty_set empty_subsetI insert_subset singletonI)
next
  fix A
  assume A: ‹set A ⊆ S› ‹A ⊢ p›

  have bot: ‹∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢ q)›
    using assms(1) unfolding consistent_underivable by blast

  have ‹consistent ({p} ∪ S)›
    unfolding consistent_underivable
  proof safe
    fix B
    assume B: ‹set B ⊆ {p} ∪ S›
    show ‹∃q. ¬ B ⊢ q›
    proof (rule ccontr)
      assume *: ‹∄q. ¬ B ⊢ q›
      then have ‹∀q. B ⊢ q›
        by blast
      show False
      proof (cases ‹p ∈ set B›)
        case True
        then have ‹set (p # removeAll p B) = set B›
          by auto
        then have ‹∀q. p # removeAll p B ⊢ q›
          using ‹∀q. B ⊢ q› derive_set by blast
        then have ‹∀q. A @ removeAll p B ⊢ q›
          using A(2) derive_cut by blast
        moreover have ‹set (A @ removeAll p B) ⊆ S›
          using A(1) B by auto
        ultimately show False
          using bot by blast
      next
        case False
        then show False
          using * B bot by auto
      qed
    qed
  qed
  then show ‹p ∈ S›
    using assms unfolding maximal_def by auto
qed

end

section ‹Proof Rules›

locale Derivations_Bot = Derivations_Cut_MCS consistent derive
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50) +
  fixes bot :: 'fm (‹❙⊥›)
  assumes botE: ‹⋀A p. A ⊢ ❙⊥ ⟹ A ⊢ p›
begin

corollary MCS_botE [elim]:
  assumes ‹consistent S› ‹maximal S›
    and ‹❙⊥ ∈ S›
  shows ‹p ∈ S›
  using assms botE MCS_derive by blast

corollary MCS_bot [simp]:
  assumes ‹consistent S› ‹maximal S›
  shows ‹❙⊥ ∉ S›
  using assms botE MCS_derive consistent_underivable by blast

end

locale Derivations_Top = Derivations_Cut_MCS +
  fixes top (‹❙⊤›)
  assumes topI: ‹⋀A. A ⊢ ❙⊤›
begin

corollary MCS_topI [simp]:
  assumes ‹consistent S› ‹maximal S›
  shows ‹❙⊤ ∈ S›
  using assms topI MCS_derive by (metis empty_set empty_subsetI)

end

locale Derivations_Not = Derivations_Bot consistent derive bot
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)
    and bot :: 'fm (‹❙⊥›) +
  fixes not :: ‹'fm ⇒ 'fm› (‹❙¬›)
  assumes
    notI: ‹⋀A p. p # A ⊢ ❙⊥ ⟹ A  ⊢ ❙¬ p› and
    notE: ‹⋀A p. A ⊢ p ⟹ A ⊢ ❙¬ p ⟹ A ⊢ ❙⊥›
begin

corollary MCS_not_xor:
  assumes ‹consistent S› ‹maximal S›
  shows ‹p ∈ S ⟷ ❙¬ p ∉ S›
proof safe
  assume ‹p ∈ S› ‹❙¬ p ∈ S›
  then have ‹set [p, ❙¬ p] ⊆ S›
    by simp
  moreover have ‹[p, ❙¬ p] ⊢ ❙⊥›
    using notE derive_assm by (meson list.set_intros(1) list.set_intros(2))
  ultimately have ‹❙⊥ ∈ S›
    using assms MCS_derive by blast
  then show False
    using assms MCS_bot by blast
next
  assume *: ‹❙¬ p ∉ S›
  show ‹p ∈ S›
  proof (rule ccontr)
    assume ‹p ∉ S›
    then obtain A where A: ‹set A ⊆ S› ‹∀q. p # A ⊢ q›
      using assms MCS_explode by blast
    then have ‹p # A ⊢ ❙⊥›
      by fast
    then have ‹A ⊢ ❙¬ p›
      using notI by blast
    then have ‹❙¬ p ∈ S›
      using A(1) assms MCS_derive by blast
    then show False
      using * by blast
  qed
qed
    
corollary MCS_not_both:
  assumes ‹consistent S› ‹maximal S›
  shows ‹p ∉ S ∨ ❙¬ p ∉ S›
  using assms MCS_not_xor by blast

corollary MCS_not_neither:
  assumes ‹consistent S› ‹maximal S›
  shows ‹p ∈ S ∨ ❙¬ p ∈ S›
  using assms MCS_not_xor by blast

end

locale Derivations_Con = Derivations_Cut_MCS consistent derive
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)  +
  fixes con :: ‹'fm ⇒ 'fm ⇒ 'fm› (‹_ ❙∧ _›)
  assumes
    conI: ‹⋀A p q. A ⊢ p ⟹ A ⊢ q ⟹ A ⊢ (p ❙∧ q)› and
    conE: ‹⋀A p q r. A ⊢ (p ❙∧ q) ⟹ p # q # A ⊢ r ⟹ A ⊢ r›
begin

corollary MCS_conI [intro]:
  assumes ‹consistent S› ‹maximal S›
    and ‹p ∈ S› ‹q ∈ S›
  shows ‹(p ❙∧ q) ∈ S›
  using assms MCS_derive derive_assm conI
  by (metis (mono_tags, lifting) insert_subset list.set_intros(1) list.simps(15) set_subset_Cons)

corollary MCS_conE [dest]:
  assumes ‹consistent S› ‹maximal S›
    and ‹(p ❙∧ q) ∈ S›
  shows ‹p ∈ S ∧ q ∈ S›
proof -
  have ‹p # q # A ⊢ p› ‹p # q # A ⊢ q› for A
    using derive_assm by simp_all
  then show ?thesis
    using assms MCS_derive conE by blast
qed

corollary MCS_con:
  assumes ‹consistent S› ‹maximal S›
  shows ‹(p ❙∧ q) ∈ S ⟷ p ∈ S ∧ q ∈ S›
  using assms MCS_conI MCS_conE by blast

end

locale Derivations_Dis = Derivations_Cut_MCS consistent derive
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)  +
  fixes dis :: ‹'fm ⇒ 'fm ⇒ 'fm› (‹_ ❙∨ _›)
  assumes
    disI1: ‹⋀A p q. A ⊢ p ⟹ A ⊢ (p ❙∨ q)› and
    disI2: ‹⋀A p q. A ⊢ q ⟹ A ⊢ (p ❙∨ q)› and
    disE: ‹⋀A p q r. A ⊢ (p ❙∨ q) ⟹ p # A ⊢ r ⟹ q # A ⊢ r ⟹ A ⊢ r›
begin

corollary MCS_disI1 [intro]:
  assumes ‹consistent S› ‹maximal S›
    and ‹p ∈ S›
  shows ‹(p ❙∨ q) ∈ S›
  using assms disI1 MCS_derive by auto

corollary MCS_disI2 [intro]:
  assumes ‹consistent S› ‹maximal S›
    and ‹q ∈ S›
  shows ‹(p ❙∨ q) ∈ S›
  using assms disI2 MCS_derive by auto

corollary MCS_disE [elim]:
  assumes ‹consistent S› ‹maximal S›
    and ‹(p ❙∨ q) ∈ S›
  shows ‹p ∈ S ∨ q ∈ S›
proof (rule ccontr)
  have bot: ‹∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢ q)›
    using assms(1) unfolding consistent_underivable by blast

  assume ‹¬ (p ∈ S ∨ q ∈ S)›
  then obtain P Q where
    P: ‹set P ⊆ S› ‹∀r. p # P ⊢ r› and
    Q: ‹set Q ⊆ S› ‹∀r. q # Q ⊢ r›
    using assms MCS_explode by auto

  have ‹p # (p ❙∨ q) # Q ⊢ p›
    by simp
  then have ‹p # (p ❙∨ q) # Q @ P ⊢ r› for r
    using P derive_cut[of _ p] by (metis append_Cons)
  then have ‹p # (p ❙∨ q) # P @ Q ⊢ r› for r
    using derive_set[where B=‹p # (p ❙∨ q) # P @ Q›] by fastforce
  moreover have ‹q # (p ❙∨ q) # P ⊢ q›
    by simp
  then have ‹q # (p ❙∨ q) # P @ Q ⊢ r› for r
    using Q derive_cut[of _ q] by (metis append_Cons)
  moreover have ‹(p ❙∨ q) # P @ Q ⊢ (p ❙∨ q)›
    by simp
  ultimately have ‹(p ❙∨ q) # P @ Q ⊢ r› for r
    using disE by blast
  moreover have ‹set ((p ❙∨ q) # P @ Q) ⊆ S›
    using assms(3) P Q by simp
  ultimately show False
    using assms(1) unfolding consistent_underivable by blast
qed

corollary MCS_dis:
  assumes ‹consistent S› ‹maximal S›
  shows ‹(p ❙∨ q) ∈ S ⟷ p ∈ S ∨ q ∈ S›
  using assms MCS_disI1 MCS_disI2 MCS_disE by blast

end

locale Derivations_Imp = Derivations_Cut_MCS consistent derive
  for consistent :: ‹'fm set ⇒ bool›
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)  +
  fixes imp :: ‹'fm ⇒ 'fm ⇒ 'fm› (‹_ ❙→ _›)
  assumes
    impI: ‹⋀A p q. p # A ⊢ q ⟹ A ⊢ (p ❙→ q)› and
    impE: ‹⋀A p q. A ⊢ p ⟹ A ⊢ (p ❙→ q) ⟹ A ⊢ q›
begin

corollary MCS_impI [intro]:
  assumes ‹consistent S› ‹maximal S›
    and ‹p ∈ S ⟶ q ∈ S›
  shows ‹(p ❙→ q) ∈ S›
    using assms impI derive_assm MCS_derive MCS_explode
    by (metis insert_subset list.simps(15) subsetI)

corollary MCS_impE [dest]:
  assumes ‹consistent S› ‹maximal S›
    and ‹(p ❙→ q) ∈ S› ‹p ∈ S›
  shows ‹q ∈ S›
  using assms(3-4) impE MCS_derive[OF assms(1-2)] derive_assm
  by (metis insert_subset list.set_intros(1) list.simps(15) set_subset_Cons)

corollary MCS_imp:
  assumes ‹consistent S› ‹maximal S›
  shows ‹(p ❙→ q) ∈ S ⟷ (p ∈ S ⟶ q ∈ S)›
  using assms MCS_impI MCS_impE by blast

end

locale Derivations_Exi = MCS_Witness consistent witness params + Derivations_Cut_MCS consistent derive
  for consistent :: ‹'fm set ⇒ bool›
    and witness params
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)  +
  fixes exi :: ‹'fm ⇒ 'fm› (‹❙∃›)
    and inst :: ‹'t ⇒ 'fm ⇒ 'fm› (‹⟨_⟩›)
  assumes
    exi_witness: ‹⋀S S' p. MCS S ⟹ witness (❙∃p) S' ⊆ S ⟹ ∃t. ⟨t⟩p ∈ S› and
    exiI: ‹⋀A p t. A ⊢ ⟨t⟩p ⟹ A ⊢ ❙∃p›
begin

corollary MCS_exiI [intro]:
  assumes ‹consistent S› ‹maximal S›
    and ‹⟨t⟩p ∈ S›
  shows ‹❙∃p ∈ S›
  using assms MCS_derive exiI by blast

corollary MCS_exiE [dest]:
  assumes ‹consistent S› ‹maximal S› ‹witnessed S›
    and ‹❙∃p ∈ S›
  shows ‹∃t. ⟨t⟩p ∈ S›
  using assms exi_witness unfolding witnessed_def by blast

corollary MCS_exi:
  assumes ‹consistent S› ‹maximal S› ‹witnessed S›
  shows ‹❙∃p ∈ S ⟷ (∃t. ⟨t⟩p ∈ S)›
  using assms MCS_exiI MCS_exiE by blast

end

locale Derivations_Uni = MCS_Witness consistent witness params + Derivations_Not consistent derive bot not
  for consistent :: ‹'fm set ⇒ bool›
    and witness params
    and derive :: ‹'fm list ⇒ 'fm ⇒ bool› (infix ‹⊢› 50)
    and bot :: 'fm (‹❙⊥›)
    and not :: ‹'fm ⇒ 'fm› (‹❙¬›) +
  fixes uni :: ‹'fm ⇒ 'fm› (‹❙∀›)
    and inst :: ‹'t ⇒ 'fm ⇒ 'fm› (‹⟨_⟩›)
  assumes
    uni_witness: ‹⋀S S' p. MCS S ⟹ witness (❙¬ (❙∀p)) S' ⊆ S ⟹ ∃t. ❙¬ (⟨t⟩p) ∈ S› and
    uniE: ‹⋀A p t. A ⊢ ❙∀p ⟹ A ⊢ ⟨t⟩p›
begin

corollary MCS_uniE [dest]:
  assumes ‹consistent S› ‹maximal S›
    and ‹❙∀p ∈ S›
  shows ‹⟨t⟩p ∈ S›
  using assms MCS_derive uniE by blast

corollary MCS_uniI [intro]:
  assumes ‹consistent S› ‹maximal S› ‹witnessed S›
    and ‹∀t. ⟨t⟩p ∈ S›
  shows ‹❙∀p ∈ S›
proof (rule ccontr)
  assume ‹❙∀p ∉ S›
  then have ‹❙¬ (❙∀p) ∈ S›
    using assms MCS_not_xor by blast
  then have ‹∃t. ❙¬ (⟨t⟩p) ∈ S›
    using assms uni_witness unfolding witnessed_def by blast
  then show False
    using assms MCS_not_xor by blast
qed

corollary MCS_uni:
  assumes ‹consistent S› ‹maximal S› ‹witnessed S›
  shows ‹❙∀p ∈ S ⟷ (∀t. ⟨t⟩p ∈ S)›
  using assms MCS_uniI MCS_uniE by blast

end

end