Theory Labelled_Natural_Deduction

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

    Parametric labelled natural-deduction kernel: a locale fixing inert
    label constructors for the logical rules, with the labelled judgement
    and its structural metatheory.
*)

theory Labelled_Natural_Deduction
  imports Natural_Deduction
begin

text ‹
This theory introduces the parametric labelled natural-deduction kernel.  A
locale fixes inert label constructors for the logical rules, but imposes no
equations on them; concrete label disciplines are supplied later by
interpretation.
›

locale label_structure =
  fixes app :: "'l ⇒ 'l ⇒ 'l"
    and lam :: "'l ⇒ 'l ⇒ 'l"
    and pair :: "'l ⇒ 'l ⇒ 'l"
    and fst_l :: "'l ⇒ 'l"
    and snd_l :: "'l ⇒ 'l"
    and abort :: "'l ⇒ 'l"
    and inl :: "'l ⇒ 'l"
    and inr :: "'l ⇒ 'l"
    and cases :: "'l ⇒ 'l ⇒ 'l ⇒ 'l ⇒ 'l ⇒ 'l"
begin

inductive lderives :: "('l, 'a) lfm list ⇒ ('l, 'a) lfm ⇒ bool"
    ("_ ⊢L _" [50, 50] 50)
where
  LAssm: "x ∈ set Γ ⟹ Γ ⊢L x"
| LBotE: "Γ ⊢L (l, Bot) ⟹ Γ ⊢L (abort l, A)"
| LImpI: "(l, A) # Γ ⊢L (m, B) ⟹ Γ ⊢L (lam l m, Imp A B)"
| LImpE: "Γ ⊢L (l, Imp A B) ⟹ Γ ⊢L (m, A) ⟹ Γ ⊢L (app l m, B)"
| LConI: "Γ ⊢L (l, A) ⟹ Γ ⊢L (m, B) ⟹ Γ ⊢L (pair l m, Con A B)"
| LConE1: "Γ ⊢L (l, Con A B) ⟹ Γ ⊢L (fst_l l, A)"
| LConE2: "Γ ⊢L (l, Con A B) ⟹ Γ ⊢L (snd_l l, B)"
| LDisI1: "Γ ⊢L (l, A) ⟹ Γ ⊢L (inl l, Dis A B)"
| LDisI2: "Γ ⊢L (l, B) ⟹ Γ ⊢L (inr l, Dis A B)"
| LDisE:
    "Γ ⊢L (l, Dis A B) ⟹
     (m, A) # Γ ⊢L (n, C) ⟹
     (p, B) # Γ ⊢L (q, C) ⟹
     Γ ⊢L (cases l m n p q, C)"

lemma labelled_weakening:
  assumes "Γ ⊢L x" and "set Γ ⊆ set Δ"
  shows "Δ ⊢L x"
  using assms
proof (induction arbitrary: Δ rule: lderives.induct)
  case (LAssm x Γ)
  then have "x ∈ set Δ"
    by auto
  then show ?case
    by (rule lderives.intros(1))
next
  case (LBotE Γ l A)
  then show ?case
    by (meson lderives.intros)
next
  case (LImpI l A Γ m B)
  show ?case
  proof (rule lderives.intros(3))
    show "(l, A) # Δ ⊢L (m, B)"
      by (rule LImpI.IH) (use LImpI.prems in auto)
  qed
next
  case (LImpE Γ l A B m)
  then show ?case
    by (meson lderives.intros)
next
  case (LConI Γ l A m B)
  then show ?case
    by (meson lderives.intros)
next
  case (LConE1 Γ l A B)
  then show ?case
    by (meson lderives.intros)
next
  case (LConE2 Γ l A B)
  then show ?case
    by (meson lderives.intros)
next
  case (LDisI1 Γ l A B)
  then show ?case
    by (meson lderives.intros)
next
  case (LDisI2 Γ l B A)
  then show ?case
    by (meson lderives.intros)
next
  case (LDisE Γ l A B m n C p q)
  show ?case
  proof (rule lderives.intros(10))
    show "Δ ⊢L (l, Dis A B)"
      using LDisE.IH(1) LDisE.prems by blast
    show "(m, A) # Δ ⊢L (n, C)"
      by (rule LDisE.IH(2)) (use LDisE.prems in auto)
    show "(p, B) # Δ ⊢L (q, C)"
      by (rule LDisE.IH(3)) (use LDisE.prems in auto)
  qed
qed

lemma labelled_weakening_cons:
  assumes "Γ ⊢L x"
  shows "y # Γ ⊢L x"
  using assms by (rule labelled_weakening) auto

lemma labelled_exchange:
  assumes "x # y # Γ ⊢L z"
  shows "y # x # Γ ⊢L z"
  using assms by (rule labelled_weakening) auto

lemma labelled_cut_general:
  assumes "Γ ⊢L x"
    and "Δ ⊢L y"
    and "set Δ ⊆ insert x (set Σ)"
    and "set Γ ⊆ set Σ"
  shows "Σ ⊢L y"
  using assms(2,3,1,4)
proof (induction arbitrary: Γ x Σ rule: lderives.induct)
  case (LAssm y Δ)
  from LAssm.hyps LAssm.prems(1) have "y = x ∨ y ∈ set Σ"
    by auto
  then show ?case
  proof
    assume "y = x"
    then show ?thesis
      using LAssm.prems(2,3) labelled_weakening by blast
  next
    assume "y ∈ set Σ"
    then show ?thesis
      by (rule lderives.intros(1))
  qed
