Theory Init

theory Init
imports Action
```(*  Title:      HOL/TLA/Init.thy
Author:     Stephan Merz

Introduces type of temporal formulas.  Defines interface between
temporal formulas and its "subformulas" (state predicates and
actions).
*)

theory Init
imports Action
begin

typedecl behavior
instance behavior :: world ..

type_synonym temporal = "behavior form"

consts
first_world :: "behavior ⇒ ('w::world)"
st1         :: "behavior ⇒ state"
st2         :: "behavior ⇒ state"

definition Initial :: "('w::world ⇒ bool) ⇒ temporal"
where Init_def: "Initial F sigma = F (first_world sigma)"

syntax
"_TEMP"    :: "lift ⇒ 'a"                          ("(TEMP _)")
"_Init"    :: "lift ⇒ lift"                        ("(Init _)"[40] 50)
translations
"TEMP F"   => "(F::behavior ⇒ _)"
"_Init"    == "CONST Initial"
"sigma ⊨ Init F"  <= "_Init F sigma"

fw_temp ≡ "first_world :: behavior ⇒ behavior"
fw_stp ≡ "first_world :: behavior ⇒ state"
fw_act ≡ "first_world :: behavior ⇒ state × state"
begin

definition "first_world == λsigma. sigma"
definition "first_world == st1"
definition "first_world == λsigma. (st1 sigma, st2 sigma)"

end

lemma const_simps [int_rewrite, simp]:
"⊢ (Init #True) = #True"
"⊢ (Init #False) = #False"
by (auto simp: Init_def)

lemma Init_simps1 [int_rewrite]:
"⋀F. ⊢ (Init ¬F) = (¬ Init F)"
"⊢ (Init (P ⟶ Q)) = (Init P ⟶ Init Q)"
"⊢ (Init (P ∧ Q)) = (Init P ∧ Init Q)"
"⊢ (Init (P ∨ Q)) = (Init P ∨ Init Q)"
"⊢ (Init (P = Q)) = ((Init P) = (Init Q))"
"⊢ (Init (∀x. F x)) = (∀x. (Init F x))"
"⊢ (Init (∃x. F x)) = (∃x. (Init F x))"
"⊢ (Init (∃!x. F x)) = (∃!x. (Init F x))"
by (auto simp: Init_def)

lemma Init_stp_act: "⊢ (Init \$P) = (Init P)"
by (auto simp add: Init_def fw_act_def fw_stp_def)

lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]

lemma Init_temp: "⊢ (Init F) = F"
by (auto simp add: Init_def fw_temp_def)

lemmas Init_simps = Init_temp [int_rewrite] Init_simps2

(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
lemma Init_stp: "(sigma ⊨ Init P) = P (st1 sigma)"