Theory T_G_Prelim

(* Preliminaries on the tag and guard encodings  *)
theory T_G_Prelim
imports Mcalc
begin


(* Copy of ProblemIk, together with a partitioning of the types.
O stands for the original---this copy shall be used
as ``the original problem: *)

locale ProblemIkTpart =
Ik? : ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym ⇒ bool"
and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp +
fixes
    prot :: "'tp ⇒ bool" (* types aimed to be protected (with tags or guards) *)
and protFw :: "'tp ⇒ bool" (* types aimed to be protected in a featherweight fashion  *)
assumes
    tp_disj: "⋀ σ. ¬ prot σ ∨ ¬ protFw σ"
and tp_mcalc: "⋀ σ. prot σ ∨ protFw σ ∨ (∀ c ∈ Φ. σ ⊢ c)"
begin

(* The notion of being a result type of some operation symbol: *)
definition isRes where "isRes σ ≡ ∃ f. wtFsym f ∧ resOf f = σ"

(* Types meant to be left unprotected:
-- in the case of tags, terms of these type are not tagged;
-- in the case of guards, no guards are added for these types  *)
definition "unprot σ ≡ ¬ prot σ ∧ ¬ protFw σ"

lemma unprot_mcalc[simp]: "⟦unprot σ; c ∈ Φ⟧ ⟹ σ ⊢ c "
using tp_mcalc unfolding unprot_def by auto

end (* context ProblemIkTpart *)


(* Problem with type partition and model: *)
locale ModelIkTpart =
Ik? : ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw +
Ik? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP
for wtFsym :: "'fsym ⇒ bool"
and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp and prot and protFw
and intT and intF and intP

end