Theory Label_Algebra

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

    Label-algebra locale packaging the two generic adequacy obligations
    (erasure-to-unit uniformity and lift coherence), and the
    framework-adequacy meta-theorem reducing labelled derivability up to a
    label to ordinary derivability after erasure.
*)

theory Label_Algebra
  imports Erasure
begin

text ‹
The label-algebra layer packages the two generic adequacy requirements used by
the concrete interpretations.  Label erasure targets @{typ unit}, so every
erasure map is extensionally the unique one.  The lift operation may inspect
the labelled context, which is needed for calculi whose assumption labels carry
semantic data.
›

lemma erase_ctx_mem_label:
  assumes "A ∈ set (erase_ctx Γ)"
  obtains l where "(l, A) ∈ set Γ"
proof -
  from assms obtain x where "x ∈ set Γ" and "snd x = A"
    unfolding erase_ctx_def by auto
  obtain l B where "x = (l, B)"
    by (cases x)
  with ‹x ∈ set Γ› ‹snd x = A› have "(l, A) ∈ set Γ"
    by simp
  then show thesis
    by (rule that)
qed

context label_structure
begin

lemma lifting_general_aux:
  assumes "Δ ⊢ A" and "erase_ctx Γ = Δ"
  shows "∃l. Γ ⊢L (l, A)"
  using assms
proof (induction arbitrary: Γ rule: derives.induct)
  case (Assm A Δ)
  then have "A ∈ set (erase_ctx Γ)"
    by simp
  then obtain l where "(l, A) ∈ set Γ"
    by (rule erase_ctx_mem_label)
  then have "Γ ⊢L (l, A)"
    by (rule LAssm)
  then show ?case
    by blast
next
  case (BotE Δ A)
  then obtain l where "Γ ⊢L (l, Bot)"
    by blast
  then have "Γ ⊢L (abort l, A)"
    by (rule LBotE)
  then show ?case
    by blast
next
  case (ImpI A Δ B)
  have "erase_ctx ((undefined, A) # Γ) = A # Δ"
    using ImpI.prems by simp
  then obtain m where "(undefined, A) # Γ ⊢L (m, B)"
    using ImpI.IH by blast
  then have "Γ ⊢L (lam undefined m, Imp A B)"
    by (rule LImpI)
  then show ?case
    by blast
next
  case (ImpE Δ A B)
  then obtain l where imp: "Γ ⊢L (l, Imp A B)"
    by blast
  from ImpE obtain m where arg: "Γ ⊢L (m, A)"
    by blast
  from imp arg have "Γ ⊢L (app l m, B)"
    by (rule LImpE)
  then show ?case
    by blast
next
  case (ConI Δ A B)
  then obtain l where left: "Γ ⊢L (l, A)"
    by blast
  from ConI obtain m where right: "Γ ⊢L (m, B)"
    by blast
  from left right have "Γ ⊢L (pair l m, Con A B)"
    by (rule LConI)
  then show ?case
    by blast
next
  case (ConE1 Δ A B)
  then obtain l where "Γ ⊢L (l, Con A B)"
    by blast
  then have "Γ ⊢L (fst_l l, A)"
    by (rule LConE1)
  then show ?case
    by blast
next
  case (ConE2 Δ A B)
  then obtain l where "Γ ⊢L (l, Con A B)"
    by blast
  then have "Γ ⊢L (snd_l l, B)"
    by (rule LConE2)
  then show ?case
    by blast
next
  case (DisI1 Δ A B)
  then obtain l where "Γ ⊢L (l, A)"
    by blast
  then have "Γ ⊢L (inl l, Dis A B)"
    by (rule LDisI1)
  then show ?case
    by blast
next
  case (DisI2 Δ B A)
  then obtain l where "Γ ⊢L (l, B)"
    by blast
  then have "Γ ⊢L (inr l, Dis A B)"
    by (rule LDisI2)
  then show ?case
    by blast
next
  case (DisE Δ A B C)
  then obtain l where disj: "Γ ⊢L (l, Dis A B)"
    by blast
  have left_ctx: "erase_ctx ((undefined, A) # Γ) = A # Δ"
    using DisE.prems by simp
  then obtain n where left: "(undefined, A) # Γ ⊢L (n, C)"
    using DisE.IH(2) by blast
  have right_ctx: "erase_ctx ((undefined, B) # Γ) = B # Δ"
    using DisE.prems by simp
  then obtain q where right: "(undefined, B) # Γ ⊢L (q, C)"
    using DisE.IH(3) by blast
  from disj left right have "Γ ⊢L (cases l undefined n undefined q, C)"
    by (rule LDisE)
  then show ?case
    by blast
