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