Theory Completeness

```section ‹Completeness›

theory Completeness imports Prover Semantics begin

subsection ‹Hintikka Counter Model›

locale Hintikka =
fixes A B :: ‹fm set›
assumes
Basic: ‹❙‡P ts ∈ A ⟹ ❙‡P ts ∈ B ⟹ False› and
FlsA: ‹❙⊥ ∉ A› and
ImpA: ‹p ❙⟶ q ∈ A ⟹ p ∈ B ∨ q ∈ A› and
ImpB: ‹p ❙⟶ q ∈ B ⟹ p ∈ A ∧ q ∈ B› and
UniA: ‹❙∀p ∈ A ⟹ ∀t. ⟨t⟩p ∈ A› and
UniB: ‹❙∀p ∈ B ⟹ ∃t. ⟨t⟩p ∈ B›

abbreviation ‹M A ≡ ⟦❙#, ❙†, λP ts. ❙‡P ts ∈ A⟧›

lemma id_tm [simp]: ‹⦇❙#, ❙†⦈ t = t›
by (induct t) (auto cong: map_cong)

lemma size_sub_fm [simp]: ‹size (sub_fm s p) = size p›
by (induct p arbitrary: s) auto

theorem Hintikka_counter_model:
assumes ‹Hintikka A B›
shows ‹(p ∈ A ⟶ M A p) ∧ (p ∈ B ⟶ ¬ M A p)›
proof (induct p rule: wf_induct [where r=‹measure size›])
case 1
then show ?case ..
next
case (2 x)
then show ?case
proof (cases x; safe del: notI)
case Falsity
show ‹❙⊥ ∈ A ⟹ M A ❙⊥› ‹❙⊥ ∈ B ⟹ ¬ M A ❙⊥›
using Hintikka.FlsA assms by simp_all
next
case (Pre P ts)
show ‹❙‡P ts ∈ A ⟹ M A (❙‡P ts)› ‹❙‡P ts ∈ B ⟹ ¬ M A (❙‡P ts)›
using Hintikka.Basic assms by (auto cong: map_cong)
next
case (Imp p q)
show ‹p ❙⟶ q ∈ A ⟹ M A (p ❙⟶ q)› ‹p ❙⟶ q ∈ B ⟹ ¬ M A (p ❙⟶ q)›
using assms Hintikka.ImpA[of A B p q] Hintikka.ImpB[of A B p q] Imp 2 by auto
next
case (Uni p)
have ‹⟨t⟩p ∈ A ⟹ M A (⟨t⟩p)› ‹⟨t⟩p ∈ B ⟹ ¬ M A (⟨t⟩p)› for t
using Uni 2 by (metis fm.size(8) in_measure lessI less_add_same_cancel1 size_sub_fm)+
then show ‹❙∀p ∈ A ⟹ M A (❙∀p)› ‹❙∀p ∈ B ⟹ ¬ M A (❙∀p)›
using assms Hintikka.UniA[of A B p] Hintikka.UniB[of A B p] by auto
qed
qed

subsection ‹Escape Paths Form Hintikka Sets›

lemma sset_sdrop: ‹sset (sdrop n s) ⊆ sset s›
by (induct n arbitrary: s) (auto intro: stl_sset in_mono)

lemma epath_sdrop: ‹epath steps ⟹ epath (sdrop n steps)›
by (induct n) (auto elim: epath.cases)

lemma eff_preserves_Pre:
assumes ‹effStep ((A, B), r) ss› ‹(A', B') |∈| ss›
shows ‹(❙‡P ts [∈] A ⟹ ❙‡P ts [∈] A')› ‹❙‡P ts [∈] B ⟹ ❙‡P ts [∈] B'›
using assms by (induct r ‹(A, B)› rule: eff.induct) (auto split: if_splits)

lemma epath_eff:
assumes ‹epath steps› ‹effStep (shd steps) ss›
shows ‹fst (shd (stl steps)) |∈| ss›
using assms by (auto elim: epath.cases)

abbreviation ‹lhs s ≡ fst (fst s)›
abbreviation ‹rhs s ≡ snd (fst s)›
abbreviation ‹lhsd s ≡ lhs (shd s)›
abbreviation ‹rhsd s ≡ rhs (shd s)›

lemma epath_Pre_sdrop:
assumes ‹epath steps› shows
‹❙‡P ts [∈] lhs (shd steps) ⟹ ❙‡P ts [∈] lhsd (sdrop m steps)›
‹❙‡P ts [∈] rhs (shd steps) ⟹ ❙‡P ts [∈] rhsd (sdrop m steps)›
using assms eff_preserves_Pre
by (induct m arbitrary: steps) (simp; metis (no_types, lifting) epath.cases surjective_pairing)+

lemma Saturated_sdrop:
assumes ‹Saturated steps›
shows ‹Saturated (sdrop n steps)›
using assms unfolding Saturated_def saturated_def by (simp add: alw_iff_sdrop)

definition treeA :: ‹(sequent × rule) stream ⇒ fm set› where
‹treeA steps ≡ ⋃s ∈ sset steps. set (lhs s)›

definition treeB :: ‹(sequent × rule) stream ⇒ fm set› where
‹treeB steps ≡ ⋃s ∈ sset steps. set (rhs s)›

lemma treeA_snth: ‹p ∈ treeA steps ⟹ ∃n. p [∈] lhsd (sdrop n steps)›
unfolding treeA_def using sset_range[of steps] by simp

lemma treeB_snth: ‹p ∈ treeB steps ⟹ ∃n. p [∈] rhsd (sdrop n steps)›
unfolding treeB_def using sset_range[of steps] by simp

lemma treeA_sdrop: ‹treeA (sdrop n steps) ⊆ treeA steps›
unfolding treeA_def by (induct n) (simp, metis SUP_subset_mono order_refl sset_sdrop)

lemma treeB_sdrop: ‹treeB (sdrop n steps) ⊆ treeB steps›
unfolding treeB_def by (induct n) (simp, metis SUP_subset_mono order_refl sset_sdrop)

lemma enabled_ex_taken:
assumes ‹epath steps› ‹Saturated steps› ‹enabled r (fst (shd steps))›
shows ‹∃k. takenAtStep r (shd (sdrop k steps))›
using assms unfolding Saturated_def saturated_def UNIV_rules by (auto simp: ev_iff_sdrop)

lemma Hintikka_epath:
assumes ‹epath steps› ‹Saturated steps›
shows ‹Hintikka (treeA steps) (treeB steps)›
proof
fix P ts
assume ‹❙‡P ts ∈ treeA steps›
then obtain m where m: ‹❙‡P ts [∈] lhsd (sdrop m steps)›
using treeA_snth by auto

assume ‹❙‡P ts ∈ treeB steps›
then obtain k where k: ‹❙‡P ts [∈] rhsd (sdrop k steps)›
using treeB_snth by auto

let ?j = ‹m + k›
let ?jstep = ‹shd (sdrop ?j steps)›

have ‹❙‡P ts [∈] lhs ?jstep›
using assms m epath_sdrop epath_Pre_sdrop by (metis (no_types, lifting) sdrop_add)
moreover have ‹❙‡P ts [∈] rhs ?jstep›
ultimately have ‹enabled (Axiom P ts) (fst ?jstep)›
unfolding enabled_def by (metis eff.simps(2) prod.exhaust_sel)
then obtain j' where ‹takenAtStep (Axiom P ts) (shd (sdrop j' steps))›
using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
then have ‹eff (snd (shd (sdrop j' steps))) (fst (shd (sdrop j' steps))) = None›
using assms(1) epath_sdrop epath_eff
by (metis (no_types, lifting) eff.simps(2) epath.simps equalsffemptyD surjective_pairing)
then show False
using assms(1) epath_sdrop by (metis epath.cases option.discI)
next
show ‹❙⊥ ∉ treeA steps›
proof
assume ‹❙⊥ ∈ treeA steps›
then have ‹∃j. enabled FlsL (fst (shd (sdrop j steps)))›
unfolding enabled_def using treeA_snth by (metis eff.simps(3) prod.exhaust_sel sdrop_simps(1))
then obtain j where ‹takenAtStep FlsL (shd (sdrop j steps))› (is ‹takenAtStep _ (shd ?steps)›)
using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
then have ‹eff (snd (shd ?steps)) (fst (shd ?steps)) = None›
using assms(1) epath_sdrop epath_eff
by (metis (no_types, lifting) eff.simps(3) epath.simps equalsffemptyD surjective_pairing)
then show False
using assms(1) epath_sdrop by (metis epath.cases option.discI)
qed
next
fix p q
assume ‹p ❙⟶ q ∈ treeA steps›
then have ‹∃k. enabled (ImpL p q) (fst (shd (sdrop k steps)))›
unfolding enabled_def using treeA_snth by (metis eff.simps(5) prod.exhaust_sel sdrop_simps(1))
then obtain j where ‹takenAtStep (ImpL p q) (shd (sdrop j steps))› (is ‹takenAtStep _ (shd ?s)›)
using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
then have ‹fst (shd (stl ?s)) |∈|
{| (lhsd ?s [÷] (p ❙⟶ q), p # rhsd ?s), (q # lhsd ?s [÷] (p ❙⟶ q), rhsd ?s) |}›
using assms(1) epath_sdrop epath_eff
by (metis (no_types, lifting) eff.simps(5) epath.cases option.distinct(1) prod.collapse)
then have ‹p [∈] rhs (shd (stl ?s)) ∨ q [∈] lhs (shd (stl ?s))›
by auto
then have ‹p ∈ treeB (stl ?s) ∨ q ∈ treeA (stl ?s)›
unfolding treeA_def treeB_def by (meson UN_I shd_sset)
then show ‹p ∈ treeB steps ∨ q ∈ treeA steps›
using treeA_sdrop treeB_sdrop by (metis sdrop_simps(2) subsetD)
next
fix p q
assume ‹p ❙⟶ q ∈ treeB steps›
then have ‹∃k. enabled (ImpR p q) (fst (shd (sdrop k steps)))›
unfolding enabled_def using treeB_snth by (metis eff.simps(6) prod.exhaust_sel sdrop_simps(1))
then obtain j where ‹takenAtStep (ImpR p q) (shd (sdrop j steps))› (is ‹takenAtStep _ (shd ?s)›)
using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
then have ‹fst (shd (stl ?s)) |∈| {| (p # lhsd ?s, q # rhsd ?s [÷] (p ❙⟶ q)) |}›
using assms(1) epath_sdrop epath_eff
by (metis (no_types, lifting) eff.simps(6) epath.cases option.distinct(1) prod.collapse)
then have ‹p [∈] lhs (shd (stl ?s)) ∧ q [∈] rhs (shd (stl ?s))›
by auto
then have ‹p ∈ treeA (stl ?s) ∧ q ∈ treeB (stl ?s)›
unfolding treeA_def treeB_def by (meson UN_I shd_sset)
then show ‹p ∈ treeA steps ∧ q ∈ treeB steps›
using treeA_sdrop treeB_sdrop by (metis sdrop_simps(2) subsetD)
next
fix p
assume *: ‹❙∀p ∈ treeA steps›
show ‹∀t. ⟨t⟩p ∈ treeA steps›
proof
fix t
from * have ‹∃k. enabled (UniL t p) (fst (shd (sdrop k steps)))›
unfolding enabled_def using treeA_snth by (metis eff.simps(7) prod.exhaust_sel sdrop_simps(1))
then obtain j where ‹takenAtStep (UniL t p) (shd (sdrop j steps))›(is ‹takenAtStep _ (shd ?s)›)
using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
then have ‹fst (shd (stl ?s)) |∈| {| (⟨t⟩p # lhsd ?s, rhsd ?s) |}›
using assms(1) epath_sdrop epath_eff
by (metis (no_types, lifting) eff.simps(7) epath.cases option.distinct(1) prod.collapse)
then have ‹⟨t⟩p [∈] lhs (shd (stl ?s))›
by auto
then have ‹⟨t⟩p ∈ treeA (stl ?s)›
unfolding treeA_def by (meson UN_I shd_sset)
then show ‹⟨t⟩p ∈ treeA steps›
using treeA_sdrop by (metis sdrop_simps(2) subsetD)
qed
next
fix p
assume *: ‹❙∀p ∈ treeB steps›
then have ‹∃k. enabled (UniR p) (fst (shd (sdrop k steps)))›
unfolding enabled_def using treeB_snth by (metis eff.simps(8) prod.exhaust_sel sdrop_simps(1))
then obtain j where ‹takenAtStep (UniR p) (shd (sdrop j steps))›(is ‹takenAtStep _ (shd ?s)›)
using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
then have ‹fst (shd (stl ?s)) |∈|
{| (lhsd ?s, ⟨❙#(fresh (lhsd ?s @ rhsd ?s))⟩p # rhsd ?s [÷] ❙∀p) |}›
using assms(1) epath_sdrop epath_eff
by (metis (no_types, lifting) eff.simps(8) epath.cases option.distinct(1) prod.collapse)
then have ‹∃t. ⟨t⟩p [∈] rhs (shd (stl ?s))›
by auto
then have ‹∃t. ⟨t⟩p ∈ treeB (stl ?s)›
unfolding treeB_def by (meson UN_I shd_sset)
then show ‹∃t. ⟨t⟩p ∈ treeB steps›
using treeB_sdrop by (metis sdrop_simps(2) subsetD)
qed

subsection ‹Completeness›

lemma fair_stream_rules: ‹Fair_Stream.fair rules›
unfolding rules_def using fair_stream surj_rule_of_nat .

lemma fair_rules: ‹fair rules›
using fair_stream_rules unfolding Fair_Stream.fair_def fair_def alw_iff_sdrop ev_holds_sset
by (metis dual_order.refl le_Suc_ex sdrop_snth snth_sset)

lemma epath_prover:
fixes A B :: ‹fm list›
defines ‹t ≡ prover (A, B)›
shows ‹(fst (root t) = (A, B) ∧ wf t ∧ tfinite t) ∨
(∃steps. fst (shd steps) = (A, B) ∧ epath steps ∧ Saturated steps)› (is ‹?A ∨ ?B›)
proof -
{ assume ‹¬ ?A›
with assms have ‹¬ tfinite (mkTree rules (A, B))›
unfolding prover_def using wf_mkTree fair_rules by simp
then obtain steps where ‹ipath (mkTree rules (A, B)) steps› using Konig by blast
with assms have ‹fst (shd steps) = (A, B) ∧ epath steps ∧ Saturated steps›
by (metis (no_types, lifting) fair_rules UNIV_I fst_conv ipath.cases
ipath_mkTree_Saturated mkTree.simps(1) wf_ipath_epath wf_mkTree)
then have ?B by blast
}
then show ?thesis by blast
qed

lemma epath_countermodel:
assumes ‹fst (shd steps) = (A, B)› ‹epath steps› ‹Saturated steps›
shows ‹∃(E :: _ ⇒ tm) F G. ¬ sc (E, F, G) (A, B)›
proof -
have ‹Hintikka (treeA steps) (treeB steps)› (is ‹Hintikka ?A ?B›)
using assms Hintikka_epath assms by simp
moreover have ‹∀p [∈] A. p ∈ ?A› ‹∀p [∈] B. p ∈ ?B›
using assms shd_sset unfolding treeA_def treeB_def by fastforce+
ultimately have ‹∀p [∈] A. M ?A p› ‹∀p [∈] B. ¬ M ?A p›
using Hintikka_counter_model assms by blast+
then show ?thesis
by auto
qed

theorem prover_completeness:
assumes ‹∀(E :: _ ⇒ tm) F G. sc (E, F, G) (A, B)›
defines ‹t ≡ prover (A, B)›
shows ‹fst (root t) = (A, B) ∧ wf t ∧ tfinite t›
using assms epath_prover epath_countermodel by blast

corollary
assumes ‹∀(E :: _ ⇒ tm) F G. ⟦E, F, G⟧ p›
defines ‹t ≡ prover ([], [p])›
shows ‹fst (root t) = ([], [p]) ∧ wf t ∧ tfinite t›
using assms prover_completeness by simp

end
```