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. tp  A and
    UniB: p  B  t. tp  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 tp  A  M A (tp) tp  B  ¬ M A (tp) 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. tp  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)) |∈| {| (tp # 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 tp [∈] lhs (shd (stl ?s))
      by auto
    then have tp  treeA (stl ?s)
      unfolding treeA_def by (meson UN_I shd_sset)
    then show tp  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. tp [∈] rhs (shd (stl ?s))
    by auto
  then have t. tp  treeB (stl ?s)
    unfolding treeB_def by (meson UN_I shd_sset)
  then show t. tp  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