src/HOL/TLA/Init.thy
author haftmann
Tue Feb 23 10:11:16 2010 +0100 (2010-02-23)
changeset 35318 e1b61c5fd494
parent 35108 e384e27c229f
child 42018 878f33040280
permissions -rw-r--r--
dropped axclass, going back to purely syntactic type classes
     1 (*  Title:      HOL/TLA/Init.thy
     2     Author:     Stephan Merz
     3     Copyright:  1998 University of Munich
     4 
     5 Introduces type of temporal formulas.  Defines interface between
     6 temporal formulas and its "subformulas" (state predicates and
     7 actions).
     8 *)
     9 
    10 theory Init
    11 imports Action
    12 begin
    13 
    14 typedecl behavior
    15 arities behavior :: world
    16 
    17 types
    18   temporal = "behavior form"
    19 
    20 
    21 consts
    22   Initial     :: "('w::world => bool) => temporal"
    23   first_world :: "behavior => ('w::world)"
    24   st1         :: "behavior => state"
    25   st2         :: "behavior => state"
    26 
    27 syntax
    28   "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
    29   "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
    30 
    31 translations
    32   "TEMP F"   => "(F::behavior => _)"
    33   "_Init"    == "CONST Initial"
    34   "sigma |= Init F"  <= "_Init F sigma"
    35 
    36 defs
    37   Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
    38   fw_temp_def: "first_world == %sigma. sigma"
    39   fw_stp_def:  "first_world == st1"
    40   fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
    41 
    42 lemma const_simps [int_rewrite, simp]:
    43   "|- (Init #True) = #True"
    44   "|- (Init #False) = #False"
    45   by (auto simp: Init_def)
    46 
    47 lemma Init_simps1 [int_rewrite]:
    48   "!!F. |- (Init ~F) = (~ Init F)"
    49   "|- (Init (P --> Q)) = (Init P --> Init Q)"
    50   "|- (Init (P & Q)) = (Init P & Init Q)"
    51   "|- (Init (P | Q)) = (Init P | Init Q)"
    52   "|- (Init (P = Q)) = ((Init P) = (Init Q))"
    53   "|- (Init (!x. F x)) = (!x. (Init F x))"
    54   "|- (Init (? x. F x)) = (? x. (Init F x))"
    55   "|- (Init (?! x. F x)) = (?! x. (Init F x))"
    56   by (auto simp: Init_def)
    57 
    58 lemma Init_stp_act: "|- (Init $P) = (Init P)"
    59   by (auto simp add: Init_def fw_act_def fw_stp_def)
    60 
    61 lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
    62 lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
    63 
    64 lemma Init_temp: "|- (Init F) = F"
    65   by (auto simp add: Init_def fw_temp_def)
    66 
    67 lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
    68 
    69 (* Trivial instances of the definitions that avoid introducing lambda expressions. *)
    70 lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
    71   by (simp add: Init_def fw_stp_def)
    72 
    73 lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
    74   by (simp add: Init_def fw_act_def)
    75 
    76 lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
    77 
    78 end