Theory SC_Sema

subsubsection‹Soundness, Completeness›

theory SC_Sema
imports SC Sema
begin

definition sequent_semantics :: "'a valuation ⇒ 'a formula multiset ⇒ 'a formula multiset ⇒ bool" (‹(_ ⊨ (_ ⇒/ _))› [53, 53,53] 53) where
"𝒜 ⊨ Γ ⇒ Δ ≡ (∀γ ∈# Γ. 𝒜 ⊨ γ) ⟶ (∃δ ∈# Δ. 𝒜 ⊨ δ)"
abbreviation sequent_valid :: "'a formula multiset ⇒ 'a formula multiset ⇒ bool" (‹(⊨ (_ ⇒/ _))› [53,53] 53) where
"⊨ Γ ⇒ Δ ≡ ∀A. A ⊨ Γ ⇒ Δ"
abbreviation sequent_nonvalid :: "'a valuation ⇒ 'a formula multiset ⇒ 'a formula multiset ⇒ bool" (‹(_ ¬⊨ (_ ⇒/ _))› [53, 53,53] 53) where
"𝒜 ¬⊨ Γ ⇒ Δ ≡ ¬𝒜⊨ Γ ⇒ Δ"

lemma sequent_intuitonistic_semantics: "⊨ Γ ⇒ {#δ#} ⟷ set_mset Γ ⊫ δ"
  unfolding sequent_semantics_def entailment_def by simp

lemma SC_soundness: "Γ ⇒ Δ ⟹ ⊨ Γ ⇒ Δ"
  by(induction rule: SCp.induct) (auto simp add: sequent_semantics_def)

definition "sequent_cost Γ Δ = Suc (sum_list (sorted_list_of_multiset (image_mset size (Γ + Δ))))"

function(sequential)
  sc :: "'a formula list ⇒ 'a list ⇒ 'a formula list ⇒ 'a list ⇒ ('a list × 'a list) set" where
"sc (⊥ # Γ) A Δ B = {}" |
"sc [] A [] B = (if set A ∩ set B = {} then {(remdups A,remdups B)} else {})" |
"sc (Atom k # Γ) A  Δ B = sc Γ (k#A) Δ B" |
"sc (Not F # Γ) A Δ B = sc Γ A (F#Δ) B" |
"sc (And F G # Γ) A Δ B = sc (F#G#Γ) A Δ B" |
"sc (Or F G # Γ) A Δ B = sc (F#Γ) A Δ B ∪ sc (G#Γ) A Δ B" |
"sc (Imp F G # Γ) A Δ B = sc Γ A (F#Δ) B ∪ sc (G#Γ) A Δ B" |
"sc Γ A (⊥#Δ) B = sc Γ A Δ B" |
"sc Γ A (Atom k # Δ) B = sc Γ A Δ (k#B)" |
"sc Γ A (Not F # Δ) B = sc (F#Γ) A Δ B" |
"sc Γ A (And F G # Δ) B = sc Γ A (F#Δ) B ∪ sc Γ A (G#Δ) B" |
"sc Γ A (Or F G # Δ) B = sc Γ A (F#G#Δ) B" |
"sc Γ A (Imp F G # Δ) B = sc (F#Γ) A (G#Δ) B"
  by pat_completeness auto
(* Paremeters 2 and 4:
   atoms are stored in lists, not sets, simply because lists are automatically finite;
   finiteness is required when we relate back to sequents, which are finite. *)

definition "list_sequent_cost Γ Δ = 2*sum_list (map size (Γ@Δ)) + length (Γ@Δ)"
termination sc by (relation "measure (λ(Γ,A,Δ,B). list_sequent_cost Γ Δ)") (simp_all add: list_sequent_cost_def)

lemma "sc [] [] [((Atom 0 ❙→ Atom 1) ❙→ Atom 0) ❙→ Atom 1] [] = {([0], [1 :: nat])}"
  (* An atom may appear twice in one of the lists, but that is of no concern. 
     Using sets for the atoms stands in the way of automation. *)
by code_simp

