Theory SC_Cut

theory SC_Cut
imports SC
begin
  
subsubsection‹Contraction›
  
text‹First, we need contraction:›
lemma contract:
  "(F,F,Γ ⇒ Δ ⟶ F,Γ ⇒ Δ) ∧ (Γ ⇒ F,F,Δ ⟶ Γ ⇒ F,Δ)"
proof(induction F arbitrary: Γ Δ)
  case (Atom k)
  have "Atom k, Atom k, Γ ⇒ Δ ⟹ Atom k, Γ ⇒ Δ"
    by(induction "Atom k, Atom k, Γ" Δ arbitrary: Γ rule: SCp.induct)
      (auto dest!: multi_member_split intro!: SCp.intros(3-) simp add: lem2 lem1 SCp.intros)  
  moreover have "Γ ⇒ Atom k, Atom k, Δ ⟹ Γ ⇒ Atom k, Δ"
    by(induction "Γ" "Atom k, Atom k, Δ" arbitrary: Δ rule: SCp.induct)
      (auto dest!: multi_member_split intro!: SCp.intros(3-) simp add: lem2 lem1 SCp.intros)
  ultimately show ?case by blast
next
  case Bot
  have "⊥, ⊥, Γ ⇒ Δ ⟹ ⊥, Γ ⇒ Δ" by(blast)
  moreover have "(Γ ⇒ ⊥, ⊥, Δ ⟹ Γ ⇒ ⊥, Δ)"    
    using Bot_delR by fastforce
  ultimately show ?case by blast
next
  case (Not F)
  then show ?case by (meson NotL_inv NotR_inv SCp.NotL SCp.NotR)
next
  case (And F1 F2) then show ?case by(auto intro!: SCp.intros(3-) dest!: AndR_inv AndL_inv) (metis add_mset_commute)
next
  case (Or F1 F2) then show ?case by(auto intro!: SCp.intros(3-) dest!: OrR_inv OrL_inv) (metis add_mset_commute)
next
  (* Okay, so the induction hypothesis is poison for the simplifier. 
     For some reason, this didn't cause trouble for the other two cases, but here, it does. *)
  case (Imp F1 F2) show ?case by(auto dest!: ImpR_inv ImpL_inv intro!: SCp.intros(3-)) (insert Imp.IH; blast)+
qed
corollary
  shows contractL: "F, F, Γ ⇒ Δ ⟹ F, Γ ⇒ Δ"
  and contractR:   "Γ ⇒ F, F, Δ ⟹ Γ ⇒ F, Δ"
  using contract by blast+
    
subsubsection‹Cut›
  
text‹Which cut rule we show is up to us:›
lemma cut_cs_cf:
  assumes context_sharing_Cut: "⋀(A::'a formula) Γ Δ. Γ ⇒ A,Δ ⟹ A,Γ ⇒ Δ ⟹ Γ ⇒ Δ"
  shows context_free_Cut: "Γ ⇒ (A::'a formula),Δ ⟹ A,Γ' ⇒ Δ' ⟹ Γ + Γ' ⇒ Δ + Δ'"
  by(intro context_sharing_Cut[of "Γ + Γ'" A "Δ + Δ'"])
    (metis add.commute union_mset_add_mset_left weakenL_set weakenR_set)+
lemma cut_cf_cs:
  assumes context_free_Cut: "⋀(A::'a formula) Γ Γ' Δ Δ'. Γ ⇒ A,Δ ⟹ A,Γ' ⇒ Δ' ⟹ Γ + Γ' ⇒ Δ + Δ'"
  shows context_sharing_Cut: "Γ ⇒ (A::'a formula),Δ ⟹ A,Γ ⇒ Δ ⟹ Γ ⇒ Δ"
proof - 
  have contractΓΓ: "Γ+Γ' ⇒ Δ ⟹ Γ' ⊆# Γ ⟹ Γ ⇒ Δ" for Γ Γ' Δ
  proof(induction "Γ'" arbitrary: Γ)
    case empty thus ?case using weakenL_set by force
  next
    case (add x Γ' Γ)
    from add.prems(2) have "x ∈# Γ" by (simp add: insert_subset_eq_iff)
    then obtain Γ'' where Γ[simp]: "Γ = x,Γ''" by (meson multi_member_split)
    from add.prems(1) have "x,x,Γ'' + Γ' ⇒ Δ" by simp
    with contractL have "x, Γ'' + Γ' ⇒ Δ" .
    with add.IH[of Γ] show ?case using Γ  add.prems(2) subset_mset.trans by force
  qed
  have contractΔΔ: "Γ ⇒ Δ+Δ' ⟹ Δ' ⊆# Δ ⟹ Γ ⇒ Δ" for Γ Δ Δ'
  proof(induction "Δ'" arbitrary: Δ)
    case empty thus ?case using weakenL_set by force
  next
    case (add x Δ' Δ)
    from add.prems(2) have "x ∈# Δ" by (simp add: insert_subset_eq_iff)
    then obtain Δ'' where Δ[simp]: "Δ = x,Δ''" by (metis multi_member_split)
    from add.prems(1) have "Γ ⇒ x,x,Δ'' + Δ'" by simp
    with contractR have "Γ ⇒ x, Δ'' + Δ'" .
    with add.IH[of Δ] show ?case using Δ add.prems(2) subset_mset.trans by force
  qed
  show "Γ ⇒ A,Δ ⟹ A,Γ ⇒ Δ ⟹ Γ ⇒ Δ"
    using context_free_Cut[of Γ A Δ Γ Δ] contractΓΓ contractΔΔ
    by blast
qed
(* since these are the only lemmas that need contraction on sets, I've decided to transfer those in place *)
text‹According to Troelstra and Schwichtenberg~\<^cite>‹"troelstra2000basic"›, the sharing variant is the one we want to prove.›
  
lemma Cut_Atom_pre: "Atom k,Γ ⇒ Δ ⟹ Γ ⇒ Atom k,Δ ⟹ Γ ⇒ Δ"
proof(induction "Atom k,Γ" "Δ" arbitrary: Γ rule: SCp.induct)
  case BotL
  hence "⊥ ∈# Γ" by simp
  thus ?case using SCp.BotL by blast
next
  case (Ax l Δ)
  show ?case proof cases
    assume "l = k"
    with ‹Atom l ∈# Δ› obtain Δ' where "Δ = Atom k, Δ'" by (meson multi_member_split)
    with ‹Γ ⇒ Atom k, Δ› have "Γ ⇒ Δ" using contractR by blast
    thus ?thesis by auto
  next
    assume "l ≠ k"
    with ‹Atom l ∈# Atom k, Γ› have "Atom l ∈# Γ" by simp
    with ‹Atom l ∈# Δ› show ?thesis using SCp.Ax[of l] by blast
  qed
next
  case NotL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.NotL dest!: NotL_inv)
next
  case NotR
  then show ?case by(auto intro!: SCp.NotR dest!: NotR_inv)
next
  case AndL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.AndL dest!: AndL_inv)
next
  case AndR
  then show ?case by(auto intro!: SCp.AndR dest!: AndR_inv)
next
  case OrL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.OrL dest!: OrL_inv)
next
  case OrR
  thus ?case by(auto intro!: SCp.OrR dest!: OrR_inv)
next
  case ImpL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.ImpL dest!: ImpL_inv)
