Theory MiniSC_HC

subsubsection‹SC to HC›
theory MiniSC_HC
imports MiniSC HC
begin

inductive_set AX1 where
"F ∈ AX0 ⟹ F ∈ AX1" |
"((F ❙→ ⊥) ❙→ ⊥) ❙→ F ∈ AX1"
lemma AX01: "AX0 ⊆ AX1" by (simp add: AX1.intros(1) subsetI)
lemma AX1_away: "AX1 ∪ Γ = AX0 ∪ (Γ ∪ AX1)" using AX01 by blast

lemma Deduction1: "F ▹ (AX1 ∪ Γ ) ⊢⇩H ⊥ ⟷ (AX1 ∪ Γ) ⊢⇩H (F ❙→ ⊥)" unfolding AX1_away by (metis Deduction_theorem HC.simps HC_mono Un_commute Un_insert_left insertI1 subset_insertI)
lemma Deduction2: "(F ❙→ ⊥) ▹ (AX1 ∪ Γ) ⊢⇩H ⊥ ⟷ (AX1 ∪ Γ) ⊢⇩H F" (is "?l ⟷ ?r")
proof
  assume l: ?l
  with Deduction_theorem[where Γ="AX1 ∪ Γ" and F="F ❙→ ⊥" and G=⊥]
  have "AX1 ∪ Γ ⊢⇩H (F ❙→ ⊥) ❙→ ⊥" unfolding AX1_away by(simp add: Un_commute)
  moreover have "AX1 ∪ Γ ⊢⇩H ((F ❙→ ⊥) ❙→ ⊥) ❙→ F" using AX1.intros(2) HC.Ax by blast
  ultimately show ?r using HC.MP by blast
next
  assume r: ?r thus ?l by (meson HC.simps HC_mono insertI1 subset_insertI)
qed

lemma 
  "Γ ⇒ Δ ⟹ is_mini_mset Γ ⟹ is_mini_mset Δ ⟹
  (set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ ∪ AX1) ⊢⇩H ⊥"
proof(induction "Γ" "Δ" rule: SCp.induct)
  case (ImpL Γ F Δ G)
  from ImpL.prems have "is_mini_mset Γ" "is_mini_mset (F, Δ)" by simp_all
  with ImpL.IH(1) have IH1: "set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset (F, Δ) ∪ AX1 ⊢⇩H ⊥" .
  hence IH1: "F ❙→ ⊥ ▹ set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ ∪ AX1 ⊢⇩H ⊥" by simp
  from ImpL.prems have "is_mini_mset (G, Γ)" "is_mini_mset Δ" by simp_all
  with ImpL.IH(2) have IH2: "set_mset (G, Γ) ∪ (λF. F ❙→ ⊥) ` set_mset Δ ∪ AX1 ⊢⇩H ⊥" .
  hence IH2: "G ▹ (set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ ∪ AX1) ⊢⇩H ⊥" by simp
  have R: "F ❙→ G ▹ AX1 ∪ Γ ⊢⇩H ⊥" if "G ▹ AX1 ∪ Γ ⊢⇩H ⊥" "F ❙→ ⊥ ▹ AX1 ∪ Γ ⊢⇩H ⊥" for Γ 
    using that by (metis Ax Deduction1 Deduction2 HC_mono MP insertI1 subset_insertI)
    (* I don't construct the actual proofs for the Rs. Sledgehammer is doing all the interesting work. :/ *)
  from R[where Γ="set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ"]
  have "F ❙→ G ▹ (set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ ∪ AX1) ⊢⇩H ⊥" using IH2 IH1 by(simp add: Un_commute)
  thus ?case by simp
next
  case (ImpR F Γ G Δ)
  hence "is_mini_mset (F, Γ)" "is_mini_mset (G, Δ)" by simp_all
  with ImpR.IH have IH: "F ▹ G ❙→ ⊥ ▹ set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ ∪ AX1 ⊢⇩H ⊥" by(simp add: insert_commute)
  have R: "(F ❙→ G) ❙→ ⊥ ▹ Γ ∪ AX1 ⊢⇩H ⊥" if "F ▹ G ❙→ ⊥ ▹ Γ ∪ AX1 ⊢⇩H ⊥" for Γ using that
    by (metis AX1_away Deduction2 Deduction_theorem Un_commute Un_insert_right)
  thus ?case using IH by simp
next
  case (Ax k Γ Δ)
  have R: "F ▹ F ❙→ ⊥ ▹ Γ ∪ AX1 ⊢⇩H ⊥" for F :: "'a formula" and Γ by (meson HC.simps insert_iff)
  from R[where F="Atom k" and Γ="set_mset Γ ∪ (λF. F ❙→ ⊥) ` set_mset Δ"] show ?case using Ax.hyps
    by (simp add: insert_absorb)
next
  case BotL thus ?case by (simp add: HC.Ax)
qed simp_all

end