Theory Natural_Deduction

(*  Title:      Natural_Deduction.thy
    Author:     Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz, 2026
    Maintainer: Arthur Freitas Ramos

    Ordinary intuitionistic propositional natural deduction over list
    contexts, with weakening, exchange, substitution, and cut admissibility.
*)

theory Natural_Deduction
  imports Labelled_Formulas
begin

text ‹
This theory defines ordinary intuitionistic propositional natural deduction
over list contexts.  The structural metatheory is stated in terms of the set of
assumptions represented by a list, which keeps exchange and weakening explicit
while avoiding dependence on a particular context order.
›

primrec fm_subst :: "('a ⇒ 'b fm) ⇒ 'a fm ⇒ 'b fm" where
  "fm_subst σ (Atom p) = σ p"
| "fm_subst σ Bot = Bot"
| "fm_subst σ (Imp A B) = Imp (fm_subst σ A) (fm_subst σ B)"
| "fm_subst σ (Con A B) = Con (fm_subst σ A) (fm_subst σ B)"
| "fm_subst σ (Dis A B) = Dis (fm_subst σ A) (fm_subst σ B)"

inductive derives :: "'a fm list ⇒ 'a fm ⇒ bool"  ("_ ⊢ _" [50, 50] 50)
where
  Assm: "A ∈ set Γ ⟹ Γ ⊢ A"
| BotE: "Γ ⊢ Bot ⟹ Γ ⊢ A"
| ImpI: "A # Γ ⊢ B ⟹ Γ ⊢ Imp A B"
| ImpE: "Γ ⊢ Imp A B ⟹ Γ ⊢ A ⟹ Γ ⊢ B"
| ConI: "Γ ⊢ A ⟹ Γ ⊢ B ⟹ Γ ⊢ Con A B"
| ConE1: "Γ ⊢ Con A B ⟹ Γ ⊢ A"
| ConE2: "Γ ⊢ Con A B ⟹ Γ ⊢ B"
| DisI1: "Γ ⊢ A ⟹ Γ ⊢ Dis A B"
| DisI2: "Γ ⊢ B ⟹ Γ ⊢ Dis A B"
| DisE: "Γ ⊢ Dis A B ⟹ A # Γ ⊢ C ⟹ B # Γ ⊢ C ⟹ Γ ⊢ C"

lemma weakening:
  assumes "Γ ⊢ A" and "set Γ ⊆ set Δ"
  shows "Δ ⊢ A"
  using assms
proof (induction arbitrary: Δ rule: derives.induct)
  case (Assm A Γ)
  then show ?case
    by (meson derives.Assm subsetD)
next
  case (BotE Γ A)
  then show ?case
    by (meson derives.BotE)
next
  case (ImpI A Γ B)
  show ?case
  proof (rule derives.ImpI)
    show "A # Δ ⊢ B"
      by (rule ImpI.IH) (use ImpI.prems in auto)
  qed
next
  case (ImpE Γ A B)
  then show ?case
    by (meson derives.ImpE)
next
  case (ConI Γ A B)
  then show ?case
    by (meson derives.ConI)
next
  case (ConE1 Γ A B)
  then show ?case
    by (meson derives.ConE1)
next
  case (ConE2 Γ A B)
  then show ?case
    by (meson derives.ConE2)
next
  case (DisI1 Γ A B)
  then show ?case
    by (meson derives.DisI1)
next
  case (DisI2 Γ B A)
  then show ?case
    by (meson derives.DisI2)
next
  case (DisE Γ A B C)
  show ?case
  proof (rule derives.DisE)
    show "Δ ⊢ Dis A B"
      using DisE.IH(1) DisE.prems by blast
    show "A # Δ ⊢ C"
      by (rule DisE.IH(2)) (use DisE.prems in auto)
    show "B # Δ ⊢ C"
      by (rule DisE.IH(3)) (use DisE.prems in auto)
  qed
qed

