src/HOL/TLA/Init.thy
author wenzelm
Mon Feb 08 13:02:56 1999 +0100 (1999-02-08)
changeset 6255 db63752140c7
child 11703 6e5de8d4290a
permissions -rw-r--r--
updated (Stephan Merz);
     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    :: term
    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
    45 
    46 ML