src/HOL/TLA/Init.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 42018 878f33040280
child 55382 9218fa411c15
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 type_synonym temporal = "behavior form"
    18 
    19 
    20 consts
    21   Initial     :: "('w::world => bool) => temporal"
    22   first_world :: "behavior => ('w::world)"
    23   st1         :: "behavior => state"
    24   st2         :: "behavior => state"
    25 
    26 syntax
    27   "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
    28   "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
    29 
    30 translations
    31   "TEMP F"   => "(F::behavior => _)"
    32   "_Init"    == "CONST Initial"
    33   "sigma |= Init F"  <= "_Init F sigma"
    34 
    35 defs
    36   Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
    37   fw_temp_def: "first_world == %sigma. sigma"
    38   fw_stp_def:  "first_world == st1"
    39   fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
    40 
    41 lemma const_simps [int_rewrite, simp]:
    42   "|- (Init #True) = #True"
    43   "|- (Init #False) = #False"
    44   by (auto simp: Init_def)
    45 
    46 lemma Init_simps1 [int_rewrite]:
    47   "!!F. |- (Init ~F) = (~ Init F)"
    48   "|- (Init (P --> Q)) = (Init P --> Init Q)"
    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 (!x. F x)) = (!x. (Init F x))"
    53   "|- (Init (? x. F x)) = (? x. (Init F x))"
    54   "|- (Init (?! x. F x)) = (?! x. (Init F x))"
    55   by (auto simp: Init_def)
    56 
    57 lemma Init_stp_act: "|- (Init $P) = (Init P)"
    58   by (auto simp add: Init_def fw_act_def fw_stp_def)
    59 
    60 lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
    61 lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
    62 
    63 lemma Init_temp: "|- (Init F) = F"
    64   by (auto simp add: Init_def fw_temp_def)
    65 
    66 lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
    67 
    68 (* Trivial instances of the definitions that avoid introducing lambda expressions. *)
    69 lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
    70   by (simp add: Init_def fw_stp_def)
    71 
    72 lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
    73   by (simp add: Init_def fw_act_def)
    74 
    75 lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
    76 
    77 end