Theory SC_Gentzen

subsubsection‹Mimicking the original›

theory SC_Gentzen
imports SC_Depth SC_Cut
begin

text‹This system attempts to mimic the original sequent calculus 
  (``Reihen von Formeln, durch Kommata getrennt'', translates roughly to sequences of formulas, separated by a comma)~\<^cite>‹"gentzen1935untersuchungen"›.›
inductive SCg :: "'a formula list ⇒ 'a formula list ⇒ bool" (infix "⇒" 30) where
Anfang: "[𝔇] ⇒ [𝔇]" |
FalschA: "[⊥] ⇒ []" |
VerduennungA: "Γ ⇒ Θ ⟹ 𝔇#Γ ⇒ Θ" |
VerduennungS: "Γ ⇒ Θ ⟹ Γ ⇒ 𝔇#Θ" |
ZusammenziehungA: "𝔇#𝔇#Γ ⇒ Θ ⟹ 𝔇#Γ ⇒ Θ" |
ZusammenziehungS: "Γ ⇒ 𝔇#𝔇#Θ ⟹ Γ ⇒ 𝔇#Θ" |
VertauschungA: "Δ@𝔇#𝔈#Γ ⇒ Θ ⟹ Δ@𝔈#𝔇#Γ ⇒ Θ" |
VertauschungS: "Γ ⇒ Θ@𝔈#𝔇#Λ ⟹ Γ ⇒ Θ@𝔇#𝔈#Λ" |
Schnitt: "⟦Γ ⇒ 𝔇#Θ; 𝔇#Δ ⇒ Λ⟧ ⟹ Γ@Δ ⇒ Θ@Λ" |
UES: "⟦Γ ⇒ 𝔄#Θ; Γ ⇒ 𝔅#Θ⟧ ⟹ Γ ⇒ 𝔄❙∧𝔅#Θ" |
UEA1: "𝔄#Γ ⇒ Θ ⟹ 𝔄❙∧𝔅#Γ ⇒ Θ" | UEA2: "𝔅#Γ ⇒ Θ ⟹ 𝔄❙∧𝔅#Γ ⇒ Θ" |
OEA: "⟦𝔄#Γ ⇒ Θ; 𝔅#Γ ⇒ Θ⟧ ⟹ 𝔄❙∨𝔅#Γ ⇒ Θ" |
OES1: "Γ ⇒ 𝔄#Θ ⟹ Γ ⇒ 𝔄❙∨𝔅#Θ" | OES2: "Γ ⇒ 𝔅#Θ ⟹ Γ ⇒ 𝔄❙∨𝔅#Θ" |
FES: "𝔄#Γ ⇒ 𝔅#Θ ⟹ Γ ⇒ 𝔄❙→𝔅#Θ" |
FEA: "⟦Γ ⇒ 𝔄#Θ; 𝔅#Δ ⇒ Λ⟧ ⟹ 𝔄❙→𝔅#Γ@Δ ⇒ Θ@Λ" |
NES: "𝔄#Γ ⇒ Θ ⟹ Γ ⇒ ❙¬𝔄#Θ" |
NEA: "Γ ⇒ 𝔄#Θ ⟹ ❙¬𝔄#Γ ⇒ Θ"
text‹Nota bene: E here stands for ``Einführung'', which is introduction and not elemination.›
text‹The rule for @{term ⊥} is not part of the original calculus. Its addition is necessary to show equivalence to our @{const SCp}.›

text‹Note that we purposefully did not recreate the fact that Gentzen sometimes puts his principal formulas on end and sometimes on the beginning of the list.›

lemma AnfangTauschA: "𝔇#Δ@Γ ⇒ Θ ⟹ Δ@𝔇#Γ ⇒ Θ"
  by(induction Δ arbitrary: Γ rule: List.rev_induct) (simp_all add: VertauschungA)
lemma AnfangTauschS: "Γ ⇒ 𝔇#Δ@Θ ⟹ Γ ⇒ Δ@𝔇#Θ"
  by(induction Δ arbitrary: Θ rule: List.rev_induct) (simp_all add: VertauschungS)
lemma MittenTauschA: "Δ@𝔇#Γ ⇒ Θ ⟹ 𝔇#Δ@Γ ⇒ Θ"
  by(induction Δ arbitrary: Γ rule: List.rev_induct) (simp_all add: VertauschungA)
lemma MittenTauschS: "Γ ⇒ Δ@𝔇#Θ ⟹ Γ ⇒ 𝔇#Δ@Θ"
  by(induction Δ arbitrary: Θ rule: List.rev_induct) (simp_all add: VertauschungS)

