Theory HCSC

section‹Proof Transformation›
text‹This is organized as a ring closure›
subsection‹HC to SC›
theory HCSC
imports HC SC_Cut
begin

lemma extended_AxE[intro!]: "F, Γ ⇒ F, Δ" by (intro extended_Ax) (simp add: add.commute inter_add_right2)

theorem HCSC: "AX10 ∪ set_mset Γ ⊢⇩H F ⟹ Γ ⇒ {#F#}"
proof(induction rule: HC.induct)
  case (Ax F) thus ?case proof
    note SCp.intros(3-)[intro!]
    text‹Essentially, we need to prove all the axioms of Hibert Calculus in Sequent Calculus.›
    have A: "Γ ⇒ {#F ❙→ (F ❙∨ G)#}" for F G by blast
    have B: "Γ ⇒ {#G ❙→ (F ❙∨ G)#}" for G F by blast
    have C: "Γ ⇒ {#(F ❙→ H) ❙→ ((G ❙→ H) ❙→ ((F ❙∨ G) ❙→ H))#}" for F H G by blast
    have D: "Γ ⇒ {#(F ❙∧ G) ❙→ F#}" for F G by blast
    have E: "Γ ⇒ {#(F ❙∧ G) ❙→ G#}" for F G by blast
    have F: "Γ ⇒ {#F ❙→ (G ❙→ (F ❙∧ G))#}" for F G by blast
    have G: "Γ ⇒ {#(F ❙→ ⊥) ❙→ ❙¬ F#}" for F by blast
    have H: "Γ ⇒ {#❙¬ F ❙→ (F ❙→ ⊥)#}" for F by blast
    have I: "Γ ⇒ {#(❙¬ F ❙→ ⊥) ❙→ F#}" for F  by blast
    have K: "Γ ⇒ {#F ❙→ (G ❙→ F)#}" for F G by blast
    have L: "Γ ⇒ {#(F ❙→ (G ❙→ H)) ❙→ ((F ❙→ G) ❙→ (F ❙→ H))#}" for F G H by blast
    have J: "F ∈ AX0 ⟹ Γ ⇒ {#F#}" for F by(induction rule: AX0.induct; intro K L)
    assume "F ∈ AX10" thus ?thesis by(induction rule: AX10.induct; intro A B C D E F G H I J)
  next
    assume "F ∈ set_mset Γ" thus ?thesis by(intro extended_Ax) simp
  qed
next
  case (MP F G)
  from MP have IH: "Γ ⇒ {#F#}" "Γ ⇒ {#F ❙→ G#}" by blast+
  with ImpR_inv[where Δ=‹{#}›, simplified] have "F,Γ ⇒ {#G#}" by auto
  moreover from IH(1) weakenR have "Γ ⇒ F, {#G#}" by blast
  ultimately show "Γ ⇒ {#G#}" using cut[where F=F] by simp
qed

end