Theory Modal_Labels_Example

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

    Possible-world modal instance: instantiates the framework locale as
    @{term modal_labels} and extends the propositional labelled calculus
    with modal BoxI and BoxE rules; carries the soundness link to Kripke
    validity.
*)

theory Modal_Labels_Example
  imports Label_Algebra
begin

text ‹
This theory instantiates the framework locale as @{term modal_labels} and then
extends the resulting propositional labelled calculus with modal @{text BoxI}
and @{text BoxE} rules.  Modal labels carry possible-world annotations; the
propositional constructors preserve the current world, while box elimination
projects to an accessible world.
›

datatype modal_label =
    MWorld nat
  | MApp modal_label modal_label
  | MLam modal_label modal_label
  | MPair modal_label modal_label
  | MFst modal_label
  | MSnd modal_label
  | MInl modal_label
  | MInr modal_label
  | MCases modal_label modal_label modal_label modal_label modal_label
  | MAbort modal_label
  | MBoxI modal_label
  | MBoxE modal_label

fun world_of :: "modal_label ⇒ nat" where
  "world_of (MWorld w) = w"
| "world_of (MApp l m) = world_of l"
| "world_of (MLam l m) = world_of m"
| "world_of (MPair l m) = world_of l"
| "world_of (MFst l) = world_of l"
| "world_of (MSnd l) = world_of l"
| "world_of (MInl l) = world_of l"
| "world_of (MInr l) = world_of l"
| "world_of (MCases l m n p q) = world_of l"
| "world_of (MAbort l) = world_of l"
| "world_of (MBoxI l) = world_of l"
| "world_of (MBoxE l) = world_of l"

interpretation modal_labels: label_structure
  where app = MApp
    and lam = MLam
    and pair = MPair
    and fst_l = MFst
    and snd_l = MSnd
    and abort = MAbort
    and inl = MInl
    and inr = MInr
    and cases = MCases
  .

definition modal_erase_label :: "modal_label ⇒ unit" where
  "modal_erase_label l = ()"

definition modal_lift_label :: "(modal_label, 'a) lfm list ⇒ 'a fm ⇒ modal_label" where
  "modal_lift_label Γ A =
    (SOME l. modal_labels.lderives Γ (l, A))"

interpretation modal_labels: label_algebra
  where app = MApp
    and lam = MLam
    and pair = MPair
    and fst_l = MFst
    and snd_l = MSnd
    and abort = MAbort
    and inl = MInl
    and inr = MInr
    and cases = MCases
    and lderives = modal_labels.lderives
    and erase_label = modal_erase_label
    and lift_label = modal_lift_label
proof
  fix l
  show "modal_erase_label l = ()"
    by (simp add: modal_erase_label_def)
next
  fix Γ :: "(modal_label, 'a) lfm list" and x :: "(modal_label, 'a) lfm"
  assume "modal_labels.lderives Γ x"
  then show "erase_ctx Γ ⊢ erase_lfm x"
    by (rule modal_labels.erasure_sound)
next
  fix Γ :: "(modal_label, 'a) lfm list" and A :: "'a fm"
  assume ordinary: "erase_ctx Γ ⊢ A"
  have "∃l. modal_labels.lderives Γ (l, A)"
    by (rule modal_labels.lifting_general[OF ordinary])
  then show "modal_labels.lderives Γ (modal_lift_label Γ A, A)"
    unfolding modal_lift_label_def by (rule someI_ex)
qed

datatype 'a mfm =
    MAtom 'a
  | MBot
  | MImp "'a mfm" "'a mfm"
  | MCon "'a mfm" "'a mfm"
  | MDis "'a mfm" "'a mfm"
  | Box "'a mfm"

primrec modalise_fm :: "'a fm ⇒ 'a mfm" where
  "modalise_fm (Atom p) = MAtom p"
| "modalise_fm Bot = MBot"
| "modalise_fm (Imp A B) = MImp (modalise_fm A) (modalise_fm B)"
| "modalise_fm (Con A B) = MCon (modalise_fm A) (modalise_fm B)"
| "modalise_fm (Dis A B) = MDis (modalise_fm A) (modalise_fm B)"

definition modalise_lfm :: "nat ⇒ (modal_label, 'a) lfm ⇒ modal_label × 'a mfm" where
  "modalise_lfm w x = (MWorld w, modalise_fm (snd x))"

primrec modal_kripke_sat ::
    "(nat ⇒ 'a ⇒ bool) ⇒ (nat ⇒ nat ⇒ bool) ⇒ nat ⇒ 'a mfm ⇒ bool"
where
  "modal_kripke_sat V R w (MAtom p) = V w p"