lemma weakening_cons:
  assumes "Γ ⊢ A"
  shows "B # Γ ⊢ A"
  using assms by (rule weakening) auto

lemma exchange:
  assumes "A # B # Γ ⊢ C"
  shows "B # A # Γ ⊢ C"
  using assms by (rule weakening) auto

lemma cut_general:
  assumes "Γ ⊢ A" and "Δ ⊢ B" and "set Δ ⊆ insert A (set Γ)"
  shows "Γ ⊢ B"
  using assms(2,3,1)
proof (induction arbitrary: Γ A rule: derives.induct)
  case (Assm B Δ)
  from Assm.hyps Assm.prems(1) have "B = A ∨ B ∈ set Γ"
    by auto
  then show ?case
  proof
    assume "B = A"
    then show ?thesis
      using Assm.prems(2) by simp
  next
    assume "B ∈ set Γ"
    then show ?thesis
      by (rule derives.Assm)
  qed
next
  case (BotE Δ B)
  then show ?case
    by (meson derives.BotE)
next
  case (ImpI C Δ D)
  show ?case
  proof (rule derives.ImpI)
    have deriv: "C # Γ ⊢ A"
      using ImpI.prems(2) by (rule weakening_cons)
    have sub: "set (C # Δ) ⊆ insert A (set (C # Γ))"
      using ImpI.prems(1) by auto
    show "C # Γ ⊢ D"
      by (rule ImpI.IH[OF sub deriv])
  qed
next
  case (ImpE Δ C D)
  then show ?case
    by (meson derives.ImpE)
next
  case (ConI Δ C D)
  then show ?case
    by (meson derives.ConI)
next
  case (ConE1 Δ C D)
  then show ?case
    by (meson derives.ConE1)
next
  case (ConE2 Δ C D)
  then show ?case
    by (meson derives.ConE2)
next
  case (DisI1 Δ C D)
  then show ?case
    by (meson derives.DisI1)
next
  case (DisI2 Δ D C)
  then show ?case
    by (meson derives.DisI2)
next
  case (DisE Δ C D E)
  show ?case
  proof (rule derives.DisE)
    show "Γ ⊢ Dis C D"
      using DisE.IH(1) DisE.prems by blast
    have deriv_C: "C # Γ ⊢ A"
      using DisE.prems(2) by (rule weakening_cons)
    have sub_C: "set (C # Δ) ⊆ insert A (set (C # Γ))"
      using DisE.prems(1) by auto
    show "C # Γ ⊢ E"
      by (rule DisE.IH(2)[OF sub_C deriv_C])
    have deriv_D: "D # Γ ⊢ A"
      using DisE.prems(2) by (rule weakening_cons)
    have sub_D: "set (D # Δ) ⊆ insert A (set (D # Γ))"
      using DisE.prems(1) by auto
    show "D # Γ ⊢ E"
      by (rule DisE.IH(3)[OF sub_D deriv_D])
  qed
qed

lemma cut:
  assumes "Γ ⊢ A" and "A # Γ ⊢ B"
  shows "Γ ⊢ B"
  using assms by (rule cut_general) auto

theorem deduction_theorem:
  "A # Γ ⊢ B ⟷ Γ ⊢ Imp A B"
proof
  show "A # Γ ⊢ B ⟹ Γ ⊢ Imp A B"
    by (rule derives.ImpI)
next
  assume "Γ ⊢ Imp A B"
  then have "A # Γ ⊢ Imp A B"
    by (rule weakening_cons)
  moreover have "A # Γ ⊢ A"
    by (rule derives.Assm) simp
  ultimately show "A # Γ ⊢ B"
    by (rule derives.ImpE)
qed

lemma substitution_atom:
  assumes "Γ ⊢ A"
  shows "map (fm_subst σ) Γ ⊢ fm_subst σ A"
  using assms
  by (induction rule: derives.induct) (auto intro: derives.intros)

end