Theory Labelled_Formulas

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

    Propositional formula language and elementary label-erasure operations.
*)

theory Labelled_Formulas
  imports Main
begin

text ‹
This theory fixes the propositional formula language and the elementary
operations that erase labels from labelled formulae, databases, and list
contexts.  Labels are deliberately represented by a product component, so the
logical shape of a labelled formula is recovered by taking its second
projection.
›

datatype 'a fm =
    Atom 'a
  | Bot
  | Imp "'a fm" "'a fm"
  | Con "'a fm" "'a fm"
  | Dis "'a fm" "'a fm"

type_synonym ('l, 'a) lfm = "'l × 'a fm"

definition erase_lfm :: "('l, 'a) lfm ⇒ 'a fm" where
  "erase_lfm x = snd x"

definition erase_db :: "('l, 'a) lfm set ⇒ 'a fm set" where
  "erase_db Γ = snd ` Γ"

definition erase_ctx :: "('l, 'a) lfm list ⇒ 'a fm list" where
  "erase_ctx Γ = map snd Γ"

lemma erase_lfm_simps [simp]:
  "erase_lfm (l, A) = A"
  by (simp add: erase_lfm_def)

lemma erase_ctx_Nil [simp]:
  "erase_ctx [] = []"
  by (simp add: erase_ctx_def)

lemma erase_ctx_Cons [simp]:
  "erase_ctx (x # Γ) = erase_lfm x # erase_ctx Γ"
  by (cases x) (simp add: erase_ctx_def)

lemma erase_ctx_append [simp]:
  "erase_ctx (Γ @ Δ) = erase_ctx Γ @ erase_ctx Δ"
  by (simp add: erase_ctx_def)

lemma erase_db_insert [simp]:
  "erase_db (insert x Γ) = insert (erase_lfm x) (erase_db Γ)"
  by (cases x) (auto simp: erase_db_def erase_lfm_def)

lemma erase_db_Un [simp]:
  "erase_db (Γ ∪ Δ) = erase_db Γ ∪ erase_db Δ"
  by (auto simp: erase_db_def)

end