| "modal_kripke_sat V R w MBot = False"
| "modal_kripke_sat V R w (MImp A B) =
    (modal_kripke_sat V R w A ⟶ modal_kripke_sat V R w B)"
| "modal_kripke_sat V R w (MCon A B) =
    (modal_kripke_sat V R w A ∧ modal_kripke_sat V R w B)"
| "modal_kripke_sat V R w (MDis A B) =
    (modal_kripke_sat V R w A ∨ modal_kripke_sat V R w B)"
| "modal_kripke_sat V R w (Box A) =
    (∀v. R w v ⟶ modal_kripke_sat V R v A)"

inductive mlderives ::
    "(modal_label × 'a mfm) list ⇒
      (nat ⇒ nat ⇒ bool) ⇒ (modal_label × 'a mfm) ⇒ bool"
where
  MAssm: "x ∈ set Γ ⟹ mlderives Γ R x"
| MBotE: "mlderives Γ R (l, MBot) ⟹ mlderives Γ R (MAbort l, A)"
| MImpI:
    "world_of l = world_of m ⟹
     mlderives ((l, A) # Γ) R (m, B) ⟹
     mlderives Γ R (MLam l m, MImp A B)"
| MImpE:
    "world_of l = world_of m ⟹
     mlderives Γ R (l, MImp A B) ⟹
     mlderives Γ R (m, A) ⟹
     mlderives Γ R (MApp l m, B)"
| MConI:
    "world_of l = world_of m ⟹
     mlderives Γ R (l, A) ⟹
     mlderives Γ R (m, B) ⟹
     mlderives Γ R (MPair l m, MCon A B)"
| MConE1: "mlderives Γ R (l, MCon A B) ⟹ mlderives Γ R (MFst l, A)"
| MConE2: "mlderives Γ R (l, MCon A B) ⟹ mlderives Γ R (MSnd l, B)"
| MDisI1: "mlderives Γ R (l, A) ⟹ mlderives Γ R (MInl l, MDis A B)"
| MDisI2: "mlderives Γ R (l, B) ⟹ mlderives Γ R (MInr l, MDis A B)"
| MDisE:
    "world_of l = world_of m ⟹
     world_of l = world_of n ⟹
     world_of l = world_of p ⟹
     world_of l = world_of q ⟹
     mlderives Γ R (l, MDis A B) ⟹
     mlderives ((m, A) # Γ) R (n, C) ⟹
     mlderives ((p, B) # Γ) R (q, C) ⟹
     mlderives Γ R (MCases l m n p q, C)"
| MBoxI:
    "(⋀v. R (world_of l) v ⟹
      ∃m. world_of m = v ∧ mlderives Γ R (m, A)) ⟹
     mlderives Γ R (MBoxI l, Box A)"
| MBoxE:
    "mlderives Γ R (l, Box A) ⟹
     R (world_of l) v ⟹
     mlderives Γ R (MBoxE (MWorld v), A)"

theorem propositional_modal_sound:
  assumes "modal_labels.lderives Γ x"
  shows "∃l. world_of l = w ∧
    mlderives (map (modalise_lfm w) Γ) R (l, modalise_fm (snd x))"
  using assms
proof (induction arbitrary: w R rule: modal_labels.lderives.induct)
  case (LAssm x Γ)
  then show ?case
    by (intro exI[of _ "MWorld w"])
      (auto simp: modalise_lfm_def intro: mlderives.MAssm)
next
  case (LBotE Γ l A)
  then obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, MBot)"
    by auto
  then show ?case
    by (intro exI[of _ "MAbort k"]) (auto intro: mlderives.MBotE)
next
  case (LImpI l A Γ m B)
  then obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) ((l, A) # Γ)) R (k, modalise_fm B)"
    by auto
  then have body: "mlderives ((MWorld w, modalise_fm A) #
      map (modalise_lfm w) Γ) R (k, modalise_fm B)"
    by (simp add: modalise_lfm_def)
  then have "mlderives (map (modalise_lfm w) Γ) R
      (MLam (MWorld w) k, MImp (modalise_fm A) (modalise_fm B))"
    using k(1) by (auto intro: mlderives.MImpI)
  then show ?case
    by (intro exI[of _ "MLam (MWorld w) k"]) (simp add: k(1))
next
  case (LImpE Γ l A B m)
  from LImpE.IH(1)[of w R] obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, MImp (modalise_fm A) (modalise_fm B))"
    by auto
  from LImpE.IH(2)[of w R] obtain h where h: "world_of h = w"
      "mlderives (map (modalise_lfm w) Γ) R (h, modalise_fm A)"
    by auto
  then have "mlderives (map (modalise_lfm w) Γ) R (MApp k h, modalise_fm B)"
    using k by (auto intro: mlderives.MImpE)
  then show ?case
    by (intro exI[of _ "MApp k h"]) (simp add: k h)
