--- a/src/HOL/TLA/Action.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Action.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/Action.thy
+(*
+ File: TLA/Action.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -9,43 +10,46 @@
Define the action level of TLA as an Isabelle theory.
*)
-Action = Intensional + Stfun +
+theory Action
+imports Stfun
+begin
+
(** abstract syntax **)
types
'a trfun = "(state * state) => 'a"
- action = bool trfun
+ action = "bool trfun"
instance
- "*" :: (world, world) world
+ "*" :: (world, world) world ..
consts
(** abstract syntax **)
- before :: 'a stfun => 'a trfun
- after :: 'a stfun => 'a trfun
- unch :: 'a stfun => action
+ before :: "'a stfun => 'a trfun"
+ after :: "'a stfun => 'a trfun"
+ unch :: "'a stfun => action"
- SqAct :: [action, 'a stfun] => action
- AnAct :: [action, 'a stfun] => action
- enabled :: action => stpred
+ SqAct :: "[action, 'a stfun] => action"
+ AnAct :: "[action, 'a stfun] => action"
+ enabled :: "action => stpred"
(** concrete syntax **)
syntax
(* Syntax for writing action expressions in arbitrary contexts *)
- "ACT" :: lift => 'a ("(ACT _)")
+ "ACT" :: "lift => 'a" ("(ACT _)")
- "_before" :: lift => lift ("($_)" [100] 99)
- "_after" :: lift => lift ("(_$)" [100] 99)
- "_unchanged" :: lift => lift ("(unchanged _)" [100] 99)
+ "_before" :: "lift => lift" ("($_)" [100] 99)
+ "_after" :: "lift => lift" ("(_$)" [100] 99)
+ "_unchanged" :: "lift => lift" ("(unchanged _)" [100] 99)
(*** Priming: same as "after" ***)
- "_prime" :: lift => lift ("(_`)" [100] 99)
+ "_prime" :: "lift => lift" ("(_`)" [100] 99)
- "_SqAct" :: [lift, lift] => lift ("([_]'_(_))" [0,1000] 99)
- "_AnAct" :: [lift, lift] => lift ("(<_>'_(_))" [0,1000] 99)
- "_Enabled" :: lift => lift ("(Enabled _)" [100] 100)
+ "_SqAct" :: "[lift, lift] => lift" ("([_]'_(_))" [0,1000] 99)
+ "_AnAct" :: "[lift, lift] => lift" ("(<_>'_(_))" [0,1000] 99)
+ "_Enabled" :: "lift => lift" ("(Enabled _)" [100] 100)
translations
"ACT A" => "(A::state*state => _)"
@@ -61,13 +65,16 @@
"s |= Enabled A" <= "_Enabled A s"
"w |= unchanged f" <= "_unchanged f w"
-rules
- unl_before "(ACT $v) (s,t) == v s"
- unl_after "(ACT v$) (s,t) == v t"
+axioms
+ unl_before: "(ACT $v) (s,t) == v s"
+ unl_after: "(ACT v$) (s,t) == v t"
- unchanged_def "(s,t) |= unchanged v == (v t = v s)"
- square_def "ACT [A]_v == ACT (A | unchanged v)"
- angle_def "ACT <A>_v == ACT (A & ~ unchanged v)"
+ unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
+ square_def: "ACT [A]_v == ACT (A | unchanged v)"
+ angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)"
- enabled_def "s |= Enabled A == EX u. (s,u) |= A"
+ enabled_def: "s |= Enabled A == EX u. (s,u) |= A"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end