src/HOL/TLA/Init.thy
author wenzelm
Wed Sep 07 20:22:39 2005 +0200 (2005-09-07)
changeset 17309 c43ed29bd197
parent 12338 de0f4a63baa5
child 21624 6f79647cf536
permissions -rw-r--r--
converted to Isar theory format;
     1 (*
     2     File:        TLA/Init.thy
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1998 University of Munich
     6 
     7     Theory Name: Init
     8     Logic Image: HOL
     9 
    10 Introduces type of temporal formulas. Defines interface between
    11 temporal formulas and its "subformulas" (state predicates and actions).
    12 *)
    13 
    14 theory Init
    15 imports Action
    16 begin
    17 
    18 typedecl behavior
    19 instance behavior :: world ..
    20 
    21 types
    22   temporal = "behavior form"
    23 
    24 
    25 consts
    26   Initial     :: "('w::world => bool) => temporal"
    27   first_world :: "behavior => ('w::world)"
    28   st1         :: "behavior => state"
    29   st2         :: "behavior => state"
    30 
    31 syntax
    32   TEMP       :: "lift => 'a"                          ("(TEMP _)")
    33   "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
    34 
    35 translations
    36   "TEMP F"   => "(F::behavior => _)"
    37   "_Init"    == "Initial"
    38   "sigma |= Init F"  <= "_Init F sigma"
    39 
    40 defs
    41   Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
    42   fw_temp_def: "first_world == %sigma. sigma"
    43   fw_stp_def:  "first_world == st1"
    44   fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
    45 
    46 ML {* use_legacy_bindings (the_context ()) *}
    47 
    48 end