Theory Sema_Craig

subsection‹Craig Interpolation using Semantics›

theory Sema_Craig
imports Substitution_Sema
begin

text‹Semantic proof of Craig interpolation following Harrison~\<^cite>‹"harrison2009handbook"›.›
  
(* we don't really need this lemma, sledgehammer would find a proof anyway. But it would be massively ugly. *)
lemma subst_true_false:
  assumes "𝒜 ⊨ F"
  shows "𝒜 ⊨ ((F[⊤ / n]) ❙∨ (F[⊥ / n]))"
using assms by(cases "𝒜 n"; simp add: substitution_lemma fun_upd_idem)

theorem interpolation:
  assumes "⊨ Γ ❙→ Δ"
  obtains ρ where
    "⊨ Γ ❙→ ρ" "⊨ ρ ❙→ Δ"
    "atoms ρ ⊆ atoms Γ"
    "atoms ρ ⊆ atoms Δ"
proof(goal_cases)
  let ?as = "atoms Γ - atoms Δ"
  have fas: "finite ?as" by simp
  from fas assms have "∃ρ. ((⊨ Γ ❙→ ρ) ∧ (⊨ ρ ❙→ Δ) ∧ (atoms ρ ⊆ atoms Γ) ∧ (atoms ρ ⊆ atoms Δ))"
  proof(induction ?as arbitrary: Γ rule: finite_induct)
    case empty
    from ‹{} = atoms Γ - atoms Δ› have "atoms Γ ⊆ atoms Δ" by blast
    with ‹⊨ Γ ❙→ Δ› show ?case by(intro exI[where x=Γ]) simp
  next
    case (insert a A)
    hence e: "a ∈ atoms Γ" "a ∉ atoms Δ" by auto
    define Γ' where "Γ' = (Γ[⊤ / a]) ❙∨ (Γ[⊥ / a])"
    have su: "atoms Γ' ⊆ atoms Γ" unfolding Γ'_def by(cases "a ∈ atoms Γ"; simp add: subst_atoms)
    from ‹⊨ Γ ❙→ Δ› e have "⊨ Γ' ❙→ Δ" by (auto simp add: substitution_lemma Γ'_def)
    from ‹a ▹ A = atoms Γ - atoms Δ› ‹a ∉ A› e have "A = atoms Γ' - atoms Δ" by(simp add: subst_atoms Γ'_def) blast
    from insert.hyps(3)[OF this ‹⊨ Γ' ❙→ Δ›] obtain ρ where ρ: "⊨ Γ' ❙→ ρ" "⊨ ρ ❙→ Δ" "atoms ρ ⊆ atoms Γ'" "atoms ρ ⊆ atoms Δ" by clarify
    have "⊨ Γ ❙→ ρ" using ρ(1) subst_true_false unfolding Γ'_def by fastforce
    with ρ su show ?case by(intro exI[where x=ρ]) simp
  qed
  moreover case 1
  ultimately show thesis by blast
qed
  
text‹The above proof is constructive, and it is actually very easy to write a procedure down.›
function interpolate where
"interpolate F H = (
let K = atoms F - atoms H in
  if K = {}
  then F
  else (
    let k = Min K
    in interpolate ((F[⊤ / k]) ❙∨ (F[⊥ / k])) H
  )
)" by pat_completeness simp
(* I tried Inf instead of Min first. Only has downsides. *)

text‹Showing termination is slightly technical\dots›
termination interpolate
  apply(relation "measure (λ(F,H). card (atoms F - atoms H))") 
              (* "measure (λ(F,H). card (atoms F))" also works, but doesn't make things more beautiful *)
   subgoal by simp
  apply (simp add: subst_atoms_simp)
  apply(intro conjI impI)
   apply(intro psubset_card_mono)
    subgoal by simp
   apply(subgoal_tac "Min (atoms F - atoms H) ∉ atoms H")
    subgoal by blast
   apply (meson atoms_finite Diff_eq_empty_iff Diff_iff Min_in finite_Diff)+
done

text‹Surprisingly, @{const interpolate} is even executable,
  despite all the set operations involving @{const atoms}›
lemma "interpolate (And (Atom (0::nat)) (Atom 1)) (Or (Atom 1) (Atom 2)) = 
  (⊤ ❙∧ Atom 1) ❙∨ (⊥ ❙∧ Atom 1)" by simp
value[code] "simplify_consts (interpolate (And (Atom (0::nat)) (Atom 1)) (Or (Atom 1) (Atom 2)))"
(* and the wikipedia example: *)
lemma "let P = Atom (0 :: nat); Q = Atom 1; R = Atom 2; T = Atom 3;
φ = (❙¬(P ❙∧ Q)) ❙→ (❙¬R ❙∧ Q);
ψ = (T ❙→ P) ❙∨ (T ❙→ (❙¬R));
I = interpolate φ ψ in
(size I) = 23 ∧ simplify_consts I = Atom 2 ❙→ Atom 0"
  by code_simp

theorem nonexistential_interpolation:
  assumes "⊨ F ❙→ H"
  shows
    "⊨ F ❙→ interpolate F H" (is "?t1") "⊨ interpolate F H ❙→ H" (is "?t2")
    "atoms (interpolate F H) ⊆ atoms F ∩ atoms H" (is "?s")
proof -
  let ?as = "atoms F - atoms H"
  have fas: "finite ?as" by simp
  hence "?t1 ∧ ?t2 ∧ ?s" using assms
  proof(induction "card ?as" arbitrary: F H)
    case (Suc n)
    let ?inf = "Min (atoms F - atoms H)"
    define G where "G = (F[⊤ / ?inf]) ❙∨ (F[⊥ / ?inf])"
    have e: "Min (atoms F - atoms H) ∈ atoms F - atoms H" by (metis Min_in Suc.hyps(2) Suc.prems(1) card.empty nat.simps(3))
    with Suc(2) have "n = card (atoms G - atoms H)" unfolding G_def subst_atoms_simp
    proof -
      assume a1: "Suc n = card (atoms F - atoms H)"
      assume "Min (atoms F - atoms H) ∈ atoms F - atoms H"
      hence a2: "Min (atoms F - atoms H) ∈ atoms F ∧ Min (atoms F - atoms H) ∉ atoms H" by simp
      have "n = card (atoms F - atoms H) - 1"
        using a1 by presburger
      hence "n = card (atoms (F[⊤ / Min (atoms F - atoms H)]) ∪ atoms (F[⊥ / Min (atoms F - atoms H)]) - atoms H)"
        using a2 by (metis (full_types) formula.set(2) Diff_insert Diff_insert2 Suc.prems(1) Un_absorb Un_empty_right card_Diff_singleton e subst_atoms top_atoms_simp)
        (* you need to tell sledgehammer about formula.set if you want it to find a proof here… *)
      thus "n = card (atoms ((F[⊤ / Min (atoms F - atoms H)]) ❙∨ (F[⊥ / Min (atoms F - atoms H)])) - atoms H)" by simp
    qed
    moreover have "finite (atoms G - atoms H)" "⊨ G ❙→ H" using Suc(3-) e
      by(auto simp: G_def substitution_lemma)
    ultimately have IH: "⊨ G ❙→ interpolate G H" "⊨ interpolate G H ❙→ H" 
        "atoms (interpolate G H) ⊆ atoms G ∩ atoms H" using Suc by blast+
    moreover have "⊨ F ❙→ G" unfolding G_def 
      using subst_true_false by fastforce
    moreover { (* sledgehammer… *)
        assume a1: "atoms (interpolate ((F[⊤/Min (atoms F - atoms H)]) ❙∨ (F[⊥/Min (atoms F - atoms H)])) H) ⊆ atoms (F[⊤/Min (atoms F - atoms H)]) ∪ atoms (F[⊥/Min (atoms F - atoms H)]) ∧ atoms (interpolate ((F[⊤/Min (atoms F - atoms H)]) ❙∨ (F[⊥/Min (atoms F - atoms H)])) H) ⊆ atoms H"
        have f2: "atoms ((⊥::'a formula) ❙→ ⊥) = atoms ⊥"
          by simp
        then have f3: "atoms F - {Min (atoms F - atoms H)} = atoms (F[⊤/Min (atoms F - atoms H)])"
          by (metis (no_types) DiffD1 Top_def Un_empty_right e formula.simps(91) subst_atoms)
        have "atoms (F[⊥/Min (atoms F - atoms H)]) = atoms (F[⊤/Min (atoms F - atoms H)])"
          using f2 by (metis (no_types) DiffD1 Top_def e subst_atoms)
        then have "¬ atoms F ⊆ atoms H ⟶ atoms (interpolate ((F[⊤/Min (atoms F - atoms H)]) ❙∨ (F[⊥/Min (atoms F - atoms H)])) H) ⊆ atoms F"
          using f3 a1 by blast
    } ultimately show ?case
      by (intro conjI; subst interpolate.simps; simp del: interpolate.simps add: Let_def G_def; blast?)
  qed auto
  thus "?t1" "?t2" "?s" by simp_all
qed
text‹So no, the proof is by no means easier this way.
  Admittedly, part of the fuzz is due to @{const Min},
  but replacing atoms with something that returns lists doesn't make it better.›
    

end