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