Theory MLSS_Typing_Defs

theory MLSS_Typing_Defs
  imports MLSS_Semantics "HOL-Library.Adhoc_Overloading"
begin

section ‹Typing Rules›
text ‹
  We define the typing rules for set terms and atoms, as well as
  for formulae
›

inductive types_pset_term :: "('a ⇒ nat) ⇒ 'a pset_term ⇒ nat ⇒ bool" ("_ ⊢ _ : _" [46, 46, 46] 46) where
  "v ⊢ ∅ n : Suc n"
| "v ⊢ Var x : v x"
| "v ⊢ t : l ⟹ v ⊢ Single t : Suc l"
| "v ⊢ s : l ⟹ v ⊢ t : l ⟹ l ≠ 0 ⟹ v ⊢ s ⊔⇩s t : l"
| "v ⊢ s : l ⟹ v ⊢ t : l ⟹ l ≠ 0 ⟹ v ⊢ s ⊓⇩s t : l"
| "v ⊢ s : l ⟹ v ⊢ t : l ⟹ l ≠ 0 ⟹ v ⊢ s -⇩s t : l"

text ‹Activate this bundle to avoid ambiguity between
      \<^const>‹Set.member› and \<^const>‹types_pset_term›.›
bundle Set_member_no_ascii_notation
begin
no_notation Set.member ("(_/ : _)" [51, 51] 50)
end

inductive_cases types_pset_term_cases:
  "v ⊢ ∅ n : l" "v ⊢ Var x : l" "v ⊢ Single t : l"
  "v ⊢ s ⊔⇩s t : l" "v ⊢ s ⊓⇩s t : l" "v ⊢ s -⇩s t : l"

lemma types_pset_term_intros':
  "l = Suc n ⟹ v ⊢ ∅ n : l"
  "l = v x ⟹ v ⊢ Var x : l"
  "l ≠ 0 ⟹ v ⊢ t : nat.pred l ⟹ v ⊢ Single t : l"
  by (auto simp add: types_pset_term.intros(1,2,3) pred_def split: nat.splits)

definition type_of_term :: "('a ⇒ nat) ⇒ 'a pset_term ⇒ nat" where
  "type_of_term v t ≡ THE l. v ⊢ t : l"

inductive types_pset_atom :: "('a ⇒ nat) ⇒ 'a pset_atom ⇒ bool" where
  "⟦ v ⊢ s : l; v ⊢ t : l ⟧ ⟹ types_pset_atom v (s =⇩s t)"
| "⟦ v ⊢ s : l; v ⊢ t : Suc l⟧ ⟹ types_pset_atom v (s ∈⇩s t)"

definition types_pset_fm :: "('a ⇒ nat) ⇒ 'a pset_fm ⇒ bool" where
  "types_pset_fm v φ ≡ (∀a ∈ atoms φ. types_pset_atom v a)"

consts types :: "('a ⇒ nat) ⇒ 'b ⇒ bool" (infix "⊢" 45)
adhoc_overloading types types_pset_atom types_pset_fm

inductive_cases types_pset_atom_Member_cases:
  "v ⊢ s ∈⇩s t1 ⊔⇩s t2" "v ⊢ s ∈⇩s t1 ⊓⇩s t2" "v ⊢ s ∈⇩s t1 -⇩s t2" "v ⊢ s ∈⇩s Single t"

context includes Set_member_no_ascii_notation
begin
abbreviation "urelem' v (φ :: 'a pset_fm) t ≡ v ⊢ φ ∧ v ⊢ t : 0"
end

definition urelem :: "'a pset_fm ⇒ 'a pset_term ⇒ bool" where
  "urelem φ t ≡ (∃v. urelem' v φ t)"

end