src/HOL/TLA/Init.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 12338 de0f4a63baa5
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
     1 (* 
     2     File:	 TLA/Init.thy
     3     Author:      Stephan Merz
     4     Copyright:   1998 University of Munich
     5 
     6     Theory Name: Init
     7     Logic Image: HOL
     8 
     9 Introduces type of temporal formulas. Defines interface between
    10 temporal formulas and its "subformulas" (state predicates and actions).
    11 *)
    12 
    13 Init  =  Action +
    14 
    15 types
    16   behavior
    17   temporal = behavior form
    18 
    19 arities
    20   behavior    :: type
    21 
    22 instance
    23   behavior    :: world
    24 
    25 consts
    26   Initial     :: ('w::world => bool) => temporal
    27   first_world :: behavior => ('w::world)
    28   st1, st2    :: behavior => state
    29 
    30 syntax
    31   TEMP       :: lift => 'a                          ("(TEMP _)")
    32   "_Init"    :: lift => lift                        ("(Init _)"[40] 50)
    33 
    34 translations
    35   "TEMP F"   => "(F::behavior => _)"
    36   "_Init"    == "Initial"
    37   "sigma |= Init F"  <= "_Init F sigma"
    38 
    39 defs
    40   Init_def    "sigma |= Init F  ==  (first_world sigma) |= F"
    41   fw_temp_def "first_world == %sigma. sigma"
    42   fw_stp_def  "first_world == st1"
    43   fw_act_def  "first_world == %sigma. (st1 sigma, st2 sigma)"
    44 end