(* Title: HOL/TLA/Init.thy
Author: Stephan Merz
Copyright: 1998 University of Munich
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"
overloading
fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> 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)"
by (simp add: Init_def fw_stp_def)
lemma Init_act: "(sigma \ Init A) = A (st1 sigma, st2 sigma)"
by (simp add: Init_def fw_act_def)
lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