next
  case ImpR
  then show ?case by (auto dest!: ImpR_inv intro!: SCp.ImpR)
qed
  
text‹We can show the admissibility of the cut rule by induction on the cut formula 
(or, if you will, as a procedure that splits the cut into smaller formulas that get cut).
The only mildly complicated case is that of cutting in an @{term "Atom k"}.
It is, contrary to the general case, only mildly complicated, since the cut formula can only appear principal in the axiom rules.›

theorem cut: "Γ ⇒ F,Δ ⟹ F,Γ ⇒ Δ ⟹ Γ ⇒ Δ"
proof(induction F arbitrary: Γ Δ)
  case Atom thus ?case using Cut_Atom_pre by metis
next
  case Bot thus ?case using Bot_delR by fastforce 
next
  case Not with  NotL_inv NotR_inv show ?case by blast
next
  case And thus ?case by (meson AndL_inv AndR_inv weakenL)
next
  case Or thus ?case by (metis OrL_inv OrR_inv weakenR)
next
  case (Imp F G)
(* an automatic proof:
  thus ?case by (meson ImpL_inv ImpR_inv weakenR)
   a readable one: *)
  from ImpR_inv ‹Γ ⇒ F ❙→ G, Δ› have R: "F, Γ ⇒ G, Δ" by blast
  from ImpL_inv ‹F ❙→ G, Γ ⇒ Δ› have L: "Γ ⇒ F, Δ" "G, Γ ⇒ Δ" by blast+
  from L(1) have "Γ ⇒ F, G, Δ" using weakenR add_ac(3) by blast
  with R have "Γ ⇒ G, Δ" using Imp.IH(1) by simp
  with L(2) show "Γ ⇒ Δ" using Imp.IH(2) by clarsimp
qed
  (* For this proof to work with FOL, I think we would need very special inversion rules.
  For example, for ∀R, we would need that there's a (finite!) multiset of substitutions S, such that
  instead of having ∀x.F,Δ, having {F[s/x] | s ∈ S} + Δ is enough. I don't think that holds,
  but we may be able to cheat ourselves around it… *)
  
corollary cut_cf: "⟦ Γ ⇒ A, Δ; A, Γ' ⇒ Δ'⟧ ⟹ Γ + Γ' ⇒ Δ + Δ'"
  using cut_cs_cf cut by metis

lemma assumes cut: "⋀ Γ' Δ' (A::'a formula). ⟦Γ' ⇒ A, Δ'; A, Γ' ⇒ Δ'⟧ ⟹ Γ' ⇒ Δ'"
  shows contraction_admissibility: "F,F,Γ ⇒ Δ ⟹ (F::'a formula),Γ ⇒ Δ"
  by(rule cut[of "F,Γ" F Δ, OF extended_Ax]) simp_all
(* yes, unpublished Chapman p 2/5, second to last paragraph. that's right. we can prove contraction with cut. but what's that good for? *)
  
end