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