Theory NDHC

subsection‹ND to HC›
theory NDHC
imports ND HC
begin

text‹The fundamental difference between the two is that Natural Deduction updates its set of assumptions while Hilbert Calculus does not.
The Deduction Theorem @{thm Deduction_theorem} helps with this.›
theorem NDHC: "Γ ⊢ F ⟹ AX10 ∪ Γ ⊢⇩H F"
proof(induction rule: ND.induct)
  case Ax thus ?case by(auto intro: HC.Ax)
next
  case NotE thus ?case by (meson AX10.intros(9) HC.simps subsetCE sup_ge1)
next
  case (NotI  F Γ)
  from HC_intros(11) have HC_NotI: "AX10 ∪ Γ ⊢⇩H A ❙→ ⊥ ⟹ AX10 ∪ Γ ⊢⇩H ❙¬ A" for A 
    using MP HC_mono by (metis sup_ge1)
  from NotI show ?case using Deduction_theorem[where Γ="AX10 ∪ Γ"] HC_NotI by (metis AX100 Un_assoc Un_insert_right)
next
  case (CC F Γ)
  hence "AX10 ∪ Γ ⊢⇩H ❙¬ F ❙→ ⊥" using Deduction_theorem[where Γ="AX10 ∪ Γ"] by (metis AX100 Un_assoc Un_insert_right)
  thus "AX10 ∪ Γ ⊢⇩H F" using AX10.intros(10) by (metis HC.simps UnCI)
next
  case (AndE1 Γ F G) thus ?case by (meson AX10.intros(5) HC.simps UnCI)
next
  case (AndE2 Γ F G) thus ?case by (meson AX10.intros(6) HC.simps UnCI)
next
  case (AndI Γ F G) thus ?case by (meson HC_intros(10) HC_mono HC.simps sup_ge1)
next
  case (OrE Γ F G H)
  from ‹AX10 ∪ (F ▹ Γ) ⊢⇩H H› ‹AX10 ∪ (G ▹ Γ) ⊢⇩H H› have
       "AX10 ∪ Γ ⊢⇩H F ❙→ H" "AX10 ∪ Γ ⊢⇩H G ❙→ H"
    using Deduction_theorem[where Γ="AX10 ∪ Γ"] by (metis AX100 Un_assoc Un_insert_right)+
  with HC_intros(7)[THEN HC_mono[OF _ sup_ge1]] MP
  have "AX10 ∪ Γ ⊢⇩H  (F ❙∨ G) ❙→ H" by metis
  with MP ‹AX10 ∪ Γ ⊢⇩H F ❙∨ G› show ?case  .
next
  case (OrI1 Γ F G) thus ?case by (meson AX10.intros(2) HC.simps UnCI)
next
  case (OrI2 Γ F G) thus ?case by (meson AX10.intros(3) HC.simps UnCI)
next
  case (ImpE Γ F G) 
  from MP  ‹AX10 ∪ Γ ⊢⇩H F›  ‹AX10 ∪ Γ ⊢⇩H F ❙→ G› show ?case .
next
  case (ImpI F Γ G) thus ?case using Deduction_theorem[where Γ="AX10 ∪ Γ"] by (metis AX100 Un_assoc Un_insert_right)
qed

end