lemma sc_sim:
  fixes Γ Δ :: "'a formula list" and G D :: "'a list"
  assumes "sc Γ A Δ B = {}"
  shows "image_mset Atom (mset A) + mset Γ ⇒ image_mset Atom (mset B) + mset Δ"
proof -
  have *[simp]: "image_mset Atom (mset A) ⇒ image_mset Atom (mset B)" (is ?k) if "k ∈ set A" "k ∈ set B" for A B :: "'a list" and k
  proof -
    from that obtain a where "a ∈ set A" "a ∈ set B" by blast
    thus ?k by(force simp: in_image_mset intro: SCp.Ax[where k=a])
  qed
  from assms show ?thesis
    by(induction rule: sc.induct[where 'a='a]) (auto
        simp add: list_sequent_cost_def add.assoc Bot_delR_simp
        split: if_splits option.splits 
        intro: SCp.intros(3-))
qed

lemma scc_ce_distinct:
  "(C,E) ∈ sc Γ G Δ D ⟹ set C ∩ set E = {}"
by(induction Γ G Δ D arbitrary: C E rule: sc.induct)
  (fastforce split: if_splits)+

text‹Completeness set aside, this is an interesting fact on the side: Sequent Calculus can provide counterexamples.›
theorem SC_counterexample:
  "(C,D) ∈ sc Γ A Δ B ⟹
  (λa. a ∈ set C) ¬⊨ image_mset Atom (mset A) + mset Γ ⇒ image_mset Atom (mset B) + mset Δ"
by(induction rule: sc.induct[where 'a='a]; 
   simp add: sequent_semantics_def split: if_splits; 
   (* used to be only for one, now it's four… *) blast)

corollary SC_counterexample':
  assumes "(C,D) ∈ sc Γ [] Δ []"
  shows "(λk. k ∈ set C) ¬⊨ mset Γ ⇒ mset Δ"
using SC_counterexample[OF assms] by simp

theorem SC_sound_complete: "Γ ⇒ Δ ⟷ ⊨ Γ ⇒ Δ"
proof
  assume "Γ ⇒ Δ" thus "⊨ Γ ⇒ Δ" using SC_soundness by blast
next
  obtain Γ' Δ' where [simp]: "Γ = mset  Γ'" "Δ = mset Δ'" by (metis ex_mset)
  assume "⊨ Γ ⇒ Δ"
  hence "sc Γ' [] Δ' [] = {}"
  proof(rule contrapos_pp)
    assume "sc Γ' [] Δ' [] ≠ {}"
    then obtain C E where "(C,E) ∈ sc Γ' [] Δ' []" by fast
    thus "¬ ⊨ Γ ⇒ Δ" using SC_counterexample' by fastforce
  qed
  from sc_sim[OF this] show "Γ ⇒ Δ" by auto
qed
  
theorem "⊨ Γ ⇒ Δ ⟹ Γ ⇒ Δ"
proof -
  assume s: "⊨ Γ ⇒ Δ"
  obtain Γ' Δ' where p: "Γ = mset Γ'" "Δ = mset Δ'" by (metis ex_mset)
  have "mset Γ' ⇒ mset Δ'"
  proof cases ― ‹just to show that we didn't need to show the lemma above by contraposition. It's just quicker to do so.›
    assume "sc Γ' [] Δ' [] = {}"
    from sc_sim[OF this] show "mset Γ' ⇒ mset Δ'" by auto
  next
    assume "sc Γ' [] Δ' [] ≠ {}"
    with SC_counterexample have "¬ ⊨ mset Γ' ⇒ mset Δ'" by fastforce
    moreover note s[unfolded p]
    ultimately have False ..
    thus "mset Γ' ⇒ mset Δ'" ..
  qed
  thus ?thesis unfolding p .
qed

(*
Just as a side-note: some textbooks advertise completeness as a consequence of cut elimination.
This only makes sense if you have a cut-rule in the rules of SC to begin with.
But even if we did, this proof of completeness would not change a bit.
So… huh.
*)
  
end