src/HOL/TLA/Action.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Action.thy	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,60 @@
+(* 
+    File:	 TLA/Action.thy
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    Theory Name: Action
+    Logic Image: HOL
+
+Define the action level of TLA as an Isabelle theory.
+*)
+
+Action  =  Intensional + Stfun +
+
+types
+    state2      (* intention: pair of states *)
+    'a trfct = "('a, state2) term"
+    action   = "state2 form"
+
+arities
+    state2 :: world
+    
+consts
+  mkstate2      :: "[state,state] => state2"  ("([[_,_]])")
+
+  (* lift state variables to transition functions *)
+  before        :: "'a stfun => 'a trfct"            ("($_)"  [100] 99)
+  after         :: "'a stfun => 'a trfct"            ("(_$)"  [100] 99)
+  unchanged     :: "'a stfun => action"
+
+  (* Priming *)
+  prime         :: "'a trfct => 'a trfct"            ("(_`)" [90] 89)
+
+  SqAct         :: "[action, 'a stfun] => action"    ("([_]'_(_))" [0,60] 59)
+  AnAct         :: "[action, 'a stfun] => action"    ("(<_>'_(_))" [0,60] 59)
+  Enabled       :: "action => stpred"
+
+rules
+  (* The following says that state2 is generated by mkstate2 *)
+  state2_ext    "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A"
+
+  unl_before    "($v) [[s,t]] == v s"
+  unl_after     "(v$) [[s,t]] == v t"
+
+  pr_con        "(#c)` == #c"
+  pr_before     "($v)` == v$"
+  (* no corresponding rule for "after"! *)
+  pr_lift       "(F[x])` == F[x`]"
+  pr_lift2      "(F[x,y])` == F[x`,y`]"
+  pr_lift3      "(F[x,y,z])` == F[x`,y`,z`]"
+  pr_all        "(RALL x. P(x))` == (RALL x. P(x)`)"
+  pr_ex         "(REX x. P(x))` == (REX x. P(x)`)"
+
+  unchanged_def "(unchanged v) [[s,t]] == (v t = v s)"
+  square_def    "[A]_v == A .| unchanged v"
+  angle_def     "<A>_v == A .& .~ unchanged v"
+
+  enabled_def   "(Enabled A) s  ==  EX u. A[[s,u]]"
+end
+
+