(* File: TLA/Init.thy ID: $Id: Init.thy,v 1.4 2005/09/07 18:22:39 wenzelm Exp $ Author: Stephan Merz Copyright: 1998 University of Munich Theory Name: Init Logic Image: HOL 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 .. types temporal = "behavior form" consts Initial :: "('w::world => bool) => temporal" first_world :: "behavior => ('w::world)" st1 :: "behavior => state" st2 :: "behavior => state" syntax TEMP :: "lift => 'a" ("(TEMP _)") "_Init" :: "lift => lift" ("(Init _)"[40] 50) translations "TEMP F" => "(F::behavior => _)" "_Init" == "Initial" "sigma |= Init F" <= "_Init F sigma" defs Init_def: "sigma |= Init F == (first_world sigma) |= F" fw_temp_def: "first_world == %sigma. sigma" fw_stp_def: "first_world == st1" fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)" ML {* use_legacy_bindings (the_context ()) *} end
theorem Init_stp_act:
|- Init $P = (Init P)
theorem Init_stp_act_rev:
Init P == Init $P
theorem Init_temp:
|- Init F = F
theorem Init_stp:
(sigma |= Init P) = P (st1 sigma)
theorem Init_act:
(sigma |= Init A) = A (st1 sigma, st2 sigma)