src/HOL/TLA/Init.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Init.thy	Mon Feb 08 13:02:56 1999 +0100
@@ -0,0 +1,46 @@
+(* 
+    File:	 TLA/Init.thy
+    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).
+*)
+
+Init  =  Action +
+
+types
+  behavior
+  temporal = behavior form
+
+arities
+  behavior    :: term
+
+instance
+  behavior    :: world
+
+consts
+  Initial     :: ('w::world => bool) => temporal
+  first_world :: behavior => ('w::world)
+  st1, 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)"
+end
+
+ML