Theory Unit_Labels

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

    Singleton-label instance of the framework: labelled derivability
    coincides with ordinary natural deduction, witnessing conservativity.
*)

theory Unit_Labels
  imports Label_Algebra
begin

text ‹
This theory instantiates the labelled kernel with a singleton label type.  Since
all label constructors return the unique label, labelled derivability over the
lifted context is equivalent to ordinary natural deduction.
›

datatype unit_label = Star

interpretation unit_labels: label_structure
  where app = "λ_ _. Star"
    and lam = "λ_ _. Star"
    and pair = "λ_ _. Star"
    and fst_l = "λ_. Star"
    and snd_l = "λ_. Star"
    and abort = "λ_. Star"
    and inl = "λ_. Star"
    and inr = "λ_. Star"
    and cases = "λ_ _ _ _ _. Star"
  .

definition unit_erase_label :: "unit_label ⇒ unit" where
  "unit_erase_label l = ()"

definition unit_lift_label :: "(unit_label, 'a) lfm list ⇒ 'a fm ⇒ unit_label" where
  "unit_lift_label Γ A = Star"

interpretation unit_labels: label_algebra
  where app = "λ_ _. Star"
    and lam = "λ_ _. Star"
    and pair = "λ_ _. Star"
    and fst_l = "λ_. Star"
    and snd_l = "λ_. Star"
    and abort = "λ_. Star"
    and inl = "λ_. Star"
    and inr = "λ_. Star"
    and cases = "λ_ _ _ _ _. Star"
    and lderives = unit_labels.lderives
    and erase_label = unit_erase_label
    and lift_label = unit_lift_label
proof
  fix l
  show "unit_erase_label l = ()"
    by (simp add: unit_erase_label_def)
next
  fix Γ :: "(unit_label, 'a) lfm list" and x :: "(unit_label, 'a) lfm"
  assume "unit_labels.lderives Γ x"
  then show "erase_ctx Γ ⊢ erase_lfm x"
    by (rule unit_labels.erasure_sound)
next
  fix Γ :: "(unit_label, 'a) lfm list" and A :: "'a fm"
  assume ordinary: "erase_ctx Γ ⊢ A"
  then obtain l where deriv: "unit_labels.lderives Γ (l, A)"
    using unit_labels.lifting_general by blast
  then show "unit_labels.lderives Γ (unit_lift_label Γ A, A)"
    by (cases l) (simp add: unit_lift_label_def)
qed

definition unit_lift :: "'a fm list ⇒ (unit_label × 'a fm) list" where
  "unit_lift Γ = map (λA. (Star, A)) Γ"

lemma erase_ctx_unit_lift [simp]:
  "erase_ctx (unit_lift Γ) = Γ"
  by (simp add: unit_lift_def erase_ctx_def comp_def)

lemma unit_labels_from_ordinary:
  assumes "Γ ⊢ A"
  shows "unit_labels.lderives (unit_lift Γ) (Star, A)"
  using assms
proof (induction rule: derives.induct)
  case (Assm A Γ)
  then have "(Star, A) ∈ set (unit_lift Γ)"
    by (auto simp: unit_lift_def)
  then show ?case
    by (rule unit_labels.LAssm)
next
  case (BotE Γ A)
  have "unit_labels.lderives (unit_lift Γ) ((λ_. Star) Star, A)"
    using BotE.IH by (rule unit_labels.LBotE)
  then show ?case
    by simp
next
  case (ImpI A Γ B)
  have "unit_labels.lderives ((Star, A) # unit_lift Γ) (Star, B)"
    using ImpI.IH by (simp add: unit_lift_def)
  then show ?case
    by (rule unit_labels.LImpI)
next
  case (ImpE Γ A B)
  have "unit_labels.lderives (unit_lift Γ) ((λ_ _. Star) Star Star, B)"
    using ImpE.IH by (rule unit_labels.LImpE)
  then show ?case
    by simp
next
  case (ConI Γ A B)
  have "unit_labels.lderives (unit_lift Γ) ((λ_ _. Star) Star Star, Con A B)"
    using ConI.IH by (rule unit_labels.LConI)
  then show ?case
    by simp
next
  case (ConE1 Γ A B)
  have "unit_labels.lderives (unit_lift Γ) ((λ_. Star) Star, A)"
    using ConE1.IH by (rule unit_labels.LConE1)
  then show ?case
    by simp
next
  case (ConE2 Γ A B)
  have "unit_labels.lderives (unit_lift Γ) ((λ_. Star) Star, B)"
    using ConE2.IH by (rule unit_labels.LConE2)
  then show ?case
    by simp
next
  case (DisI1 Γ A B)
  have "unit_labels.lderives (unit_lift Γ) ((λ_. Star) Star, Dis A B)"
    using DisI1.IH by (rule unit_labels.LDisI1)
  then show ?case
    by simp
next
  case (DisI2 Γ B A)
  have "unit_labels.lderives (unit_lift Γ) ((λ_. Star) Star, Dis A B)"
    using DisI2.IH by (rule unit_labels.LDisI2)
  then show ?case
    by simp
next
  case (DisE Γ A B C)
  have disj: "unit_labels.lderives (unit_lift Γ) (Star, Dis A B)"
    by (rule DisE.IH(1))
  have left: "unit_labels.lderives ((Star, A) # unit_lift Γ) (Star, C)"
    using DisE.IH(2) by (simp add: unit_lift_def)
  have right: "unit_labels.lderives ((Star, B) # unit_lift Γ) (Star, C)"
    using DisE.IH(3) by (simp add: unit_lift_def)
  have "unit_labels.lderives (unit_lift Γ) ((λ_ _ _ _ _. Star) Star Star Star Star Star, C)"
    using disj left right by (rule unit_labels.LDisE)
  then show ?case
    by simp
qed

theorem unit_labels_conservative:
  "Γ ⊢ A ⟷ unit_labels.lderives (unit_lift Γ) (Star, A)"
proof
  assume ordinary: "Γ ⊢ A"
  then have ordinary_erased: "erase_ctx (unit_lift Γ) ⊢ A"
    by simp
  have "unit_labels.lderives
      (unit_lift Γ) (unit_lift_label (unit_lift Γ) A, A)"
    using ordinary_erased by (rule unit_labels.lift_coherence)
  with ordinary_erased have "∃l. unit_labels.lderives (unit_lift Γ) (l, A)"
    using unit_labels.framework_adequacy by blast
  then obtain l where "unit_labels.lderives (unit_lift Γ) (l, A)"
    by blast
  then show "unit_labels.lderives (unit_lift Γ) (Star, A)"
    by (cases l) simp
next
  assume "unit_labels.lderives (unit_lift Γ) (Star, A)"
  then have "∃l. unit_labels.lderives (unit_lift Γ) (l, A)"
    by blast
  then have "erase_ctx (unit_lift Γ) ⊢ A"
    using unit_labels.framework_adequacy by blast
  then show "Γ ⊢ A"
    by simp
qed

end