next
  case (LConI Γ l A m B)
  from LConI.IH(1)[of w R] obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, modalise_fm A)"
    by auto
  from LConI.IH(2)[of w R] obtain h where h: "world_of h = w"
      "mlderives (map (modalise_lfm w) Γ) R (h, modalise_fm B)"
    by auto
  then have "mlderives (map (modalise_lfm w) Γ) R
      (MPair k h, MCon (modalise_fm A) (modalise_fm B))"
    using k by (auto intro: mlderives.MConI)
  then show ?case
    by (intro exI[of _ "MPair k h"]) (simp add: k h)
next
  case (LConE1 Γ l A B)
  then obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, MCon (modalise_fm A) (modalise_fm B))"
    by auto
  then show ?case
    by (intro exI[of _ "MFst k"]) (auto intro: mlderives.MConE1)
next
  case (LConE2 Γ l A B)
  then obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, MCon (modalise_fm A) (modalise_fm B))"
    by auto
  then show ?case
    by (intro exI[of _ "MSnd k"]) (auto intro: mlderives.MConE2)
next
  case (LDisI1 Γ l A B)
  then obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, modalise_fm A)"
    by auto
  then show ?case
    by (intro exI[of _ "MInl k"]) (auto intro: mlderives.MDisI1)
next
  case (LDisI2 Γ l B A)
  then obtain k where k: "world_of k = w"
      "mlderives (map (modalise_lfm w) Γ) R (k, modalise_fm B)"
    by auto
  then show ?case
    by (intro exI[of _ "MInr k"]) (auto intro: mlderives.MDisI2)
next
  case (LDisE Γ l A B m n C p q)
  from LDisE.IH(1)[of w R] obtain d where d:
      "world_of d = w"
      "mlderives (map (modalise_lfm w) Γ) R (d, MDis (modalise_fm A) (modalise_fm B))"
    by auto
  from LDisE.IH(2)[of w R] obtain left where left:
      "world_of left = w"
      "mlderives (map (modalise_lfm w) ((m, A) # Γ)) R (left, modalise_fm C)"
    by auto
  from LDisE.IH(3)[of w R] obtain right where right:
      "world_of right = w"
      "mlderives (map (modalise_lfm w) ((p, B) # Γ)) R (right, modalise_fm C)"
    by auto
  from left have left_deriv: "mlderives ((MWorld w, modalise_fm A) #
      map (modalise_lfm w) Γ) R (left, modalise_fm C)"
    by (simp add: modalise_lfm_def)
  from right have right_deriv: "mlderives ((MWorld w, modalise_fm B) #
      map (modalise_lfm w) Γ) R (right, modalise_fm C)"
    by (simp add: modalise_lfm_def)
  have "mlderives (map (modalise_lfm w) Γ) R
      (MCases d (MWorld w) left (MWorld w) right, modalise_fm C)"
    using d left right left_deriv right_deriv by (auto intro: mlderives.MDisE)
  then show ?case
    by (intro exI[of _ "MCases d (MWorld w) left (MWorld w) right"])
      (simp add: d left right)
qed

theorem modal_labels_sound:
  assumes "mlderives Γ R x"
    and "∀(l, A) ∈ set Γ. modal_kripke_sat V R (world_of l) A"
  shows "modal_kripke_sat V R (world_of (fst x)) (snd x)"
  using assms
proof (induction arbitrary: V rule: mlderives.induct)
  case (MAssm x Γ R)
  then show ?case
    by (cases x) auto
next
  case (MBotE Γ R l A)
  then show ?case
    by auto
next
  case (MImpI l m A Γ R B)
  then show ?case
    by auto
next
  case (MImpE l m Γ R A B)
  then show ?case
    by auto
next
  case (MConI l m Γ R A B)
  then show ?case
    by auto
next
  case (MConE1 Γ R l A B)
  then show ?case
    by auto
next
  case (MConE2 Γ R l A B)
  then show ?case
    by auto
next
  case (MDisI1 Γ R l A B)
  then show ?case
    by auto
next
  case (MDisI2 Γ R l B A)
  then show ?case
    by auto
next
  case (MDisE l m n p q Γ R A B C)
  then show ?case
    by auto
next
  case (MBoxI l R Γ A)
  then show ?case
    by auto
next
  case (MBoxE Γ R l A v)
  then show ?case
    by auto
qed

end