lemma BotLe: "⊥∈set Γ ⟹ Γ⇒Δ"
proof -
  have A: "⊥#Γ⇒[]" for Γ by(induction Γ) (simp_all add: FalschA VerduennungA VertauschungA[where Δ=Nil, simplified])
  have *: "⊥#Γ⇒Δ" for Γ by(induction Δ) (simp_all add: A VerduennungS)
  assume "⊥∈set Γ" then obtain Γ1 Γ2 where Γ: "Γ = Γ1@⊥#Γ2" by (meson split_list)
  show ?thesis unfolding Γ using AnfangTauschA * by blast
qed

lemma Axe: "A ∈ set Γ ⟹ A ∈ set Δ ⟹ Γ ⇒ Δ"
proof -
  have A: "A#Γ ⇒ [A]" for Γ by(induction Γ) (simp_all add: Anfang VertauschungA[where Δ=Nil, simplified] VerduennungA)
  have S: "A#Γ ⇒ A#Δ" for Γ Δ by(induction Δ) (simp_all add: A Anfang VertauschungS[where Θ=Nil, simplified] VerduennungS)
  assume "A ∈ set Γ" "A ∈ set Δ" thus ?thesis
    apply(-)
    apply(drule split_list)+
    apply(clarify)
    apply(intro AnfangTauschA AnfangTauschS)
    apply(rule S)
  done
qed

