converted to Isar theory format;
authorwenzelm
Wed Sep 07 20:22:39 2005 +0200 (2005-09-07)
changeset 17309c43ed29bd197
parent 17308 5d9bbc0d9bd3
child 17310 1322ed8e0ee4
converted to Isar theory format;
src/HOL/TLA/Action.ML
src/HOL/TLA/Action.thy
src/HOL/TLA/Buffer/Buffer.ML
src/HOL/TLA/Buffer/Buffer.thy
src/HOL/TLA/Buffer/DBuffer.ML
src/HOL/TLA/Buffer/DBuffer.thy
src/HOL/TLA/Buffer/ROOT.ML
src/HOL/TLA/Inc/Inc.ML
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Inc/Pcount.thy
src/HOL/TLA/Inc/ROOT.ML
src/HOL/TLA/Init.ML
src/HOL/TLA/Init.thy
src/HOL/TLA/Intensional.ML
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/MIParameters.thy
src/HOL/TLA/Memory/MIsafe.ML
src/HOL/TLA/Memory/MemClerk.ML
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/MemClerkParameters.ML
src/HOL/TLA/Memory/MemClerkParameters.thy
src/HOL/TLA/Memory/Memory.ML
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.ML
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/MemoryParameters.ML
src/HOL/TLA/Memory/MemoryParameters.thy
src/HOL/TLA/Memory/ProcedureInterface.ML
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/ROOT.ML
src/HOL/TLA/Memory/RPC.ML
src/HOL/TLA/Memory/RPC.thy
src/HOL/TLA/Memory/RPCMemoryParams.thy
src/HOL/TLA/Memory/RPCParameters.ML
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/TLA/ROOT.ML
src/HOL/TLA/Stfun.ML
src/HOL/TLA/Stfun.thy
src/HOL/TLA/TLA.ML
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/Action.ML	Wed Sep 07 20:22:15 2005 +0200
     1.2 +++ b/src/HOL/TLA/Action.ML	Wed Sep 07 20:22:39 2005 +0200
     1.3 @@ -1,15 +1,16 @@
     1.4 -(* 
     1.5 -    File:	 Action.ML
     1.6 +(*
     1.7 +    File:        Action.ML
     1.8 +    ID:          $Id$
     1.9      Author:      Stephan Merz
    1.10      Copyright:   1997 University of Munich
    1.11  
    1.12  Lemmas and tactics for TLA actions.
    1.13  *)
    1.14  
    1.15 -(* The following assertion specializes "intI" for any world type 
    1.16 +(* The following assertion specializes "intI" for any world type
    1.17     which is a pair, not just for "state * state".
    1.18  *)
    1.19 -val [prem] = goal thy "(!!s t. (s,t) |= A) ==> |- A";
    1.20 +val [prem] = goal (the_context ()) "(!!s t. (s,t) |= A) ==> |- A";
    1.21  by (REPEAT (resolve_tac [prem,intI,prod_induct] 1));
    1.22  qed "actionI";
    1.23  
    1.24 @@ -18,8 +19,8 @@
    1.25  qed "actionD";
    1.26  
    1.27  local
    1.28 -  fun prover s = prove_goal Action.thy s 
    1.29 -                    (fn _ => [rtac actionI 1, 
    1.30 +  fun prover s = prove_goal (the_context ()) s
    1.31 +                    (fn _ => [rtac actionI 1,
    1.32                                rewrite_goals_tac (unl_after::intensional_rews),
    1.33                                rtac refl 1])
    1.34  in
    1.35 @@ -44,8 +45,8 @@
    1.36     functions defined in Intensional.ML in that they introduce a
    1.37     "world" parameter of the form (s,t) and apply additional rewrites.
    1.38  *)
    1.39 -fun action_unlift th = 
    1.40 -    (rewrite_rule action_rews (th RS actionD)) 
    1.41 +fun action_unlift th =
    1.42 +    (rewrite_rule action_rews (th RS actionD))
    1.43      handle _ => int_unlift th;
    1.44  
    1.45  (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
    1.46 @@ -72,7 +73,7 @@
    1.47  by (Asm_simp_tac 1);
    1.48  qed "busy_squareI";
    1.49  
    1.50 -val prems = goal thy
    1.51 +val prems = goal (the_context ())
    1.52    "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)";
    1.53  by (cut_facts_tac prems 1);
    1.54  by (rewrite_goals_tac (square_def::action_rews));
    1.55 @@ -80,18 +81,18 @@
    1.56  by (REPEAT (eresolve_tac prems 1));
    1.57  qed "squareE";
    1.58  
    1.59 -val prems = goalw thy (square_def::action_rews)
    1.60 +val prems = goalw (the_context ()) (square_def::action_rews)
    1.61    "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v";
    1.62  by (rtac disjCI 1);
    1.63  by (eresolve_tac prems 1);
    1.64  qed "squareCI";
    1.65  
    1.66 -goalw thy [angle_def]
    1.67 +goalw (the_context ()) [angle_def]
    1.68    "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v";
    1.69  by (Asm_simp_tac 1);
    1.70  qed "angleI";
    1.71  
    1.72 -val prems = goalw thy (angle_def::action_rews)
    1.73 +val prems = goalw (the_context ()) (angle_def::action_rews)
    1.74    "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R";
    1.75  by (cut_facts_tac prems 1);
    1.76  by (etac conjE 1);
    1.77 @@ -101,7 +102,7 @@
    1.78  AddIs [angleI, squareCI];
    1.79  AddEs [angleE, squareE];
    1.80  
    1.81 -goal thy
    1.82 +goal (the_context ())
    1.83     "!!f. [| |- unchanged f & ~B --> unchanged g;   \
    1.84  \           |- A & ~unchanged g --> B              \
    1.85  \        |] ==> |- [A]_f --> [B]_g";
    1.86 @@ -110,23 +111,23 @@
    1.87  by (auto_tac (claset(), simpset() addsimps [square_def]));
    1.88  qed "square_simulation";
    1.89  
    1.90 -goalw thy [square_def,angle_def]
    1.91 +goalw (the_context ()) [square_def,angle_def]
    1.92     "|- (~ [A]_v) = <~A>_v";
    1.93  by Auto_tac;
    1.94  qed "not_square";
    1.95  
    1.96 -goalw thy [square_def,angle_def]
    1.97 +goalw (the_context ()) [square_def,angle_def]
    1.98     "|- (~ <A>_v) = [~A]_v";
    1.99  by Auto_tac;
   1.100  qed "not_angle";
   1.101  
   1.102  (* ============================== Facts about ENABLED ============================== *)
   1.103  
   1.104 -goal thy "|- A --> $Enabled A";
   1.105 +goal (the_context ()) "|- A --> $Enabled A";
   1.106  by (auto_tac (claset(), simpset() addsimps [enabled_def]));
   1.107  qed "enabledI";
   1.108  
   1.109 -val prems = goalw thy [enabled_def]
   1.110 +val prems = goalw (the_context ()) [enabled_def]
   1.111    "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q";
   1.112  by (cut_facts_tac prems 1);
   1.113  by (etac exE 1);
   1.114 @@ -134,12 +135,12 @@
   1.115  by (atac 1);
   1.116  qed "enabledE";
   1.117  
   1.118 -goal thy "|- ~$Enabled G --> ~ G";
   1.119 +goal (the_context ()) "|- ~$Enabled G --> ~ G";
   1.120  by (auto_tac (claset(), simpset() addsimps [enabled_def]));
   1.121  qed "notEnabledD";
   1.122  
   1.123  (* Monotonicity *)
   1.124 -val [min,maj] = goal thy
   1.125 +val [min,maj] = goal (the_context ())
   1.126    "[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G";
   1.127  by (rtac (min RS enabledE) 1);
   1.128  by (rtac (action_use enabledI) 1);
   1.129 @@ -147,30 +148,30 @@
   1.130  qed "enabled_mono";
   1.131  
   1.132  (* stronger variant *)
   1.133 -val [min,maj] = goal thy
   1.134 +val [min,maj] = goal (the_context ())
   1.135    "[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G";
   1.136  by (rtac (min RS enabledE) 1);
   1.137  by (rtac (action_use enabledI) 1);
   1.138  by (etac maj 1);
   1.139  qed "enabled_mono2";
   1.140  
   1.141 -goal thy "|- Enabled F --> Enabled (F | G)";
   1.142 +goal (the_context ()) "|- Enabled F --> Enabled (F | G)";
   1.143  by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   1.144  qed "enabled_disj1";
   1.145  
   1.146 -goal thy "|- Enabled G --> Enabled (F | G)";
   1.147 +goal (the_context ()) "|- Enabled G --> Enabled (F | G)";
   1.148  by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   1.149  qed "enabled_disj2";
   1.150  
   1.151 -goal thy "|- Enabled (F & G) --> Enabled F";
   1.152 +goal (the_context ()) "|- Enabled (F & G) --> Enabled F";
   1.153  by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   1.154  qed "enabled_conj1";
   1.155  
   1.156 -goal thy "|- Enabled (F & G) --> Enabled G";
   1.157 +goal (the_context ()) "|- Enabled (F & G) --> Enabled G";
   1.158  by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   1.159  qed "enabled_conj2";
   1.160  
   1.161 -val prems = goal thy
   1.162 +val prems = goal (the_context ())
   1.163    "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q";
   1.164  by (cut_facts_tac prems 1);
   1.165  by (resolve_tac prems 1);
   1.166 @@ -178,24 +179,24 @@
   1.167  by (etac (action_use enabled_conj2) 1);
   1.168  qed "enabled_conjE";
   1.169  
   1.170 -goal thy "|- Enabled (F | G) --> Enabled F | Enabled G";
   1.171 +goal (the_context ()) "|- Enabled (F | G) --> Enabled F | Enabled G";
   1.172  by (auto_tac (claset(), simpset() addsimps [enabled_def]));
   1.173  qed "enabled_disjD";
   1.174  
   1.175 -goal thy "|- Enabled (F | G) = (Enabled F | Enabled G)";
   1.176 +goal (the_context ()) "|- Enabled (F | G) = (Enabled F | Enabled G)";
   1.177  by (Clarsimp_tac 1);
   1.178  by (rtac iffI 1);
   1.179  by (etac (action_use enabled_disjD) 1);
   1.180  by (REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1));
   1.181  qed "enabled_disj";
   1.182  
   1.183 -goal thy "|- Enabled (EX x. F x) = (EX x. Enabled (F x))";
   1.184 +goal (the_context ()) "|- Enabled (EX x. F x) = (EX x. Enabled (F x))";
   1.185  by (force_tac (claset(), simpset() addsimps [enabled_def]) 1);
   1.186  qed "enabled_ex";
   1.187  
   1.188  
   1.189  (* A rule that combines enabledI and baseE, but generates fewer instantiations *)
   1.190 -val prems = goal thy
   1.191 +val prems = goal (the_context ())
   1.192    "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A";
   1.193  by (cut_facts_tac prems 1);
   1.194  by (etac exE 1);
   1.195 @@ -213,10 +214,10 @@
   1.196     Note that it applies whatever simplifications are currently active.
   1.197  *)
   1.198  fun action_simp_tac ss intros elims =
   1.199 -    asm_full_simp_tac 
   1.200 +    asm_full_simp_tac
   1.201           (ss setloop ((resolve_tac ((map action_use intros)
   1.202                                      @ [refl,impI,conjI,actionI,intI,allI]))
   1.203 -		      ORELSE' (eresolve_tac ((map action_use elims) 
   1.204 +                      ORELSE' (eresolve_tac ((map action_use elims)
   1.205                                               @ [conjE,disjE,exE]))));
   1.206  
   1.207  (* default version without additional plug-in rules *)
   1.208 @@ -240,7 +241,7 @@
   1.209  
   1.210  (* Example:
   1.211  
   1.212 -val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
   1.213 +val [prem] = goal (the_context ()) "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
   1.214  by (enabled_tac prem 1);
   1.215  by Auto_tac;
   1.216  
     2.1 --- a/src/HOL/TLA/Action.thy	Wed Sep 07 20:22:15 2005 +0200
     2.2 +++ b/src/HOL/TLA/Action.thy	Wed Sep 07 20:22:39 2005 +0200
     2.3 @@ -1,5 +1,6 @@
     2.4 -(* 
     2.5 -    File:	 TLA/Action.thy
     2.6 +(*
     2.7 +    File:        TLA/Action.thy
     2.8 +    ID:          $Id$
     2.9      Author:      Stephan Merz
    2.10      Copyright:   1998 University of Munich
    2.11  
    2.12 @@ -9,43 +10,46 @@
    2.13  Define the action level of TLA as an Isabelle theory.
    2.14  *)
    2.15  
    2.16 -Action  =  Intensional + Stfun +
    2.17 +theory Action
    2.18 +imports Stfun
    2.19 +begin
    2.20 +
    2.21  
    2.22  (** abstract syntax **)
    2.23  
    2.24  types
    2.25    'a trfun = "(state * state) => 'a"
    2.26 -  action   = bool trfun
    2.27 +  action   = "bool trfun"
    2.28  
    2.29  instance
    2.30 -  "*" :: (world, world) world
    2.31 +  "*" :: (world, world) world ..
    2.32  
    2.33  consts
    2.34    (** abstract syntax **)
    2.35 -  before        :: 'a stfun => 'a trfun
    2.36 -  after         :: 'a stfun => 'a trfun
    2.37 -  unch          :: 'a stfun => action
    2.38 +  before        :: "'a stfun => 'a trfun"
    2.39 +  after         :: "'a stfun => 'a trfun"
    2.40 +  unch          :: "'a stfun => action"
    2.41  
    2.42 -  SqAct         :: [action, 'a stfun] => action
    2.43 -  AnAct         :: [action, 'a stfun] => action
    2.44 -  enabled       :: action => stpred
    2.45 +  SqAct         :: "[action, 'a stfun] => action"
    2.46 +  AnAct         :: "[action, 'a stfun] => action"
    2.47 +  enabled       :: "action => stpred"
    2.48  
    2.49  (** concrete syntax **)
    2.50  
    2.51  syntax
    2.52    (* Syntax for writing action expressions in arbitrary contexts *)
    2.53 -  "ACT"         :: lift => 'a                      ("(ACT _)")
    2.54 +  "ACT"         :: "lift => 'a"                      ("(ACT _)")
    2.55  
    2.56 -  "_before"     :: lift => lift                    ("($_)"  [100] 99)
    2.57 -  "_after"      :: lift => lift                    ("(_$)"  [100] 99)
    2.58 -  "_unchanged"  :: lift => lift                    ("(unchanged _)" [100] 99)
    2.59 +  "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
    2.60 +  "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
    2.61 +  "_unchanged"  :: "lift => lift"                    ("(unchanged _)" [100] 99)
    2.62  
    2.63    (*** Priming: same as "after" ***)
    2.64 -  "_prime"      :: lift => lift                    ("(_`)" [100] 99)
    2.65 +  "_prime"      :: "lift => lift"                    ("(_`)" [100] 99)
    2.66  
    2.67 -  "_SqAct"      :: [lift, lift] => lift            ("([_]'_(_))" [0,1000] 99)
    2.68 -  "_AnAct"      :: [lift, lift] => lift            ("(<_>'_(_))" [0,1000] 99)
    2.69 -  "_Enabled"    :: lift => lift                    ("(Enabled _)" [100] 100)
    2.70 +  "_SqAct"      :: "[lift, lift] => lift"            ("([_]'_(_))" [0,1000] 99)
    2.71 +  "_AnAct"      :: "[lift, lift] => lift"            ("(<_>'_(_))" [0,1000] 99)
    2.72 +  "_Enabled"    :: "lift => lift"                    ("(Enabled _)" [100] 100)
    2.73  
    2.74  translations
    2.75    "ACT A"            =>   "(A::state*state => _)"
    2.76 @@ -61,13 +65,16 @@
    2.77    "s |= Enabled A"   <=   "_Enabled A s"
    2.78    "w |= unchanged f" <=   "_unchanged f w"
    2.79  
    2.80 -rules
    2.81 -  unl_before    "(ACT $v) (s,t) == v s"
    2.82 -  unl_after     "(ACT v$) (s,t) == v t"
    2.83 +axioms
    2.84 +  unl_before:    "(ACT $v) (s,t) == v s"
    2.85 +  unl_after:     "(ACT v$) (s,t) == v t"
    2.86  
    2.87 -  unchanged_def "(s,t) |= unchanged v == (v t = v s)"
    2.88 -  square_def    "ACT [A]_v == ACT (A | unchanged v)"
    2.89 -  angle_def     "ACT <A>_v == ACT (A & ~ unchanged v)"
    2.90 +  unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
    2.91 +  square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    2.92 +  angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    2.93  
    2.94 -  enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
    2.95 +  enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
    2.96 +
    2.97 +ML {* use_legacy_bindings (the_context ()) *}
    2.98 +
    2.99  end
     3.1 --- a/src/HOL/TLA/Buffer/Buffer.ML	Wed Sep 07 20:22:15 2005 +0200
     3.2 +++ b/src/HOL/TLA/Buffer/Buffer.ML	Wed Sep 07 20:22:39 2005 +0200
     3.3 @@ -1,5 +1,6 @@
     3.4 -(* 
     3.5 +(*
     3.6      File:        Buffer.ML
     3.7 +    ID:          $Id$
     3.8      Author:      Stephan Merz
     3.9      Copyright:   1997 University of Munich
    3.10  
    3.11 @@ -8,11 +9,10 @@
    3.12  
    3.13  (* ---------------------------- Data lemmas ---------------------------- *)
    3.14  
    3.15 -(*FIXME: move to List.thy? Maybe as (tl xs = xs) = (xs = [])"?*)
    3.16 +(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
    3.17  Goal "xs ~= [] --> tl xs ~= xs";
    3.18  by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
    3.19  qed_spec_mp "tl_not_self";
    3.20 -context Buffer.thy;
    3.21  
    3.22  Addsimps [tl_not_self];
    3.23  
    3.24 @@ -26,12 +26,12 @@
    3.25  (* Enabling condition for dequeue -- NOT NEEDED *)
    3.26  Goalw [temp_rewrite Deq_visible]
    3.27     "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])";
    3.28 -by (force_tac (claset() addSEs [base_enabled,enabledE], 
    3.29 +by (force_tac (claset() addSEs [base_enabled,enabledE],
    3.30                 simpset() addsimps [Deq_def]) 1);
    3.31  qed "Deq_enabled";
    3.32  
    3.33  (* For the left-to-right implication, we don't need the base variable stuff *)
    3.34 -Goalw [temp_rewrite Deq_visible] 
    3.35 +Goalw [temp_rewrite Deq_visible]
    3.36     "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])";
    3.37  by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def]));
    3.38  qed "Deq_enabledE";
     4.1 --- a/src/HOL/TLA/Buffer/Buffer.thy	Wed Sep 07 20:22:15 2005 +0200
     4.2 +++ b/src/HOL/TLA/Buffer/Buffer.thy	Wed Sep 07 20:22:39 2005 +0200
     4.3 @@ -1,15 +1,18 @@
     4.4  (*
     4.5      File:        Buffer.thy
     4.6 +    ID:          $Id$
     4.7      Author:      Stephan Merz
     4.8      Copyright:   1997 University of Munich
     4.9  
    4.10     Theory Name: Buffer
    4.11     Logic Image: TLA
    4.12 -
    4.13 -   A simple FIFO buffer (synchronous communication, interleaving)
    4.14  *)
    4.15  
    4.16 -Buffer = TLA +
    4.17 +header {* A simple FIFO buffer (synchronous communication, interleaving) *}
    4.18 +
    4.19 +theory Buffer
    4.20 +imports TLA
    4.21 +begin
    4.22  
    4.23  consts
    4.24    (* actions *)
    4.25 @@ -22,21 +25,21 @@
    4.26    IBuffer   :: "'a stfun => 'a list stfun => 'a stfun => temporal"
    4.27    Buffer    :: "'a stfun => 'a stfun => temporal"
    4.28  
    4.29 -rules
    4.30 -  BInit_def   "BInit ic q oc    == PRED q = #[]"
    4.31 -  Enq_def     "Enq ic q oc      == ACT (ic$ ~= $ic) 
    4.32 -                                     & (q$ = $q @ [ ic$ ]) 
    4.33 +defs
    4.34 +  BInit_def:   "BInit ic q oc    == PRED q = #[]"
    4.35 +  Enq_def:     "Enq ic q oc      == ACT (ic$ ~= $ic)
    4.36 +                                     & (q$ = $q @ [ ic$ ])
    4.37                                       & (oc$ = $oc)"
    4.38 -  Deq_def     "Deq ic q oc      == ACT ($q ~= #[])
    4.39 +  Deq_def:     "Deq ic q oc      == ACT ($q ~= #[])
    4.40                                       & (oc$ = hd< $q >)
    4.41                                       & (q$ = tl< $q >)
    4.42                                       & (ic$ = $ic)"
    4.43 -  Next_def    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
    4.44 -  IBuffer_def "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
    4.45 +  Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
    4.46 +  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
    4.47                                        & [][Next ic q oc]_(ic,q,oc)
    4.48                                        & WF(Deq ic q oc)_(ic,q,oc)"
    4.49 -  Buffer_def  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
    4.50 -end
    4.51 +  Buffer_def:  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
    4.52  
    4.53 +ML {* use_legacy_bindings (the_context ()) *}
    4.54  
    4.55 -
    4.56 +end
     5.1 --- a/src/HOL/TLA/Buffer/DBuffer.ML	Wed Sep 07 20:22:15 2005 +0200
     5.2 +++ b/src/HOL/TLA/Buffer/DBuffer.ML	Wed Sep 07 20:22:39 2005 +0200
     5.3 @@ -1,5 +1,6 @@
     5.4 -(* 
     5.5 +(*
     5.6      File:        DBuffer.ML
     5.7 +    ID:          $Id$
     5.8      Author:      Stephan Merz
     5.9      Copyright:   1997 University of Munich
    5.10  
    5.11 @@ -37,7 +38,7 @@
    5.12  
    5.13  Goalw [action_rewrite DBDeq_visible]
    5.14    "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])";
    5.15 -by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE] 
    5.16 +by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE]
    5.17                       addsimps2 [angle_def,DBDeq_def,Deq_def]) 1);
    5.18  qed "DBDeq_enabled";
    5.19  
    5.20 @@ -47,7 +48,7 @@
    5.21  
    5.22  Goalw [action_rewrite DBPass_visible]
    5.23     "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])";
    5.24 -by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE] 
    5.25 +by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE]
    5.26                       addsimps2 [angle_def,DBPass_def,Deq_def]) 1);
    5.27  qed "DBPass_enabled";
    5.28  
    5.29 @@ -103,7 +104,7 @@
    5.30  
    5.31  (* High-level fairness *)
    5.32  Goal "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) \
    5.33 -\                                       & WF(DBDeq)_(inp,mid,out,q1,q2)  \ 
    5.34 +\                                       & WF(DBDeq)_(inp,mid,out,q1,q2)  \
    5.35  \        --> WF(Deq inp qc out)_(inp,qc,out)";
    5.36  by (auto_tac (temp_css addSIs2 [leadsto_WF,
    5.37                                  (temp_use DBFair_1) RSN(2,(temp_use LatticeTransitivity)),
     6.1 --- a/src/HOL/TLA/Buffer/DBuffer.thy	Wed Sep 07 20:22:15 2005 +0200
     6.2 +++ b/src/HOL/TLA/Buffer/DBuffer.thy	Wed Sep 07 20:22:39 2005 +0200
     6.3 @@ -1,41 +1,53 @@
     6.4  (*
     6.5      File:        DBuffer.thy
     6.6 +    ID:          $Id$
     6.7      Author:      Stephan Merz
     6.8      Copyright:   1997 University of Munich
     6.9  
    6.10     Theory Name: DBuffer
    6.11     Logic Image: TLA
    6.12 -
    6.13 -   Two FIFO buffers in a row, with interleaving assumption.
    6.14  *)
    6.15  
    6.16 -DBuffer = Buffer +
    6.17 +header {* Two FIFO buffers in a row, with interleaving assumption *}
    6.18 +
    6.19 +theory DBuffer
    6.20 +imports Buffer
    6.21 +begin
    6.22  
    6.23  consts
    6.24    (* implementation variables *)
    6.25 -  inp, mid, out  :: nat stfun
    6.26 -  q1, q2, qc     :: nat list stfun
    6.27 +  inp  :: "nat stfun"
    6.28 +  mid  :: "nat stfun"
    6.29 +  out  :: "nat stfun"
    6.30 +  q1   :: "nat list stfun"
    6.31 +  q2   :: "nat list stfun"
    6.32 +  qc   :: "nat list stfun"
    6.33  
    6.34 -  DBInit                         :: stpred
    6.35 -  DBEnq, DBDeq, DBPass, DBNext   :: action
    6.36 -  DBuffer                        :: temporal
    6.37 +  DBInit :: stpred
    6.38 +  DBEnq :: action
    6.39 +  DBDeq :: action
    6.40 +  DBPass :: action
    6.41 +  DBNext :: action
    6.42 +  DBuffer :: temporal
    6.43  
    6.44 -rules
    6.45 -  DB_base        "basevars (inp,mid,out,q1,q2)"
    6.46 +axioms
    6.47 +  DB_base:        "basevars (inp,mid,out,q1,q2)"
    6.48  
    6.49    (* the concatenation of the two buffers *)
    6.50 -  qc_def         "PRED qc == PRED (q2 @ q1)"
    6.51 +  qc_def:         "PRED qc == PRED (q2 @ q1)"
    6.52  
    6.53 -  DBInit_def     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)"
    6.54 -  DBEnq_def      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)"
    6.55 -  DBDeq_def      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)"
    6.56 -  DBPass_def     "DBPass   == ACT  Deq inp q1 mid
    6.57 +  DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)"
    6.58 +  DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)"
    6.59 +  DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)"
    6.60 +  DBPass_def:     "DBPass   == ACT  Deq inp q1 mid
    6.61                                   & (q2$ = $q2 @ [ mid$ ])
    6.62                                   & (out$ = $out)"
    6.63 -  DBNext_def     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)"
    6.64 -  DBuffer_def    "DBuffer  == TEMP Init DBInit
    6.65 +  DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)"
    6.66 +  DBuffer_def:    "DBuffer  == TEMP Init DBInit
    6.67                                   & [][DBNext]_(inp,mid,out,q1,q2)
    6.68                                   & WF(DBDeq)_(inp,mid,out,q1,q2)
    6.69                                   & WF(DBPass)_(inp,mid,out,q1,q2)"
    6.70  
    6.71 +ML {* use_legacy_bindings (the_context ()) *}
    6.72 +
    6.73  end
    6.74 \ No newline at end of file
     7.1 --- a/src/HOL/TLA/Buffer/ROOT.ML	Wed Sep 07 20:22:15 2005 +0200
     7.2 +++ b/src/HOL/TLA/Buffer/ROOT.ML	Wed Sep 07 20:22:39 2005 +0200
     7.3 @@ -1,2 +1,4 @@
     7.4 +
     7.5 +(* $Id$ *)
     7.6  
     7.7  time_use_thy "DBuffer";
     8.1 --- a/src/HOL/TLA/Inc/Inc.ML	Wed Sep 07 20:22:15 2005 +0200
     8.2 +++ b/src/HOL/TLA/Inc/Inc.ML	Wed Sep 07 20:22:39 2005 +0200
     8.3 @@ -1,5 +1,6 @@
     8.4 -(* 
     8.5 -    File:	 TLA/ex/inc/Inc.ML
     8.6 +(*
     8.7 +    File:        TLA/ex/inc/Inc.ML
     8.8 +    ID:          $Id$
     8.9      Author:      Stephan Merz
    8.10      Copyright:   1997 University of Munich
    8.11  
    8.12 @@ -77,7 +78,7 @@
    8.13  (**** Proof of fairness ****)
    8.14  
    8.15  (*
    8.16 -   The goal is to prove Fair_M1 far below, which asserts 
    8.17 +   The goal is to prove Fair_M1 far below, which asserts
    8.18           |- Psi --> WF(M1)_(x,y)
    8.19     (the other fairness condition is symmetrical).
    8.20  
    8.21 @@ -111,7 +112,7 @@
    8.22  by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
    8.23  (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
    8.24  by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N1_enabled_at_g]
    8.25 -	              addSDs2 [STL2_gen]
    8.26 +                      addSDs2 [STL2_gen]
    8.27                        addsimps2 [Init_def]));
    8.28  qed "g1_leadsto_a1";
    8.29  
    8.30 @@ -130,7 +131,7 @@
    8.31  by (action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1);
    8.32  by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
    8.33  by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N2_enabled_at_g]
    8.34 -	              addSDs2 [STL2_gen]
    8.35 +                      addSDs2 [STL2_gen]
    8.36                        addsimps2 [Init_def]));
    8.37  qed "g2_leadsto_a2";
    8.38  
    8.39 @@ -165,7 +166,7 @@
    8.40  Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) \
    8.41  \        --> <>(pc2 = #a)";
    8.42  by (auto_tac (Inc_css addsimps2 Init_defs
    8.43 -                      addSIs2 [(temp_use N2_leadsto_a) 
    8.44 +                      addSIs2 [(temp_use N2_leadsto_a)
    8.45                                 RSN(2, (temp_use leadsto_init))]));
    8.46  by (case_tac "pc2 (st1 sigma)" 1);
    8.47  by Auto_tac;
    8.48 @@ -189,7 +190,7 @@
    8.49  by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
    8.50  by (clarsimp_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_use DmdImpl)]) 1);
    8.51  by (auto_tac (Inc_css addSIs2 [BoxDmd2_simple, N2_live]
    8.52 -	              addsimps2 split_box_conj::more_temp_simps));
    8.53 +                      addsimps2 split_box_conj::more_temp_simps));
    8.54  qed "a1_leadsto_b1";
    8.55  
    8.56  (* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
    8.57 @@ -201,14 +202,14 @@
    8.58  by (rtac (temp_use LatticeReflexivity) 1);
    8.59  by (rtac (temp_use LatticeTransitivity) 1);
    8.60  by (auto_tac (Inc_css addSIs2 [a1_leadsto_b1,g1_leadsto_a1]
    8.61 -	              addsimps2 [split_box_conj]));
    8.62 +                      addsimps2 [split_box_conj]));
    8.63  qed "N1_leadsto_b";
    8.64  
    8.65  Goal "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))             \
    8.66  \        & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
    8.67  \        --> <>(pc1 = #b)";
    8.68  by (auto_tac (Inc_css addsimps2 Init_defs
    8.69 -                      addSIs2 [(temp_use N1_leadsto_b) 
    8.70 +                      addSIs2 [(temp_use N1_leadsto_b)
    8.71                                 RSN(2, temp_use leadsto_init)]));
    8.72  by (case_tac "pc1 (st1 sigma)" 1);
    8.73  by Auto_tac;
    8.74 @@ -233,11 +234,11 @@
    8.75  by (force_tac (Inc_css addsimps2 angle_def::Psi_defs) 1);
    8.76  by (force_tac (Inc_css addSEs2 [N1_enabled_at_b]) 1);
    8.77     (* temporal premise: use previous lemmas and simple TL *)
    8.78 -by (force_tac (Inc_css addSIs2 [DmdStable, N1_live,Stuck_at_b] 
    8.79 +by (force_tac (Inc_css addSIs2 [DmdStable, N1_live,Stuck_at_b]
    8.80                         addEs2 [STL4E] addsimps2 [square_def]) 1);
    8.81  qed "Fair_M1_lemma";
    8.82  
    8.83  Goal "|- Psi --> WF(M1)_(x,y)";
    8.84  by (auto_tac (Inc_css addSIs2 [SFImplWF, Fair_M1_lemma, PsiInv]
    8.85 -		      addsimps2 [Psi_def,split_box_conj]@more_temp_simps));
    8.86 +                      addsimps2 [Psi_def,split_box_conj]@more_temp_simps));
    8.87  qed "Fair_M1";
     9.1 --- a/src/HOL/TLA/Inc/Inc.thy	Wed Sep 07 20:22:15 2005 +0200
     9.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Wed Sep 07 20:22:39 2005 +0200
     9.3 @@ -1,69 +1,90 @@
     9.4 -(* 
     9.5 +(*
     9.6      File:        TLA/Inc/Inc.thy
     9.7 +    ID:          $Id$
     9.8      Author:      Stephan Merz
     9.9      Copyright:   1997 University of Munich
    9.10  
    9.11      Theory Name: Inc
    9.12 -    Logic Image: TLA
    9.13 -
    9.14 -    Lamport's "increment" example.
    9.15 +    Logic Image: TLA    
    9.16  *)
    9.17  
    9.18 -Inc  =  TLA +
    9.19 +header {* Lamport's "increment" example *}
    9.20 +
    9.21 +theory Inc
    9.22 +imports TLA
    9.23 +begin
    9.24  
    9.25  (* program counter as an enumeration type *)
    9.26  datatype pcount = a | b | g
    9.27  
    9.28  consts
    9.29    (* program variables *)
    9.30 -  x,y,sem                 :: nat stfun
    9.31 -  pc1,pc2                 :: pcount stfun
    9.32 +  x :: "nat stfun"
    9.33 +  y :: "nat stfun"
    9.34 +  sem :: "nat stfun"
    9.35 +  pc1 :: "pcount stfun"
    9.36 +  pc2 :: "pcount stfun"
    9.37  
    9.38    (* names of actions and predicates *)
    9.39 -  M1,M2,N1,N2                             :: action
    9.40 -  alpha1,alpha2,beta1,beta2,gamma1,gamma2 :: action
    9.41 -  InitPhi, InitPsi                        :: stpred
    9.42 -  PsiInv,PsiInv1,PsiInv2,PsiInv3          :: stpred
    9.43 +  M1 :: action
    9.44 +  M2 :: action
    9.45 +  N1 :: action
    9.46 +  N2 :: action
    9.47 +  alpha1 :: action
    9.48 +  alpha2 :: action
    9.49 +  beta1 :: action
    9.50 +  beta2 :: action
    9.51 +  gamma1 :: action
    9.52 +  gamma2 :: action
    9.53 +  InitPhi :: stpred
    9.54 +  InitPsi :: stpred
    9.55 +  PsiInv :: stpred
    9.56 +  PsiInv1 :: stpred
    9.57 +  PsiInv2 :: stpred
    9.58 +  PsiInv3 :: stpred
    9.59  
    9.60    (* temporal formulas *)
    9.61 -  Phi, Psi                                :: temporal
    9.62 -  
    9.63 -rules
    9.64 +  Phi :: temporal
    9.65 +  Psi :: temporal
    9.66 +
    9.67 +axioms
    9.68    (* the "base" variables, required to compute enabledness predicates *)
    9.69 -  Inc_base      "basevars (x, y, sem, pc1, pc2)"
    9.70 +  Inc_base:      "basevars (x, y, sem, pc1, pc2)"
    9.71  
    9.72    (* definitions for high-level program *)
    9.73 -  InitPhi_def   "InitPhi == PRED x = # 0 & y = # 0"
    9.74 -  M1_def        "M1      == ACT  x$ = Suc<$x> & y$ = $y"
    9.75 -  M2_def        "M2      == ACT  y$ = Suc<$y> & x$ = $x"
    9.76 -  Phi_def       "Phi     == TEMP Init InitPhi & [][M1 | M2]_(x,y)
    9.77 +  InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0"
    9.78 +  M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y"
    9.79 +  M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x"
    9.80 +  Phi_def:       "Phi     == TEMP Init InitPhi & [][M1 | M2]_(x,y)
    9.81                                   & WF(M1)_(x,y) & WF(M2)_(x,y)"
    9.82  
    9.83    (* definitions for low-level program *)
    9.84 -  InitPsi_def   "InitPsi == PRED pc1 = #a & pc2 = #a
    9.85 +  InitPsi_def:   "InitPsi == PRED pc1 = #a & pc2 = #a
    9.86                                   & x = # 0 & y = # 0 & sem = # 1"
    9.87 -  alpha1_def    "alpha1  == ACT  $pc1 = #a & pc1$ = #b & $sem = Suc<sem$> 
    9.88 +  alpha1_def:    "alpha1  == ACT  $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
    9.89                                   & unchanged(x,y,pc2)"
    9.90 -  alpha2_def    "alpha2  == ACT  $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
    9.91 +  alpha2_def:    "alpha2  == ACT  $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
    9.92                                   & unchanged(x,y,pc1)"
    9.93 -  beta1_def     "beta1   == ACT  $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
    9.94 +  beta1_def:     "beta1   == ACT  $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
    9.95                                   & unchanged(y,sem,pc2)"
    9.96 -  beta2_def     "beta2   == ACT  $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
    9.97 +  beta2_def:     "beta2   == ACT  $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
    9.98                                   & unchanged(x,sem,pc1)"
    9.99 -  gamma1_def    "gamma1  == ACT  $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
   9.100 +  gamma1_def:    "gamma1  == ACT  $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
   9.101                                   & unchanged(x,y,pc2)"
   9.102 -  gamma2_def    "gamma2  == ACT  $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
   9.103 +  gamma2_def:    "gamma2  == ACT  $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
   9.104                                   & unchanged(x,y,pc1)"
   9.105 -  N1_def        "N1      == ACT  (alpha1 | beta1 | gamma1)"
   9.106 -  N2_def        "N2      == ACT  (alpha2 | beta2 | gamma2)"
   9.107 -  Psi_def       "Psi     == TEMP Init InitPsi
   9.108 +  N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)"
   9.109 +  N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)"
   9.110 +  Psi_def:       "Psi     == TEMP Init InitPsi
   9.111                                 & [][N1 | N2]_(x,y,sem,pc1,pc2)
   9.112                                 & SF(N1)_(x,y,sem,pc1,pc2)
   9.113                                 & SF(N2)_(x,y,sem,pc1,pc2)"
   9.114  
   9.115 -  PsiInv1_def  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a"
   9.116 -  PsiInv2_def  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
   9.117 -  PsiInv3_def  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
   9.118 -  PsiInv_def   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
   9.119 -  
   9.120 +  PsiInv1_def:  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a"
   9.121 +  PsiInv2_def:  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
   9.122 +  PsiInv3_def:  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
   9.123 +  PsiInv_def:   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
   9.124 +
   9.125 +ML {* use_legacy_bindings (the_context ()) *}
   9.126 +
   9.127  end
    10.1 --- a/src/HOL/TLA/Inc/Pcount.thy	Wed Sep 07 20:22:15 2005 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,18 +0,0 @@
    10.4 -(* 
    10.5 -    File:	 TLA/ex/inc/Pcount.thy
    10.6 -    Author:      Stephan Merz
    10.7 -    Copyright:   1997 University of Munich
    10.8 -
    10.9 -    Theory Name: Pcount
   10.10 -    Logic Image: TLA
   10.11 -
   10.12 -Data type "program counter" for the increment example.
   10.13 -Isabelle/HOL's datatype package generates useful simplifications
   10.14 -and case distinction tactics.
   10.15 -*)
   10.16 -
   10.17 -Pcount  =  Main +
   10.18 -
   10.19 -datatype pcount = a | b | g
   10.20 -
   10.21 -end
    11.1 --- a/src/HOL/TLA/Inc/ROOT.ML	Wed Sep 07 20:22:15 2005 +0200
    11.2 +++ b/src/HOL/TLA/Inc/ROOT.ML	Wed Sep 07 20:22:39 2005 +0200
    11.3 @@ -1,3 +1,4 @@
    11.4  
    11.5 -time_use_thy "Pcount";
    11.6 +(* $Id$ *)
    11.7 +
    11.8  time_use_thy "Inc";
    12.1 --- a/src/HOL/TLA/Init.ML	Wed Sep 07 20:22:15 2005 +0200
    12.2 +++ b/src/HOL/TLA/Init.ML	Wed Sep 07 20:22:39 2005 +0200
    12.3 @@ -1,5 +1,8 @@
    12.4 +
    12.5 +(* $Id$ *)
    12.6 +
    12.7  local
    12.8 -  fun prover s = prove_goal Init.thy s 
    12.9 +  fun prover s = prove_goal (the_context ()) s
   12.10                      (K [force_tac (claset(), simpset() addsimps [Init_def]) 1])
   12.11  in
   12.12    val const_simps = map (int_rewrite o prover)
   12.13 @@ -40,4 +43,3 @@
   12.14  qed "Init_act";
   12.15  
   12.16  val Init_defs = [Init_stp, Init_act, int_use Init_temp];
   12.17 -
    13.1 --- a/src/HOL/TLA/Init.thy	Wed Sep 07 20:22:15 2005 +0200
    13.2 +++ b/src/HOL/TLA/Init.thy	Wed Sep 07 20:22:39 2005 +0200
    13.3 @@ -1,5 +1,6 @@
    13.4 -(* 
    13.5 -    File:	 TLA/Init.thy
    13.6 +(*
    13.7 +    File:        TLA/Init.thy
    13.8 +    ID:          $Id$
    13.9      Author:      Stephan Merz
   13.10      Copyright:   1998 University of Munich
   13.11  
   13.12 @@ -10,26 +11,26 @@
   13.13  temporal formulas and its "subformulas" (state predicates and actions).
   13.14  *)
   13.15  
   13.16 -Init  =  Action +
   13.17 +theory Init
   13.18 +imports Action
   13.19 +begin
   13.20 +
   13.21 +typedecl behavior
   13.22 +instance behavior :: world ..
   13.23  
   13.24  types
   13.25 -  behavior
   13.26 -  temporal = behavior form
   13.27 +  temporal = "behavior form"
   13.28  
   13.29 -arities
   13.30 -  behavior    :: type
   13.31 -
   13.32 -instance
   13.33 -  behavior    :: world
   13.34  
   13.35  consts
   13.36 -  Initial     :: ('w::world => bool) => temporal
   13.37 -  first_world :: behavior => ('w::world)
   13.38 -  st1, st2    :: behavior => state
   13.39 +  Initial     :: "('w::world => bool) => temporal"
   13.40 +  first_world :: "behavior => ('w::world)"
   13.41 +  st1         :: "behavior => state"
   13.42 +  st2         :: "behavior => state"
   13.43  
   13.44  syntax
   13.45 -  TEMP       :: lift => 'a                          ("(TEMP _)")
   13.46 -  "_Init"    :: lift => lift                        ("(Init _)"[40] 50)
   13.47 +  TEMP       :: "lift => 'a"                          ("(TEMP _)")
   13.48 +  "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
   13.49  
   13.50  translations
   13.51    "TEMP F"   => "(F::behavior => _)"
   13.52 @@ -37,8 +38,11 @@
   13.53    "sigma |= Init F"  <= "_Init F sigma"
   13.54  
   13.55  defs
   13.56 -  Init_def    "sigma |= Init F  ==  (first_world sigma) |= F"
   13.57 -  fw_temp_def "first_world == %sigma. sigma"
   13.58 -  fw_stp_def  "first_world == st1"
   13.59 -  fw_act_def  "first_world == %sigma. (st1 sigma, st2 sigma)"
   13.60 +  Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
   13.61 +  fw_temp_def: "first_world == %sigma. sigma"
   13.62 +  fw_stp_def:  "first_world == st1"
   13.63 +  fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
   13.64 +
   13.65 +ML {* use_legacy_bindings (the_context ()) *}
   13.66 +
   13.67  end
    14.1 --- a/src/HOL/TLA/Intensional.ML	Wed Sep 07 20:22:15 2005 +0200
    14.2 +++ b/src/HOL/TLA/Intensional.ML	Wed Sep 07 20:22:39 2005 +0200
    14.3 @@ -1,5 +1,6 @@
    14.4 -(* 
    14.5 -    File:	 Intensional.ML
    14.6 +(*
    14.7 +    File:        Intensional.ML
    14.8 +    ID:          $Id$
    14.9      Author:      Stephan Merz
   14.10      Copyright:   1998 University of Munich
   14.11  
   14.12 @@ -14,7 +15,7 @@
   14.13  by (etac spec 1);
   14.14  qed "inteq_reflection";
   14.15  
   14.16 -val [prem] = goalw thy [Valid_def] "(!!w. w |= A) ==> |- A";
   14.17 +val [prem] = goalw (the_context ()) [Valid_def] "(!!w. w |= A) ==> |- A";
   14.18  by (REPEAT (resolve_tac [allI,prem] 1));
   14.19  qed "intI";
   14.20  
   14.21 @@ -25,8 +26,8 @@
   14.22  (** Lift usual HOL simplifications to "intensional" level. **)
   14.23  local
   14.24  
   14.25 -fun prover s = (prove_goal Intensional.thy s 
   14.26 -                 (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews), 
   14.27 +fun prover s = (prove_goal (the_context ()) s
   14.28 +                 (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews),
   14.29                             blast_tac HOL_cs 1])) RS inteq_reflection
   14.30  
   14.31  in
   14.32 @@ -34,19 +35,19 @@
   14.33  val int_simps = map prover
   14.34   [ "|- (x=x) = #True",
   14.35     "|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P",
   14.36 -   "|- ((~P) = P) = #False", "|- (P = (~P)) = #False", 
   14.37 +   "|- ((~P) = P) = #False", "|- (P = (~P)) = #False",
   14.38     "|- (P ~= Q) = (P = (~Q))",
   14.39     "|- (#True=P) = P", "|- (P=#True) = P",
   14.40 -   "|- (#True --> P) = P", "|- (#False --> P) = #True", 
   14.41 +   "|- (#True --> P) = P", "|- (#False --> P) = #True",
   14.42     "|- (P --> #True) = #True", "|- (P --> P) = #True",
   14.43     "|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)",
   14.44 -   "|- (P & #True) = P", "|- (#True & P) = P", 
   14.45 -   "|- (P & #False) = #False", "|- (#False & P) = #False", 
   14.46 +   "|- (P & #True) = P", "|- (#True & P) = P",
   14.47 +   "|- (P & #False) = #False", "|- (#False & P) = #False",
   14.48     "|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False",
   14.49 -   "|- (P | #True) = #True", "|- (#True | P) = #True", 
   14.50 -   "|- (P | #False) = P", "|- (#False | P) = P", 
   14.51 +   "|- (P | #True) = #True", "|- (#True | P) = #True",
   14.52 +   "|- (P | #False) = P", "|- (#False | P) = P",
   14.53     "|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True",
   14.54 -   "|- (! x. P) = P", "|- (? x. P) = P", 
   14.55 +   "|- (! x. P) = P", "|- (? x. P) = P",
   14.56     "|- (~Q --> ~P) = (P --> Q)",
   14.57     "|- (P|Q --> R) = ((P-->R)&(Q-->R))" ]
   14.58  end;
   14.59 @@ -72,7 +73,7 @@
   14.60    rewrite_rule intensional_rews ((th RS intD) handle _ => th);
   14.61  
   14.62  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
   14.63 -fun int_rewrite th = 
   14.64 +fun int_rewrite th =
   14.65      zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection));
   14.66  
   14.67  (* flattening turns "-->" into "==>" and eliminates conjunctions in the
   14.68 @@ -85,18 +86,18 @@
   14.69     unification, therefore the code is a little awkward.
   14.70  *)
   14.71  fun flatten t =
   14.72 -  let 
   14.73 +  let
   14.74      (* analogous to RS, but using matching instead of resolution *)
   14.75      fun matchres tha i thb =
   14.76        case Seq.chop (2, biresolution true [(false,tha)] i thb) of
   14.77 -	  ([th],_) => th
   14.78 -	| ([],_)   => raise THM("matchres: no match", i, [tha,thb])
   14.79 -	|      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
   14.80 +          ([th],_) => th
   14.81 +        | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
   14.82 +        |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
   14.83  
   14.84      (* match tha with some premise of thb *)
   14.85      fun matchsome tha thb =
   14.86        let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
   14.87 -	    | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
   14.88 +            | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
   14.89        in hmatch (nprems_of thb) end
   14.90  
   14.91      fun hflatten t =
   14.92 @@ -122,4 +123,3 @@
   14.93  Goalw [Valid_def] "|- (~ (? x. F x)) = (! x. ~ F x)";
   14.94  by (Simp_tac 1);
   14.95  qed "Not_Rex";
   14.96 -
    15.1 --- a/src/HOL/TLA/Intensional.thy	Wed Sep 07 20:22:15 2005 +0200
    15.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Sep 07 20:22:39 2005 +0200
    15.3 @@ -1,5 +1,6 @@
    15.4 -(* 
    15.5 -    File:	 TLA/Intensional.thy
    15.6 +(*
    15.7 +    File:        TLA/Intensional.thy
    15.8 +    ID:          $Id$
    15.9      Author:      Stephan Merz
   15.10      Copyright:   1998 University of Munich
   15.11  
   15.12 @@ -10,7 +11,9 @@
   15.13  on top of HOL, with lifting of constants and functions.
   15.14  *)
   15.15  
   15.16 -Intensional  =  Main +
   15.17 +theory Intensional
   15.18 +imports Main
   15.19 +begin
   15.20  
   15.21  axclass
   15.22    world < type
   15.23 @@ -18,15 +21,15 @@
   15.24  (** abstract syntax **)
   15.25  
   15.26  types
   15.27 -  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::type *)
   15.28 -  'w form = ('w, bool) expr
   15.29 +  ('w,'a) expr = "'w => 'a"               (* intention: 'w::world, 'a::type *)
   15.30 +  'w form = "('w, bool) expr"
   15.31  
   15.32  consts
   15.33 -  Valid    :: ('w::world) form => bool
   15.34 -  const    :: 'a => ('w::world, 'a) expr
   15.35 -  lift     :: ['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr
   15.36 -  lift2    :: ['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr
   15.37 -  lift3    :: ['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr
   15.38 +  Valid    :: "('w::world) form => bool"
   15.39 +  const    :: "'a => ('w::world, 'a) expr"
   15.40 +  lift     :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr"
   15.41 +  lift2    :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr"
   15.42 +  lift3    :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr"
   15.43  
   15.44    (* "Rigid" quantification (logic level) *)
   15.45    RAll     :: "('a => ('w::world) form) => 'w form"       (binder "Rall " 10)
   15.46 @@ -40,59 +43,59 @@
   15.47    liftargs
   15.48  
   15.49  syntax
   15.50 -  ""            :: id => lift                          ("_")
   15.51 -  ""            :: longid => lift                      ("_")
   15.52 -  ""            :: var => lift                         ("_")
   15.53 -  "_applC"      :: [lift, cargs] => lift               ("(1_/ _)" [1000, 1000] 999)
   15.54 -  ""            :: lift => lift                        ("'(_')")
   15.55 -  "_lambda"     :: [idts, 'a] => lift                  ("(3%_./ _)" [0, 3] 3)
   15.56 -  "_constrain"  :: [lift, type] => lift                ("(_::_)" [4, 0] 3)
   15.57 -  ""            :: lift => liftargs                    ("_")
   15.58 -  "_liftargs"   :: [lift, liftargs] => liftargs        ("_,/ _")
   15.59 -  "_Valid"      :: lift => bool                        ("(|- _)" 5)
   15.60 -  "_holdsAt"    :: ['a, lift] => bool                  ("(_ |= _)" [100,10] 10)
   15.61 +  ""            :: "id => lift"                          ("_")
   15.62 +  ""            :: "longid => lift"                      ("_")
   15.63 +  ""            :: "var => lift"                         ("_")
   15.64 +  "_applC"      :: "[lift, cargs] => lift"               ("(1_/ _)" [1000, 1000] 999)
   15.65 +  ""            :: "lift => lift"                        ("'(_')")
   15.66 +  "_lambda"     :: "[idts, 'a] => lift"                  ("(3%_./ _)" [0, 3] 3)
   15.67 +  "_constrain"  :: "[lift, type] => lift"                ("(_::_)" [4, 0] 3)
   15.68 +  ""            :: "lift => liftargs"                    ("_")
   15.69 +  "_liftargs"   :: "[lift, liftargs] => liftargs"        ("_,/ _")
   15.70 +  "_Valid"      :: "lift => bool"                        ("(|- _)" 5)
   15.71 +  "_holdsAt"    :: "['a, lift] => bool"                  ("(_ |= _)" [100,10] 10)
   15.72  
   15.73    (* Syntax for lifted expressions outside the scope of |- or |= *)
   15.74 -  "LIFT"        :: lift => 'a                          ("LIFT _")
   15.75 +  "LIFT"        :: "lift => 'a"                          ("LIFT _")
   15.76  
   15.77    (* generic syntax for lifted constants and functions *)
   15.78 -  "_const"      :: 'a => lift                          ("(#_)" [1000] 999)
   15.79 -  "_lift"       :: ['a, lift] => lift                  ("(_<_>)" [1000] 999)
   15.80 -  "_lift2"      :: ['a, lift, lift] => lift            ("(_<_,/ _>)" [1000] 999)
   15.81 -  "_lift3"      :: ['a, lift, lift, lift] => lift      ("(_<_,/ _,/ _>)" [1000] 999)
   15.82 +  "_const"      :: "'a => lift"                          ("(#_)" [1000] 999)
   15.83 +  "_lift"       :: "['a, lift] => lift"                  ("(_<_>)" [1000] 999)
   15.84 +  "_lift2"      :: "['a, lift, lift] => lift"            ("(_<_,/ _>)" [1000] 999)
   15.85 +  "_lift3"      :: "['a, lift, lift, lift] => lift"      ("(_<_,/ _,/ _>)" [1000] 999)
   15.86  
   15.87    (* concrete syntax for common infix functions: reuse same symbol *)
   15.88 -  "_liftEqu"    :: [lift, lift] => lift                ("(_ =/ _)" [50,51] 50)
   15.89 -  "_liftNeq"    :: [lift, lift] => lift                ("(_ ~=/ _)" [50,51] 50)
   15.90 -  "_liftNot"    :: lift => lift                        ("(~ _)" [40] 40)
   15.91 -  "_liftAnd"    :: [lift, lift] => lift                ("(_ &/ _)" [36,35] 35)
   15.92 -  "_liftOr"     :: [lift, lift] => lift                ("(_ |/ _)" [31,30] 30)
   15.93 -  "_liftImp"    :: [lift, lift] => lift                ("(_ -->/ _)" [26,25] 25)
   15.94 -  "_liftIf"     :: [lift, lift, lift] => lift          ("(if (_)/ then (_)/ else (_))" 10)
   15.95 -  "_liftPlus"   :: [lift, lift] => lift                ("(_ +/ _)" [66,65] 65)
   15.96 -  "_liftMinus"  :: [lift, lift] => lift                ("(_ -/ _)" [66,65] 65)
   15.97 -  "_liftTimes"  :: [lift, lift] => lift                ("(_ */ _)" [71,70] 70)
   15.98 -  "_liftDiv"    :: [lift, lift] => lift                ("(_ div _)" [71,70] 70)
   15.99 -  "_liftMod"    :: [lift, lift] => lift                ("(_ mod _)" [71,70] 70)
  15.100 -  "_liftLess"   :: [lift, lift] => lift                ("(_/ < _)"  [50, 51] 50)
  15.101 -  "_liftLeq"    :: [lift, lift] => lift                ("(_/ <= _)" [50, 51] 50)
  15.102 -  "_liftMem"    :: [lift, lift] => lift                ("(_/ : _)" [50, 51] 50)
  15.103 -  "_liftNotMem" :: [lift, lift] => lift                ("(_/ ~: _)" [50, 51] 50)
  15.104 -  "_liftFinset" :: liftargs => lift                    ("{(_)}")
  15.105 +  "_liftEqu"    :: "[lift, lift] => lift"                ("(_ =/ _)" [50,51] 50)
  15.106 +  "_liftNeq"    :: "[lift, lift] => lift"                ("(_ ~=/ _)" [50,51] 50)
  15.107 +  "_liftNot"    :: "lift => lift"                        ("(~ _)" [40] 40)
  15.108 +  "_liftAnd"    :: "[lift, lift] => lift"                ("(_ &/ _)" [36,35] 35)
  15.109 +  "_liftOr"     :: "[lift, lift] => lift"                ("(_ |/ _)" [31,30] 30)
  15.110 +  "_liftImp"    :: "[lift, lift] => lift"                ("(_ -->/ _)" [26,25] 25)
  15.111 +  "_liftIf"     :: "[lift, lift, lift] => lift"          ("(if (_)/ then (_)/ else (_))" 10)
  15.112 +  "_liftPlus"   :: "[lift, lift] => lift"                ("(_ +/ _)" [66,65] 65)
  15.113 +  "_liftMinus"  :: "[lift, lift] => lift"                ("(_ -/ _)" [66,65] 65)
  15.114 +  "_liftTimes"  :: "[lift, lift] => lift"                ("(_ */ _)" [71,70] 70)
  15.115 +  "_liftDiv"    :: "[lift, lift] => lift"                ("(_ div _)" [71,70] 70)
  15.116 +  "_liftMod"    :: "[lift, lift] => lift"                ("(_ mod _)" [71,70] 70)
  15.117 +  "_liftLess"   :: "[lift, lift] => lift"                ("(_/ < _)"  [50, 51] 50)
  15.118 +  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ <= _)" [50, 51] 50)
  15.119 +  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ : _)" [50, 51] 50)
  15.120 +  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ ~: _)" [50, 51] 50)
  15.121 +  "_liftFinset" :: "liftargs => lift"                    ("{(_)}")
  15.122    (** TODO: syntax for lifted collection / comprehension **)
  15.123 -  "_liftPair"   :: [lift,liftargs] => lift                   ("(1'(_,/ _'))")
  15.124 +  "_liftPair"   :: "[lift,liftargs] => lift"                   ("(1'(_,/ _'))")
  15.125    (* infix syntax for list operations *)
  15.126 -  "_liftCons" :: [lift, lift] => lift                  ("(_ #/ _)" [65,66] 65)
  15.127 -  "_liftApp"  :: [lift, lift] => lift                  ("(_ @/ _)" [65,66] 65)
  15.128 -  "_liftList" :: liftargs => lift                      ("[(_)]")
  15.129 +  "_liftCons" :: "[lift, lift] => lift"                  ("(_ #/ _)" [65,66] 65)
  15.130 +  "_liftApp"  :: "[lift, lift] => lift"                  ("(_ @/ _)" [65,66] 65)
  15.131 +  "_liftList" :: "liftargs => lift"                      ("[(_)]")
  15.132  
  15.133    (* Rigid quantification (syntax level) *)
  15.134 -  "_ARAll"  :: [idts, lift] => lift                    ("(3! _./ _)" [0, 10] 10)
  15.135 -  "_AREx"   :: [idts, lift] => lift                    ("(3? _./ _)" [0, 10] 10)
  15.136 -  "_AREx1"  :: [idts, lift] => lift                    ("(3?! _./ _)" [0, 10] 10)
  15.137 -  "_RAll" :: [idts, lift] => lift                      ("(3ALL _./ _)" [0, 10] 10)
  15.138 -  "_REx"  :: [idts, lift] => lift                      ("(3EX _./ _)" [0, 10] 10)
  15.139 -  "_REx1" :: [idts, lift] => lift                      ("(3EX! _./ _)" [0, 10] 10)
  15.140 +  "_ARAll"  :: "[idts, lift] => lift"                    ("(3! _./ _)" [0, 10] 10)
  15.141 +  "_AREx"   :: "[idts, lift] => lift"                    ("(3? _./ _)" [0, 10] 10)
  15.142 +  "_AREx1"  :: "[idts, lift] => lift"                    ("(3?! _./ _)" [0, 10] 10)
  15.143 +  "_RAll" :: "[idts, lift] => lift"                      ("(3ALL _./ _)" [0, 10] 10)
  15.144 +  "_REx"  :: "[idts, lift] => lift"                      ("(3EX _./ _)" [0, 10] 10)
  15.145 +  "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)
  15.146  
  15.147  translations
  15.148    "_const"        == "const"
  15.149 @@ -135,7 +138,7 @@
  15.150    "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
  15.151    "_liftList x"   == "_liftCons x (_const [])"
  15.152  
  15.153 -  
  15.154 +
  15.155  
  15.156    "w |= ~A"       <= "_liftNot A w"
  15.157    "w |= A & B"    <= "_liftAnd A B w"
  15.158 @@ -147,41 +150,44 @@
  15.159    "w |= EX! x. A"  <= "_REx1 x A w"
  15.160  
  15.161  syntax (xsymbols)
  15.162 -  "_Valid"      :: lift => bool                        ("(\\<turnstile> _)" 5)
  15.163 -  "_holdsAt"    :: ['a, lift] => bool                  ("(_ \\<Turnstile> _)" [100,10] 10)
  15.164 -  "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
  15.165 -  "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
  15.166 -  "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
  15.167 -  "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
  15.168 -  "_liftImp"    :: [lift, lift] => lift                (infixr "\\<longrightarrow>" 25)
  15.169 -  "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
  15.170 -  "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
  15.171 -  "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
  15.172 -  "_liftLeq"    :: [lift, lift] => lift                ("(_/ \\<le> _)" [50, 51] 50)
  15.173 -  "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
  15.174 -  "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
  15.175 +  "_Valid"      :: "lift => bool"                        ("(\<turnstile> _)" 5)
  15.176 +  "_holdsAt"    :: "['a, lift] => bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
  15.177 +  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
  15.178 +  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
  15.179 +  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
  15.180 +  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
  15.181 +  "_liftImp"    :: "[lift, lift] => lift"                (infixr "\<longrightarrow>" 25)
  15.182 +  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
  15.183 +  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
  15.184 +  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
  15.185 +  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
  15.186 +  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
  15.187 +  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
  15.188  
  15.189  syntax (HTML output)
  15.190 -  "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
  15.191 -  "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
  15.192 -  "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
  15.193 -  "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
  15.194 -  "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
  15.195 -  "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
  15.196 -  "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
  15.197 -  "_liftLeq"    :: [lift, lift] => lift                ("(_/ \\<le> _)" [50, 51] 50)
  15.198 -  "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
  15.199 -  "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
  15.200 +  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
  15.201 +  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
  15.202 +  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
  15.203 +  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
  15.204 +  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
  15.205 +  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
  15.206 +  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
  15.207 +  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
  15.208 +  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
  15.209 +  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
  15.210  
  15.211 -rules
  15.212 -  Valid_def   "|- A    ==  ALL w. w |= A"
  15.213 +axioms
  15.214 +  Valid_def:   "|- A    ==  ALL w. w |= A"
  15.215 +
  15.216 +  unl_con:     "LIFT #c w  ==  c"
  15.217 +  unl_lift:    "LIFT f<x> w == f (x w)"
  15.218 +  unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
  15.219 +  unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
  15.220  
  15.221 -  unl_con     "LIFT #c w  ==  c" 
  15.222 -  unl_lift    "LIFT f<x> w == f (x w)"
  15.223 -  unl_lift2   "LIFT f<x, y> w == f (x w) (y w)"
  15.224 -  unl_lift3   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
  15.225 +  unl_Rall:    "w |= ALL x. A x  ==  ALL x. (w |= A x)"
  15.226 +  unl_Rex:     "w |= EX x. A x   ==  EX x. (w |= A x)"
  15.227 +  unl_Rex1:    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
  15.228  
  15.229 -  unl_Rall    "w |= ALL x. A x  ==  ALL x. (w |= A x)" 
  15.230 -  unl_Rex     "w |= EX x. A x   ==  EX x. (w |= A x)"
  15.231 -  unl_Rex1    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
  15.232 +ML {* use_legacy_bindings (the_context ()) *}
  15.233 +
  15.234  end
    16.1 --- a/src/HOL/TLA/Memory/MIParameters.thy	Wed Sep 07 20:22:15 2005 +0200
    16.2 +++ b/src/HOL/TLA/Memory/MIParameters.thy	Wed Sep 07 20:22:39 2005 +0200
    16.3 @@ -1,5 +1,6 @@
    16.4  (*
    16.5      File:        MIParameters.thy
    16.6 +    ID:          $Id$
    16.7      Author:      Stephan Merz
    16.8      Copyright:   1997 University of Munich
    16.9  
   16.10 @@ -13,4 +14,6 @@
   16.11  
   16.12  datatype  histState  =  histA | histB
   16.13  
   16.14 +ML {* use_legacy_bindings (the_context ()) *}
   16.15 +
   16.16  end
    17.1 --- a/src/HOL/TLA/Memory/MIsafe.ML	Wed Sep 07 20:22:15 2005 +0200
    17.2 +++ b/src/HOL/TLA/Memory/MIsafe.ML	Wed Sep 07 20:22:39 2005 +0200
    17.3 @@ -1,5 +1,6 @@
    17.4  (* 
    17.5      File:        MIsafe.ML
    17.6 +    ID:          $Id$
    17.7      Author:      Stephan Merz
    17.8      Copyright:   1997 University of Munich
    17.9  
    18.1 --- a/src/HOL/TLA/Memory/MemClerk.ML	Wed Sep 07 20:22:15 2005 +0200
    18.2 +++ b/src/HOL/TLA/Memory/MemClerk.ML	Wed Sep 07 20:22:39 2005 +0200
    18.3 @@ -1,12 +1,13 @@
    18.4 -(* 
    18.5 +(*
    18.6      File:        MemClerk.ML
    18.7 +    ID:          $Id$
    18.8      Author:      Stephan Merz
    18.9      Copyright:   1997 University of Munich
   18.10  
   18.11      RPC-Memory example: Memory clerk specification (theorems and proofs)
   18.12  *)
   18.13  
   18.14 -val MC_action_defs = 
   18.15 +val MC_action_defs =
   18.16     [MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
   18.17  
   18.18  val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
   18.19 @@ -41,7 +42,7 @@
   18.20  Goal "|- MClkReply send rcv cst p --> \
   18.21  \        <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)";
   18.22  by (auto_tac (mem_css addsimps2 [angle_def,MClkReply_def]
   18.23 -	              addEs2 [Return_changed]));
   18.24 +                      addEs2 [Return_changed]));
   18.25  qed "MClkReply_change";
   18.26  
   18.27  Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \
    19.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Wed Sep 07 20:22:15 2005 +0200
    19.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Wed Sep 07 20:22:39 2005 +0200
    19.3 @@ -1,5 +1,6 @@
    19.4  (*
    19.5      File:        MemClerk.thy
    19.6 +    ID:          $Id$
    19.7      Author:      Stephan Merz
    19.8      Copyright:   1997 University of Munich
    19.9  
   19.10 @@ -9,7 +10,9 @@
   19.11      RPC-Memory example: specification of the memory clerk.
   19.12  *)
   19.13  
   19.14 -MemClerk = Memory + RPC + MemClerkParameters +
   19.15 +theory MemClerk
   19.16 +imports Memory RPC MemClerkParameters
   19.17 +begin
   19.18  
   19.19  types
   19.20    (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
   19.21 @@ -64,4 +67,6 @@
   19.22    MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
   19.23        "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
   19.24  
   19.25 +ML {* use_legacy_bindings (the_context ()) *}
   19.26 +
   19.27  end
    20.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.ML	Wed Sep 07 20:22:15 2005 +0200
    20.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.ML	Wed Sep 07 20:22:39 2005 +0200
    20.3 @@ -1,5 +1,6 @@
    20.4 -(* 
    20.5 +(*
    20.6      File:        MemClerkParameters.ML
    20.7 +    ID:          $Id$
    20.8      Author:      Stephan Merz
    20.9      Copyright:   1997 University of Munich
   20.10  
   20.11 @@ -8,5 +9,4 @@
   20.12  
   20.13  (*
   20.14  val CP_simps = RP_simps @ mClkState.simps;
   20.15 -
   20.16  *)
    21.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed Sep 07 20:22:15 2005 +0200
    21.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed Sep 07 20:22:39 2005 +0200
    21.3 @@ -1,5 +1,6 @@
    21.4  (*
    21.5      File:        MemClerkParameters.thy
    21.6 +    ID:          $Id$
    21.7      Author:      Stephan Merz
    21.8      Copyright:   1997 University of Munich
    21.9  
   21.10 @@ -9,9 +10,11 @@
   21.11      RPC-Memory example: Parameters of the memory clerk.
   21.12  *)
   21.13  
   21.14 -MemClerkParameters = RPCParameters + 
   21.15 +theory MemClerkParameters
   21.16 +imports RPCParameters
   21.17 +begin
   21.18  
   21.19 -datatype  mClkState  =  clkA | clkB
   21.20 +datatype mClkState = clkA | clkB
   21.21  
   21.22  types
   21.23    (* types sent on the clerk's send and receive channels are argument types
   21.24 @@ -27,4 +30,6 @@
   21.25    MClkReplyVal     :: "Vals => Vals"
   21.26      "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
   21.27  
   21.28 +ML {* use_legacy_bindings (the_context ()) *}
   21.29 +
   21.30  end
    22.1 --- a/src/HOL/TLA/Memory/Memory.ML	Wed Sep 07 20:22:15 2005 +0200
    22.2 +++ b/src/HOL/TLA/Memory/Memory.ML	Wed Sep 07 20:22:39 2005 +0200
    22.3 @@ -1,12 +1,13 @@
    22.4 -(* 
    22.5 +(*
    22.6      File:        Memory.ML
    22.7 +    ID:          $Id$
    22.8      Author:      Stephan Merz
    22.9      Copyright:   1997 University of Munich
   22.10  
   22.11      RPC-Memory example: Memory specification (theorems and proofs)
   22.12  *)
   22.13  
   22.14 -val RM_action_defs = 
   22.15 +val RM_action_defs =
   22.16     [MInit_def, PInit_def, RdRequest_def, WrRequest_def, MemInv_def,
   22.17      GoodRead_def, BadRead_def, ReadInner_def, Read_def,
   22.18      GoodWrite_def, BadWrite_def, WriteInner_def, Write_def,
   22.19 @@ -24,7 +25,7 @@
   22.20  (* The reliable memory is an implementation of the unreliable one *)
   22.21  Goal "|- IRSpec ch mm rs --> IUSpec ch mm rs";
   22.22  by (force_tac (temp_css addsimps2 ([UNext_def,UPSpec_def,IUSpec_def] @ RM_temp_defs)
   22.23 -			addSEs2 [STL4E,squareE]) 1);
   22.24 +                        addSEs2 [STL4E,squareE]) 1);
   22.25  qed "ReliableImplementsUnReliable";
   22.26  
   22.27  (* The memory spec implies the memory invariant *)
   22.28 @@ -43,7 +44,7 @@
   22.29  by (auto_tac (temp_css addSEs2 [MemoryInvariant,NonMemLocInvariant]));
   22.30  qed "MemoryInvariantAll";
   22.31  
   22.32 -(* The memory engages in an action for process p only if there is an 
   22.33 +(* The memory engages in an action for process p only if there is an
   22.34     unanswered call from p.
   22.35     We need this only for the reliable memory.
   22.36  *)
   22.37 @@ -79,14 +80,14 @@
   22.38  \     |- Calling ch p & (arg<ch!p> = #(write l v)) \
   22.39  \        --> Enabled (WriteInner ch mm rs p l v)";
   22.40  by (case_tac "l:MemLoc & v:MemVal" 1);
   22.41 -by (ALLGOALS 
   22.42 +by (ALLGOALS
   22.43       (force_tac (mem_css addsimps2 [WriteInner_def,GoodWrite_def,
   22.44                                      BadWrite_def,WrRequest_def]
   22.45                           addSIs2 [exI] addSEs2 [base_enabled])));
   22.46  qed "WriteInner_enabled";
   22.47  
   22.48  Goal "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult";
   22.49 -by (force_tac (mem_css addsimps2 
   22.50 +by (force_tac (mem_css addsimps2
   22.51                         [Read_def,ReadInner_def,GoodRead_def,BadRead_def,MemInv_def]) 1);
   22.52  qed "ReadResult";
   22.53  
   22.54 @@ -103,8 +104,8 @@
   22.55  \        & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l)) \
   22.56  \        --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))";
   22.57  by (force_tac (mem_css addsimps2 [RNext_def,angle_def]
   22.58 -	               addSEs2 [enabled_mono2]
   22.59 -	               addDs2 [ReadResult, WriteResult]) 1);
   22.60 +                       addSEs2 [enabled_mono2]
   22.61 +                       addDs2 [ReadResult, WriteResult]) 1);
   22.62  qed "RWRNext_enabled";
   22.63  
   22.64  
   22.65 @@ -121,5 +122,5 @@
   22.66   by (force_tac (mem_css addDs2 [base_pair]) 1);
   22.67  by (etac contrapos_np 1);
   22.68  by (action_simp_tac (simpset() addsimps [Write_def,enabled_ex])
   22.69 -	            [WriteInner_enabled,exI] [] 1);
   22.70 +                    [WriteInner_enabled,exI] [] 1);
   22.71  qed "RNext_enabled";
    23.1 --- a/src/HOL/TLA/Memory/Memory.thy	Wed Sep 07 20:22:15 2005 +0200
    23.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Wed Sep 07 20:22:39 2005 +0200
    23.3 @@ -1,5 +1,6 @@
    23.4  (*
    23.5      File:        Memory.thy
    23.6 +    ID:          $Id$
    23.7      Author:      Stephan Merz
    23.8      Copyright:   1997 University of Munich
    23.9  
   23.10 @@ -9,7 +10,9 @@
   23.11      RPC-Memory example: Memory specification
   23.12  *)
   23.13  
   23.14 -Memory = MemoryParameters + ProcedureInterface +
   23.15 +theory Memory
   23.16 +imports MemoryParameters ProcedureInterface
   23.17 +begin
   23.18  
   23.19  types
   23.20    memChType  = "(memOp, Vals) channel"
   23.21 @@ -50,86 +53,89 @@
   23.22    USpec      :: "memChType => temporal"
   23.23  
   23.24    (* memory invariant: in the paper, the invariant is hidden in the definition of
   23.25 -     the predicate S used in the implementation proof, but it is easier to verify 
   23.26 +     the predicate S used in the implementation proof, but it is easier to verify
   23.27       at this level. *)
   23.28    MemInv    :: "memType => Locs => stpred"
   23.29  
   23.30 -rules
   23.31 -  MInit_def         "MInit mm l == PRED mm!l = #InitVal"
   23.32 -  PInit_def         "PInit rs p == PRED rs!p = #NotAResult"
   23.33 +defs
   23.34 +  MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
   23.35 +  PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
   23.36  
   23.37 -  RdRequest_def     "RdRequest ch p l == PRED
   23.38 +  RdRequest_def:     "RdRequest ch p l == PRED
   23.39                           Calling ch p & (arg<ch!p> = #(read l))"
   23.40 -  WrRequest_def     "WrRequest ch p l v == PRED
   23.41 +  WrRequest_def:     "WrRequest ch p l v == PRED
   23.42                           Calling ch p & (arg<ch!p> = #(write l v))"
   23.43    (* a read that doesn't raise BadArg *)
   23.44 -  GoodRead_def      "GoodRead mm rs p l == ACT
   23.45 +  GoodRead_def:      "GoodRead mm rs p l == ACT
   23.46                          #l : #MemLoc & ((rs!p)$ = $(mm!l))"
   23.47    (* a read that raises BadArg *)
   23.48 -  BadRead_def       "BadRead mm rs p l == ACT
   23.49 +  BadRead_def:       "BadRead mm rs p l == ACT
   23.50                          #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
   23.51    (* the read action with l visible *)
   23.52 -  ReadInner_def     "ReadInner ch mm rs p l == ACT
   23.53 +  ReadInner_def:     "ReadInner ch mm rs p l == ACT
   23.54                           $(RdRequest ch p l)
   23.55                           & (GoodRead mm rs p l  |  BadRead mm rs p l)
   23.56                           & unchanged (rtrner ch ! p)"
   23.57    (* the read action with l quantified *)
   23.58 -  Read_def          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
   23.59 +  Read_def:          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
   23.60  
   23.61    (* similar definitions for the write action *)
   23.62 -  GoodWrite_def     "GoodWrite mm rs p l v == ACT
   23.63 +  GoodWrite_def:     "GoodWrite mm rs p l v == ACT
   23.64                          #l : #MemLoc & #v : #MemVal
   23.65                          & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
   23.66 -  BadWrite_def      "BadWrite mm rs p l v == ACT
   23.67 +  BadWrite_def:      "BadWrite mm rs p l v == ACT
   23.68                          ~ (#l : #MemLoc & #v : #MemVal)
   23.69                          & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
   23.70 -  WriteInner_def    "WriteInner ch mm rs p l v == ACT
   23.71 +  WriteInner_def:    "WriteInner ch mm rs p l v == ACT
   23.72                          $(WrRequest ch p l v)
   23.73                          & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
   23.74                          & unchanged (rtrner ch ! p)"
   23.75 -  Write_def         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
   23.76 +  Write_def:         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
   23.77  
   23.78    (* the return action *)
   23.79 -  MemReturn_def     "MemReturn ch rs p == ACT
   23.80 +  MemReturn_def:     "MemReturn ch rs p == ACT
   23.81                         (   ($(rs!p) ~= #NotAResult)
   23.82                          & ((rs!p)$ = #NotAResult)
   23.83                          & Return ch p (rs!p))"
   23.84  
   23.85    (* the failure action of the unreliable memory *)
   23.86 -  MemFail_def       "MemFail ch rs p == ACT
   23.87 +  MemFail_def:       "MemFail ch rs p == ACT
   23.88                          $(Calling ch p)
   23.89                          & ((rs!p)$ = #MemFailure)
   23.90                          & unchanged (rtrner ch ! p)"
   23.91    (* next-state relations for reliable / unreliable memory *)
   23.92 -  RNext_def         "RNext ch mm rs p == ACT 
   23.93 +  RNext_def:         "RNext ch mm rs p == ACT
   23.94                         (  Read ch mm rs p
   23.95                          | (EX l. Write ch mm rs p l)
   23.96                          | MemReturn ch rs p)"
   23.97 -  UNext_def         "UNext ch mm rs p == ACT
   23.98 +  UNext_def:         "UNext ch mm rs p == ACT
   23.99                          (RNext ch mm rs p | MemFail ch rs p)"
  23.100  
  23.101 -  RPSpec_def        "RPSpec ch mm rs p == TEMP
  23.102 +  RPSpec_def:        "RPSpec ch mm rs p == TEMP
  23.103                          Init(PInit rs p)
  23.104                          & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
  23.105                          & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
  23.106                          & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  23.107 -  UPSpec_def        "UPSpec ch mm rs p == TEMP
  23.108 +  UPSpec_def:        "UPSpec ch mm rs p == TEMP
  23.109                          Init(PInit rs p)
  23.110                          & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
  23.111                          & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
  23.112                          & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  23.113 -  MSpec_def         "MSpec ch mm rs l == TEMP
  23.114 +  MSpec_def:         "MSpec ch mm rs l == TEMP
  23.115                          Init(MInit mm l)
  23.116                          & [][ EX p. Write ch mm rs p l ]_(mm!l)"
  23.117 -  IRSpec_def        "IRSpec ch mm rs == TEMP
  23.118 +  IRSpec_def:        "IRSpec ch mm rs == TEMP
  23.119                          (ALL p. RPSpec ch mm rs p)
  23.120                          & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
  23.121 -  IUSpec_def        "IUSpec ch mm rs == TEMP
  23.122 +  IUSpec_def:        "IUSpec ch mm rs == TEMP
  23.123                          (ALL p. UPSpec ch mm rs p)
  23.124                          & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
  23.125  
  23.126 -  RSpec_def         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
  23.127 -  USpec_def         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
  23.128 +  RSpec_def:         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
  23.129 +  USpec_def:         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
  23.130  
  23.131 -  MemInv_def        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
  23.132 +  MemInv_def:        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
  23.133 +
  23.134 +ML {* use_legacy_bindings (the_context ()) *}
  23.135 +
  23.136  end
    24.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Wed Sep 07 20:22:15 2005 +0200
    24.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Wed Sep 07 20:22:39 2005 +0200
    24.3 @@ -1,5 +1,6 @@
    24.4 -(* 
    24.5 +(*
    24.6      File:        MemoryImplementation.ML
    24.7 +    ID:          $Id$
    24.8      Author:      Stephan Merz
    24.9      Copyright:   1997 University of Munich
   24.10  
   24.11 @@ -25,7 +26,7 @@
   24.12     (but it can be a lot faster than MI_css)
   24.13  *)
   24.14  val MI_fast_css =
   24.15 -  let 
   24.16 +  let
   24.17      val (cs,ss) = MI_css
   24.18    in
   24.19      (cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
   24.20 @@ -40,8 +41,8 @@
   24.21  \        --> (EEX rmhist. Init(ALL p. HInit rmhist p) \
   24.22  \                         & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))";
   24.23  by (Clarsimp_tac 1);
   24.24 -by (rtac historyI 1); 
   24.25 -by (TRYALL atac); 
   24.26 +by (rtac historyI 1);
   24.27 +by (TRYALL atac);
   24.28  by (rtac MI_base 1);
   24.29  by (action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1);
   24.30  by (etac fun_cong 1);
   24.31 @@ -52,7 +53,7 @@
   24.32  Goal "|- Implementation --> (EEX rmhist. Hist rmhist)";
   24.33  by (Clarsimp_tac 1);
   24.34  by (rtac ((temp_use HistoryLemma) RS eex_mono) 1);
   24.35 -by (force_tac (MI_css 
   24.36 +by (force_tac (MI_css
   24.37                 addsimps2 [Hist_def,HistP_def,Init_def,all_box,split_box_conj]) 3);
   24.38  by (auto_tac (MI_css
   24.39                addsimps2 [Implementation_def,MClkISpec_def,RPCISpec_def,IRSpec_def,
   24.40 @@ -77,7 +78,7 @@
   24.41  Goal "|- ImpInit p & HInit rmhist p --> S1 rmhist p";
   24.42  by (auto_tac (MI_fast_css
   24.43                addsimps2 [MVNROKBA_def,MClkInit_def,RPCInit_def,PInit_def,
   24.44 -		         HInit_def,ImpInit_def,S_def,S1_def]));
   24.45 +                         HInit_def,ImpInit_def,S_def,S1_def]));
   24.46  qed "Step1_1";
   24.47  
   24.48  (* ========== Step 1.2 ================================================== *)
   24.49 @@ -105,8 +106,8 @@
   24.50  \        --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) \
   24.51  \            | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))";
   24.52  by (action_simp_tac (simpset() addsimps [ImpNext_def]) []
   24.53 -	            (map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1);
   24.54 -by (action_simp_tac (simpset()) [] 
   24.55 +                    (map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1);
   24.56 +by (action_simp_tac (simpset()) []
   24.57                      (squareE::map temp_elim [S3RPC,S3Forward,S3Fail]) 1);
   24.58  by (auto_tac (MI_css addDs2 [S3Hist]));
   24.59  qed "Step1_2_3";
   24.60 @@ -181,7 +182,7 @@
   24.61  \        --> unchanged (rtrner memCh!p, resbar rmhist!p)";
   24.62  by (Clarsimp_tac 1);
   24.63  by (REPEAT (dresolve_tac (map temp_use [S3_excl,S4_excl]) 1));
   24.64 -by (action_simp_tac 
   24.65 +by (action_simp_tac
   24.66        (simpset() addsimps [e_def,c_def,m_def,resbar_def,S_def, S3_def]) [] [] 1);
   24.67  qed "Step1_4_3a";
   24.68  
   24.69 @@ -191,7 +192,7 @@
   24.70  by (Clarsimp_tac 1);
   24.71  by (dtac (temp_use S6_excl) 1);
   24.72  by (auto_tac (MI_css addsimps2 [RPCFail_def,MemFail_def,e_def,c_def,m_def,
   24.73 -	                        resbar_def]));
   24.74 +                                resbar_def]));
   24.75  by (force_tac (MI_css addsimps2 [S3_def,S_def]) 1);
   24.76  by (auto_tac (MI_css addsimps2 [Return_def]));
   24.77  qed "Step1_4_3b";
   24.78 @@ -201,14 +202,14 @@
   24.79  \        --> ReadInner memCh mm (resbar rmhist) p l";
   24.80  by (Clarsimp_tac 1);
   24.81  by (REPEAT (dtac (temp_use S4_excl) 1));
   24.82 -by (action_simp_tac 
   24.83 -      (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def]) 
   24.84 +by (action_simp_tac
   24.85 +      (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def])
   24.86        [] [] 1);
   24.87  by (auto_tac (MI_css addsimps2 [resbar_def]));
   24.88 -by (ALLGOALS (action_simp_tac 
   24.89 +by (ALLGOALS (action_simp_tac
   24.90                  (simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
   24.91 -	                             S_def,S4_def,RdRequest_def,MemInv_def])
   24.92 -		[] [impE,MemValNotAResultE]));
   24.93 +                                     S_def,S4_def,RdRequest_def,MemInv_def])
   24.94 +                [] [impE,MemValNotAResultE]));
   24.95  qed "Step1_4_4a1";
   24.96  
   24.97  Goal "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ \
   24.98 @@ -222,15 +223,15 @@
   24.99  \        --> WriteInner memCh mm (resbar rmhist) p l v";
  24.100  by (Clarsimp_tac 1);
  24.101  by (REPEAT (dtac (temp_use S4_excl) 1));
  24.102 -by (action_simp_tac 
  24.103 +by (action_simp_tac
  24.104        (simpset() addsimps [WriteInner_def, GoodWrite_def, BadWrite_def,
  24.105 -		           e_def, c_def, m_def])
  24.106 +                           e_def, c_def, m_def])
  24.107        [] [] 1);
  24.108  by (auto_tac (MI_css addsimps2 [resbar_def]));
  24.109  by (ALLGOALS (action_simp_tac
  24.110                  (simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
  24.111 -	                             S_def,S4_def,WrRequest_def])
  24.112 -		[] []));
  24.113 +                                     S_def,S4_def,WrRequest_def])
  24.114 +                [] []));
  24.115  qed "Step1_4_4b1";
  24.116  
  24.117  Goal "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$   \
  24.118 @@ -254,7 +255,7 @@
  24.119  by (Clarsimp_tac 1);
  24.120  by (REPEAT (dresolve_tac [temp_use S5_excl, temp_use S6_excl] 1));
  24.121  by (auto_tac (MI_css addsimps2 [e_def,c_def,m_def, resbar_def]));
  24.122 -by (auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def] 
  24.123 +by (auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def]
  24.124                       addSDs2 [MVOKBAnotRF]));
  24.125  qed "Step1_4_5a";
  24.126  
  24.127 @@ -264,7 +265,7 @@
  24.128  by (Clarsimp_tac 1);
  24.129  by (dtac (temp_use S6_excl) 1);
  24.130  by (auto_tac (MI_css addsimps2 [e_def, c_def, m_def, RPCFail_def, Return_def,
  24.131 -		 		MemFail_def, resbar_def]));
  24.132 +                                MemFail_def, resbar_def]));
  24.133  by (auto_tac (MI_css addsimps2 [S5_def,S_def]));
  24.134  qed "Step1_4_5b";
  24.135  
  24.136 @@ -275,11 +276,11 @@
  24.137  by (dtac (temp_use S6_excl) 1);
  24.138  by (action_simp_tac
  24.139        (simpset() addsimps [e_def,r_def,m_def,MClkReply_def,MemReturn_def,
  24.140 -		           Return_def,resbar_def]) [] [] 1);
  24.141 +                           Return_def,resbar_def]) [] [] 1);
  24.142  by (ALLGOALS Asm_full_simp_tac);  (* simplify if-then-else *)
  24.143  by (ALLGOALS (action_simp_tac
  24.144                  (simpset() addsimps [MClkReplyVal_def,S6_def,S_def])
  24.145 -	        [] [MVOKBARFnotNR]));
  24.146 +                [] [MVOKBARFnotNR]));
  24.147  qed "Step1_4_6a";
  24.148  
  24.149  Goal "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$   \
  24.150 @@ -296,7 +297,7 @@
  24.151  Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \
  24.152  \        --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)";
  24.153  by (auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,caller_def,rtrner_def,
  24.154 -			        S_def,Calling_def]));
  24.155 +                                S_def,Calling_def]));
  24.156  qed "S_lemma";
  24.157  
  24.158  Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \
  24.159 @@ -322,13 +323,13 @@
  24.160  (* Frequently needed abbreviation: distinguish between idling and non-idling
  24.161     steps of the implementation, and try to solve the idling case by simplification
  24.162  *)
  24.163 -fun split_idle_tac simps i = 
  24.164 +fun split_idle_tac simps i =
  24.165      EVERY [TRY (rtac actionI i),
  24.166 -	   case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
  24.167 -	   rewrite_goals_tac action_rews,
  24.168 -	   forward_tac [temp_use Step1_4_7] i,
  24.169 -	   asm_full_simp_tac (simpset() addsimps simps) i
  24.170 -	  ];
  24.171 +           case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
  24.172 +           rewrite_goals_tac action_rews,
  24.173 +           forward_tac [temp_use Step1_4_7] i,
  24.174 +           asm_full_simp_tac (simpset() addsimps simps) i
  24.175 +          ];
  24.176  
  24.177  (* ----------------------------------------------------------------------
  24.178     Combine steps 1.2 and 1.4 to prove that the implementation satisfies
  24.179 @@ -386,7 +387,7 @@
  24.180  by (rtac unchanged_safeI 1);
  24.181  by (auto_tac (MI_css addSDs2 [Step1_2_5]));
  24.182  by (auto_tac (MI_css addsimps2 [square_def,UNext_def]
  24.183 -	             addSDs2 [Step1_4_5a,Step1_4_5b]));
  24.184 +                     addSDs2 [Step1_4_5a,Step1_4_5b]));
  24.185  qed "S5safe";
  24.186  
  24.187  Goal "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
  24.188 @@ -395,7 +396,7 @@
  24.189  by (rtac unchanged_safeI 1);
  24.190  by (auto_tac (MI_css addSDs2 [Step1_2_6]));
  24.191  by (auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def]
  24.192 -	             addSDs2 [Step1_4_6a,Step1_4_6b]));
  24.193 +                     addSDs2 [Step1_4_6a,Step1_4_6b]));
  24.194  qed "S6safe";
  24.195  
  24.196  (* ----------------------------------------------------------------------
  24.197 @@ -424,13 +425,13 @@
  24.198  Goal "|- S1 rmhist p --> \
  24.199  \        ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))";
  24.200  by (action_simp_tac (simpset() addsimps [angle_def,S_def,S1_def])
  24.201 -	            [notI] [enabledE,temp_elim Memoryidle] 1);
  24.202 +                    [notI] [enabledE,temp_elim Memoryidle] 1);
  24.203  by (Force_tac 1);
  24.204  qed "S1_RNextdisabled";
  24.205  
  24.206  Goal "|- S1 rmhist p --> \
  24.207  \        ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))";
  24.208 -by (action_simp_tac 
  24.209 +by (action_simp_tac
  24.210        (simpset() addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def])
  24.211        [notI] [enabledE] 1);
  24.212  qed "S1_Returndisabled";
  24.213 @@ -438,13 +439,13 @@
  24.214  Goal "|- []<>S1 rmhist p   \
  24.215  \        --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)";
  24.216  by (auto_tac (MI_css addsimps2 [WF_alt]
  24.217 -		     addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE]));
  24.218 +                     addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE]));
  24.219  qed "RNext_fair";
  24.220  
  24.221  Goal "|- []<>S1 rmhist p   \
  24.222  \        --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)";
  24.223  by (auto_tac (MI_css addsimps2 [WF_alt]
  24.224 -		     addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE]));
  24.225 +                     addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE]));
  24.226  qed "Return_fair";
  24.227  
  24.228  (* ------------------------------ State S2 ------------------------------ *)
  24.229 @@ -493,7 +494,7 @@
  24.230  Goal "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\
  24.231  \        --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))";
  24.232  by (auto_tac (MI_css addsimps2 [r_def]
  24.233 -		     addSIs2 [RPCFail_Next_enabled,RPCFail_enabled]));
  24.234 +                     addSIs2 [RPCFail_Next_enabled,RPCFail_enabled]));
  24.235  by (cut_facts_tac [MI_base] 1);
  24.236  by (blast_tac (claset() addDs [base_pair]) 1);
  24.237  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S3_def])));
  24.238 @@ -529,7 +530,7 @@
  24.239  \        & <RNext rmCh mm ires p>_(m p) \
  24.240  \        --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$";
  24.241  by (auto_tac (MI_css addsimps2 [angle_def]
  24.242 -		     addSDs2 [Step1_2_4, ReadResult, WriteResult]));
  24.243 +                     addSDs2 [Step1_2_4, ReadResult, WriteResult]));
  24.244  qed "S4aRNext_successors";
  24.245  
  24.246  Goal "|- $(S4 rmhist p & ires!p = #NotAResult) \
  24.247 @@ -598,7 +599,7 @@
  24.248  Goal "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
  24.249  \        --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))";
  24.250  by (auto_tac (MI_css addsimps2 [r_def]
  24.251 -		     addSIs2 [RPCFail_Next_enabled, RPCFail_enabled]));
  24.252 +                     addSIs2 [RPCFail_Next_enabled, RPCFail_enabled]));
  24.253  by (cut_facts_tac [MI_base] 1);
  24.254  by (blast_tac (claset() addDs [base_pair]) 1);
  24.255  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S5_def])));
  24.256 @@ -627,7 +628,7 @@
  24.257  Goal "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p";
  24.258  by (action_simp_tac
  24.259        (simpset() addsimps [angle_def,MClkReply_def,Return_def,
  24.260 -		     ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
  24.261 +                     ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
  24.262        [] [] 1);
  24.263  qed "MClkReplyS6";
  24.264  
  24.265 @@ -643,10 +644,10 @@
  24.266  \        --> []<>(S1 rmhist p)";
  24.267  by (Clarsimp_tac 1);
  24.268  by (subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1);
  24.269 -by (etac InfiniteEnsures 1); 
  24.270 +by (etac InfiniteEnsures 1);
  24.271  by (atac 1);
  24.272  by (action_simp_tac (simpset()) []
  24.273 -	            (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1);
  24.274 +                    (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1);
  24.275  by (auto_tac (MI_css addsimps2 [SF_def]));
  24.276  by (etac contrapos_np 1);
  24.277  by (auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE]));
  24.278 @@ -664,7 +665,7 @@
  24.279  \     ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p \
  24.280  \                   ~> S6 rmhist p";
  24.281  by (auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6]
  24.282 -		     addIs2 [LatticeTransitivity]));
  24.283 +                     addIs2 [LatticeTransitivity]));
  24.284  qed "S4bS5S6LeadstoS6";
  24.285  
  24.286  Goal "[| sigma |= S4 rmhist p & ires!p = #NotAResult \
  24.287 @@ -672,19 +673,19 @@
  24.288  \        sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
  24.289  \        sigma |= S5 rmhist p ~> S6 rmhist p |]  \
  24.290  \     ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p";
  24.291 -by (subgoal_tac 
  24.292 +by (subgoal_tac
  24.293       "sigma |= (S4 rmhist p & ires!p = #NotAResult)\
  24.294  \            | (S4 rmhist p & ires!p ~= #NotAResult)\
  24.295  \            | S5 rmhist p | S6 rmhist p ~> S6 rmhist p" 1);
  24.296 - by (eres_inst_tac 
  24.297 + by (eres_inst_tac
  24.298        [("G", "PRED ((S4 rmhist p & ires!p = #NotAResult)\
  24.299  \                | (S4 rmhist p & ires!p ~= #NotAResult)\
  24.300 -\                | S5 rmhist p | S6 rmhist p)")] 
  24.301 +\                | S5 rmhist p | S6 rmhist p)")]
  24.302        (temp_use LatticeTransitivity) 1);
  24.303   by (force_tac (MI_css addsimps2 Init_defs addSIs2 [ImplLeadsto_gen, necT]) 1);
  24.304  by (rtac (temp_use LatticeDisjunctionIntro) 1);
  24.305  by (etac (temp_use LatticeTransitivity) 1);
  24.306 -by (etac (temp_use LatticeTriangle2) 1); 
  24.307 +by (etac (temp_use LatticeTriangle2) 1);
  24.308  by (atac 1);
  24.309  by (auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6]));
  24.310  qed "S4S5S6LeadstoS6";
  24.311 @@ -699,7 +700,7 @@
  24.312  by (etac (temp_use LatticeTriangle2) 1);
  24.313  by (rtac (S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1);
  24.314  by (auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,necT]
  24.315 -	             addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
  24.316 +                     addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
  24.317  qed "S3S4S5S6LeadstoS6";
  24.318  
  24.319  Goal "[| sigma |= S2 rmhist p ~> S3 rmhist p; \
  24.320 @@ -711,11 +712,11 @@
  24.321  \     ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \
  24.322  \                  ~> S6 rmhist p";
  24.323  by (rtac (temp_use LatticeDisjunctionIntro) 1);
  24.324 -by (rtac (temp_use LatticeTransitivity) 1); 
  24.325 +by (rtac (temp_use LatticeTransitivity) 1);
  24.326  by (atac 2);
  24.327  by (rtac (S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1);
  24.328  by (auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,necT]
  24.329 -	             addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
  24.330 +                     addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
  24.331  qed "S2S3S4S5S6LeadstoS6";
  24.332  
  24.333  Goal "[| sigma |= []ImpInv rmhist p; \
  24.334 @@ -750,7 +751,7 @@
  24.335  *)
  24.336  Goal "|- IPImp p --> (ALL l. []$MemInv mm l)";
  24.337  by (auto_tac (MI_css addsimps2 [IPImp_def,box_stp_act]
  24.338 -	             addSIs2 [MemoryInvariantAll]));
  24.339 +                     addSIs2 [MemoryInvariantAll]));
  24.340  qed "Step1_5_1a";
  24.341  
  24.342  Goal "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p) \
  24.343 @@ -759,8 +760,8 @@
  24.344  by (inv_tac MI_css 1);
  24.345  by (auto_tac (MI_css addsimps2 [Init_def, ImpInv_def, box_stp_act]
  24.346                       addSDs2 [Step1_1]
  24.347 -	             addDs2 [S1_successors,S2_successors,S3_successors,
  24.348 -		             S4_successors,S5_successors,S6_successors]));
  24.349 +                     addDs2 [S1_successors,S2_successors,S3_successors,
  24.350 +                             S4_successors,S5_successors,S6_successors]));
  24.351  qed "Step1_5_1b";
  24.352  
  24.353  (*** Initialization ***)
  24.354 @@ -790,9 +791,9 @@
  24.355  \             & [](ALL l. $MemInv mm l)" 1);
  24.356  by (auto_tac (MI_css addsimps2 [split_box_conj,box_stp_act] addSDs2 [Step1_5_1b]));
  24.357  by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
  24.358 -				 ImpLive_def,c_def,r_def,m_def]) 1);
  24.359 +                                 ImpLive_def,c_def,r_def,m_def]) 1);
  24.360  by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
  24.361 -	                         HistP_def,Init_def,ImpInit_def]) 1);
  24.362 +                                 HistP_def,Init_def,ImpInit_def]) 1);
  24.363  by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
  24.364                                   ImpNext_def,c_def,r_def,m_def,split_box_conj]) 1);
  24.365  by (force_tac (MI_css addsimps2 [HistP_def]) 1);
  24.366 @@ -828,7 +829,7 @@
  24.367  (* QED step of step 1 *)
  24.368  Goal "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p";
  24.369  by (auto_tac (MI_css addsimps2 [UPSpec_def,split_box_conj]
  24.370 -		     addSDs2 [GoodImpl]
  24.371 +                     addSDs2 [GoodImpl]
  24.372                       addSIs2 [Step1_5_2a,Step1_5_2b,Step1_5_3b,Step1_5_3c]));
  24.373  qed "Step1";
  24.374  
  24.375 @@ -840,10 +841,10 @@
  24.376  \        & $ImpInv rmhist p  \
  24.377  \        --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)";
  24.378  by (Clarsimp_tac 1);
  24.379 -by (dtac (action_use WriteS4) 1); 
  24.380 +by (dtac (action_use WriteS4) 1);
  24.381  by (atac 1);
  24.382  by (split_idle_tac [] 1);
  24.383 -by (auto_tac (MI_css addsimps2 [ImpNext_def] 
  24.384 +by (auto_tac (MI_css addsimps2 [ImpNext_def]
  24.385                       addSDs2 [S4EnvUnch,S4ClerkUnch,S4RPCUnch]));
  24.386  by (auto_tac (MI_css addsimps2 [square_def] addDs2 [S4Write]));
  24.387  qed "Step2_2a";
  24.388 @@ -872,7 +873,7 @@
  24.389  by (auto_tac (MI_css addsimps2 [MSpec_def]));
  24.390  by (force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 1);
  24.391  by (auto_tac (MI_css addSIs2 [Step2_lemma]
  24.392 -	             addsimps2 [split_box_conj,all_box]));
  24.393 +                     addsimps2 [split_box_conj,all_box]));
  24.394  by (force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 4);
  24.395  by (auto_tac (MI_css addsimps2 [split_box_conj] addSEs2 [allE] addSDs2 [GoodImpl]));
  24.396  qed "Step2";
  24.397 @@ -889,15 +890,15 @@
  24.398  *)
  24.399  Goal "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)";
  24.400  by (auto_tac (MI_css addsimps2 [IUSpec_def,Implementation_def,IPImp_def,
  24.401 -			        MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def]
  24.402 -		     addSIs2 [Step1,Step2]));
  24.403 +                                MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def]
  24.404 +                     addSIs2 [Step1,Step2]));
  24.405  qed "Impl_IUSpec";
  24.406  
  24.407  (* The main theorem: introduce hiding and eliminate history variable. *)
  24.408  Goal "|- Implementation --> USpec memCh";
  24.409  by (Clarsimp_tac 1);
  24.410  by (forward_tac [temp_use History] 1);
  24.411 -by (auto_tac (MI_css addsimps2 [USpec_def] 
  24.412 +by (auto_tac (MI_css addsimps2 [USpec_def]
  24.413                       addIs2 [eexI, Impl_IUSpec, MI_base]
  24.414                       addSEs2 [eexE]));
  24.415  qed "Implementation";
    25.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Sep 07 20:22:15 2005 +0200
    25.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Sep 07 20:22:39 2005 +0200
    25.3 @@ -1,5 +1,6 @@
    25.4  (*
    25.5      File:        MemoryImplementation.thy
    25.6 +    ID:          $Id$
    25.7      Author:      Stephan Merz
    25.8      Copyright:   1997 University of Munich
    25.9  
   25.10 @@ -9,9 +10,11 @@
   25.11      RPC-Memory example: Memory implementation
   25.12  *)
   25.13  
   25.14 -MemoryImplementation = Memory + RPC + MemClerk + Datatype +
   25.15 +theory MemoryImplementation
   25.16 +imports Memory RPC MemClerk
   25.17 +begin
   25.18  
   25.19 -datatype  histState  =  histA | histB
   25.20 +datatype histState = histA | histB
   25.21  
   25.22  types
   25.23    histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
   25.24 @@ -22,7 +25,7 @@
   25.25    memCh         :: "memChType"
   25.26       (* internal variables *)
   25.27    mm            :: "memType"
   25.28 -  
   25.29 +
   25.30    (* the state variables of the implementation *)
   25.31       (* channels *)
   25.32    (* same interface channel memCh *)
   25.33 @@ -80,29 +83,29 @@
   25.34    (* the implementation *)
   25.35    IPImp          :: "PrIds => temporal"
   25.36       "IPImp p == TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
   25.37 -	               & MClkIPSpec memCh crCh cst p
   25.38 -  	               & RPCIPSpec crCh rmCh rst p
   25.39 -	               & RPSpec rmCh mm ires p
   25.40 -		       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"
   25.41 +                       & MClkIPSpec memCh crCh cst p
   25.42 +                       & RPCIPSpec crCh rmCh rst p
   25.43 +                       & RPSpec rmCh mm ires p
   25.44 +                       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"
   25.45  
   25.46    ImpInit        :: "PrIds => stpred"
   25.47        "ImpInit p == PRED (  ~Calling memCh p
   25.48                            & MClkInit crCh cst p
   25.49 -	                  & RPCInit rmCh rst p
   25.50 -	                  & PInit ires p)"
   25.51 +                          & RPCInit rmCh rst p
   25.52 +                          & PInit ires p)"
   25.53  
   25.54    ImpNext        :: "PrIds => action"
   25.55 -      "ImpNext p == ACT  [ENext p]_(e p) 
   25.56 +      "ImpNext p == ACT  [ENext p]_(e p)
   25.57                         & [MClkNext memCh crCh cst p]_(c p)
   25.58 -                       & [RPCNext crCh rmCh rst p]_(r p) 
   25.59 +                       & [RPCNext crCh rmCh rst p]_(r p)
   25.60                         & [RNext rmCh mm ires p]_(m p)"
   25.61  
   25.62    ImpLive        :: "PrIds => temporal"
   25.63 -      "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p) 
   25.64 -			& SF(MClkReply memCh crCh cst p)_(c p)
   25.65 -			& WF(RPCNext crCh rmCh rst p)_(r p) 
   25.66 -			& WF(RNext rmCh mm ires p)_(m p)
   25.67 -			& WF(MemReturn rmCh ires p)_(m p)"
   25.68 +      "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
   25.69 +                        & SF(MClkReply memCh crCh cst p)_(c p)
   25.70 +                        & WF(RPCNext crCh rmCh rst p)_(r p)
   25.71 +                        & WF(RNext rmCh mm ires p)_(m p)
   25.72 +                        & WF(MemReturn rmCh ires p)_(m p)"
   25.73  
   25.74    Implementation :: "temporal"
   25.75        "Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
   25.76 @@ -148,14 +151,14 @@
   25.77    (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
   25.78    ImpInv         :: "histType => PrIds => stpred"
   25.79        "ImpInv rmhist p == PRED (  S1 rmhist p | S2 rmhist p | S3 rmhist p
   25.80 -				| S4 rmhist p | S5 rmhist p | S6 rmhist p)"
   25.81 +                                | S4 rmhist p | S5 rmhist p | S6 rmhist p)"
   25.82  
   25.83    resbar        :: "histType => resType"        (* refinement mapping *)
   25.84 -      "resbar rmhist s p == 
   25.85 +      "resbar rmhist s p ==
   25.86                    (if (S1 rmhist p s | S2 rmhist p s)
   25.87                     then ires s p
   25.88                     else if S3 rmhist p s
   25.89 -                   then if rmhist s p = histA 
   25.90 +                   then if rmhist s p = histA
   25.91                          then ires s p else MemFailure
   25.92                     else if S4 rmhist p s
   25.93                     then if (rmhist s p = histB & ires s p = NotAResult)
   25.94 @@ -167,11 +170,13 @@
   25.95                          then MemFailure else res (crCh s p)
   25.96                     else NotAResult)" (* dummy value *)
   25.97  
   25.98 -rules
   25.99 +axioms
  25.100    (* the "base" variables: everything except resbar and hist (for any index) *)
  25.101 -  MI_base       "basevars (caller memCh!p,
  25.102 -			   (rtrner memCh!p, caller crCh!p, cst!p),
  25.103 -			   (rtrner crCh!p, caller rmCh!p, rst!p),
  25.104 -			   (mm!l, rtrner rmCh!p, ires!p))"
  25.105 +  MI_base:       "basevars (caller memCh!p,
  25.106 +                           (rtrner memCh!p, caller crCh!p, cst!p),
  25.107 +                           (rtrner crCh!p, caller rmCh!p, rst!p),
  25.108 +                           (mm!l, rtrner rmCh!p, ires!p))"
  25.109 +
  25.110 +ML {* use_legacy_bindings (the_context ()) *}
  25.111  
  25.112  end
    26.1 --- a/src/HOL/TLA/Memory/MemoryParameters.ML	Wed Sep 07 20:22:15 2005 +0200
    26.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.ML	Wed Sep 07 20:22:39 2005 +0200
    26.3 @@ -1,5 +1,6 @@
    26.4 -(* 
    26.5 +(*
    26.6      File:        MemoryParameters.ML
    26.7 +    ID:          $Id$
    26.8      Author:      Stephan Merz
    26.9      Copyright:   1997 University of Munich
   26.10  
   26.11 @@ -8,10 +9,10 @@
   26.12  
   26.13  Addsimps ([BadArgNoMemVal,MemFailNoMemVal,InitValMemVal,NotAResultNotVal,
   26.14                    NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]
   26.15 -               @ (map (fn x => x RS not_sym) 
   26.16 +               @ (map (fn x => x RS not_sym)
   26.17                        [NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]));
   26.18  
   26.19 -val prems = goal thy "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P";
   26.20 +val prems = goal (the_context ()) "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P";
   26.21  by (resolve_tac prems 1);
   26.22  by (cut_facts_tac (NotAResultNotVal::prems) 1);
   26.23  by (Force_tac 1);
    27.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Wed Sep 07 20:22:15 2005 +0200
    27.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Wed Sep 07 20:22:39 2005 +0200
    27.3 @@ -1,5 +1,6 @@
    27.4  (*
    27.5      File:        MemoryParameters.thy
    27.6 +    ID:          $Id$
    27.7      Author:      Stephan Merz
    27.8      Copyright:   1997 University of Munich
    27.9  
   27.10 @@ -9,32 +10,37 @@
   27.11      RPC-Memory example: Memory parameters
   27.12  *)
   27.13  
   27.14 -MemoryParameters = Datatype + RPCMemoryParams +
   27.15 +theory MemoryParameters
   27.16 +imports RPCMemoryParams
   27.17 +begin
   27.18  
   27.19  (* the memory operations *)
   27.20  datatype memOp = read Locs | write Locs Vals
   27.21  
   27.22  consts
   27.23    (* memory locations and contents *)
   27.24 -  MemLoc         :: Locs set
   27.25 -  MemVal         :: Vals set
   27.26 +  MemLoc         :: "Locs set"
   27.27 +  MemVal         :: "Vals set"
   27.28  
   27.29    (* some particular values *)
   27.30    OK             :: "Vals"
   27.31    BadArg         :: "Vals"
   27.32    MemFailure     :: "Vals"
   27.33    NotAResult     :: "Vals"  (* defined here for simplicity *)
   27.34 -  
   27.35 +
   27.36    (* the initial value stored in each memory cell *)
   27.37    InitVal        :: "Vals"
   27.38  
   27.39 -rules
   27.40 +axioms
   27.41    (* basic assumptions about the above constants and predicates *)
   27.42 -  BadArgNoMemVal    "BadArg ~: MemVal"
   27.43 -  MemFailNoMemVal   "MemFailure ~: MemVal"
   27.44 -  InitValMemVal     "InitVal : MemVal"
   27.45 -  NotAResultNotVal  "NotAResult ~: MemVal"
   27.46 -  NotAResultNotOK   "NotAResult ~= OK"
   27.47 -  NotAResultNotBA   "NotAResult ~= BadArg"
   27.48 -  NotAResultNotMF   "NotAResult ~= MemFailure"
   27.49 +  BadArgNoMemVal:    "BadArg ~: MemVal"
   27.50 +  MemFailNoMemVal:   "MemFailure ~: MemVal"
   27.51 +  InitValMemVal:     "InitVal : MemVal"
   27.52 +  NotAResultNotVal:  "NotAResult ~: MemVal"
   27.53 +  NotAResultNotOK:   "NotAResult ~= OK"
   27.54 +  NotAResultNotBA:   "NotAResult ~= BadArg"
   27.55 +  NotAResultNotMF:   "NotAResult ~= MemFailure"
   27.56 +
   27.57 +ML {* use_legacy_bindings (the_context ()) *}
   27.58 +
   27.59  end
    28.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.ML	Wed Sep 07 20:22:15 2005 +0200
    28.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.ML	Wed Sep 07 20:22:39 2005 +0200
    28.3 @@ -1,5 +1,6 @@
    28.4 -(* 
    28.5 +(*
    28.6      File:        ProcedureInterface.ML
    28.7 +    ID:          $Id$
    28.8      Author:      Stephan Merz
    28.9      Copyright:   1997 University of Munich
   28.10  
   28.11 @@ -11,10 +12,10 @@
   28.12  
   28.13  (* ---------------------------------------------------------------------------- *)
   28.14  
   28.15 -val Procedure_defs = [caller_def, rtrner_def, Calling_def, 
   28.16 +val Procedure_defs = [caller_def, rtrner_def, Calling_def,
   28.17                        Call_def, Return_def,
   28.18 -		      PLegalCaller_def, LegalCaller_def,
   28.19 -		      PLegalReturner_def, LegalReturner_def];
   28.20 +                      PLegalCaller_def, LegalCaller_def,
   28.21 +                      PLegalReturner_def, LegalReturner_def];
   28.22  
   28.23  (* Calls and returns change their subchannel *)
   28.24  Goal "|- Call ch p v --> <Call ch p v>_((caller ch)!p)";
    29.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Wed Sep 07 20:22:15 2005 +0200
    29.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Wed Sep 07 20:22:39 2005 +0200
    29.3 @@ -1,5 +1,6 @@
    29.4  (*
    29.5      File:        ProcedureInterface.thy
    29.6 +    ID:          $Id$
    29.7      Author:      Stephan Merz
    29.8      Copyright:   1997 University of Munich
    29.9  
   29.10 @@ -9,28 +10,29 @@
   29.11     Procedure interface for RPC-Memory components.
   29.12  *)
   29.13  
   29.14 -ProcedureInterface = TLA + RPCMemoryParams +
   29.15 +theory ProcedureInterface
   29.16 +imports TLA RPCMemoryParams
   29.17 +begin
   29.18  
   29.19 -types
   29.20 +typedecl
   29.21    (* type of channels with argument type 'a and return type 'r.
   29.22 -     we model a channel as an array of variables (of type chan) 
   29.23 -     rather than a single array-valued variable because the 
   29.24 +     we model a channel as an array of variables (of type chan)
   29.25 +     rather than a single array-valued variable because the
   29.26       notation gets a little simpler.
   29.27    *)
   29.28    ('a,'r) chan
   29.29 -  ('a,'r) channel = (PrIds => ('a,'r) chan) stfun
   29.30 -
   29.31 -arities
   29.32 -  chan :: (type,type) type
   29.33 +types
   29.34 +  ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
   29.35  
   29.36  consts
   29.37    (* data-level functions *)
   29.38 -  cbit,rbit	:: "('a,'r) chan => bit"
   29.39 +  cbit          :: "('a,'r) chan => bit"
   29.40 +  rbit          :: "('a,'r) chan => bit"
   29.41    arg           :: "('a,'r) chan => 'a"
   29.42    res           :: "('a,'r) chan => 'r"
   29.43  
   29.44    (* state functions *)
   29.45 -  caller	:: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
   29.46 +  caller        :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
   29.47    rtrner        :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
   29.48  
   29.49    (* state predicates *)
   29.50 @@ -50,10 +52,10 @@
   29.51    slice        :: "('a => 'b) stfun => 'a => 'b stfun"
   29.52  
   29.53  syntax
   29.54 -  "_slice"     :: [lift, 'a] => lift       ("(_!_)" [70,70] 70)
   29.55 +  "_slice"    :: "[lift, 'a] => lift"      ("(_!_)" [70,70] 70)
   29.56  
   29.57 -  "_Call"     :: ['a, 'b, lift] => lift    ("(Call _ _ _)" [90,90,90] 90)
   29.58 -  "_Return"   :: ['a, 'b, lift] => lift    ("(Return _ _ _)" [90,90,90] 90)
   29.59 +  "_Call"     :: "['a, 'b, lift] => lift"    ("(Call _ _ _)" [90,90,90] 90)
   29.60 +  "_Return"   :: "['a, 'b, lift] => lift"    ("(Return _ _ _)" [90,90,90] 90)
   29.61  
   29.62  translations
   29.63    "_slice"  ==  "slice"
   29.64 @@ -61,25 +63,27 @@
   29.65    "_Call"   ==  "ACall"
   29.66    "_Return" ==  "AReturn"
   29.67  
   29.68 -rules
   29.69 -  slice_def     "(PRED (x!i)) s == x s i"
   29.70 +defs
   29.71 +  slice_def:     "(PRED (x!i)) s == x s i"
   29.72  
   29.73 -  caller_def	"caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
   29.74 -  rtrner_def	"rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
   29.75 +  caller_def:    "caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
   29.76 +  rtrner_def:    "rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
   29.77  
   29.78 -  Calling_def	"Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
   29.79 -  Call_def      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
   29.80 +  Calling_def:   "Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
   29.81 +  Call_def:      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
   29.82                                       & (cbit<ch!p>$ ~= $rbit<ch!p>)
   29.83                                       & (arg<ch!p>$ = $v)"
   29.84 -  Return_def    "(ACT Return ch p v) == ACT  $Calling ch p
   29.85 +  Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
   29.86                                       & (rbit<ch!p>$ = $cbit<ch!p>)
   29.87                                       & (res<ch!p>$ = $v)"
   29.88 -  PLegalCaller_def      "PLegalCaller ch p == TEMP
   29.89 +  PLegalCaller_def:      "PLegalCaller ch p == TEMP
   29.90                               Init(~ Calling ch p)
   29.91                               & [][ ? a. Call ch p a ]_((caller ch)!p)"
   29.92 -  LegalCaller_def       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
   29.93 -  PLegalReturner_def    "PLegalReturner ch p == TEMP
   29.94 +  LegalCaller_def:       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
   29.95 +  PLegalReturner_def:    "PLegalReturner ch p == TEMP
   29.96                                  [][ ? v. Return ch p v ]_((rtrner ch)!p)"
   29.97 -  LegalReturner_def     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
   29.98 +  LegalReturner_def:     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
   29.99 +
  29.100 +ML {* use_legacy_bindings (the_context ()) *}
  29.101  
  29.102  end
    30.1 --- a/src/HOL/TLA/Memory/ROOT.ML	Wed Sep 07 20:22:15 2005 +0200
    30.2 +++ b/src/HOL/TLA/Memory/ROOT.ML	Wed Sep 07 20:22:39 2005 +0200
    30.3 @@ -1,2 +1,4 @@
    30.4 +
    30.5 +(* $Id$ *)
    30.6  
    30.7  time_use_thy "MemoryImplementation";
    31.1 --- a/src/HOL/TLA/Memory/RPC.ML	Wed Sep 07 20:22:15 2005 +0200
    31.2 +++ b/src/HOL/TLA/Memory/RPC.ML	Wed Sep 07 20:22:39 2005 +0200
    31.3 @@ -1,12 +1,13 @@
    31.4 -(* 
    31.5 +(*
    31.6      File:        RPC.ML
    31.7 +    ID:          $Id$
    31.8      Author:      Stephan Merz
    31.9      Copyright:   1997 University of Munich
   31.10  
   31.11      RPC-Memory example: RPC specification (theorems and proofs)
   31.12  *)
   31.13  
   31.14 -val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def, 
   31.15 +val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def,
   31.16                         RPCReply_def, RPCNext_def];
   31.17  
   31.18  val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def];
   31.19 @@ -29,7 +30,7 @@
   31.20  Goal "|- RPCFail send rcv rst p --> \
   31.21  \        <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)";
   31.22  by (auto_tac (claset() addSDs [Return_changed],
   31.23 -	     simpset() addsimps [angle_def,RPCNext_def,RPCFail_def]));
   31.24 +             simpset() addsimps [angle_def,RPCNext_def,RPCFail_def]));
   31.25  qed "RPCFail_vis";
   31.26  
   31.27  Goal "|- Enabled (RPCFail send rcv rst p) --> \
    32.1 --- a/src/HOL/TLA/Memory/RPC.thy	Wed Sep 07 20:22:15 2005 +0200
    32.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Wed Sep 07 20:22:39 2005 +0200
    32.3 @@ -1,5 +1,6 @@
    32.4  (*
    32.5      File:        RPC.thy
    32.6 +    ID:          $Id$
    32.7      Author:      Stephan Merz
    32.8      Copyright:   1997 University of Munich
    32.9  
   32.10 @@ -9,7 +10,9 @@
   32.11      RPC-Memory example: RPC specification
   32.12  *)
   32.13  
   32.14 -RPC = RPCParameters + ProcedureInterface + Memory +
   32.15 +theory RPC
   32.16 +imports RPCParameters ProcedureInterface Memory
   32.17 +begin
   32.18  
   32.19  types
   32.20    rpcSndChType  = "(rpcOp,Vals) channel"
   32.21 @@ -31,10 +34,10 @@
   32.22    RPCIPSpec   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
   32.23    RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
   32.24  
   32.25 -rules
   32.26 -  RPCInit_def       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
   32.27 +defs
   32.28 +  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
   32.29  
   32.30 -  RPCFwd_def        "RPCFwd send rcv rst p == ACT
   32.31 +  RPCFwd_def:        "RPCFwd send rcv rst p == ACT
   32.32                           $(Calling send p)
   32.33                           & $(rst!p) = # rpcA
   32.34                           & IsLegalRcvArg<arg<$(send!p)>>
   32.35 @@ -42,36 +45,38 @@
   32.36                           & (rst!p)$ = # rpcB
   32.37                           & unchanged (rtrner send!p)"
   32.38  
   32.39 -  RPCReject_def     "RPCReject send rcv rst p == ACT
   32.40 +  RPCReject_def:     "RPCReject send rcv rst p == ACT
   32.41                             $(rst!p) = # rpcA
   32.42                           & ~IsLegalRcvArg<arg<$(send!p)>>
   32.43                           & Return send p #BadCall
   32.44                           & unchanged ((rst!p), (caller rcv!p))"
   32.45  
   32.46 -  RPCFail_def       "RPCFail send rcv rst p == ACT
   32.47 +  RPCFail_def:       "RPCFail send rcv rst p == ACT
   32.48                             ~$(Calling rcv p)
   32.49                           & Return send p #RPCFailure
   32.50                           & (rst!p)$ = #rpcA
   32.51                           & unchanged (caller rcv!p)"
   32.52  
   32.53 -  RPCReply_def      "RPCReply send rcv rst p == ACT
   32.54 +  RPCReply_def:      "RPCReply send rcv rst p == ACT
   32.55                             ~$(Calling rcv p)
   32.56                           & $(rst!p) = #rpcB
   32.57 -		         & Return send p res<rcv!p>
   32.58 +                         & Return send p res<rcv!p>
   32.59                           & (rst!p)$ = #rpcA
   32.60                           & unchanged (caller rcv!p)"
   32.61  
   32.62 -  RPCNext_def       "RPCNext send rcv rst p == ACT
   32.63 +  RPCNext_def:       "RPCNext send rcv rst p == ACT
   32.64                          (  RPCFwd send rcv rst p
   32.65                           | RPCReject send rcv rst p
   32.66                           | RPCFail send rcv rst p
   32.67                           | RPCReply send rcv rst p)"
   32.68  
   32.69 -  RPCIPSpec_def     "RPCIPSpec send rcv rst p == TEMP
   32.70 +  RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
   32.71                             Init RPCInit rcv rst p
   32.72                           & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
   32.73                           & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
   32.74  
   32.75 -  RPCISpec_def      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
   32.76 +  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
   32.77 +
   32.78 +ML {* use_legacy_bindings (the_context ()) *}
   32.79  
   32.80  end
    33.1 --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Wed Sep 07 20:22:15 2005 +0200
    33.2 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Wed Sep 07 20:22:39 2005 +0200
    33.3 @@ -1,5 +1,6 @@
    33.4 -(* 
    33.5 +(*
    33.6      File:        RPCMemoryParams.thy
    33.7 +    ID:          $Id$
    33.8      Author:      Stephan Merz
    33.9      Copyright:   1997 University of Munich
   33.10  
   33.11 @@ -9,7 +10,9 @@
   33.12      Basic declarations for the RPC-memory example.
   33.13  *)
   33.14  
   33.15 -theory RPCMemoryParams imports Main begin
   33.16 +theory RPCMemoryParams
   33.17 +imports Main
   33.18 +begin
   33.19  
   33.20  types
   33.21    bit = "bool"   (* Signal wires for the procedure interface.
    34.1 --- a/src/HOL/TLA/Memory/RPCParameters.ML	Wed Sep 07 20:22:15 2005 +0200
    34.2 +++ b/src/HOL/TLA/Memory/RPCParameters.ML	Wed Sep 07 20:22:39 2005 +0200
    34.3 @@ -1,11 +1,11 @@
    34.4 -(* 
    34.5 +(*
    34.6      File:        RPCParameters.ML
    34.7 +    ID:          $Id$
    34.8      Author:      Stephan Merz
    34.9      Copyright:   1997 University of Munich
   34.10  
   34.11      RPC-Memory example: RPC parameters (theorems and proofs)
   34.12  *)
   34.13  
   34.14 -
   34.15  Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF]
   34.16            @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF]));
    35.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Wed Sep 07 20:22:15 2005 +0200
    35.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Wed Sep 07 20:22:39 2005 +0200
    35.3 @@ -1,5 +1,6 @@
    35.4  (*
    35.5      File:        RPCParameters.thy
    35.6 +    ID:          $Id$
    35.7      Author:      Stephan Merz
    35.8      Copyright:   1997 University of Munich
    35.9  
   35.10 @@ -11,10 +12,12 @@
   35.11      memory implementation.
   35.12  *)
   35.13  
   35.14 -RPCParameters = MemoryParameters +
   35.15 +theory RPCParameters
   35.16 +imports MemoryParameters
   35.17 +begin
   35.18  
   35.19 -datatype  rpcOp = memcall memOp | othercall Vals
   35.20 -datatype  rpcState = rpcA | rpcB
   35.21 +datatype rpcOp = memcall memOp | othercall Vals
   35.22 +datatype rpcState = rpcA | rpcB
   35.23  
   35.24  consts
   35.25    (* some particular return values *)
   35.26 @@ -25,21 +28,24 @@
   35.27       is legal for the receiver (i.e., the memory). This can now be a little
   35.28       simpler than for the generic RPC component. RelayArg returns an arbitrary
   35.29       memory call for illegal arguments. *)
   35.30 -  IsLegalRcvArg  :: rpcOp => bool
   35.31 -  RPCRelayArg    :: rpcOp => memOp
   35.32 +  IsLegalRcvArg  :: "rpcOp => bool"
   35.33 +  RPCRelayArg    :: "rpcOp => memOp"
   35.34  
   35.35 -rules
   35.36 +axioms
   35.37    (* RPCFailure is different from MemVals and exceptions *)
   35.38 -  RFNoMemVal        "RPCFailure ~: MemVal"
   35.39 -  NotAResultNotRF   "NotAResult ~= RPCFailure"
   35.40 -  OKNotRF           "OK ~= RPCFailure"
   35.41 -  BANotRF           "BadArg ~= RPCFailure"
   35.42 +  RFNoMemVal:        "RPCFailure ~: MemVal"
   35.43 +  NotAResultNotRF:   "NotAResult ~= RPCFailure"
   35.44 +  OKNotRF:           "OK ~= RPCFailure"
   35.45 +  BANotRF:           "BadArg ~= RPCFailure"
   35.46  
   35.47  defs
   35.48 -  IsLegalRcvArg_def "IsLegalRcvArg ra ==
   35.49 +  IsLegalRcvArg_def: "IsLegalRcvArg ra ==
   35.50  		         case ra of (memcall m) => True
   35.51  		                  | (othercall v) => False"
   35.52 -  RPCRelayArg_def   "RPCRelayArg ra ==
   35.53 +  RPCRelayArg_def:   "RPCRelayArg ra ==
   35.54  		         case ra of (memcall m) => m
   35.55  		                  | (othercall v) => arbitrary"
   35.56 +
   35.57 +ML {* use_legacy_bindings (the_context ()) *}
   35.58 +
   35.59  end
    36.1 --- a/src/HOL/TLA/ROOT.ML	Wed Sep 07 20:22:15 2005 +0200
    36.2 +++ b/src/HOL/TLA/ROOT.ML	Wed Sep 07 20:22:39 2005 +0200
    36.3 @@ -1,4 +1,5 @@
    36.4  (*  Title:      TLA/ROOT.ML
    36.5 +    ID:         $Id$
    36.6  
    36.7  Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
    36.8  *)
    37.1 --- a/src/HOL/TLA/Stfun.ML	Wed Sep 07 20:22:15 2005 +0200
    37.2 +++ b/src/HOL/TLA/Stfun.ML	Wed Sep 07 20:22:39 2005 +0200
    37.3 @@ -1,5 +1,6 @@
    37.4 -(* 
    37.5 -    File:	 Stfun.ML
    37.6 +(*
    37.7 +    File:        Stfun.ML
    37.8 +    ID:          $Id$
    37.9      Author:      Stephan Merz
   37.10      Copyright:   1998 University of Munich
   37.11  
   37.12 @@ -51,7 +52,7 @@
   37.13  
   37.14  Goal "!!v. basevars (v::bool stfun, v) ==> False";
   37.15  by (etac baseE 1);
   37.16 -by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1); 
   37.17 +by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1);
   37.18  by (atac 2);
   37.19  by (Asm_full_simp_tac 1);
   37.20  
    38.1 --- a/src/HOL/TLA/Stfun.thy	Wed Sep 07 20:22:15 2005 +0200
    38.2 +++ b/src/HOL/TLA/Stfun.thy	Wed Sep 07 20:22:39 2005 +0200
    38.3 @@ -1,5 +1,6 @@
    38.4 -(* 
    38.5 -    File:	 TLA/Stfun.thy
    38.6 +(*
    38.7 +    File:        TLA/Stfun.thy
    38.8 +    ID:          $Id$
    38.9      Author:      Stephan Merz
   38.10      Copyright:   1998 University of Munich
   38.11  
   38.12 @@ -9,18 +10,18 @@
   38.13  States and state functions for TLA as an "intensional" logic.
   38.14  *)
   38.15  
   38.16 -Stfun  =  Intensional +
   38.17 +theory Stfun
   38.18 +imports Intensional
   38.19 +begin
   38.20 +
   38.21 +typedecl state
   38.22 +
   38.23 +instance state :: world ..
   38.24  
   38.25  types
   38.26 -    state
   38.27 -    'a stfun = "state => 'a"
   38.28 -    stpred   = "bool stfun"
   38.29 +  'a stfun = "state => 'a"
   38.30 +  stpred  = "bool stfun"
   38.31  
   38.32 -arities
   38.33 -  state :: type
   38.34 -
   38.35 -instance
   38.36 -  state :: world
   38.37  
   38.38  consts
   38.39    (* Formalizing type "state" would require formulas to be tagged with
   38.40 @@ -39,20 +40,22 @@
   38.41    stvars    :: "'a stfun => bool"
   38.42  
   38.43  syntax
   38.44 -  "PRED"    :: lift => 'a                          ("PRED _")
   38.45 -  "_stvars" :: lift => bool                        ("basevars _")
   38.46 +  "PRED"    :: "lift => 'a"                          ("PRED _")
   38.47 +  "_stvars" :: "lift => bool"                        ("basevars _")
   38.48  
   38.49  translations
   38.50    "PRED P"   =>  "(P::state => _)"
   38.51    "_stvars"  ==  "stvars"
   38.52  
   38.53  defs
   38.54 -  (* Base variables may be assigned arbitrary (type-correct) values. 
   38.55 +  (* Base variables may be assigned arbitrary (type-correct) values.
   38.56       Note that vs may be a tuple of variables. The correct identification
   38.57       of base variables is up to the user who must take care not to
   38.58       introduce an inconsistency. For example, "basevars (x,x)" would
   38.59       definitely be inconsistent.
   38.60    *)
   38.61 -  basevars_def	"stvars vs == range vs = UNIV"
   38.62 +  basevars_def:  "stvars vs == range vs = UNIV"
   38.63 +
   38.64 +ML {* use_legacy_bindings (the_context ()) *}
   38.65  
   38.66  end
    39.1 --- a/src/HOL/TLA/TLA.ML	Wed Sep 07 20:22:15 2005 +0200
    39.2 +++ b/src/HOL/TLA/TLA.ML	Wed Sep 07 20:22:39 2005 +0200
    39.3 @@ -1,5 +1,6 @@
    39.4 -(* 
    39.5 -    File:	 TLA/TLA.ML
    39.6 +(*
    39.7 +    File:        TLA/TLA.ML
    39.8 +    ID:          $Id$
    39.9      Author:      Stephan Merz
   39.10      Copyright:   1998 University of Munich
   39.11  
   39.12 @@ -8,11 +9,11 @@
   39.13  
   39.14  (* Specialize intensional introduction/elimination rules for temporal formulas *)
   39.15  
   39.16 -val [prem] = goal thy "(!!sigma. sigma |= (F::temporal)) ==> |- F";
   39.17 +val [prem] = goal (the_context ()) "(!!sigma. sigma |= (F::temporal)) ==> |- F";
   39.18  by (REPEAT (resolve_tac [prem,intI] 1));
   39.19  qed "tempI";
   39.20  
   39.21 -val [prem] = goal thy "|- (F::temporal) ==> sigma |= F";
   39.22 +val [prem] = goal (the_context ()) "|- (F::temporal) ==> sigma |= F";
   39.23  by (rtac (prem RS intD) 1);
   39.24  qed "tempD";
   39.25  
   39.26 @@ -23,14 +24,14 @@
   39.27     functions defined in Intensional.ML in that they introduce a
   39.28     "world" parameter of type "behavior".
   39.29  *)
   39.30 -fun temp_unlift th = 
   39.31 +fun temp_unlift th =
   39.32      (rewrite_rule action_rews (th RS tempD))
   39.33      handle _ => action_unlift th;
   39.34  
   39.35  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
   39.36  val temp_rewrite = int_rewrite;
   39.37  
   39.38 -fun temp_use th = 
   39.39 +fun temp_use th =
   39.40      case (concl_of th) of
   39.41        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   39.42                ((flatten (temp_unlift th)) handle _ => th)
   39.43 @@ -77,7 +78,7 @@
   39.44  section "Simple temporal logic";
   39.45  
   39.46  (* []~F == []~Init F *)
   39.47 -bind_thm("boxNotInit", 
   39.48 +bind_thm("boxNotInit",
   39.49           rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] boxInit));
   39.50  
   39.51  Goalw [dmd_def] "TEMP <>F == TEMP <> Init F";
   39.52 @@ -85,7 +86,7 @@
   39.53  by (simp_tac (simpset() addsimps Init_simps) 1);
   39.54  qed "dmdInit";
   39.55  
   39.56 -bind_thm("dmdNotInit", 
   39.57 +bind_thm("dmdNotInit",
   39.58           rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] dmdInit));
   39.59  
   39.60  (* boxInit and dmdInit cannot be used as rewrites, because they loop.
   39.61 @@ -133,7 +134,7 @@
   39.62  by (force_tac (temp_css addEs2 [transT,STL2]) 1);
   39.63  qed "STL3";
   39.64  
   39.65 -(* corresponding elimination rule introduces double boxes: 
   39.66 +(* corresponding elimination rule introduces double boxes:
   39.67     [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
   39.68  *)
   39.69  bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2));
   39.70 @@ -148,7 +149,7 @@
   39.71  
   39.72  
   39.73  (* ------------------------ STL4 ------------------------------------------- *)
   39.74 -val [prem] = goal thy "|- F --> G  ==> |- []F --> []G";
   39.75 +val [prem] = goal (the_context ()) "|- F --> G  ==> |- []F --> []G";
   39.76  by (Clarsimp_tac 1);
   39.77  by (rtac (temp_use normalT) 1);
   39.78  by (rtac (temp_use (prem RS necT)) 1);
   39.79 @@ -156,15 +157,15 @@
   39.80  qed "STL4";
   39.81  
   39.82  (* Unlifted version as an elimination rule *)
   39.83 -val prems = goal thy "[| sigma |= []F; |- F --> G |] ==> sigma |= []G";
   39.84 +val prems = goal (the_context ()) "[| sigma |= []F; |- F --> G |] ==> sigma |= []G";
   39.85  by (REPEAT (resolve_tac (prems @ [temp_use STL4]) 1));
   39.86  qed "STL4E";
   39.87  
   39.88 -val [prem] = goal thy "|- Init F --> Init G ==> |- []F --> []G";
   39.89 +val [prem] = goal (the_context ()) "|- Init F --> Init G ==> |- []F --> []G";
   39.90  by (rtac (rewrite_rule [boxInitD] (prem RS STL4)) 1);
   39.91  qed "STL4_gen";
   39.92  
   39.93 -val prems = goal thy
   39.94 +val prems = goal (the_context ())
   39.95     "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G";
   39.96  by (REPEAT (resolve_tac (prems @ [temp_use STL4_gen]) 1));
   39.97  qed "STL4E_gen";
   39.98 @@ -176,12 +177,12 @@
   39.99  *)
  39.100  
  39.101  (* The dual versions for <> *)
  39.102 -val [prem] = goalw thy [dmd_def]
  39.103 +val [prem] = goalw (the_context ()) [dmd_def]
  39.104     "|- F --> G ==> |- <>F --> <>G";
  39.105  by (fast_tac (temp_cs addSIs [prem] addSEs [STL4E]) 1);
  39.106  qed "DmdImpl";
  39.107  
  39.108 -val prems = goal thy "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G";
  39.109 +val prems = goal (the_context ()) "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G";
  39.110  by (REPEAT (resolve_tac (prems @ [temp_use DmdImpl]) 1));
  39.111  qed "DmdImplE";
  39.112  
  39.113 @@ -201,7 +202,7 @@
  39.114     (NB: F and G must have the same type, i.e., both actions or temporals.)
  39.115     Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
  39.116  *)
  39.117 -val prems = goal thy
  39.118 +val prems = goal (the_context ())
  39.119     "[| sigma |= []F; sigma |= []G; sigma |= [](F&G) ==> PROP R |] ==> PROP R";
  39.120  by (REPEAT (resolve_tac (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1));
  39.121  qed "box_conjE";
  39.122 @@ -225,15 +226,15 @@
  39.123     REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]);
  39.124  
  39.125  fun merge_temp_box_tac i =
  39.126 -   REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i, 
  39.127 +   REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i,
  39.128                           eres_inst_tac [("'a","behavior")] box_thin i]);
  39.129  
  39.130  fun merge_stp_box_tac i =
  39.131 -   REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i, 
  39.132 +   REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i,
  39.133                           eres_inst_tac [("'a","state")] box_thin i]);
  39.134  
  39.135  fun merge_act_box_tac i =
  39.136 -   REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i, 
  39.137 +   REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i,
  39.138                           eres_inst_tac [("'a","state * state")] box_thin i]);
  39.139  
  39.140  
  39.141 @@ -245,8 +246,8 @@
  39.142  
  39.143  Goal "|- (<>(F | G)) = (<>F | <>G)";
  39.144  by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]));
  39.145 -by (ALLGOALS (EVERY' [etac contrapos_np, 
  39.146 -                      merge_box_tac, 
  39.147 +by (ALLGOALS (EVERY' [etac contrapos_np,
  39.148 +                      merge_box_tac,
  39.149                        fast_tac (temp_cs addSEs [STL4E])]));
  39.150  qed "DmdOr";
  39.151  
  39.152 @@ -255,7 +256,7 @@
  39.153  qed "exT";
  39.154  
  39.155  bind_thm("ex_dmd", standard((temp_unlift exT) RS sym));
  39.156 -	     
  39.157 +
  39.158  
  39.159  Goal "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G";
  39.160  by (etac dup_boxE 1);
  39.161 @@ -272,7 +273,7 @@
  39.162  by (fast_tac (temp_cs addSEs [STL4E]) 1);
  39.163  qed "DmdImpl2";
  39.164  
  39.165 -val [prem1,prem2,prem3] = goal thy
  39.166 +val [prem1,prem2,prem3] = goal (the_context ())
  39.167    "[| sigma |= []<>F; sigma |= []G; |- F & G --> H |] ==> sigma |= []<>H";
  39.168  by (cut_facts_tac [prem1,prem2] 1);
  39.169  by (eres_inst_tac [("F","G")] dup_boxE 1);
  39.170 @@ -303,7 +304,7 @@
  39.171  by (fast_tac (temp_cs addSEs [notE,STL4E]) 1);
  39.172  qed "BoxDmd2_simple";
  39.173  
  39.174 -val [p1,p2,p3] = goal thy
  39.175 +val [p1,p2,p3] = goal (the_context ())
  39.176     "[| sigma |= []A; sigma |= <>F; |- []A & F --> G |] ==> sigma |= <>G";
  39.177  by (rtac ((p2 RS (p1 RS (temp_use BoxDmd))) RS DmdImplE) 1);
  39.178  by (rtac p3 1);
  39.179 @@ -312,7 +313,7 @@
  39.180  Goal "|- <>[]F & <>[]G --> <>[](F & G)";
  39.181  by (auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]));
  39.182  by (dtac (temp_use linT) 1);
  39.183 -by (atac 1); 
  39.184 +by (atac 1);
  39.185  by (etac thin_rl 1);
  39.186  by (rtac ((temp_unlift DmdDmd) RS iffD1) 1);
  39.187  by (etac disjE 1);
  39.188 @@ -320,8 +321,8 @@
  39.189  by (rtac BoxDmd 1);
  39.190  by (etac DmdImplE 1);
  39.191  by Auto_tac;
  39.192 -by (dtac (temp_use BoxDmd) 1); 
  39.193 -by (atac 1); 
  39.194 +by (dtac (temp_use BoxDmd) 1);
  39.195 +by (atac 1);
  39.196  by (etac thin_rl 1);
  39.197  by (fast_tac (temp_cs addSEs [DmdImplE]) 1);
  39.198  qed "STL6";
  39.199 @@ -333,7 +334,7 @@
  39.200  Goal "|- ([]#P) = #P";
  39.201  by (rtac tempI 1);
  39.202  by (case_tac "P" 1);
  39.203 -by (auto_tac (temp_css addSIs2 [necT] addDs2 [STL2_gen] 
  39.204 +by (auto_tac (temp_css addSIs2 [necT] addDs2 [STL2_gen]
  39.205                         addsimps2 Init_simps));
  39.206  qed "BoxConst";
  39.207  
  39.208 @@ -365,7 +366,7 @@
  39.209     e.g. []F & ~[]F becomes []F & <>~F !! *)
  39.210  val more_temp_simps =  (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd])
  39.211                         @ (map (fn th => (temp_unlift th) RS eq_reflection)
  39.212 -		         [NotBox, NotDmd]);
  39.213 +                         [NotBox, NotDmd]);
  39.214  
  39.215  Goal "|- ([]<>[]F) = (<>[]F)";
  39.216  by (auto_tac (temp_css addSDs2 [STL2]));
  39.217 @@ -373,7 +374,7 @@
  39.218  by (subgoal_tac "sigma |= <>[][]F & <>[]~[]F" 1);
  39.219  by (etac thin_rl 1);
  39.220  by Auto_tac;
  39.221 -by (dtac (temp_use STL6) 1); 
  39.222 +by (dtac (temp_use STL6) 1);
  39.223  by (atac 1);
  39.224  by (Asm_full_simp_tac 1);
  39.225  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps)));
  39.226 @@ -397,7 +398,7 @@
  39.227  by (Clarsimp_tac 1);
  39.228  by (rtac ccontr 1);
  39.229  by (asm_full_simp_tac (simpset() addsimps more_temp_simps) 1);
  39.230 -by (dtac (temp_use STL6) 1); 
  39.231 +by (dtac (temp_use STL6) 1);
  39.232  by (atac 1);
  39.233  by (Asm_full_simp_tac 1);
  39.234  qed "DBImplBD";
  39.235 @@ -433,14 +434,14 @@
  39.236  by (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_pr]));
  39.237  qed "BoxPrime";
  39.238  
  39.239 -val prems = goal thy "|- $P & P$ --> A  ==>  |- []P --> []A";
  39.240 +val prems = goal (the_context ()) "|- $P & P$ --> A  ==>  |- []P --> []A";
  39.241  by (Clarsimp_tac 1);
  39.242  by (dtac (temp_use BoxPrime) 1);
  39.243 -by (auto_tac (temp_css addsimps2 [Init_stp_act_rev] 
  39.244 +by (auto_tac (temp_css addsimps2 [Init_stp_act_rev]
  39.245                         addSIs2 prems addSEs2 [STL4E]));
  39.246  qed "TLA2";
  39.247  
  39.248 -val prems = goal thy 
  39.249 +val prems = goal (the_context ())
  39.250    "[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A";
  39.251  by (REPEAT (resolve_tac (prems @ (prems RL [temp_use TLA2])) 1));
  39.252  qed "TLA2E";
  39.253 @@ -454,7 +455,7 @@
  39.254  (* ------------------------ INV1, stable --------------------------------------- *)
  39.255  section "stable, invariant";
  39.256  
  39.257 -val prems = goal thy
  39.258 +val prems = goal (the_context ())
  39.259     "[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |] \
  39.260  \   ==> sigma |= []F";
  39.261  by (rtac (temp_use indT) 1);
  39.262 @@ -469,7 +470,7 @@
  39.263  
  39.264  val more_temp_simps = (temp_rewrite box_stp_act)::more_temp_simps;
  39.265  
  39.266 -Goalw [stable_def,boxInit_stp,boxInit_act] 
  39.267 +Goalw [stable_def,boxInit_stp,boxInit_act]
  39.268    "|- (Init P) --> (stable P) --> []P";
  39.269  by (Clarsimp_tac 1);
  39.270  by (etac ind_rule 1);
  39.271 @@ -481,7 +482,7 @@
  39.272  by (fast_tac (temp_cs addSEs [STL4E]) 1);
  39.273  qed "StableT";
  39.274  
  39.275 -val prems = goal thy
  39.276 +val prems = goal (the_context ())
  39.277     "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P";
  39.278  by (REPEAT (resolve_tac (prems @ [temp_use StableT]) 1));
  39.279  qed "Stable";
  39.280 @@ -560,7 +561,7 @@
  39.281  by (fast_tac (temp_cs addIs [DmdPrime] addSEs [STL4E]) 1);
  39.282  qed "InfinitePrime";
  39.283  
  39.284 -val prems = goalw thy [temp_rewrite InfinitePrime]
  39.285 +val prems = goalw (the_context ()) [temp_rewrite InfinitePrime]
  39.286    "[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P";
  39.287  by (rtac InfImpl 1);
  39.288  by (REPEAT (resolve_tac prems 1));
  39.289 @@ -570,7 +571,7 @@
  39.290  section "fairness";
  39.291  
  39.292  (* alternative definitions of fairness *)
  39.293 -Goalw [WF_def,dmd_def] 
  39.294 +Goalw [WF_def,dmd_def]
  39.295    "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)";
  39.296  by (fast_tac temp_cs 1);
  39.297  qed "WF_alt";
  39.298 @@ -582,7 +583,7 @@
  39.299  
  39.300  (* theorems to "box" fairness conditions *)
  39.301  Goal "|- WF(A)_v --> []WF(A)_v";
  39.302 -by (auto_tac (temp_css addsimps2 (WF_alt::more_temp_simps) 
  39.303 +by (auto_tac (temp_css addsimps2 (WF_alt::more_temp_simps)
  39.304                         addSIs2 [BoxOr]));
  39.305  qed "BoxWFI";
  39.306  
  39.307 @@ -591,7 +592,7 @@
  39.308  qed "WF_Box";
  39.309  
  39.310  Goal "|- SF(A)_v --> []SF(A)_v";
  39.311 -by (auto_tac (temp_css addsimps2 (SF_alt::more_temp_simps) 
  39.312 +by (auto_tac (temp_css addsimps2 (SF_alt::more_temp_simps)
  39.313                         addSIs2 [BoxOr]));
  39.314  qed "BoxSFI";
  39.315  
  39.316 @@ -618,7 +619,7 @@
  39.317  qed "leadsto_init";
  39.318  
  39.319  (* |- F & (F ~> G) --> <>G *)
  39.320 -bind_thm("leadsto_init_temp", 
  39.321 +bind_thm("leadsto_init_temp",
  39.322           rewrite_rule Init_simps (read_instantiate [("'a","behavior")] leadsto_init));
  39.323  
  39.324  Goalw [leadsto_def] "|- ([]<>Init F --> []<>G) = (<>(F ~> G))";
  39.325 @@ -628,14 +629,14 @@
  39.326  by (fast_tac (temp_cs addSIs [InitDmd] addSEs [STL4E]) 1);
  39.327  by (subgoal_tac "sigma |= []<><>G" 1);
  39.328  by (asm_full_simp_tac (simpset() addsimps more_temp_simps) 1);
  39.329 -by (dtac (temp_use BoxDmdDmdBox) 1); 
  39.330 +by (dtac (temp_use BoxDmdDmdBox) 1);
  39.331  by (atac 1);
  39.332  by (fast_tac (temp_cs addSEs [DmdImplE,STL4E]) 1);
  39.333  qed "streett_leadsto";
  39.334  
  39.335  Goal "|- []<>F & (F ~> G) --> []<>G";
  39.336  by (Clarsimp_tac 1);
  39.337 -by (etac ((temp_use InitDmd) RS 
  39.338 +by (etac ((temp_use InitDmd) RS
  39.339            ((temp_unlift streett_leadsto) RS iffD2 RS mp)) 1);
  39.340  by (asm_simp_tac (simpset() addsimps [dmdInitD]) 1);
  39.341  qed "leadsto_infinite";
  39.342 @@ -656,7 +657,7 @@
  39.343  *)
  39.344  Goalw [leadsto_def] "|- []I & (P & I ~> Q) --> (P ~> Q)";
  39.345  by (Clarsimp_tac 1);
  39.346 -by (etac STL4Edup 1); 
  39.347 +by (etac STL4Edup 1);
  39.348  by (atac 1);
  39.349  by (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_gen]));
  39.350  qed "INV_leadsto";
  39.351 @@ -682,17 +683,17 @@
  39.352  qed "ImplLeadsto_gen";
  39.353  
  39.354  bind_thm("ImplLeadsto",
  39.355 -         rewrite_rule Init_simps 
  39.356 +         rewrite_rule Init_simps
  39.357               (read_instantiate [("'a","behavior"), ("'b","behavior")] ImplLeadsto_gen));
  39.358  
  39.359  Goal "!!F G. |- F --> G ==> |- F ~> G";
  39.360 -by (auto_tac (temp_css addsimps2 [Init_def] 
  39.361 +by (auto_tac (temp_css addsimps2 [Init_def]
  39.362                         addSIs2 [ImplLeadsto_gen,necT]));
  39.363  qed "ImplLeadsto_simple";
  39.364  
  39.365 -val [prem] = goalw thy [leadsto_def]
  39.366 +val [prem] = goalw (the_context ()) [leadsto_def]
  39.367    "|- A & $P --> Q` ==> |- []A --> (P ~> Q)";
  39.368 -by (clarsimp_tac (temp_css addSEs2 [INV_leadsto]) 1); 
  39.369 +by (clarsimp_tac (temp_css addSEs2 [INV_leadsto]) 1);
  39.370  by (etac STL4E_gen 1);
  39.371  by (auto_tac (temp_css addsimps2 Init_defs addSIs2 [PrimeDmd,prem]));
  39.372  qed "EnsuresLeadsto";
  39.373 @@ -703,12 +704,12 @@
  39.374  by (auto_tac (temp_css addsimps2 Init_simps addSIs2 [PrimeDmd]));
  39.375  qed "EnsuresLeadsto2";
  39.376  
  39.377 -val [p1,p2] = goalw thy [leadsto_def]
  39.378 +val [p1,p2] = goalw (the_context ()) [leadsto_def]
  39.379    "[| |- $P & N --> P` | Q`; \
  39.380  \     |- ($P & N) & A --> Q` \
  39.381  \  |] ==> |- []N & []([]P --> <>A) --> (P ~> Q)";
  39.382  by (Clarsimp_tac 1);
  39.383 -by (etac STL4Edup 1); 
  39.384 +by (etac STL4Edup 1);
  39.385  by (atac 1);
  39.386  by (Clarsimp_tac 1);
  39.387  by (subgoal_tac "sigmaa |= []($P --> P` | Q`)" 1);
  39.388 @@ -720,7 +721,7 @@
  39.389  by (force_tac (temp_css addEs2 [STL4E] addDs2 [p1]) 1);
  39.390  qed "ensures";
  39.391  
  39.392 -val prems = goal thy
  39.393 +val prems = goal (the_context ())
  39.394    "[| |- $P & N --> P` | Q`; \
  39.395  \     |- ($P & N) & A --> Q` \
  39.396  \  |] ==> |- []N & []<>A --> (P ~> Q)";
  39.397 @@ -730,9 +731,9 @@
  39.398  by (force_tac (temp_css addSEs2 [STL4E]) 1);
  39.399  qed "ensures_simple";
  39.400  
  39.401 -val prems = goal thy
  39.402 +val prems = goal (the_context ())
  39.403    "[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q";
  39.404 -by (REPEAT (resolve_tac (prems @ 
  39.405 +by (REPEAT (resolve_tac (prems @
  39.406                           (map temp_use [leadsto_infinite, EnsuresLeadsto])) 1));
  39.407  qed "EnsuresInfinite";
  39.408  
  39.409 @@ -751,7 +752,7 @@
  39.410  by (clarsimp_tac (temp_css addSEs2 [STL4E]) 1);
  39.411  by (rtac dup_dmdD 1);
  39.412  by (subgoal_tac "sigmaa |= <>Init G" 1);
  39.413 - by (etac DmdImpl2 1); 
  39.414 + by (etac DmdImpl2 1);
  39.415   by (atac 1);
  39.416  by (asm_simp_tac (simpset() addsimps [dmdInitD]) 1);
  39.417  qed "LatticeTransitivity";
  39.418 @@ -785,7 +786,7 @@
  39.419  Goal "|- (A ~> D | B) & (B ~> D) --> (A ~> D)";
  39.420  by (Clarsimp_tac 1);
  39.421  by (subgoal_tac "sigma |= (D | B) ~> D" 1);
  39.422 -by (eres_inst_tac [("G", "LIFT (D | B)")] (temp_use LatticeTransitivity) 1); 
  39.423 +by (eres_inst_tac [("G", "LIFT (D | B)")] (temp_use LatticeTransitivity) 1);
  39.424  by (atac 1);
  39.425  by (auto_tac (temp_css addIs2 [LatticeDisjunctionIntro,LatticeReflexivity]));
  39.426  qed "LatticeTriangle";
  39.427 @@ -793,7 +794,7 @@
  39.428  Goal "|- (A ~> B | D) & (B ~> D) --> (A ~> D)";
  39.429  by (Clarsimp_tac 1);
  39.430  by (subgoal_tac "sigma |= B | D ~> D" 1);
  39.431 -by (eres_inst_tac [("G", "LIFT (B | D)")] (temp_use LatticeTransitivity) 1); 
  39.432 +by (eres_inst_tac [("G", "LIFT (B | D)")] (temp_use LatticeTransitivity) 1);
  39.433  by (atac 1);
  39.434  by (auto_tac (temp_css addIs2 [LatticeDisjunctionIntro,LatticeReflexivity]));
  39.435  qed "LatticeTriangle2";
  39.436 @@ -801,7 +802,7 @@
  39.437  (*** Lamport's fairness rules ***)
  39.438  section "Fairness rules";
  39.439  
  39.440 -val prems = goal thy
  39.441 +val prems = goal (the_context ())
  39.442    "[| |- $P & N  --> P` | Q`;   \
  39.443  \     |- ($P & N) & <A>_v --> Q`;   \
  39.444  \     |- $P & N --> $(Enabled(<A>_v)) |]   \
  39.445 @@ -809,7 +810,7 @@
  39.446  by (clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1);
  39.447  by (rtac (temp_use ensures) 1);
  39.448  by (TRYALL (ares_tac prems));
  39.449 -by (etac STL4Edup 1); 
  39.450 +by (etac STL4Edup 1);
  39.451  by (atac 1);
  39.452  by (clarsimp_tac (temp_css addsimps2 [WF_def]) 1);
  39.453  by (rtac (temp_use STL2) 1);
  39.454 @@ -819,17 +820,17 @@
  39.455  qed "WF1";
  39.456  
  39.457  (* Sometimes easier to use; designed for action B rather than state predicate Q *)
  39.458 -val [prem1,prem2,prem3] = goalw thy [leadsto_def]
  39.459 +val [prem1,prem2,prem3] = goalw (the_context ()) [leadsto_def]
  39.460    "[| |- N & $P --> $Enabled (<A>_v);            \
  39.461 -\     |- N & <A>_v --> B;                  \ 
  39.462 +\     |- N & <A>_v --> B;                  \
  39.463  \     |- [](N & [~A]_v) --> stable P  |]  \
  39.464  \  ==> |- []N & WF(A)_v --> (P ~> B)";
  39.465  by (clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1);
  39.466 -by (etac STL4Edup 1); 
  39.467 +by (etac STL4Edup 1);
  39.468  by (atac 1);
  39.469  by (Clarsimp_tac 1);
  39.470  by (rtac (temp_use (prem2 RS DmdImpl)) 1);
  39.471 -by (rtac (temp_use BoxDmd_simple) 1); 
  39.472 +by (rtac (temp_use BoxDmd_simple) 1);
  39.473  by (atac 1);
  39.474  by (rtac classical 1);
  39.475  by (rtac (temp_use STL2) 1);
  39.476 @@ -841,7 +842,7 @@
  39.477  by (asm_full_simp_tac (simpset() addsimps [split_box_conj,temp_use NotDmd,not_angle]) 1);
  39.478  qed "WF_leadsto";
  39.479  
  39.480 -val prems = goal thy
  39.481 +val prems = goal (the_context ())
  39.482    "[| |- $P & N  --> P` | Q`;   \
  39.483  \     |- ($P & N) & <A>_v --> Q`;   \
  39.484  \     |- []P & []N & []F --> <>Enabled(<A>_v) |]   \
  39.485 @@ -851,26 +852,26 @@
  39.486  by (TRYALL (ares_tac prems));
  39.487  by (eres_inst_tac [("F","F")] dup_boxE 1);
  39.488  by (merge_temp_box_tac 1);
  39.489 -by (etac STL4Edup 1); 
  39.490 +by (etac STL4Edup 1);
  39.491  by (atac 1);
  39.492  by (clarsimp_tac (temp_css addsimps2 [SF_def]) 1);
  39.493 -by (rtac (temp_use STL2) 1); 
  39.494 +by (rtac (temp_use STL2) 1);
  39.495  by (etac mp 1);
  39.496  by (resolve_tac (map temp_use (prems RL [STL4])) 1);
  39.497  by (asm_simp_tac (simpset() addsimps [split_box_conj, STL3]) 1);
  39.498  qed "SF1";
  39.499  
  39.500 -val [prem1,prem2,prem3,prem4] = goal thy
  39.501 +val [prem1,prem2,prem3,prem4] = goal (the_context ())
  39.502    "[| |- N & <B>_f --> <M>_g;   \
  39.503  \     |- $P & P` & <N & A>_f --> B;   \
  39.504  \     |- P & Enabled(<M>_g) --> Enabled(<A>_f);   \
  39.505  \     |- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P |]   \
  39.506  \ ==> |- []N & WF(A)_f & []F --> WF(M)_g";
  39.507 -by (clarsimp_tac (temp_css addSDs2 [BoxWFI, (temp_use BoxDmdBox) RS iffD2] 
  39.508 +by (clarsimp_tac (temp_css addSDs2 [BoxWFI, (temp_use BoxDmdBox) RS iffD2]
  39.509                             addsimps2 [read_instantiate [("A","M")] WF_def]) 1);
  39.510  by (eres_inst_tac [("F","F")] dup_boxE 1);
  39.511  by (merge_temp_box_tac 1);
  39.512 -by (etac STL4Edup 1); 
  39.513 +by (etac STL4Edup 1);
  39.514  by (atac 1);
  39.515  by (clarsimp_tac (temp_css addSIs2
  39.516           [(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1);
  39.517 @@ -880,36 +881,36 @@
  39.518  by (rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1);
  39.519  by (asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1);
  39.520  by (merge_act_box_tac 1);
  39.521 -by (forward_tac [temp_use prem4] 1); 
  39.522 +by (forward_tac [temp_use prem4] 1);
  39.523  by (TRYALL atac);
  39.524 -by (dtac (temp_use STL6) 1); 
  39.525 +by (dtac (temp_use STL6) 1);
  39.526  by (atac 1);
  39.527  by (eres_inst_tac [("V","sigmaa |= <>[]P")] thin_rl 1);
  39.528  by (eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1);
  39.529  by (dtac (temp_use BoxWFI) 1);
  39.530  by (eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1);
  39.531  by (merge_temp_box_tac 1);
  39.532 -by (etac DmdImpldup 1); 
  39.533 +by (etac DmdImpldup 1);
  39.534  by (atac 1);
  39.535  by (auto_tac (temp_css addsimps2 [split_box_conj,STL3,WF_Box,box_stp_act]));
  39.536   by (force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1);
  39.537  by (rtac (temp_use STL2) 1);
  39.538 -by (force_tac (temp_css addsimps2 [WF_def,split_box_conj] addSEs2 [mp] 
  39.539 +by (force_tac (temp_css addsimps2 [WF_def,split_box_conj] addSEs2 [mp]
  39.540                          addSIs2 [InitDmd, prem3 RS STL4]) 1);
  39.541  qed "WF2";
  39.542  
  39.543 -val [prem1,prem2,prem3,prem4] = goal thy
  39.544 +val [prem1,prem2,prem3,prem4] = goal (the_context ())
  39.545    "[| |- N & <B>_f --> <M>_g;   \
  39.546  \     |- $P & P` & <N & A>_f --> B;   \
  39.547  \     |- P & Enabled(<M>_g) --> Enabled(<A>_f);   \
  39.548  \     |- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P |]   \
  39.549  \ ==> |- []N & SF(A)_f & []F --> SF(M)_g";
  39.550 -by (clarsimp_tac (temp_css addSDs2 [BoxSFI] 
  39.551 +by (clarsimp_tac (temp_css addSDs2 [BoxSFI]
  39.552                             addsimps2 [read_instantiate [("A","M")] SF_def]) 1);
  39.553  by (eres_inst_tac [("F","F")] dup_boxE 1);
  39.554  by (eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1);
  39.555  by (merge_temp_box_tac 1);
  39.556 -by (etac STL4Edup 1); 
  39.557 +by (etac STL4Edup 1);
  39.558  by (atac 1);
  39.559  by (clarsimp_tac (temp_css addSIs2
  39.560          [(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1);
  39.561 @@ -919,19 +920,19 @@
  39.562  by (rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1);
  39.563  by (asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1);
  39.564  by (merge_act_box_tac 1);
  39.565 -by (forward_tac [temp_use prem4] 1); 
  39.566 +by (forward_tac [temp_use prem4] 1);
  39.567  by (TRYALL atac);
  39.568  by (eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1);
  39.569  by (dtac (temp_use BoxSFI) 1);
  39.570  by (eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1);
  39.571  by (eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1);
  39.572  by (merge_temp_box_tac 1);
  39.573 -by (etac DmdImpldup 1); 
  39.574 +by (etac DmdImpldup 1);
  39.575  by (atac 1);
  39.576  by (auto_tac (temp_css addsimps2 [split_box_conj,STL3,SF_Box,box_stp_act]));
  39.577   by (force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1);
  39.578  by (rtac (temp_use STL2) 1);
  39.579 -by (force_tac (temp_css addsimps2 [SF_def,split_box_conj] addSEs2 [mp,InfImpl] 
  39.580 +by (force_tac (temp_css addsimps2 [SF_def,split_box_conj] addSEs2 [mp,InfImpl]
  39.581                          addSIs2 [prem3]) 1);
  39.582  qed "SF2";
  39.583  
  39.584 @@ -940,7 +941,7 @@
  39.585  (* ------------------------------------------------------------------------- *)
  39.586  section "Well-founded orderings";
  39.587  
  39.588 -val p1::prems = goal thy
  39.589 +val p1::prems = goal (the_context ())
  39.590    "[| wf r;  \
  39.591  \     !!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y))   \
  39.592  \  |] ==> sigma |= F x ~> G";
  39.593 @@ -962,7 +963,7 @@
  39.594   by (force_tac (temp_css addsimps2 Init_defs) 1);
  39.595  by (clarsimp_tac (temp_css addsimps2 [leadsto_exists,not_square]@more_temp_simps) 1);
  39.596  by (etac wf_leadsto 1);
  39.597 -by (rtac (temp_use ensures_simple) 1); 
  39.598 +by (rtac (temp_use ensures_simple) 1);
  39.599  by (TRYALL atac);
  39.600  by (auto_tac (temp_css addsimps2 [square_def,angle_def]));
  39.601  qed "wf_not_box_decrease";
  39.602 @@ -974,13 +975,13 @@
  39.603  (* If there are infinitely many steps where v decreases, then there
  39.604     have to be infinitely many non-stuttering steps where v doesn't decrease.
  39.605  *)
  39.606 -val [prem] = goal thy
  39.607 +val [prem] = goal (the_context ())
  39.608    "wf r ==> |- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v";
  39.609  by (Clarsimp_tac 1);
  39.610  by (rtac ccontr 1);
  39.611  by (asm_full_simp_tac (simpset() addsimps not_angle::more_temp_simps) 1);
  39.612  by (dtac (prem RS (temp_use wf_not_dmd_box_decrease)) 1);
  39.613 -by (dtac (temp_use BoxDmdDmdBox) 1); 
  39.614 +by (dtac (temp_use BoxDmdDmdBox) 1);
  39.615  by (atac 1);
  39.616  by (subgoal_tac "sigma |= []<>((#False)::action)" 1);
  39.617   by (Force_tac 1);
  39.618 @@ -995,8 +996,8 @@
  39.619  Goal "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)";
  39.620  by (Clarsimp_tac 1);
  39.621  by (subgoal_tac "sigma |= []<><~( (n`,$n) : #less_than )>_n" 1);
  39.622 - by (etac thin_rl 1); 
  39.623 - by (etac STL4E 1); 
  39.624 + by (etac thin_rl 1);
  39.625 + by (etac STL4E 1);
  39.626   by (rtac DmdImpl 1);
  39.627   by (clarsimp_tac (temp_css addsimps2 [angle_def]) 1);
  39.628  by (rtac (temp_use wf_box_dmd_decrease) 1);
  39.629 @@ -1009,10 +1010,10 @@
  39.630  (* ------------------------------------------------------------------------- *)
  39.631  section "Flexible quantification";
  39.632  
  39.633 -val [prem1,prem2] = goal thy
  39.634 +val [prem1,prem2] = goal (the_context ())
  39.635    "[| basevars vs; (!!x. basevars (x,vs) ==> sigma |= F x) |]\
  39.636  \  ==> sigma |= (AALL x. F x)";
  39.637 -by (auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] 
  39.638 +by (auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE]
  39.639                         addSIs2 [prem1] addSDs2 [prem2]));
  39.640  qed "aallI";
  39.641  
  39.642 @@ -1023,14 +1024,14 @@
  39.643  qed "aallE";
  39.644  
  39.645  (* monotonicity of quantification *)
  39.646 -val [min,maj] = goal thy
  39.647 +val [min,maj] = goal (the_context ())
  39.648    "[| sigma |= EEX x. F x; !!x. sigma |= F x --> G x |] ==> sigma |= EEX x. G x";
  39.649  by (rtac (unit_base RS (min RS eexE)) 1);
  39.650  by (rtac (temp_use eexI) 1);
  39.651  by (etac ((rewrite_rule intensional_rews maj) RS mp) 1);
  39.652  qed "eex_mono";
  39.653  
  39.654 -val [min,maj] = goal thy
  39.655 +val [min,maj] = goal (the_context ())
  39.656    "[| sigma |= AALL x. F(x); !!x. sigma |= F(x) --> G(x) |] ==> sigma |= AALL x. G(x)";
  39.657  by (rtac (unit_base RS aallI) 1);
  39.658  by (rtac ((rewrite_rule intensional_rews maj) RS mp) 1);
  39.659 @@ -1038,7 +1039,7 @@
  39.660  qed "aall_mono";
  39.661  
  39.662  (* Derived history introduction rule *)
  39.663 -val [p1,p2,p3,p4,p5] = goal thy
  39.664 +val [p1,p2,p3,p4,p5] = goal (the_context ())
  39.665    "[| sigma |= Init I; sigma |= []N; basevars vs; \
  39.666  \     (!!h. basevars(h,vs) ==> |- I & h = ha --> HI h); \
  39.667  \     (!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)) \
  39.668 @@ -1046,7 +1047,7 @@
  39.669  by (rtac ((temp_use history) RS eexE) 1);
  39.670   by (rtac p3 1);
  39.671  by (rtac (temp_use eexI) 1);
  39.672 -by (Clarsimp_tac 1); 
  39.673 +by (Clarsimp_tac 1);
  39.674  by (rtac conjI 1);
  39.675  by (cut_facts_tac [p2] 2);
  39.676  by (merge_box_tac 2);
    40.1 --- a/src/HOL/TLA/TLA.thy	Wed Sep 07 20:22:15 2005 +0200
    40.2 +++ b/src/HOL/TLA/TLA.thy	Wed Sep 07 20:22:39 2005 +0200
    40.3 @@ -1,5 +1,6 @@
    40.4 -(* 
    40.5 +(*
    40.6      File:        TLA/TLA.thy
    40.7 +    ID:          $Id$
    40.8      Author:      Stephan Merz
    40.9      Copyright:   1998 University of Munich
   40.10  
   40.11 @@ -9,32 +10,34 @@
   40.12  The temporal level of TLA.
   40.13  *)
   40.14  
   40.15 -TLA  =  Init +
   40.16 +theory TLA
   40.17 +imports Init
   40.18 +begin
   40.19  
   40.20  consts
   40.21    (** abstract syntax **)
   40.22 -  Box        :: ('w::world) form => temporal
   40.23 -  Dmd        :: ('w::world) form => temporal
   40.24 -  leadsto    :: ['w::world form, 'v::world form] => temporal
   40.25 -  Stable     :: stpred => temporal
   40.26 -  WF         :: [action, 'a stfun] => temporal
   40.27 -  SF         :: [action, 'a stfun] => temporal
   40.28 +  Box        :: "('w::world) form => temporal"
   40.29 +  Dmd        :: "('w::world) form => temporal"
   40.30 +  leadsto    :: "['w::world form, 'v::world form] => temporal"
   40.31 +  Stable     :: "stpred => temporal"
   40.32 +  WF         :: "[action, 'a stfun] => temporal"
   40.33 +  SF         :: "[action, 'a stfun] => temporal"
   40.34  
   40.35    (* Quantification over (flexible) state variables *)
   40.36 -  EEx        :: ('a stfun => temporal) => temporal       (binder "Eex " 10)
   40.37 -  AAll       :: ('a stfun => temporal) => temporal       (binder "Aall " 10)
   40.38 +  EEx        :: "('a stfun => temporal) => temporal"       (binder "Eex " 10)
   40.39 +  AAll       :: "('a stfun => temporal) => temporal"       (binder "Aall " 10)
   40.40  
   40.41    (** concrete syntax **)
   40.42  syntax
   40.43 -  "_Box"     :: lift => lift                        ("([]_)" [40] 40)
   40.44 -  "_Dmd"     :: lift => lift                        ("(<>_)" [40] 40)
   40.45 -  "_leadsto" :: [lift,lift] => lift                 ("(_ ~> _)" [23,22] 22)
   40.46 -  "_stable"  :: lift => lift                        ("(stable/ _)")
   40.47 -  "_WF"      :: [lift,lift] => lift                 ("(WF'(_')'_(_))" [0,60] 55)
   40.48 -  "_SF"      :: [lift,lift] => lift                 ("(SF'(_')'_(_))" [0,60] 55)
   40.49 +  "_Box"     :: "lift => lift"                        ("([]_)" [40] 40)
   40.50 +  "_Dmd"     :: "lift => lift"                        ("(<>_)" [40] 40)
   40.51 +  "_leadsto" :: "[lift,lift] => lift"                 ("(_ ~> _)" [23,22] 22)
   40.52 +  "_stable"  :: "lift => lift"                        ("(stable/ _)")
   40.53 +  "_WF"      :: "[lift,lift] => lift"                 ("(WF'(_')'_(_))" [0,60] 55)
   40.54 +  "_SF"      :: "[lift,lift] => lift"                 ("(SF'(_')'_(_))" [0,60] 55)
   40.55  
   40.56 -  "_EEx"     :: [idts, lift] => lift                ("(3EEX _./ _)" [0,10] 10)
   40.57 -  "_AAll"    :: [idts, lift] => lift                ("(3AALL _./ _)" [0,10] 10)
   40.58 +  "_EEx"     :: "[idts, lift] => lift"                ("(3EEX _./ _)" [0,10] 10)
   40.59 +  "_AAll"    :: "[idts, lift] => lift"                ("(3AALL _./ _)" [0,10] 10)
   40.60  
   40.61  translations
   40.62    "_Box"      ==   "Box"
   40.63 @@ -56,43 +59,46 @@
   40.64    "sigma |= AALL x. F"    <= "_AAll x F sigma"
   40.65  
   40.66  syntax (xsymbols)
   40.67 -  "_Box"     :: lift => lift                        ("(\\<box>_)" [40] 40)
   40.68 -  "_Dmd"     :: lift => lift                        ("(\\<diamond>_)" [40] 40)
   40.69 -  "_leadsto" :: [lift,lift] => lift                 ("(_ \\<leadsto> _)" [23,22] 22)
   40.70 -  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
   40.71 -  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
   40.72 +  "_Box"     :: "lift => lift"                        ("(\<box>_)" [40] 40)
   40.73 +  "_Dmd"     :: "lift => lift"                        ("(\<diamond>_)" [40] 40)
   40.74 +  "_leadsto" :: "[lift,lift] => lift"                 ("(_ \<leadsto> _)" [23,22] 22)
   40.75 +  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
   40.76 +  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
   40.77  
   40.78  syntax (HTML output)
   40.79 -  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
   40.80 -  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
   40.81 +  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
   40.82 +  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
   40.83  
   40.84 -rules
   40.85 +axioms
   40.86    (* Definitions of derived operators *)
   40.87 -  dmd_def      "TEMP <>F  ==  TEMP ~[]~F"
   40.88 -  boxInit      "TEMP []F  ==  TEMP []Init F"
   40.89 -  leadsto_def  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
   40.90 -  stable_def   "TEMP stable P  ==  TEMP []($P --> P$)"
   40.91 -  WF_def       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
   40.92 -  SF_def       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
   40.93 -  aall_def     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
   40.94 +  dmd_def:      "TEMP <>F  ==  TEMP ~[]~F"
   40.95 +  boxInit:      "TEMP []F  ==  TEMP []Init F"
   40.96 +  leadsto_def:  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
   40.97 +  stable_def:   "TEMP stable P  ==  TEMP []($P --> P$)"
   40.98 +  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
   40.99 +  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
  40.100 +  aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
  40.101  
  40.102  (* Base axioms for raw TLA. *)
  40.103 -  normalT    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
  40.104 -  reflT      "|- []F --> F"         (* F::temporal *)
  40.105 -  transT     "|- []F --> [][]F"     (* polymorphic *)
  40.106 -  linT       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
  40.107 -  discT      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
  40.108 -  primeI     "|- []P --> Init P`"
  40.109 -  primeE     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
  40.110 -  indT       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
  40.111 -  allT       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
  40.112 +  normalT:    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
  40.113 +  reflT:      "|- []F --> F"         (* F::temporal *)
  40.114 +  transT:     "|- []F --> [][]F"     (* polymorphic *)
  40.115 +  linT:       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
  40.116 +  discT:      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
  40.117 +  primeI:     "|- []P --> Init P`"
  40.118 +  primeE:     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
  40.119 +  indT:       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
  40.120 +  allT:       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
  40.121  
  40.122 -  necT       "|- F ==> |- []F"      (* polymorphic *)
  40.123 +  necT:       "|- F ==> |- []F"      (* polymorphic *)
  40.124  
  40.125  (* Flexible quantification: refinement mappings, history variables *)
  40.126 -  eexI       "|- F x --> (EEX x. F x)"
  40.127 -  eexE       "[| sigma |= (EEX x. F x); basevars vs;
  40.128 -		 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) 
  40.129 -	      |] ==> G sigma"
  40.130 -  history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
  40.131 +  eexI:       "|- F x --> (EEX x. F x)"
  40.132 +  eexE:       "[| sigma |= (EEX x. F x); basevars vs;
  40.133 +                 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
  40.134 +              |] ==> G sigma"
  40.135 +  history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
  40.136 +
  40.137 +ML {* use_legacy_bindings (the_context ()) *}
  40.138 +
  40.139  end