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›
    using assms k epath_sdrop epath_Pre_sdrop by (metis (no_types, lifting) add.commute sdrop_add)
  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