qed

theorem lifting_general:
  assumes "erase_ctx Γ ⊢ A"
  shows "∃l. Γ ⊢L (l, A)"
  using lifting_general_aux[OF assms refl] .

end

locale label_algebra =
  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"
    and lderives :: "('l, 'f) lfm list ⇒ ('l, 'f) lfm ⇒ bool"
      ("_ ⊢L _" [50, 50] 50)
    and erase_label :: "'l ⇒ unit"
    and lift_label :: "('l, 'f) lfm list ⇒ 'f fm ⇒ 'l"
  assumes erase_label_unique [simp]: "erase_label l = ()"
    and erasure_sound_law:
      "Γ ⊢L x ⟹ erase_ctx Γ ⊢ erase_lfm x"
    and lift_coherence:
      "erase_ctx Γ ⊢ A ⟹ Γ ⊢L (lift_label Γ A, A)"
begin

definition erase_judgement ::
    "(('l, 'f) lfm list × ('l, 'f) lfm) ⇒ ('f fm list × 'f fm)"
  where "erase_judgement J = (erase_ctx (fst J), erase_lfm (snd J))"

lemma erase_judgement_simps [simp]:
  "erase_judgement (Γ, (l, A)) = (erase_ctx Γ, A)"
  by (simp add: erase_judgement_def)

lemma erasure_uniformity:
  "erase_label (app l m) = ()"
  "erase_label (lam l m) = ()"
  "erase_label (pair l m) = ()"
  "erase_label (fst_l l) = ()"
  "erase_label (snd_l l) = ()"
  "erase_label (abort l) = ()"
  "erase_label (inl l) = ()"
  "erase_label (inr l) = ()"
  "erase_label (cases l m n p q) = ()"
  by simp_all

lemma erasure_uniformity_judgement:
  "erase_judgement (Γ, (app l m, A)) = (erase_ctx Γ, A)"
  "erase_judgement (Γ, (lam l m, Imp A B)) = (erase_ctx Γ, Imp A B)"
  "erase_judgement (Γ, (pair l m, Con A B)) = (erase_ctx Γ, Con A B)"
  "erase_judgement (Γ, (fst_l l, A)) = (erase_ctx Γ, A)"
  "erase_judgement (Γ, (snd_l l, B)) = (erase_ctx Γ, B)"
  "erase_judgement (Γ, (abort l, A)) = (erase_ctx Γ, A)"
  "erase_judgement (Γ, (inl l, Dis A B)) = (erase_ctx Γ, Dis A B)"
  "erase_judgement (Γ, (inr l, Dis A B)) = (erase_ctx Γ, Dis A B)"
  "erase_judgement (Γ, (cases l m n p q, C)) = (erase_ctx Γ, C)"
  by simp_all

theorem framework_adequacy:
  fixes ΓL :: "('l, 'f) lfm list"
    and A :: "'f fm"
  shows "(∃l. ΓL ⊢L (l, A)) ⟷
    (erase_ctx ΓL ⊢ A ∧ ΓL ⊢L (lift_label ΓL A, A))"
proof
  assume "∃l. ΓL ⊢L (l, A)"
  then obtain l where deriv: "ΓL ⊢L (l, A)"
    by blast
  have "erase_ctx ΓL ⊢ erase_lfm (l, A)"
    using deriv by (rule erasure_sound_law)
  then have ordinary: "erase_ctx ΓL ⊢ A"
    by simp
  moreover have "ΓL ⊢L (lift_label ΓL A, A)"
    using ordinary by (rule lift_coherence)
  ultimately show "erase_ctx ΓL ⊢ A ∧ ΓL ⊢L (lift_label ΓL A, A)"
    by blast
next
  assume "erase_ctx ΓL ⊢ A ∧ ΓL ⊢L (lift_label ΓL A, A)"
  then show "∃l. ΓL ⊢L (l, A)"
    by blast
qed

corollary framework_adequacy_iff:
  fixes ΓL :: "('l, 'f) lfm list"
    and A :: "'f fm"
  shows "(∃l. ΓL ⊢L (l, A)) ⟷ erase_ctx ΓL ⊢ A"
proof
  assume "∃l. ΓL ⊢L (l, A)"
  then show "erase_ctx ΓL ⊢ A"
    using framework_adequacy by blast
next
  assume ordinary: "erase_ctx ΓL ⊢ A"
  then have "ΓL ⊢L (lift_label ΓL A, A)"
    by (rule lift_coherence)
  with ordinary show "∃l. ΓL ⊢L (l, A)"
    using framework_adequacy by blast
qed

end

end