src/HOL/TLA/Init.thy
changeset 6255 db63752140c7
child 11703 6e5de8d4290a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TLA/Init.thy	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -0,0 +1,46 @@
     1.4 +(* 
     1.5 +    File:	 TLA/Init.thy
     1.6 +    Author:      Stephan Merz
     1.7 +    Copyright:   1998 University of Munich
     1.8 +
     1.9 +    Theory Name: Init
    1.10 +    Logic Image: HOL
    1.11 +
    1.12 +Introduces type of temporal formulas. Defines interface between
    1.13 +temporal formulas and its "subformulas" (state predicates and actions).
    1.14 +*)
    1.15 +
    1.16 +Init  =  Action +
    1.17 +
    1.18 +types
    1.19 +  behavior
    1.20 +  temporal = behavior form
    1.21 +
    1.22 +arities
    1.23 +  behavior    :: term
    1.24 +
    1.25 +instance
    1.26 +  behavior    :: world
    1.27 +
    1.28 +consts
    1.29 +  Initial     :: ('w::world => bool) => temporal
    1.30 +  first_world :: behavior => ('w::world)
    1.31 +  st1, st2    :: behavior => state
    1.32 +
    1.33 +syntax
    1.34 +  TEMP       :: lift => 'a                          ("(TEMP _)")
    1.35 +  "_Init"    :: lift => lift                        ("(Init _)"[40] 50)
    1.36 +
    1.37 +translations
    1.38 +  "TEMP F"   => "(F::behavior => _)"
    1.39 +  "_Init"    == "Initial"
    1.40 +  "sigma |= Init F"  <= "_Init F sigma"
    1.41 +
    1.42 +defs
    1.43 +  Init_def    "sigma |= Init F  ==  (first_world sigma) |= F"
    1.44 +  fw_temp_def "first_world == %sigma. sigma"
    1.45 +  fw_stp_def  "first_world == st1"
    1.46 +  fw_act_def  "first_world == %sigma. (st1 sigma, st2 sigma)"
    1.47 +end
    1.48 +
    1.49 +ML