src/HOL/TLA/Action.thy
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 6255 db63752140c7
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
     1 (* 
     2     File:	 TLA/Action.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: Action
     7     Logic Image: HOL
     8 
     9 Define the action level of TLA as an Isabelle theory.
    10 *)
    11 
    12 Action  =  Intensional + Stfun +
    13 
    14 types
    15     state2      (* intention: pair of states *)
    16     'a trfct = "('a, state2) term"
    17     action   = "state2 form"
    18 
    19 arities
    20     state2 :: world
    21     
    22 consts
    23   mkstate2      :: "[state,state] => state2"  ("([[_,_]])")
    24 
    25   (* lift state variables to transition functions *)
    26   before        :: "'a stfun => 'a trfct"            ("($_)"  [100] 99)
    27   after         :: "'a stfun => 'a trfct"            ("(_$)"  [100] 99)
    28   unchanged     :: "'a stfun => action"
    29 
    30   (* Priming *)
    31   prime         :: "'a trfct => 'a trfct"            ("(_`)" [90] 89)
    32 
    33   SqAct         :: "[action, 'a stfun] => action"    ("([_]'_(_))" [0,60] 59)
    34   AnAct         :: "[action, 'a stfun] => action"    ("(<_>'_(_))" [0,60] 59)
    35   Enabled       :: "action => stpred"
    36 
    37 rules
    38   (* The following says that state2 is generated by mkstate2 *)
    39   state2_ext    "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A"
    40 
    41   unl_before    "($v) [[s,t]] == v s"
    42   unl_after     "(v$) [[s,t]] == v t"
    43 
    44   pr_con        "(#c)` == #c"
    45   pr_before     "($v)` == v$"
    46   (* no corresponding rule for "after"! *)
    47   pr_lift       "(F[x])` == F[x`]"
    48   pr_lift2      "(F[x,y])` == F[x`,y`]"
    49   pr_lift3      "(F[x,y,z])` == F[x`,y`,z`]"
    50   pr_all        "(RALL x. P(x))` == (RALL x. P(x)`)"
    51   pr_ex         "(REX x. P(x))` == (REX x. P(x)`)"
    52 
    53   unchanged_def "(unchanged v) [[s,t]] == (v t = v s)"
    54   square_def    "[A]_v == A .| unchanged v"
    55   angle_def     "<A>_v == A .& .~ unchanged v"
    56 
    57   enabled_def   "(Enabled A) s  ==  EX u. A[[s,u]]"
    58 end
    59 
    60