next
  case (LBotE Δ l A)
  then show ?case
    by (meson lderives.intros)
next
  case (LImpI l A Δ m B)
  show ?case
  proof (rule lderives.intros(3))
    have sub: "set ((l, A) # Δ) ⊆ insert x (set ((l, A) # Σ))"
      using LImpI.prems(1) by auto
    have sub_context: "set Γ ⊆ set ((l, A) # Σ)"
      using LImpI.prems(3) by auto
    show "(l, A) # Σ ⊢L (m, B)"
      by (rule LImpI.IH[OF sub LImpI.prems(2) sub_context])
  qed
next
  case (LImpE Δ l A B m)
  then show ?case
    by (meson lderives.intros)
next
  case (LConI Δ l A m B)
  then show ?case
    by (meson lderives.intros)
next
  case (LConE1 Δ l A B)
  then show ?case
    by (meson lderives.intros)
next
  case (LConE2 Δ l A B)
  then show ?case
    by (meson lderives.intros)
next
  case (LDisI1 Δ l A B)
  then show ?case
    by (meson lderives.intros)
next
  case (LDisI2 Δ l B A)
  then show ?case
    by (meson lderives.intros)
next
  case (LDisE Δ l A B m n C p q)
  show ?case
  proof (rule lderives.intros(10))
    show "Σ ⊢L (l, Dis A B)"
      using LDisE.IH(1) LDisE.prems by blast
    have sub_m: "set ((m, A) # Δ) ⊆ insert x (set ((m, A) # Σ))"
      using LDisE.prems(1) by auto
    have sub_context_m: "set Γ ⊆ set ((m, A) # Σ)"
      using LDisE.prems(3) by auto
    show "(m, A) # Σ ⊢L (n, C)"
      by (rule LDisE.IH(2)[OF sub_m LDisE.prems(2) sub_context_m])
    have sub_p: "set ((p, B) # Δ) ⊆ insert x (set ((p, B) # Σ))"
      using LDisE.prems(1) by auto
    have sub_context_p: "set Γ ⊆ set ((p, B) # Σ)"
      using LDisE.prems(3) by auto
    show "(p, B) # Σ ⊢L (q, C)"
      by (rule LDisE.IH(3)[OF sub_p LDisE.prems(2) sub_context_p])
  qed
qed

lemma labelled_cut:
  assumes "Γ ⊢L x" and "x # Δ ⊢L y"
  shows "Γ @ Δ ⊢L y"
proof (rule labelled_cut_general)
  show "Γ ⊢L x"
    by (rule assms(1))
  show "x # Δ ⊢L y"
    by (rule assms(2))
  show "set (x # Δ) ⊆ insert x (set (Γ @ Δ))"
    by auto
  show "set Γ ⊆ set (Γ @ Δ)"
    by auto
qed

lemma assumption_substitution_lift:
  assumes "x ∈ set Γ"
  shows "(fst x, fm_subst σ (snd x)) ∈ set (map (map_prod id (fm_subst σ)) Γ)"
  using assms by (induction Γ) auto

lemma labelled_substitution_atom_aux:
  assumes "Γ ⊢L x"
  shows "map (map_prod id (fm_subst σ)) Γ ⊢L (fst x, fm_subst σ (snd x))"
  using assms
proof (induction rule: lderives.induct)
  case (LAssm x Γ)
  then have "(fst x, fm_subst σ (snd x)) ∈
      set (map (map_prod id (fm_subst σ)) Γ)"
    by (rule assumption_substitution_lift)
  then show ?case
    by (rule lderives.LAssm)
next
  case (LBotE Γ l A)
  then show ?case
    by (auto intro: lderives.LBotE)
next
  case (LImpI l A Γ m B)
  then have "(l, fm_subst σ A) # map (map_prod id (fm_subst σ)) Γ
      ⊢L (m, fm_subst σ B)"
    by (simp add: id_def)
  then have "map (map_prod id (fm_subst σ)) Γ
      ⊢L (lam l m, Imp (fm_subst σ A) (fm_subst σ B))"
    by (rule lderives.LImpI)
  then show ?case
    by (simp add: id_def)
next
  case (LImpE Γ l A B m)
  then show ?case
    by (auto intro: lderives.LImpE)
next
  case (LConI Γ l A m B)
  then show ?case
    by (auto intro: lderives.LConI)
next
  case (LConE1 Γ l A B)
  then show ?case
    by (auto intro: lderives.LConE1)
next
  case (LConE2 Γ l A B)
  then show ?case
    by (auto intro: lderives.LConE2)
next
  case (LDisI1 Γ l A B)
  then show ?case
    by (auto intro: lderives.LDisI1)
next
  case (LDisI2 Γ l B A)
  then show ?case
    by (auto intro: lderives.LDisI2)
next
  case (LDisE Γ l A B m n C p q)
  then show ?case
    by (auto intro: lderives.LDisE)
qed

lemma labelled_substitution_atom:
  assumes "Γ ⊢L (l, A)"
  shows "map (map_prod id (fm_subst σ)) Γ ⊢L (l, fm_subst σ A)"
  using labelled_substitution_atom_aux[OF assms] by simp

end

end