lemma VerduennungListeA: "Γ ⇒ Θ ⟹ Γ@Γ ⇒ Θ"
proof -
  have "Γ ⇒ Θ ⟹ ∃Γ''. Γ=Γ''@Γ' ⟹ Γ'@Γ ⇒ Θ" for Γ'
  proof(induction Γ')
    case (Cons a as)
    then obtain Γ'' where "Γ = Γ'' @ a # as" by blast
    hence "∃Γ''. Γ = Γ'' @ as" by(intro exI[where x="Γ'' @ [a]"]) simp
    from Cons.IH[OF Cons.prems(1) this] have "as @ Γ ⇒ Θ" .
    thus ?case using VerduennungA by simp
  qed simp
  thus "Γ ⇒ Θ ⟹ Γ@Γ ⇒ Θ" by simp
qed
lemma VerduennungListeS: "Γ ⇒ Θ ⟹ Γ ⇒ Θ@Θ"
proof -
  have "Γ ⇒ Θ ⟹ ∃Θ''. Θ=Θ''@Θ' ⟹ Γ ⇒ Θ'@Θ" for Θ'
  proof(induction Θ')
    case (Cons a as)
    then obtain Θ'' where "Θ = Θ'' @ a # as" by blast
    hence "∃Θ''. Θ = Θ'' @ as" by(intro exI[where x="Θ'' @ [a]"]) simp
    from Cons.IH[OF Cons.prems(1) this] have " Γ ⇒ as @ Θ" .
    thus ?case using VerduennungS by simp
  qed simp
  thus "Γ ⇒ Θ ⟹ Γ ⇒ Θ@Θ" by simp
qed
(* wak, those weren't the droids I was looking for. *)
lemma ZusammenziehungListeA: "Γ@Γ ⇒ Θ ⟹ Γ ⇒ Θ"
proof -
  have "Γ'@Γ ⇒ Θ ⟹ ∃Γ''. Γ=Γ''@Γ' ⟹ Γ ⇒ Θ" for Γ'
  proof(induction Γ')
    case (Cons a Γ')
    then obtain Γ'' where Γ'': "Γ = Γ'' @ a # Γ'" by blast
    then obtain Γ1 Γ2 where Γ: "Γ = Γ1 @ a # Γ2" by blast
    from Γ'' have **: "∃Γ''. Γ = Γ'' @ Γ'" by(intro exI[where x="Γ'' @ [a]"]) simp
    from Cons.prems(1) have "a # (a # Γ') @ Γ1 @ Γ2 ⇒ Θ" unfolding Γ  using MittenTauschA by (metis append_assoc)
    hence "(a # Γ') @ Γ1 @ Γ2 ⇒ Θ" using ZusammenziehungA by auto
    hence "Γ' @ Γ ⇒ Θ" unfolding Γ  using AnfangTauschA by (metis append_Cons append_assoc)
    from Cons.IH[OF this **] show "Γ ⇒ Θ" .
  qed simp
  thus "Γ@Γ ⇒ Θ ⟹ Γ ⇒ Θ" by simp
qed
lemma ZusammenziehungListeS: "Γ ⇒ Θ@Θ ⟹ Γ ⇒ Θ"
proof -
  have "Γ ⇒ Θ'@Θ ⟹ ∃Θ''. Θ=Θ''@Θ' ⟹ Γ ⇒ Θ" for Θ'
  proof(induction Θ')
    case (Cons a Θ')
    then obtain Θ'' where Θ'': "Θ = Θ'' @ a # Θ'" by blast
    then obtain Θ1 Θ2 where Θ: "Θ = Θ1 @ a # Θ2" by blast
    from Θ'' have **: "∃Θ''. Θ = Θ'' @ Θ'" by(intro exI[where x="Θ'' @ [a]"]) simp
    from Cons.prems(1) have "Γ ⇒ a # (a # Θ') @ Θ1 @ Θ2" unfolding Θ  using MittenTauschS by (metis append_assoc)
    hence "Γ ⇒ (a # Θ') @ Θ1 @ Θ2" using ZusammenziehungS by auto
    hence "Γ ⇒ Θ' @ Θ" unfolding Θ  using AnfangTauschS by (metis append_Cons append_assoc)
    from Cons.IH[OF this **] show "Γ ⇒ Θ" .
  qed simp
  thus "Γ ⇒ Θ@Θ ⟹ Γ ⇒Θ" by simp
qed

theorem gentzen_sc_eq: "mset Γ ⇒ mset Δ ⟷ Γ ⇒ Δ" proof
  assume "mset Γ ⇒ mset Δ" 
  then obtain n where "mset Γ ⇒ mset Δ ↓ n" unfolding SC_SCp_eq[symmetric] ..
  thus "Γ ⇒ Δ"
  (* structural induction not necessary at all. I still don't get it. *)
  proof(induction n arbitrary: Γ Δ rule: nat.induct)
    case (Suc n) 
    have sr: "∃Γ1 Γ2. Γ = Γ1 @ F # Γ2 ∧ Γ' = mset (Γ1@Γ2)" (is "?s") if "mset Γ = F, Γ'" for Γ Γ' F proof -
      from that obtain Γ1 Γ2 where Γ: "Γ = Γ1 @ F # Γ2" by (metis split_list add.commute ex_mset list.set_intros(1) mset.simps(2) set_mset_mset)
      hence Γ': "Γ' = mset (Γ1@Γ2)" using that by auto
      show ?s using Γ Γ' by blast
    qed
    from Suc.prems show ?case proof(cases rule: SCc.cases)
      case BotL thus ?thesis using BotLe by simp
    next
      case Ax thus ?thesis using Axe by simp
    next
      case (NotL Γ' F)
      from ‹mset Γ = ❙¬ F, Γ'› obtain Γ1 Γ2 where Γ: "Γ = Γ1 @ ❙¬ F # Γ2" 
        by (metis split_list add.commute ex_mset list.set_intros(1) mset.simps(2) set_mset_mset)
      hence Γ': "Γ' = mset (Γ1@Γ2)" using NotL(1) by simp
      from ‹Γ' ⇒ F, mset Δ ↓ n› have "mset (Γ1@Γ2) ⇒ mset (F#Δ) ↓ n" unfolding Γ' by (simp add: add.commute)
      from Suc.IH[OF this] show ?thesis unfolding Γ using AnfangTauschA NEA by blast
    next
      case (NotR F Δ')
      from sr[OF NotR(1)] obtain Δ1 Δ2 where Δ: "Δ = Δ1 @ ❙¬ F # Δ2 ∧ Δ' = mset (Δ1 @ Δ2)"
        by blast
      with NotR have "mset (F#Γ) ⇒ mset (Δ1@Δ2) ↓ n" by (simp add: add.commute)
      from Suc.IH[OF this] show ?thesis using Δ using AnfangTauschS NES by blast
    next
      case (AndR F Δ' G)
      from sr[OF AndR(1)] obtain Δ1 Δ2 where Δ: "Δ = Δ1 @ F ❙∧ G # Δ2 ∧ Δ' = mset (Δ1 @ Δ2)"
        by blast
      with AndR have "mset Γ ⇒ mset (F # Δ1@Δ2) ↓ n" "mset Γ ⇒ mset (G # Δ1@Δ2) ↓ n" by (simp add: add.commute)+
      from this[THEN Suc.IH] show ?thesis using Δ using AnfangTauschS UES by blast
    next
      case (OrR F G Δ')
      from sr[OF OrR(1)] obtain Δ1 Δ2 where Δ: "Δ = Δ1 @ F ❙∨ G # Δ2 ∧ Δ' = mset (Δ1 @ Δ2)"
        by blast
      with OrR have "mset Γ ⇒ mset (G # F # Δ1@Δ2) ↓ n" by (simp add: add.commute add.left_commute add_mset_commute)
      from this[THEN Suc.IH] have "Γ ⇒ G # F # Δ1 @ Δ2" .
      with OES2 have "Γ ⇒ F ❙∨ G # F # Δ1 @ Δ2" .
      with VertauschungS[where Θ=Nil, simplified] have "Γ ⇒ F # F ❙∨ G # Δ1 @ Δ2" .
      with OES1 have "Γ ⇒ F ❙∨ G # F ❙∨ G # Δ1 @ Δ2" .
      hence "Γ ⇒ F ❙∨ G # Δ1 @ Δ2" using ZusammenziehungS by fast 
      thus ?thesis unfolding Δ[THEN conjunct1] using AnfangTauschS by blast
    next
      case (ImpR F G Δ')
      from sr[OF ImpR(1)] obtain Δ1 Δ2 where Δ: "Δ = Δ1 @ F ❙→ G # Δ2 ∧ Δ' = mset (Δ1 @ Δ2)"
        by blast
      with ImpR have "mset (F#Γ) ⇒ mset (G # Δ1@Δ2) ↓ n" by (simp add: add.commute)
      from this[THEN Suc.IH] show ?thesis using Δ using AnfangTauschS FES by blast
    next
      case (AndL F G Γ')
      from sr[OF this(1)] obtain Γ1 Γ2 where Γ: "Γ = Γ1 @ F ❙∧ G # Γ2 ∧ Γ' = mset (Γ1 @ Γ2)"
        by blast
      with AndL have "mset (G # F # Γ1@Γ2) ⇒ mset Δ ↓ n" by (simp add: add.commute add.left_commute add_mset_commute)
      from this[THEN Suc.IH] have "G # F # Γ1 @ Γ2 ⇒ Δ" .
      with UEA2 have "F ❙∧ G # F # Γ1 @ Γ2 ⇒ Δ" .
      with VertauschungA[where Δ=Nil, simplified] have "F # F ❙∧ G # Γ1 @ Γ2 ⇒ Δ" .
      with UEA1 have "F ❙∧ G # F ❙∧ G # Γ1 @ Γ2 ⇒ Δ" .
      hence "F ❙∧ G # Γ1 @ Γ2 ⇒ Δ" using ZusammenziehungA by fast 
      thus ?thesis unfolding Γ[THEN conjunct1] using AnfangTauschA by blast
    next
      case (OrL F Δ' G)
      from sr[OF this(1)] obtain Γ1 Γ2 where Γ: "Γ = Γ1 @ F ❙∨ G # Γ2 ∧ Δ' = mset (Γ1 @ Γ2)"
        by blast
      with OrL have "mset (F # Γ1@Γ2) ⇒ mset Δ ↓ n" "mset (G # Γ1@Γ2) ⇒ mset Δ ↓ n" by (simp add: add.commute)+
      from this[THEN Suc.IH] show ?thesis using Γ using AnfangTauschA OEA by blast
    next
      case (ImpL Γ' F G)
      from sr[OF this(1)] obtain Γ1 Γ2 where Γ: "Γ = Γ1 @ F ❙→ G # Γ2 ∧ Γ' = mset (Γ1 @ Γ2)"
        by blast
      with ImpL have "mset (Γ1@Γ2) ⇒ mset (F#Δ) ↓ n" "mset (G # Γ1@Γ2) ⇒ mset Δ ↓ n" by (simp add: add.commute)+
      from this[THEN Suc.IH] have "Γ1 @ Γ2 ⇒ F # Δ" "G # Γ1 @ Γ2 ⇒ Δ" .
      from FEA[OF this] have "F ❙→ G # (Γ1 @ Γ2) @ (Γ1 @ Γ2) ⇒ Δ @ Δ" .
      hence "F ❙→ G # (Γ1 @ Γ2) @ (F ❙→ G # Γ1 @ Γ2) ⇒ Δ @ Δ" using AnfangTauschA VerduennungA by blast (* given the form of ZusammenziehungListeA, using this intermediate step is just easier. maybe a different from for ZusammenziehungListeA would be nice? *)
      hence "F ❙→ G # (Γ1 @ Γ2) ⇒ Δ @ Δ" using ZusammenziehungListeA[where Γ="F ❙→ G # (Γ1 @ Γ2)"] by simp
      thus ?thesis unfolding Γ[THEN conjunct1] by(intro AnfangTauschA; elim ZusammenziehungListeS)
    qed
  qed blast
next
  have mset_Cons[simp]: "mset (A # S) = A, mset S" for A::"'a formula" and S by (simp add: add.commute)
  note mset.simps(2)[simp del]
  show "Γ ⇒ Δ ⟹ mset Γ ⇒ mset Δ" proof(induction rule: SCg.induct)
    (*sed -n '/^\([^\\]*\):/ {N;s/_\\\?//g; s/let.*$//; s/\n//; s/[\\:]//g; s/fix //; s/  / /g; s/^.*$/case (&) thus ?case sorry/; p;}' ${print_cases} *)
    case (Anfang 𝔇) thus ?case using extended_Ax SC_SCp_eq by force
  next
    case (FalschA) thus ?case using SCp.BotL by force
  next
    case (VerduennungA Γ Θ 𝔇) thus ?case by (simp add: SC.weakenL)
  next
    case (VerduennungS Γ Θ 𝔇) thus ?case by (simp add: SC.weakenR)
  next
    case (ZusammenziehungA 𝔇 Γ Θ) thus ?case using contractL by force
  next
    case (ZusammenziehungS Γ 𝔇 Θ) thus ?case using contract by force
  next
    case (VertauschungA Δ 𝔇 𝔈 Γ Θ) thus ?case by fastforce
  next
    case (VertauschungS Γ Θ 𝔈 𝔇 Λ) thus ?case by fastforce
  next
    case (Schnitt Γ 𝔇 Θ Δ Λ)
    hence "mset Γ ⇒ 𝔇,mset Θ" "𝔇,mset Δ ⇒ mset Λ" using SC_SCp_eq by auto
    from cut_cf[OF this] show ?case unfolding SC_SCp_eq by simp
  next
    case (UES Γ 𝔄 Θ 𝔅) thus ?case using SCp.AndR by (simp add: SC_SCp_eq)
  next
    case (UEA1 𝔄 Γ Θ 𝔅) 
    from ‹mset (𝔄 # Γ) ⇒ mset Θ› have "𝔄,𝔅,mset Γ ⇒ mset Θ" using SC.weakenL by auto
    thus ?case using SCp.AndL by force
  next
    case (UEA2 𝔅 Γ Θ 𝔄)
    from ‹mset (𝔅 # Γ) ⇒ mset Θ› have "𝔄,𝔅,mset Γ ⇒ mset Θ" using SC.weakenL by auto
    thus ?case using SCp.AndL by force
  next
    case (OEA 𝔄 Γ Θ 𝔅) thus ?case unfolding SC_SCp_eq by (simp add: SCp.OrL)
  next
    case (OES1 Γ 𝔄 Θ 𝔅) thus ?case using SC.weakenR[where 'a='a] by(auto intro!: SCp.intros(3-))
  next
    case (OES2 Γ 𝔅 Θ 𝔄) thus ?case by (simp add: SC.weakenR SCp.OrR)
  next
    case (FES 𝔄 Γ 𝔅 Θ) thus ?case using weakenR unfolding SC_SCp_eq by (simp add: SCp.ImpR)
  next
    case (FEA Γ 𝔄 Θ 𝔅 Δ Λ) 
    from ‹mset Γ ⇒ mset (𝔄 # Θ)›[THEN weakenL_set, THEN weakenR_set, of "mset Δ" "mset Λ"]
    have S: "mset (Γ@Δ) ⇒ 𝔄,mset (Θ@Λ)" unfolding mset_append mset_Cons by (simp add: add_ac) (* sledgehammer comes up with some funny proof using cut… *)
    from FEA obtain m where "mset (𝔅 # Δ) ⇒ mset Λ" by blast
    hence "mset Γ + mset (𝔅 # Δ) ⇒ mset Θ + mset Λ" using weakenL_set weakenR_set by fast
    hence A: "𝔅,mset (Γ@Δ) ⇒ mset (Θ@Λ)" by (simp add: add.left_commute)
    show ?case using S A SC_SCp_eq SCp.ImpL unfolding mset_Cons by blast
  next
    case (NES 𝔄 Γ Θ) thus ?case using SCp.NotR by(simp add: SC_SCp_eq)
  next
    case (NEA Γ 𝔄 Θ) thus ?case using SCp.NotL by(simp add: SC_SCp_eq)
  qed
qed


end