--- a/src/HOL/TLA/Action.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Action.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,15 +1,16 @@
-(*
- File: Action.ML
+(*
+ File: Action.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
Lemmas and tactics for TLA actions.
*)
-(* The following assertion specializes "intI" for any world type
+(* The following assertion specializes "intI" for any world type
which is a pair, not just for "state * state".
*)
-val [prem] = goal thy "(!!s t. (s,t) |= A) ==> |- A";
+val [prem] = goal (the_context ()) "(!!s t. (s,t) |= A) ==> |- A";
by (REPEAT (resolve_tac [prem,intI,prod_induct] 1));
qed "actionI";
@@ -18,8 +19,8 @@
qed "actionD";
local
- fun prover s = prove_goal Action.thy s
- (fn _ => [rtac actionI 1,
+ fun prover s = prove_goal (the_context ()) s
+ (fn _ => [rtac actionI 1,
rewrite_goals_tac (unl_after::intensional_rews),
rtac refl 1])
in
@@ -44,8 +45,8 @@
functions defined in Intensional.ML in that they introduce a
"world" parameter of the form (s,t) and apply additional rewrites.
*)
-fun action_unlift th =
- (rewrite_rule action_rews (th RS actionD))
+fun action_unlift th =
+ (rewrite_rule action_rews (th RS actionD))
handle _ => int_unlift th;
(* Turn |- A = B into meta-level rewrite rule A == B *)
@@ -72,7 +73,7 @@
by (Asm_simp_tac 1);
qed "busy_squareI";
-val prems = goal thy
+val prems = goal (the_context ())
"[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)";
by (cut_facts_tac prems 1);
by (rewrite_goals_tac (square_def::action_rews));
@@ -80,18 +81,18 @@
by (REPEAT (eresolve_tac prems 1));
qed "squareE";
-val prems = goalw thy (square_def::action_rews)
+val prems = goalw (the_context ()) (square_def::action_rews)
"[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v";
by (rtac disjCI 1);
by (eresolve_tac prems 1);
qed "squareCI";
-goalw thy [angle_def]
+goalw (the_context ()) [angle_def]
"!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v";
by (Asm_simp_tac 1);
qed "angleI";
-val prems = goalw thy (angle_def::action_rews)
+val prems = goalw (the_context ()) (angle_def::action_rews)
"[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R";
by (cut_facts_tac prems 1);
by (etac conjE 1);
@@ -101,7 +102,7 @@
AddIs [angleI, squareCI];
AddEs [angleE, squareE];
-goal thy
+goal (the_context ())
"!!f. [| |- unchanged f & ~B --> unchanged g; \
\ |- A & ~unchanged g --> B \
\ |] ==> |- [A]_f --> [B]_g";
@@ -110,23 +111,23 @@
by (auto_tac (claset(), simpset() addsimps [square_def]));
qed "square_simulation";
-goalw thy [square_def,angle_def]
+goalw (the_context ()) [square_def,angle_def]
"|- (~ [A]_v) = <~A>_v";
by Auto_tac;
qed "not_square";
-goalw thy [square_def,angle_def]
+goalw (the_context ()) [square_def,angle_def]
"|- (~ <A>_v) = [~A]_v";
by Auto_tac;
qed "not_angle";
(* ============================== Facts about ENABLED ============================== *)
-goal thy "|- A --> $Enabled A";
+goal (the_context ()) "|- A --> $Enabled A";
by (auto_tac (claset(), simpset() addsimps [enabled_def]));
qed "enabledI";
-val prems = goalw thy [enabled_def]
+val prems = goalw (the_context ()) [enabled_def]
"[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q";
by (cut_facts_tac prems 1);
by (etac exE 1);
@@ -134,12 +135,12 @@
by (atac 1);
qed "enabledE";
-goal thy "|- ~$Enabled G --> ~ G";
+goal (the_context ()) "|- ~$Enabled G --> ~ G";
by (auto_tac (claset(), simpset() addsimps [enabled_def]));
qed "notEnabledD";
(* Monotonicity *)
-val [min,maj] = goal thy
+val [min,maj] = goal (the_context ())
"[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G";
by (rtac (min RS enabledE) 1);
by (rtac (action_use enabledI) 1);
@@ -147,30 +148,30 @@
qed "enabled_mono";
(* stronger variant *)
-val [min,maj] = goal thy
+val [min,maj] = goal (the_context ())
"[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G";
by (rtac (min RS enabledE) 1);
by (rtac (action_use enabledI) 1);
by (etac maj 1);
qed "enabled_mono2";
-goal thy "|- Enabled F --> Enabled (F | G)";
+goal (the_context ()) "|- Enabled F --> Enabled (F | G)";
by (auto_tac (claset() addSEs [enabled_mono], simpset()));
qed "enabled_disj1";
-goal thy "|- Enabled G --> Enabled (F | G)";
+goal (the_context ()) "|- Enabled G --> Enabled (F | G)";
by (auto_tac (claset() addSEs [enabled_mono], simpset()));
qed "enabled_disj2";
-goal thy "|- Enabled (F & G) --> Enabled F";
+goal (the_context ()) "|- Enabled (F & G) --> Enabled F";
by (auto_tac (claset() addSEs [enabled_mono], simpset()));
qed "enabled_conj1";
-goal thy "|- Enabled (F & G) --> Enabled G";
+goal (the_context ()) "|- Enabled (F & G) --> Enabled G";
by (auto_tac (claset() addSEs [enabled_mono], simpset()));
qed "enabled_conj2";
-val prems = goal thy
+val prems = goal (the_context ())
"[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q";
by (cut_facts_tac prems 1);
by (resolve_tac prems 1);
@@ -178,24 +179,24 @@
by (etac (action_use enabled_conj2) 1);
qed "enabled_conjE";
-goal thy "|- Enabled (F | G) --> Enabled F | Enabled G";
+goal (the_context ()) "|- Enabled (F | G) --> Enabled F | Enabled G";
by (auto_tac (claset(), simpset() addsimps [enabled_def]));
qed "enabled_disjD";
-goal thy "|- Enabled (F | G) = (Enabled F | Enabled G)";
+goal (the_context ()) "|- Enabled (F | G) = (Enabled F | Enabled G)";
by (Clarsimp_tac 1);
by (rtac iffI 1);
by (etac (action_use enabled_disjD) 1);
by (REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1));
qed "enabled_disj";
-goal thy "|- Enabled (EX x. F x) = (EX x. Enabled (F x))";
+goal (the_context ()) "|- Enabled (EX x. F x) = (EX x. Enabled (F x))";
by (force_tac (claset(), simpset() addsimps [enabled_def]) 1);
qed "enabled_ex";
(* A rule that combines enabledI and baseE, but generates fewer instantiations *)
-val prems = goal thy
+val prems = goal (the_context ())
"[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A";
by (cut_facts_tac prems 1);
by (etac exE 1);
@@ -213,10 +214,10 @@
Note that it applies whatever simplifications are currently active.
*)
fun action_simp_tac ss intros elims =
- asm_full_simp_tac
+ asm_full_simp_tac
(ss setloop ((resolve_tac ((map action_use intros)
@ [refl,impI,conjI,actionI,intI,allI]))
- ORELSE' (eresolve_tac ((map action_use elims)
+ ORELSE' (eresolve_tac ((map action_use elims)
@ [conjE,disjE,exE]))));
(* default version without additional plug-in rules *)
@@ -240,7 +241,7 @@
(* Example:
-val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
+val [prem] = goal (the_context ()) "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
by (enabled_tac prem 1);
by Auto_tac;
--- a/src/HOL/TLA/Action.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Action.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/Action.thy
+(*
+ File: TLA/Action.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -9,43 +10,46 @@
Define the action level of TLA as an Isabelle theory.
*)
-Action = Intensional + Stfun +
+theory Action
+imports Stfun
+begin
+
(** abstract syntax **)
types
'a trfun = "(state * state) => 'a"
- action = bool trfun
+ action = "bool trfun"
instance
- "*" :: (world, world) world
+ "*" :: (world, world) world ..
consts
(** abstract syntax **)
- before :: 'a stfun => 'a trfun
- after :: 'a stfun => 'a trfun
- unch :: 'a stfun => action
+ before :: "'a stfun => 'a trfun"
+ after :: "'a stfun => 'a trfun"
+ unch :: "'a stfun => action"
- SqAct :: [action, 'a stfun] => action
- AnAct :: [action, 'a stfun] => action
- enabled :: action => stpred
+ SqAct :: "[action, 'a stfun] => action"
+ AnAct :: "[action, 'a stfun] => action"
+ enabled :: "action => stpred"
(** concrete syntax **)
syntax
(* Syntax for writing action expressions in arbitrary contexts *)
- "ACT" :: lift => 'a ("(ACT _)")
+ "ACT" :: "lift => 'a" ("(ACT _)")
- "_before" :: lift => lift ("($_)" [100] 99)
- "_after" :: lift => lift ("(_$)" [100] 99)
- "_unchanged" :: lift => lift ("(unchanged _)" [100] 99)
+ "_before" :: "lift => lift" ("($_)" [100] 99)
+ "_after" :: "lift => lift" ("(_$)" [100] 99)
+ "_unchanged" :: "lift => lift" ("(unchanged _)" [100] 99)
(*** Priming: same as "after" ***)
- "_prime" :: lift => lift ("(_`)" [100] 99)
+ "_prime" :: "lift => lift" ("(_`)" [100] 99)
- "_SqAct" :: [lift, lift] => lift ("([_]'_(_))" [0,1000] 99)
- "_AnAct" :: [lift, lift] => lift ("(<_>'_(_))" [0,1000] 99)
- "_Enabled" :: lift => lift ("(Enabled _)" [100] 100)
+ "_SqAct" :: "[lift, lift] => lift" ("([_]'_(_))" [0,1000] 99)
+ "_AnAct" :: "[lift, lift] => lift" ("(<_>'_(_))" [0,1000] 99)
+ "_Enabled" :: "lift => lift" ("(Enabled _)" [100] 100)
translations
"ACT A" => "(A::state*state => _)"
@@ -61,13 +65,16 @@
"s |= Enabled A" <= "_Enabled A s"
"w |= unchanged f" <= "_unchanged f w"
-rules
- unl_before "(ACT $v) (s,t) == v s"
- unl_after "(ACT v$) (s,t) == v t"
+axioms
+ unl_before: "(ACT $v) (s,t) == v s"
+ unl_after: "(ACT v$) (s,t) == v t"
- unchanged_def "(s,t) |= unchanged v == (v t = v s)"
- square_def "ACT [A]_v == ACT (A | unchanged v)"
- angle_def "ACT <A>_v == ACT (A & ~ unchanged v)"
+ unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
+ square_def: "ACT [A]_v == ACT (A | unchanged v)"
+ angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)"
- enabled_def "s |= Enabled A == EX u. (s,u) |= A"
+ enabled_def: "s |= Enabled A == EX u. (s,u) |= A"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Buffer/Buffer.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: Buffer.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -8,11 +9,10 @@
(* ---------------------------- Data lemmas ---------------------------- *)
-(*FIXME: move to List.thy? Maybe as (tl xs = xs) = (xs = [])"?*)
+(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
Goal "xs ~= [] --> tl xs ~= xs";
by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
qed_spec_mp "tl_not_self";
-context Buffer.thy;
Addsimps [tl_not_self];
@@ -26,12 +26,12 @@
(* Enabling condition for dequeue -- NOT NEEDED *)
Goalw [temp_rewrite Deq_visible]
"!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])";
-by (force_tac (claset() addSEs [base_enabled,enabledE],
+by (force_tac (claset() addSEs [base_enabled,enabledE],
simpset() addsimps [Deq_def]) 1);
qed "Deq_enabled";
(* For the left-to-right implication, we don't need the base variable stuff *)
-Goalw [temp_rewrite Deq_visible]
+Goalw [temp_rewrite Deq_visible]
"|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])";
by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def]));
qed "Deq_enabledE";
--- a/src/HOL/TLA/Buffer/Buffer.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,15 +1,18 @@
(*
File: Buffer.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
Theory Name: Buffer
Logic Image: TLA
-
- A simple FIFO buffer (synchronous communication, interleaving)
*)
-Buffer = TLA +
+header {* A simple FIFO buffer (synchronous communication, interleaving) *}
+
+theory Buffer
+imports TLA
+begin
consts
(* actions *)
@@ -22,21 +25,21 @@
IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal"
Buffer :: "'a stfun => 'a stfun => temporal"
-rules
- BInit_def "BInit ic q oc == PRED q = #[]"
- Enq_def "Enq ic q oc == ACT (ic$ ~= $ic)
- & (q$ = $q @ [ ic$ ])
+defs
+ BInit_def: "BInit ic q oc == PRED q = #[]"
+ Enq_def: "Enq ic q oc == ACT (ic$ ~= $ic)
+ & (q$ = $q @ [ ic$ ])
& (oc$ = $oc)"
- Deq_def "Deq ic q oc == ACT ($q ~= #[])
+ Deq_def: "Deq ic q oc == ACT ($q ~= #[])
& (oc$ = hd< $q >)
& (q$ = tl< $q >)
& (ic$ = $ic)"
- Next_def "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)"
- IBuffer_def "IBuffer ic q oc == TEMP Init (BInit ic q oc)
+ Next_def: "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)"
+ IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc)
& [][Next ic q oc]_(ic,q,oc)
& WF(Deq ic q oc)_(ic,q,oc)"
- Buffer_def "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)"
-end
+ Buffer_def: "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)"
+ML {* use_legacy_bindings (the_context ()) *}
-
+end
--- a/src/HOL/TLA/Buffer/DBuffer.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: DBuffer.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -37,7 +38,7 @@
Goalw [action_rewrite DBDeq_visible]
"|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])";
-by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE]
+by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE]
addsimps2 [angle_def,DBDeq_def,Deq_def]) 1);
qed "DBDeq_enabled";
@@ -47,7 +48,7 @@
Goalw [action_rewrite DBPass_visible]
"|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])";
-by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE]
+by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE]
addsimps2 [angle_def,DBPass_def,Deq_def]) 1);
qed "DBPass_enabled";
@@ -103,7 +104,7 @@
(* High-level fairness *)
Goal "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) \
-\ & WF(DBDeq)_(inp,mid,out,q1,q2) \
+\ & WF(DBDeq)_(inp,mid,out,q1,q2) \
\ --> WF(Deq inp qc out)_(inp,qc,out)";
by (auto_tac (temp_css addSIs2 [leadsto_WF,
(temp_use DBFair_1) RSN(2,(temp_use LatticeTransitivity)),
--- a/src/HOL/TLA/Buffer/DBuffer.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,41 +1,53 @@
(*
File: DBuffer.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
Theory Name: DBuffer
Logic Image: TLA
-
- Two FIFO buffers in a row, with interleaving assumption.
*)
-DBuffer = Buffer +
+header {* Two FIFO buffers in a row, with interleaving assumption *}
+
+theory DBuffer
+imports Buffer
+begin
consts
(* implementation variables *)
- inp, mid, out :: nat stfun
- q1, q2, qc :: nat list stfun
+ inp :: "nat stfun"
+ mid :: "nat stfun"
+ out :: "nat stfun"
+ q1 :: "nat list stfun"
+ q2 :: "nat list stfun"
+ qc :: "nat list stfun"
- DBInit :: stpred
- DBEnq, DBDeq, DBPass, DBNext :: action
- DBuffer :: temporal
+ DBInit :: stpred
+ DBEnq :: action
+ DBDeq :: action
+ DBPass :: action
+ DBNext :: action
+ DBuffer :: temporal
-rules
- DB_base "basevars (inp,mid,out,q1,q2)"
+axioms
+ DB_base: "basevars (inp,mid,out,q1,q2)"
(* the concatenation of the two buffers *)
- qc_def "PRED qc == PRED (q2 @ q1)"
+ qc_def: "PRED qc == PRED (q2 @ q1)"
- DBInit_def "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)"
- DBEnq_def "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)"
- DBDeq_def "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)"
- DBPass_def "DBPass == ACT Deq inp q1 mid
+ DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)"
+ DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)"
+ DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)"
+ DBPass_def: "DBPass == ACT Deq inp q1 mid
& (q2$ = $q2 @ [ mid$ ])
& (out$ = $out)"
- DBNext_def "DBNext == ACT (DBEnq | DBDeq | DBPass)"
- DBuffer_def "DBuffer == TEMP Init DBInit
+ DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)"
+ DBuffer_def: "DBuffer == TEMP Init DBInit
& [][DBNext]_(inp,mid,out,q1,q2)
& WF(DBDeq)_(inp,mid,out,q1,q2)
& WF(DBPass)_(inp,mid,out,q1,q2)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
\ No newline at end of file
--- a/src/HOL/TLA/Buffer/ROOT.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/ROOT.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,2 +1,4 @@
+
+(* $Id$ *)
time_use_thy "DBuffer";
--- a/src/HOL/TLA/Inc/Inc.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/ex/inc/Inc.ML
+(*
+ File: TLA/ex/inc/Inc.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -77,7 +78,7 @@
(**** Proof of fairness ****)
(*
- The goal is to prove Fair_M1 far below, which asserts
+ The goal is to prove Fair_M1 far below, which asserts
|- Psi --> WF(M1)_(x,y)
(the other fairness condition is symmetrical).
@@ -111,7 +112,7 @@
by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
(* reduce |- []A --> <>Enabled B to |- A --> Enabled B *)
by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N1_enabled_at_g]
- addSDs2 [STL2_gen]
+ addSDs2 [STL2_gen]
addsimps2 [Init_def]));
qed "g1_leadsto_a1";
@@ -130,7 +131,7 @@
by (action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1);
by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N2_enabled_at_g]
- addSDs2 [STL2_gen]
+ addSDs2 [STL2_gen]
addsimps2 [Init_def]));
qed "g2_leadsto_a2";
@@ -165,7 +166,7 @@
Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) \
\ --> <>(pc2 = #a)";
by (auto_tac (Inc_css addsimps2 Init_defs
- addSIs2 [(temp_use N2_leadsto_a)
+ addSIs2 [(temp_use N2_leadsto_a)
RSN(2, (temp_use leadsto_init))]));
by (case_tac "pc2 (st1 sigma)" 1);
by Auto_tac;
@@ -189,7 +190,7 @@
by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
by (clarsimp_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_use DmdImpl)]) 1);
by (auto_tac (Inc_css addSIs2 [BoxDmd2_simple, N2_live]
- addsimps2 split_box_conj::more_temp_simps));
+ addsimps2 split_box_conj::more_temp_simps));
qed "a1_leadsto_b1";
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
@@ -201,14 +202,14 @@
by (rtac (temp_use LatticeReflexivity) 1);
by (rtac (temp_use LatticeTransitivity) 1);
by (auto_tac (Inc_css addSIs2 [a1_leadsto_b1,g1_leadsto_a1]
- addsimps2 [split_box_conj]));
+ addsimps2 [split_box_conj]));
qed "N1_leadsto_b";
Goal "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2)) \
\ & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2) \
\ --> <>(pc1 = #b)";
by (auto_tac (Inc_css addsimps2 Init_defs
- addSIs2 [(temp_use N1_leadsto_b)
+ addSIs2 [(temp_use N1_leadsto_b)
RSN(2, temp_use leadsto_init)]));
by (case_tac "pc1 (st1 sigma)" 1);
by Auto_tac;
@@ -233,11 +234,11 @@
by (force_tac (Inc_css addsimps2 angle_def::Psi_defs) 1);
by (force_tac (Inc_css addSEs2 [N1_enabled_at_b]) 1);
(* temporal premise: use previous lemmas and simple TL *)
-by (force_tac (Inc_css addSIs2 [DmdStable, N1_live,Stuck_at_b]
+by (force_tac (Inc_css addSIs2 [DmdStable, N1_live,Stuck_at_b]
addEs2 [STL4E] addsimps2 [square_def]) 1);
qed "Fair_M1_lemma";
Goal "|- Psi --> WF(M1)_(x,y)";
by (auto_tac (Inc_css addSIs2 [SFImplWF, Fair_M1_lemma, PsiInv]
- addsimps2 [Psi_def,split_box_conj]@more_temp_simps));
+ addsimps2 [Psi_def,split_box_conj]@more_temp_simps));
qed "Fair_M1";
--- a/src/HOL/TLA/Inc/Inc.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,69 +1,90 @@
-(*
+(*
File: TLA/Inc/Inc.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
Theory Name: Inc
- Logic Image: TLA
-
- Lamport's "increment" example.
+ Logic Image: TLA
*)
-Inc = TLA +
+header {* Lamport's "increment" example *}
+
+theory Inc
+imports TLA
+begin
(* program counter as an enumeration type *)
datatype pcount = a | b | g
consts
(* program variables *)
- x,y,sem :: nat stfun
- pc1,pc2 :: pcount stfun
+ x :: "nat stfun"
+ y :: "nat stfun"
+ sem :: "nat stfun"
+ pc1 :: "pcount stfun"
+ pc2 :: "pcount stfun"
(* names of actions and predicates *)
- M1,M2,N1,N2 :: action
- alpha1,alpha2,beta1,beta2,gamma1,gamma2 :: action
- InitPhi, InitPsi :: stpred
- PsiInv,PsiInv1,PsiInv2,PsiInv3 :: stpred
+ M1 :: action
+ M2 :: action
+ N1 :: action
+ N2 :: action
+ alpha1 :: action
+ alpha2 :: action
+ beta1 :: action
+ beta2 :: action
+ gamma1 :: action
+ gamma2 :: action
+ InitPhi :: stpred
+ InitPsi :: stpred
+ PsiInv :: stpred
+ PsiInv1 :: stpred
+ PsiInv2 :: stpred
+ PsiInv3 :: stpred
(* temporal formulas *)
- Phi, Psi :: temporal
-
-rules
+ Phi :: temporal
+ Psi :: temporal
+
+axioms
(* the "base" variables, required to compute enabledness predicates *)
- Inc_base "basevars (x, y, sem, pc1, pc2)"
+ Inc_base: "basevars (x, y, sem, pc1, pc2)"
(* definitions for high-level program *)
- InitPhi_def "InitPhi == PRED x = # 0 & y = # 0"
- M1_def "M1 == ACT x$ = Suc<$x> & y$ = $y"
- M2_def "M2 == ACT y$ = Suc<$y> & x$ = $x"
- Phi_def "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
+ InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0"
+ M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y"
+ M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x"
+ Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
& WF(M1)_(x,y) & WF(M2)_(x,y)"
(* definitions for low-level program *)
- InitPsi_def "InitPsi == PRED pc1 = #a & pc2 = #a
+ InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a
& x = # 0 & y = # 0 & sem = # 1"
- alpha1_def "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
+ alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
& unchanged(x,y,pc2)"
- alpha2_def "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
+ alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
& unchanged(x,y,pc1)"
- beta1_def "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
+ beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
& unchanged(y,sem,pc2)"
- beta2_def "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
+ beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
& unchanged(x,sem,pc1)"
- gamma1_def "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
+ gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
& unchanged(x,y,pc2)"
- gamma2_def "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
+ gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
& unchanged(x,y,pc1)"
- N1_def "N1 == ACT (alpha1 | beta1 | gamma1)"
- N2_def "N2 == ACT (alpha2 | beta2 | gamma2)"
- Psi_def "Psi == TEMP Init InitPsi
+ N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)"
+ N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)"
+ Psi_def: "Psi == TEMP Init InitPsi
& [][N1 | N2]_(x,y,sem,pc1,pc2)
& SF(N1)_(x,y,sem,pc1,pc2)
& SF(N2)_(x,y,sem,pc1,pc2)"
- PsiInv1_def "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a"
- PsiInv2_def "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
- PsiInv3_def "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
- PsiInv_def "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
-
+ PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a"
+ PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
+ PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
+ PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Inc/Pcount.thy Wed Sep 07 20:22:15 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*
- File: TLA/ex/inc/Pcount.thy
- Author: Stephan Merz
- Copyright: 1997 University of Munich
-
- Theory Name: Pcount
- Logic Image: TLA
-
-Data type "program counter" for the increment example.
-Isabelle/HOL's datatype package generates useful simplifications
-and case distinction tactics.
-*)
-
-Pcount = Main +
-
-datatype pcount = a | b | g
-
-end
--- a/src/HOL/TLA/Inc/ROOT.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Inc/ROOT.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,3 +1,4 @@
-time_use_thy "Pcount";
+(* $Id$ *)
+
time_use_thy "Inc";
--- a/src/HOL/TLA/Init.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Init.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,8 @@
+
+(* $Id$ *)
+
local
- fun prover s = prove_goal Init.thy s
+ fun prover s = prove_goal (the_context ()) s
(K [force_tac (claset(), simpset() addsimps [Init_def]) 1])
in
val const_simps = map (int_rewrite o prover)
@@ -40,4 +43,3 @@
qed "Init_act";
val Init_defs = [Init_stp, Init_act, int_use Init_temp];
-
--- a/src/HOL/TLA/Init.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Init.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/Init.thy
+(*
+ File: TLA/Init.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -10,26 +11,26 @@
temporal formulas and its "subformulas" (state predicates and actions).
*)
-Init = Action +
+theory Init
+imports Action
+begin
+
+typedecl behavior
+instance behavior :: world ..
types
- behavior
- temporal = behavior form
+ temporal = "behavior form"
-arities
- behavior :: type
-
-instance
- behavior :: world
consts
- Initial :: ('w::world => bool) => temporal
- first_world :: behavior => ('w::world)
- st1, st2 :: behavior => state
+ Initial :: "('w::world => bool) => temporal"
+ first_world :: "behavior => ('w::world)"
+ st1 :: "behavior => state"
+ st2 :: "behavior => state"
syntax
- TEMP :: lift => 'a ("(TEMP _)")
- "_Init" :: lift => lift ("(Init _)"[40] 50)
+ TEMP :: "lift => 'a" ("(TEMP _)")
+ "_Init" :: "lift => lift" ("(Init _)"[40] 50)
translations
"TEMP F" => "(F::behavior => _)"
@@ -37,8 +38,11 @@
"sigma |= Init F" <= "_Init F sigma"
defs
- Init_def "sigma |= Init F == (first_world sigma) |= F"
- fw_temp_def "first_world == %sigma. sigma"
- fw_stp_def "first_world == st1"
- fw_act_def "first_world == %sigma. (st1 sigma, st2 sigma)"
+ Init_def: "sigma |= Init F == (first_world sigma) |= F"
+ fw_temp_def: "first_world == %sigma. sigma"
+ fw_stp_def: "first_world == st1"
+ fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Intensional.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Intensional.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: Intensional.ML
+(*
+ File: Intensional.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -14,7 +15,7 @@
by (etac spec 1);
qed "inteq_reflection";
-val [prem] = goalw thy [Valid_def] "(!!w. w |= A) ==> |- A";
+val [prem] = goalw (the_context ()) [Valid_def] "(!!w. w |= A) ==> |- A";
by (REPEAT (resolve_tac [allI,prem] 1));
qed "intI";
@@ -25,8 +26,8 @@
(** Lift usual HOL simplifications to "intensional" level. **)
local
-fun prover s = (prove_goal Intensional.thy s
- (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews),
+fun prover s = (prove_goal (the_context ()) s
+ (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews),
blast_tac HOL_cs 1])) RS inteq_reflection
in
@@ -34,19 +35,19 @@
val int_simps = map prover
[ "|- (x=x) = #True",
"|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P",
- "|- ((~P) = P) = #False", "|- (P = (~P)) = #False",
+ "|- ((~P) = P) = #False", "|- (P = (~P)) = #False",
"|- (P ~= Q) = (P = (~Q))",
"|- (#True=P) = P", "|- (P=#True) = P",
- "|- (#True --> P) = P", "|- (#False --> P) = #True",
+ "|- (#True --> P) = P", "|- (#False --> P) = #True",
"|- (P --> #True) = #True", "|- (P --> P) = #True",
"|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)",
- "|- (P & #True) = P", "|- (#True & P) = P",
- "|- (P & #False) = #False", "|- (#False & P) = #False",
+ "|- (P & #True) = P", "|- (#True & P) = P",
+ "|- (P & #False) = #False", "|- (#False & P) = #False",
"|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False",
- "|- (P | #True) = #True", "|- (#True | P) = #True",
- "|- (P | #False) = P", "|- (#False | P) = P",
+ "|- (P | #True) = #True", "|- (#True | P) = #True",
+ "|- (P | #False) = P", "|- (#False | P) = P",
"|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True",
- "|- (! x. P) = P", "|- (? x. P) = P",
+ "|- (! x. P) = P", "|- (? x. P) = P",
"|- (~Q --> ~P) = (P --> Q)",
"|- (P|Q --> R) = ((P-->R)&(Q-->R))" ]
end;
@@ -72,7 +73,7 @@
rewrite_rule intensional_rews ((th RS intD) handle _ => th);
(* Turn |- F = G into meta-level rewrite rule F == G *)
-fun int_rewrite th =
+fun int_rewrite th =
zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection));
(* flattening turns "-->" into "==>" and eliminates conjunctions in the
@@ -85,18 +86,18 @@
unification, therefore the code is a little awkward.
*)
fun flatten t =
- let
+ let
(* analogous to RS, but using matching instead of resolution *)
fun matchres tha i thb =
case Seq.chop (2, biresolution true [(false,tha)] i thb) of
- ([th],_) => th
- | ([],_) => raise THM("matchres: no match", i, [tha,thb])
- | _ => raise THM("matchres: multiple unifiers", i, [tha,thb])
+ ([th],_) => th
+ | ([],_) => raise THM("matchres: no match", i, [tha,thb])
+ | _ => raise THM("matchres: multiple unifiers", i, [tha,thb])
(* match tha with some premise of thb *)
fun matchsome tha thb =
let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
- | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
+ | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
in hmatch (nprems_of thb) end
fun hflatten t =
@@ -122,4 +123,3 @@
Goalw [Valid_def] "|- (~ (? x. F x)) = (! x. ~ F x)";
by (Simp_tac 1);
qed "Not_Rex";
-
--- a/src/HOL/TLA/Intensional.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Intensional.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/Intensional.thy
+(*
+ File: TLA/Intensional.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -10,7 +11,9 @@
on top of HOL, with lifting of constants and functions.
*)
-Intensional = Main +
+theory Intensional
+imports Main
+begin
axclass
world < type
@@ -18,15 +21,15 @@
(** abstract syntax **)
types
- ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::type *)
- 'w form = ('w, bool) expr
+ ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *)
+ 'w form = "('w, bool) expr"
consts
- Valid :: ('w::world) form => bool
- const :: 'a => ('w::world, 'a) expr
- lift :: ['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr
- lift2 :: ['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr
- lift3 :: ['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr
+ Valid :: "('w::world) form => bool"
+ const :: "'a => ('w::world, 'a) expr"
+ lift :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr"
+ lift2 :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr"
+ lift3 :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr"
(* "Rigid" quantification (logic level) *)
RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10)
@@ -40,59 +43,59 @@
liftargs
syntax
- "" :: id => lift ("_")
- "" :: longid => lift ("_")
- "" :: var => lift ("_")
- "_applC" :: [lift, cargs] => lift ("(1_/ _)" [1000, 1000] 999)
- "" :: lift => lift ("'(_')")
- "_lambda" :: [idts, 'a] => lift ("(3%_./ _)" [0, 3] 3)
- "_constrain" :: [lift, type] => lift ("(_::_)" [4, 0] 3)
- "" :: lift => liftargs ("_")
- "_liftargs" :: [lift, liftargs] => liftargs ("_,/ _")
- "_Valid" :: lift => bool ("(|- _)" 5)
- "_holdsAt" :: ['a, lift] => bool ("(_ |= _)" [100,10] 10)
+ "" :: "id => lift" ("_")
+ "" :: "longid => lift" ("_")
+ "" :: "var => lift" ("_")
+ "_applC" :: "[lift, cargs] => lift" ("(1_/ _)" [1000, 1000] 999)
+ "" :: "lift => lift" ("'(_')")
+ "_lambda" :: "[idts, 'a] => lift" ("(3%_./ _)" [0, 3] 3)
+ "_constrain" :: "[lift, type] => lift" ("(_::_)" [4, 0] 3)
+ "" :: "lift => liftargs" ("_")
+ "_liftargs" :: "[lift, liftargs] => liftargs" ("_,/ _")
+ "_Valid" :: "lift => bool" ("(|- _)" 5)
+ "_holdsAt" :: "['a, lift] => bool" ("(_ |= _)" [100,10] 10)
(* Syntax for lifted expressions outside the scope of |- or |= *)
- "LIFT" :: lift => 'a ("LIFT _")
+ "LIFT" :: "lift => 'a" ("LIFT _")
(* generic syntax for lifted constants and functions *)
- "_const" :: 'a => lift ("(#_)" [1000] 999)
- "_lift" :: ['a, lift] => lift ("(_<_>)" [1000] 999)
- "_lift2" :: ['a, lift, lift] => lift ("(_<_,/ _>)" [1000] 999)
- "_lift3" :: ['a, lift, lift, lift] => lift ("(_<_,/ _,/ _>)" [1000] 999)
+ "_const" :: "'a => lift" ("(#_)" [1000] 999)
+ "_lift" :: "['a, lift] => lift" ("(_<_>)" [1000] 999)
+ "_lift2" :: "['a, lift, lift] => lift" ("(_<_,/ _>)" [1000] 999)
+ "_lift3" :: "['a, lift, lift, lift] => lift" ("(_<_,/ _,/ _>)" [1000] 999)
(* concrete syntax for common infix functions: reuse same symbol *)
- "_liftEqu" :: [lift, lift] => lift ("(_ =/ _)" [50,51] 50)
- "_liftNeq" :: [lift, lift] => lift ("(_ ~=/ _)" [50,51] 50)
- "_liftNot" :: lift => lift ("(~ _)" [40] 40)
- "_liftAnd" :: [lift, lift] => lift ("(_ &/ _)" [36,35] 35)
- "_liftOr" :: [lift, lift] => lift ("(_ |/ _)" [31,30] 30)
- "_liftImp" :: [lift, lift] => lift ("(_ -->/ _)" [26,25] 25)
- "_liftIf" :: [lift, lift, lift] => lift ("(if (_)/ then (_)/ else (_))" 10)
- "_liftPlus" :: [lift, lift] => lift ("(_ +/ _)" [66,65] 65)
- "_liftMinus" :: [lift, lift] => lift ("(_ -/ _)" [66,65] 65)
- "_liftTimes" :: [lift, lift] => lift ("(_ */ _)" [71,70] 70)
- "_liftDiv" :: [lift, lift] => lift ("(_ div _)" [71,70] 70)
- "_liftMod" :: [lift, lift] => lift ("(_ mod _)" [71,70] 70)
- "_liftLess" :: [lift, lift] => lift ("(_/ < _)" [50, 51] 50)
- "_liftLeq" :: [lift, lift] => lift ("(_/ <= _)" [50, 51] 50)
- "_liftMem" :: [lift, lift] => lift ("(_/ : _)" [50, 51] 50)
- "_liftNotMem" :: [lift, lift] => lift ("(_/ ~: _)" [50, 51] 50)
- "_liftFinset" :: liftargs => lift ("{(_)}")
+ "_liftEqu" :: "[lift, lift] => lift" ("(_ =/ _)" [50,51] 50)
+ "_liftNeq" :: "[lift, lift] => lift" ("(_ ~=/ _)" [50,51] 50)
+ "_liftNot" :: "lift => lift" ("(~ _)" [40] 40)
+ "_liftAnd" :: "[lift, lift] => lift" ("(_ &/ _)" [36,35] 35)
+ "_liftOr" :: "[lift, lift] => lift" ("(_ |/ _)" [31,30] 30)
+ "_liftImp" :: "[lift, lift] => lift" ("(_ -->/ _)" [26,25] 25)
+ "_liftIf" :: "[lift, lift, lift] => lift" ("(if (_)/ then (_)/ else (_))" 10)
+ "_liftPlus" :: "[lift, lift] => lift" ("(_ +/ _)" [66,65] 65)
+ "_liftMinus" :: "[lift, lift] => lift" ("(_ -/ _)" [66,65] 65)
+ "_liftTimes" :: "[lift, lift] => lift" ("(_ */ _)" [71,70] 70)
+ "_liftDiv" :: "[lift, lift] => lift" ("(_ div _)" [71,70] 70)
+ "_liftMod" :: "[lift, lift] => lift" ("(_ mod _)" [71,70] 70)
+ "_liftLess" :: "[lift, lift] => lift" ("(_/ < _)" [50, 51] 50)
+ "_liftLeq" :: "[lift, lift] => lift" ("(_/ <= _)" [50, 51] 50)
+ "_liftMem" :: "[lift, lift] => lift" ("(_/ : _)" [50, 51] 50)
+ "_liftNotMem" :: "[lift, lift] => lift" ("(_/ ~: _)" [50, 51] 50)
+ "_liftFinset" :: "liftargs => lift" ("{(_)}")
(** TODO: syntax for lifted collection / comprehension **)
- "_liftPair" :: [lift,liftargs] => lift ("(1'(_,/ _'))")
+ "_liftPair" :: "[lift,liftargs] => lift" ("(1'(_,/ _'))")
(* infix syntax for list operations *)
- "_liftCons" :: [lift, lift] => lift ("(_ #/ _)" [65,66] 65)
- "_liftApp" :: [lift, lift] => lift ("(_ @/ _)" [65,66] 65)
- "_liftList" :: liftargs => lift ("[(_)]")
+ "_liftCons" :: "[lift, lift] => lift" ("(_ #/ _)" [65,66] 65)
+ "_liftApp" :: "[lift, lift] => lift" ("(_ @/ _)" [65,66] 65)
+ "_liftList" :: "liftargs => lift" ("[(_)]")
(* Rigid quantification (syntax level) *)
- "_ARAll" :: [idts, lift] => lift ("(3! _./ _)" [0, 10] 10)
- "_AREx" :: [idts, lift] => lift ("(3? _./ _)" [0, 10] 10)
- "_AREx1" :: [idts, lift] => lift ("(3?! _./ _)" [0, 10] 10)
- "_RAll" :: [idts, lift] => lift ("(3ALL _./ _)" [0, 10] 10)
- "_REx" :: [idts, lift] => lift ("(3EX _./ _)" [0, 10] 10)
- "_REx1" :: [idts, lift] => lift ("(3EX! _./ _)" [0, 10] 10)
+ "_ARAll" :: "[idts, lift] => lift" ("(3! _./ _)" [0, 10] 10)
+ "_AREx" :: "[idts, lift] => lift" ("(3? _./ _)" [0, 10] 10)
+ "_AREx1" :: "[idts, lift] => lift" ("(3?! _./ _)" [0, 10] 10)
+ "_RAll" :: "[idts, lift] => lift" ("(3ALL _./ _)" [0, 10] 10)
+ "_REx" :: "[idts, lift] => lift" ("(3EX _./ _)" [0, 10] 10)
+ "_REx1" :: "[idts, lift] => lift" ("(3EX! _./ _)" [0, 10] 10)
translations
"_const" == "const"
@@ -135,7 +138,7 @@
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)"
"_liftList x" == "_liftCons x (_const [])"
-
+
"w |= ~A" <= "_liftNot A w"
"w |= A & B" <= "_liftAnd A B w"
@@ -147,41 +150,44 @@
"w |= EX! x. A" <= "_REx1 x A w"
syntax (xsymbols)
- "_Valid" :: lift => bool ("(\\<turnstile> _)" 5)
- "_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10)
- "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50)
- "_liftNot" :: lift => lift ("\\<not> _" [40] 40)
- "_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35)
- "_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30)
- "_liftImp" :: [lift, lift] => lift (infixr "\\<longrightarrow>" 25)
- "_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10)
- "_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10)
- "_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10)
- "_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50)
- "_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50)
- "_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50)
+ "_Valid" :: "lift => bool" ("(\<turnstile> _)" 5)
+ "_holdsAt" :: "['a, lift] => bool" ("(_ \<Turnstile> _)" [100,10] 10)
+ "_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50)
+ "_liftNot" :: "lift => lift" ("\<not> _" [40] 40)
+ "_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35)
+ "_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30)
+ "_liftImp" :: "[lift, lift] => lift" (infixr "\<longrightarrow>" 25)
+ "_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10)
+ "_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10)
+ "_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50)
+ "_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50)
+ "_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50)
syntax (HTML output)
- "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50)
- "_liftNot" :: lift => lift ("\\<not> _" [40] 40)
- "_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35)
- "_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30)
- "_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10)
- "_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10)
- "_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10)
- "_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50)
- "_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50)
- "_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50)
+ "_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50)
+ "_liftNot" :: "lift => lift" ("\<not> _" [40] 40)
+ "_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35)
+ "_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30)
+ "_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10)
+ "_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10)
+ "_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50)
+ "_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50)
+ "_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50)
-rules
- Valid_def "|- A == ALL w. w |= A"
+axioms
+ Valid_def: "|- A == ALL w. w |= A"
+
+ unl_con: "LIFT #c w == c"
+ unl_lift: "LIFT f<x> w == f (x w)"
+ unl_lift2: "LIFT f<x, y> w == f (x w) (y w)"
+ unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
- unl_con "LIFT #c w == c"
- unl_lift "LIFT f<x> w == f (x w)"
- unl_lift2 "LIFT f<x, y> w == f (x w) (y w)"
- unl_lift3 "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
+ unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)"
+ unl_Rex: "w |= EX x. A x == EX x. (w |= A x)"
+ unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)"
- unl_Rall "w |= ALL x. A x == ALL x. (w |= A x)"
- unl_Rex "w |= EX x. A x == EX x. (w |= A x)"
- unl_Rex1 "w |= EX! x. A x == EX! x. (w |= A x)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Memory/MIParameters.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MIParameters.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MIParameters.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -13,4 +14,6 @@
datatype histState = histA | histB
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Memory/MIsafe.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MIsafe.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MIsafe.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
--- a/src/HOL/TLA/Memory/MemClerk.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,12 +1,13 @@
-(*
+(*
File: MemClerk.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
RPC-Memory example: Memory clerk specification (theorems and proofs)
*)
-val MC_action_defs =
+val MC_action_defs =
[MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
@@ -41,7 +42,7 @@
Goal "|- MClkReply send rcv cst p --> \
\ <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)";
by (auto_tac (mem_css addsimps2 [angle_def,MClkReply_def]
- addEs2 [Return_changed]));
+ addEs2 [Return_changed]));
qed "MClkReply_change";
Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \
--- a/src/HOL/TLA/Memory/MemClerk.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MemClerk.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,7 +10,9 @@
RPC-Memory example: specification of the memory clerk.
*)
-MemClerk = Memory + RPC + MemClerkParameters +
+theory MemClerk
+imports Memory RPC MemClerkParameters
+begin
types
(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
@@ -64,4 +67,6 @@
MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
"MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Memory/MemClerkParameters.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: MemClerkParameters.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -8,5 +9,4 @@
(*
val CP_simps = RP_simps @ mClkState.simps;
-
*)
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MemClerkParameters.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,9 +10,11 @@
RPC-Memory example: Parameters of the memory clerk.
*)
-MemClerkParameters = RPCParameters +
+theory MemClerkParameters
+imports RPCParameters
+begin
-datatype mClkState = clkA | clkB
+datatype mClkState = clkA | clkB
types
(* types sent on the clerk's send and receive channels are argument types
@@ -27,4 +30,6 @@
MClkReplyVal :: "Vals => Vals"
"MClkReplyVal v == if v = RPCFailure then MemFailure else v"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Memory/Memory.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,12 +1,13 @@
-(*
+(*
File: Memory.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
RPC-Memory example: Memory specification (theorems and proofs)
*)
-val RM_action_defs =
+val RM_action_defs =
[MInit_def, PInit_def, RdRequest_def, WrRequest_def, MemInv_def,
GoodRead_def, BadRead_def, ReadInner_def, Read_def,
GoodWrite_def, BadWrite_def, WriteInner_def, Write_def,
@@ -24,7 +25,7 @@
(* The reliable memory is an implementation of the unreliable one *)
Goal "|- IRSpec ch mm rs --> IUSpec ch mm rs";
by (force_tac (temp_css addsimps2 ([UNext_def,UPSpec_def,IUSpec_def] @ RM_temp_defs)
- addSEs2 [STL4E,squareE]) 1);
+ addSEs2 [STL4E,squareE]) 1);
qed "ReliableImplementsUnReliable";
(* The memory spec implies the memory invariant *)
@@ -43,7 +44,7 @@
by (auto_tac (temp_css addSEs2 [MemoryInvariant,NonMemLocInvariant]));
qed "MemoryInvariantAll";
-(* The memory engages in an action for process p only if there is an
+(* The memory engages in an action for process p only if there is an
unanswered call from p.
We need this only for the reliable memory.
*)
@@ -79,14 +80,14 @@
\ |- Calling ch p & (arg<ch!p> = #(write l v)) \
\ --> Enabled (WriteInner ch mm rs p l v)";
by (case_tac "l:MemLoc & v:MemVal" 1);
-by (ALLGOALS
+by (ALLGOALS
(force_tac (mem_css addsimps2 [WriteInner_def,GoodWrite_def,
BadWrite_def,WrRequest_def]
addSIs2 [exI] addSEs2 [base_enabled])));
qed "WriteInner_enabled";
Goal "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult";
-by (force_tac (mem_css addsimps2
+by (force_tac (mem_css addsimps2
[Read_def,ReadInner_def,GoodRead_def,BadRead_def,MemInv_def]) 1);
qed "ReadResult";
@@ -103,8 +104,8 @@
\ & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l)) \
\ --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))";
by (force_tac (mem_css addsimps2 [RNext_def,angle_def]
- addSEs2 [enabled_mono2]
- addDs2 [ReadResult, WriteResult]) 1);
+ addSEs2 [enabled_mono2]
+ addDs2 [ReadResult, WriteResult]) 1);
qed "RWRNext_enabled";
@@ -121,5 +122,5 @@
by (force_tac (mem_css addDs2 [base_pair]) 1);
by (etac contrapos_np 1);
by (action_simp_tac (simpset() addsimps [Write_def,enabled_ex])
- [WriteInner_enabled,exI] [] 1);
+ [WriteInner_enabled,exI] [] 1);
qed "RNext_enabled";
--- a/src/HOL/TLA/Memory/Memory.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: Memory.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,7 +10,9 @@
RPC-Memory example: Memory specification
*)
-Memory = MemoryParameters + ProcedureInterface +
+theory Memory
+imports MemoryParameters ProcedureInterface
+begin
types
memChType = "(memOp, Vals) channel"
@@ -50,86 +53,89 @@
USpec :: "memChType => temporal"
(* memory invariant: in the paper, the invariant is hidden in the definition of
- the predicate S used in the implementation proof, but it is easier to verify
+ the predicate S used in the implementation proof, but it is easier to verify
at this level. *)
MemInv :: "memType => Locs => stpred"
-rules
- MInit_def "MInit mm l == PRED mm!l = #InitVal"
- PInit_def "PInit rs p == PRED rs!p = #NotAResult"
+defs
+ MInit_def: "MInit mm l == PRED mm!l = #InitVal"
+ PInit_def: "PInit rs p == PRED rs!p = #NotAResult"
- RdRequest_def "RdRequest ch p l == PRED
+ RdRequest_def: "RdRequest ch p l == PRED
Calling ch p & (arg<ch!p> = #(read l))"
- WrRequest_def "WrRequest ch p l v == PRED
+ WrRequest_def: "WrRequest ch p l v == PRED
Calling ch p & (arg<ch!p> = #(write l v))"
(* a read that doesn't raise BadArg *)
- GoodRead_def "GoodRead mm rs p l == ACT
+ GoodRead_def: "GoodRead mm rs p l == ACT
#l : #MemLoc & ((rs!p)$ = $(mm!l))"
(* a read that raises BadArg *)
- BadRead_def "BadRead mm rs p l == ACT
+ BadRead_def: "BadRead mm rs p l == ACT
#l ~: #MemLoc & ((rs!p)$ = #BadArg)"
(* the read action with l visible *)
- ReadInner_def "ReadInner ch mm rs p l == ACT
+ ReadInner_def: "ReadInner ch mm rs p l == ACT
$(RdRequest ch p l)
& (GoodRead mm rs p l | BadRead mm rs p l)
& unchanged (rtrner ch ! p)"
(* the read action with l quantified *)
- Read_def "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
+ Read_def: "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
(* similar definitions for the write action *)
- GoodWrite_def "GoodWrite mm rs p l v == ACT
+ GoodWrite_def: "GoodWrite mm rs p l v == ACT
#l : #MemLoc & #v : #MemVal
& ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
- BadWrite_def "BadWrite mm rs p l v == ACT
+ BadWrite_def: "BadWrite mm rs p l v == ACT
~ (#l : #MemLoc & #v : #MemVal)
& ((rs!p)$ = #BadArg) & unchanged (mm!l)"
- WriteInner_def "WriteInner ch mm rs p l v == ACT
+ WriteInner_def: "WriteInner ch mm rs p l v == ACT
$(WrRequest ch p l v)
& (GoodWrite mm rs p l v | BadWrite mm rs p l v)
& unchanged (rtrner ch ! p)"
- Write_def "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
+ Write_def: "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
(* the return action *)
- MemReturn_def "MemReturn ch rs p == ACT
+ MemReturn_def: "MemReturn ch rs p == ACT
( ($(rs!p) ~= #NotAResult)
& ((rs!p)$ = #NotAResult)
& Return ch p (rs!p))"
(* the failure action of the unreliable memory *)
- MemFail_def "MemFail ch rs p == ACT
+ MemFail_def: "MemFail ch rs p == ACT
$(Calling ch p)
& ((rs!p)$ = #MemFailure)
& unchanged (rtrner ch ! p)"
(* next-state relations for reliable / unreliable memory *)
- RNext_def "RNext ch mm rs p == ACT
+ RNext_def: "RNext ch mm rs p == ACT
( Read ch mm rs p
| (EX l. Write ch mm rs p l)
| MemReturn ch rs p)"
- UNext_def "UNext ch mm rs p == ACT
+ UNext_def: "UNext ch mm rs p == ACT
(RNext ch mm rs p | MemFail ch rs p)"
- RPSpec_def "RPSpec ch mm rs p == TEMP
+ RPSpec_def: "RPSpec ch mm rs p == TEMP
Init(PInit rs p)
& [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
& WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
& WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
- UPSpec_def "UPSpec ch mm rs p == TEMP
+ UPSpec_def: "UPSpec ch mm rs p == TEMP
Init(PInit rs p)
& [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
& WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
& WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
- MSpec_def "MSpec ch mm rs l == TEMP
+ MSpec_def: "MSpec ch mm rs l == TEMP
Init(MInit mm l)
& [][ EX p. Write ch mm rs p l ]_(mm!l)"
- IRSpec_def "IRSpec ch mm rs == TEMP
+ IRSpec_def: "IRSpec ch mm rs == TEMP
(ALL p. RPSpec ch mm rs p)
& (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
- IUSpec_def "IUSpec ch mm rs == TEMP
+ IUSpec_def: "IUSpec ch mm rs == TEMP
(ALL p. UPSpec ch mm rs p)
& (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
- RSpec_def "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
- USpec_def "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
+ RSpec_def: "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
+ USpec_def: "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
- MemInv_def "MemInv mm l == PRED #l : #MemLoc --> mm!l : #MemVal"
+ MemInv_def: "MemInv mm l == PRED #l : #MemLoc --> mm!l : #MemVal"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: MemoryImplementation.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -25,7 +26,7 @@
(but it can be a lot faster than MI_css)
*)
val MI_fast_css =
- let
+ let
val (cs,ss) = MI_css
in
(cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
@@ -40,8 +41,8 @@
\ --> (EEX rmhist. Init(ALL p. HInit rmhist p) \
\ & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))";
by (Clarsimp_tac 1);
-by (rtac historyI 1);
-by (TRYALL atac);
+by (rtac historyI 1);
+by (TRYALL atac);
by (rtac MI_base 1);
by (action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1);
by (etac fun_cong 1);
@@ -52,7 +53,7 @@
Goal "|- Implementation --> (EEX rmhist. Hist rmhist)";
by (Clarsimp_tac 1);
by (rtac ((temp_use HistoryLemma) RS eex_mono) 1);
-by (force_tac (MI_css
+by (force_tac (MI_css
addsimps2 [Hist_def,HistP_def,Init_def,all_box,split_box_conj]) 3);
by (auto_tac (MI_css
addsimps2 [Implementation_def,MClkISpec_def,RPCISpec_def,IRSpec_def,
@@ -77,7 +78,7 @@
Goal "|- ImpInit p & HInit rmhist p --> S1 rmhist p";
by (auto_tac (MI_fast_css
addsimps2 [MVNROKBA_def,MClkInit_def,RPCInit_def,PInit_def,
- HInit_def,ImpInit_def,S_def,S1_def]));
+ HInit_def,ImpInit_def,S_def,S1_def]));
qed "Step1_1";
(* ========== Step 1.2 ================================================== *)
@@ -105,8 +106,8 @@
\ --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) \
\ | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))";
by (action_simp_tac (simpset() addsimps [ImpNext_def]) []
- (map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1);
-by (action_simp_tac (simpset()) []
+ (map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1);
+by (action_simp_tac (simpset()) []
(squareE::map temp_elim [S3RPC,S3Forward,S3Fail]) 1);
by (auto_tac (MI_css addDs2 [S3Hist]));
qed "Step1_2_3";
@@ -181,7 +182,7 @@
\ --> unchanged (rtrner memCh!p, resbar rmhist!p)";
by (Clarsimp_tac 1);
by (REPEAT (dresolve_tac (map temp_use [S3_excl,S4_excl]) 1));
-by (action_simp_tac
+by (action_simp_tac
(simpset() addsimps [e_def,c_def,m_def,resbar_def,S_def, S3_def]) [] [] 1);
qed "Step1_4_3a";
@@ -191,7 +192,7 @@
by (Clarsimp_tac 1);
by (dtac (temp_use S6_excl) 1);
by (auto_tac (MI_css addsimps2 [RPCFail_def,MemFail_def,e_def,c_def,m_def,
- resbar_def]));
+ resbar_def]));
by (force_tac (MI_css addsimps2 [S3_def,S_def]) 1);
by (auto_tac (MI_css addsimps2 [Return_def]));
qed "Step1_4_3b";
@@ -201,14 +202,14 @@
\ --> ReadInner memCh mm (resbar rmhist) p l";
by (Clarsimp_tac 1);
by (REPEAT (dtac (temp_use S4_excl) 1));
-by (action_simp_tac
- (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def])
+by (action_simp_tac
+ (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def])
[] [] 1);
by (auto_tac (MI_css addsimps2 [resbar_def]));
-by (ALLGOALS (action_simp_tac
+by (ALLGOALS (action_simp_tac
(simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
- S_def,S4_def,RdRequest_def,MemInv_def])
- [] [impE,MemValNotAResultE]));
+ S_def,S4_def,RdRequest_def,MemInv_def])
+ [] [impE,MemValNotAResultE]));
qed "Step1_4_4a1";
Goal "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ \
@@ -222,15 +223,15 @@
\ --> WriteInner memCh mm (resbar rmhist) p l v";
by (Clarsimp_tac 1);
by (REPEAT (dtac (temp_use S4_excl) 1));
-by (action_simp_tac
+by (action_simp_tac
(simpset() addsimps [WriteInner_def, GoodWrite_def, BadWrite_def,
- e_def, c_def, m_def])
+ e_def, c_def, m_def])
[] [] 1);
by (auto_tac (MI_css addsimps2 [resbar_def]));
by (ALLGOALS (action_simp_tac
(simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
- S_def,S4_def,WrRequest_def])
- [] []));
+ S_def,S4_def,WrRequest_def])
+ [] []));
qed "Step1_4_4b1";
Goal "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$ \
@@ -254,7 +255,7 @@
by (Clarsimp_tac 1);
by (REPEAT (dresolve_tac [temp_use S5_excl, temp_use S6_excl] 1));
by (auto_tac (MI_css addsimps2 [e_def,c_def,m_def, resbar_def]));
-by (auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def]
+by (auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def]
addSDs2 [MVOKBAnotRF]));
qed "Step1_4_5a";
@@ -264,7 +265,7 @@
by (Clarsimp_tac 1);
by (dtac (temp_use S6_excl) 1);
by (auto_tac (MI_css addsimps2 [e_def, c_def, m_def, RPCFail_def, Return_def,
- MemFail_def, resbar_def]));
+ MemFail_def, resbar_def]));
by (auto_tac (MI_css addsimps2 [S5_def,S_def]));
qed "Step1_4_5b";
@@ -275,11 +276,11 @@
by (dtac (temp_use S6_excl) 1);
by (action_simp_tac
(simpset() addsimps [e_def,r_def,m_def,MClkReply_def,MemReturn_def,
- Return_def,resbar_def]) [] [] 1);
+ Return_def,resbar_def]) [] [] 1);
by (ALLGOALS Asm_full_simp_tac); (* simplify if-then-else *)
by (ALLGOALS (action_simp_tac
(simpset() addsimps [MClkReplyVal_def,S6_def,S_def])
- [] [MVOKBARFnotNR]));
+ [] [MVOKBARFnotNR]));
qed "Step1_4_6a";
Goal "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$ \
@@ -296,7 +297,7 @@
Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \
\ --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)";
by (auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,caller_def,rtrner_def,
- S_def,Calling_def]));
+ S_def,Calling_def]));
qed "S_lemma";
Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \
@@ -322,13 +323,13 @@
(* Frequently needed abbreviation: distinguish between idling and non-idling
steps of the implementation, and try to solve the idling case by simplification
*)
-fun split_idle_tac simps i =
+fun split_idle_tac simps i =
EVERY [TRY (rtac actionI i),
- case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
- rewrite_goals_tac action_rews,
- forward_tac [temp_use Step1_4_7] i,
- asm_full_simp_tac (simpset() addsimps simps) i
- ];
+ case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
+ rewrite_goals_tac action_rews,
+ forward_tac [temp_use Step1_4_7] i,
+ asm_full_simp_tac (simpset() addsimps simps) i
+ ];
(* ----------------------------------------------------------------------
Combine steps 1.2 and 1.4 to prove that the implementation satisfies
@@ -386,7 +387,7 @@
by (rtac unchanged_safeI 1);
by (auto_tac (MI_css addSDs2 [Step1_2_5]));
by (auto_tac (MI_css addsimps2 [square_def,UNext_def]
- addSDs2 [Step1_4_5a,Step1_4_5b]));
+ addSDs2 [Step1_4_5a,Step1_4_5b]));
qed "S5safe";
Goal "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
@@ -395,7 +396,7 @@
by (rtac unchanged_safeI 1);
by (auto_tac (MI_css addSDs2 [Step1_2_6]));
by (auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def]
- addSDs2 [Step1_4_6a,Step1_4_6b]));
+ addSDs2 [Step1_4_6a,Step1_4_6b]));
qed "S6safe";
(* ----------------------------------------------------------------------
@@ -424,13 +425,13 @@
Goal "|- S1 rmhist p --> \
\ ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))";
by (action_simp_tac (simpset() addsimps [angle_def,S_def,S1_def])
- [notI] [enabledE,temp_elim Memoryidle] 1);
+ [notI] [enabledE,temp_elim Memoryidle] 1);
by (Force_tac 1);
qed "S1_RNextdisabled";
Goal "|- S1 rmhist p --> \
\ ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))";
-by (action_simp_tac
+by (action_simp_tac
(simpset() addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def])
[notI] [enabledE] 1);
qed "S1_Returndisabled";
@@ -438,13 +439,13 @@
Goal "|- []<>S1 rmhist p \
\ --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)";
by (auto_tac (MI_css addsimps2 [WF_alt]
- addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE]));
+ addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE]));
qed "RNext_fair";
Goal "|- []<>S1 rmhist p \
\ --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)";
by (auto_tac (MI_css addsimps2 [WF_alt]
- addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE]));
+ addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE]));
qed "Return_fair";
(* ------------------------------ State S2 ------------------------------ *)
@@ -493,7 +494,7 @@
Goal "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\
\ --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))";
by (auto_tac (MI_css addsimps2 [r_def]
- addSIs2 [RPCFail_Next_enabled,RPCFail_enabled]));
+ addSIs2 [RPCFail_Next_enabled,RPCFail_enabled]));
by (cut_facts_tac [MI_base] 1);
by (blast_tac (claset() addDs [base_pair]) 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S3_def])));
@@ -529,7 +530,7 @@
\ & <RNext rmCh mm ires p>_(m p) \
\ --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$";
by (auto_tac (MI_css addsimps2 [angle_def]
- addSDs2 [Step1_2_4, ReadResult, WriteResult]));
+ addSDs2 [Step1_2_4, ReadResult, WriteResult]));
qed "S4aRNext_successors";
Goal "|- $(S4 rmhist p & ires!p = #NotAResult) \
@@ -598,7 +599,7 @@
Goal "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
\ --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))";
by (auto_tac (MI_css addsimps2 [r_def]
- addSIs2 [RPCFail_Next_enabled, RPCFail_enabled]));
+ addSIs2 [RPCFail_Next_enabled, RPCFail_enabled]));
by (cut_facts_tac [MI_base] 1);
by (blast_tac (claset() addDs [base_pair]) 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S5_def])));
@@ -627,7 +628,7 @@
Goal "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p";
by (action_simp_tac
(simpset() addsimps [angle_def,MClkReply_def,Return_def,
- ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
+ ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
[] [] 1);
qed "MClkReplyS6";
@@ -643,10 +644,10 @@
\ --> []<>(S1 rmhist p)";
by (Clarsimp_tac 1);
by (subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1);
-by (etac InfiniteEnsures 1);
+by (etac InfiniteEnsures 1);
by (atac 1);
by (action_simp_tac (simpset()) []
- (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1);
+ (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1);
by (auto_tac (MI_css addsimps2 [SF_def]));
by (etac contrapos_np 1);
by (auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE]));
@@ -664,7 +665,7 @@
\ ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p \
\ ~> S6 rmhist p";
by (auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6]
- addIs2 [LatticeTransitivity]));
+ addIs2 [LatticeTransitivity]));
qed "S4bS5S6LeadstoS6";
Goal "[| sigma |= S4 rmhist p & ires!p = #NotAResult \
@@ -672,19 +673,19 @@
\ sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; \
\ sigma |= S5 rmhist p ~> S6 rmhist p |] \
\ ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p";
-by (subgoal_tac
+by (subgoal_tac
"sigma |= (S4 rmhist p & ires!p = #NotAResult)\
\ | (S4 rmhist p & ires!p ~= #NotAResult)\
\ | S5 rmhist p | S6 rmhist p ~> S6 rmhist p" 1);
- by (eres_inst_tac
+ by (eres_inst_tac
[("G", "PRED ((S4 rmhist p & ires!p = #NotAResult)\
\ | (S4 rmhist p & ires!p ~= #NotAResult)\
-\ | S5 rmhist p | S6 rmhist p)")]
+\ | S5 rmhist p | S6 rmhist p)")]
(temp_use LatticeTransitivity) 1);
by (force_tac (MI_css addsimps2 Init_defs addSIs2 [ImplLeadsto_gen, necT]) 1);
by (rtac (temp_use LatticeDisjunctionIntro) 1);
by (etac (temp_use LatticeTransitivity) 1);
-by (etac (temp_use LatticeTriangle2) 1);
+by (etac (temp_use LatticeTriangle2) 1);
by (atac 1);
by (auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6]));
qed "S4S5S6LeadstoS6";
@@ -699,7 +700,7 @@
by (etac (temp_use LatticeTriangle2) 1);
by (rtac (S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1);
by (auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,necT]
- addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
+ addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
qed "S3S4S5S6LeadstoS6";
Goal "[| sigma |= S2 rmhist p ~> S3 rmhist p; \
@@ -711,11 +712,11 @@
\ ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \
\ ~> S6 rmhist p";
by (rtac (temp_use LatticeDisjunctionIntro) 1);
-by (rtac (temp_use LatticeTransitivity) 1);
+by (rtac (temp_use LatticeTransitivity) 1);
by (atac 2);
by (rtac (S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1);
by (auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,necT]
- addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
+ addIs2 [ImplLeadsto_gen] addsimps2 Init_defs));
qed "S2S3S4S5S6LeadstoS6";
Goal "[| sigma |= []ImpInv rmhist p; \
@@ -750,7 +751,7 @@
*)
Goal "|- IPImp p --> (ALL l. []$MemInv mm l)";
by (auto_tac (MI_css addsimps2 [IPImp_def,box_stp_act]
- addSIs2 [MemoryInvariantAll]));
+ addSIs2 [MemoryInvariantAll]));
qed "Step1_5_1a";
Goal "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p) \
@@ -759,8 +760,8 @@
by (inv_tac MI_css 1);
by (auto_tac (MI_css addsimps2 [Init_def, ImpInv_def, box_stp_act]
addSDs2 [Step1_1]
- addDs2 [S1_successors,S2_successors,S3_successors,
- S4_successors,S5_successors,S6_successors]));
+ addDs2 [S1_successors,S2_successors,S3_successors,
+ S4_successors,S5_successors,S6_successors]));
qed "Step1_5_1b";
(*** Initialization ***)
@@ -790,9 +791,9 @@
\ & [](ALL l. $MemInv mm l)" 1);
by (auto_tac (MI_css addsimps2 [split_box_conj,box_stp_act] addSDs2 [Step1_5_1b]));
by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
- ImpLive_def,c_def,r_def,m_def]) 1);
+ ImpLive_def,c_def,r_def,m_def]) 1);
by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
- HistP_def,Init_def,ImpInit_def]) 1);
+ HistP_def,Init_def,ImpInit_def]) 1);
by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
ImpNext_def,c_def,r_def,m_def,split_box_conj]) 1);
by (force_tac (MI_css addsimps2 [HistP_def]) 1);
@@ -828,7 +829,7 @@
(* QED step of step 1 *)
Goal "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p";
by (auto_tac (MI_css addsimps2 [UPSpec_def,split_box_conj]
- addSDs2 [GoodImpl]
+ addSDs2 [GoodImpl]
addSIs2 [Step1_5_2a,Step1_5_2b,Step1_5_3b,Step1_5_3c]));
qed "Step1";
@@ -840,10 +841,10 @@
\ & $ImpInv rmhist p \
\ --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)";
by (Clarsimp_tac 1);
-by (dtac (action_use WriteS4) 1);
+by (dtac (action_use WriteS4) 1);
by (atac 1);
by (split_idle_tac [] 1);
-by (auto_tac (MI_css addsimps2 [ImpNext_def]
+by (auto_tac (MI_css addsimps2 [ImpNext_def]
addSDs2 [S4EnvUnch,S4ClerkUnch,S4RPCUnch]));
by (auto_tac (MI_css addsimps2 [square_def] addDs2 [S4Write]));
qed "Step2_2a";
@@ -872,7 +873,7 @@
by (auto_tac (MI_css addsimps2 [MSpec_def]));
by (force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 1);
by (auto_tac (MI_css addSIs2 [Step2_lemma]
- addsimps2 [split_box_conj,all_box]));
+ addsimps2 [split_box_conj,all_box]));
by (force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 4);
by (auto_tac (MI_css addsimps2 [split_box_conj] addSEs2 [allE] addSDs2 [GoodImpl]));
qed "Step2";
@@ -889,15 +890,15 @@
*)
Goal "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)";
by (auto_tac (MI_css addsimps2 [IUSpec_def,Implementation_def,IPImp_def,
- MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def]
- addSIs2 [Step1,Step2]));
+ MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def]
+ addSIs2 [Step1,Step2]));
qed "Impl_IUSpec";
(* The main theorem: introduce hiding and eliminate history variable. *)
Goal "|- Implementation --> USpec memCh";
by (Clarsimp_tac 1);
by (forward_tac [temp_use History] 1);
-by (auto_tac (MI_css addsimps2 [USpec_def]
+by (auto_tac (MI_css addsimps2 [USpec_def]
addIs2 [eexI, Impl_IUSpec, MI_base]
addSEs2 [eexE]));
qed "Implementation";
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MemoryImplementation.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,9 +10,11 @@
RPC-Memory example: Memory implementation
*)
-MemoryImplementation = Memory + RPC + MemClerk + Datatype +
+theory MemoryImplementation
+imports Memory RPC MemClerk
+begin
-datatype histState = histA | histB
+datatype histState = histA | histB
types
histType = "(PrIds => histState) stfun" (* the type of the history variable *)
@@ -22,7 +25,7 @@
memCh :: "memChType"
(* internal variables *)
mm :: "memType"
-
+
(* the state variables of the implementation *)
(* channels *)
(* same interface channel memCh *)
@@ -80,29 +83,29 @@
(* the implementation *)
IPImp :: "PrIds => temporal"
"IPImp p == TEMP ( Init ~Calling memCh p & [][ENext p]_(e p)
- & MClkIPSpec memCh crCh cst p
- & RPCIPSpec crCh rmCh rst p
- & RPSpec rmCh mm ires p
- & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"
+ & MClkIPSpec memCh crCh cst p
+ & RPCIPSpec crCh rmCh rst p
+ & RPSpec rmCh mm ires p
+ & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"
ImpInit :: "PrIds => stpred"
"ImpInit p == PRED ( ~Calling memCh p
& MClkInit crCh cst p
- & RPCInit rmCh rst p
- & PInit ires p)"
+ & RPCInit rmCh rst p
+ & PInit ires p)"
ImpNext :: "PrIds => action"
- "ImpNext p == ACT [ENext p]_(e p)
+ "ImpNext p == ACT [ENext p]_(e p)
& [MClkNext memCh crCh cst p]_(c p)
- & [RPCNext crCh rmCh rst p]_(r p)
+ & [RPCNext crCh rmCh rst p]_(r p)
& [RNext rmCh mm ires p]_(m p)"
ImpLive :: "PrIds => temporal"
- "ImpLive p == TEMP WF(MClkFwd memCh crCh cst p)_(c p)
- & SF(MClkReply memCh crCh cst p)_(c p)
- & WF(RPCNext crCh rmCh rst p)_(r p)
- & WF(RNext rmCh mm ires p)_(m p)
- & WF(MemReturn rmCh ires p)_(m p)"
+ "ImpLive p == TEMP WF(MClkFwd memCh crCh cst p)_(c p)
+ & SF(MClkReply memCh crCh cst p)_(c p)
+ & WF(RPCNext crCh rmCh rst p)_(r p)
+ & WF(RNext rmCh mm ires p)_(m p)
+ & WF(MemReturn rmCh ires p)_(m p)"
Implementation :: "temporal"
"Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
@@ -148,14 +151,14 @@
(* The invariant asserts that the system is always in one of S1 - S6, for every p *)
ImpInv :: "histType => PrIds => stpred"
"ImpInv rmhist p == PRED ( S1 rmhist p | S2 rmhist p | S3 rmhist p
- | S4 rmhist p | S5 rmhist p | S6 rmhist p)"
+ | S4 rmhist p | S5 rmhist p | S6 rmhist p)"
resbar :: "histType => resType" (* refinement mapping *)
- "resbar rmhist s p ==
+ "resbar rmhist s p ==
(if (S1 rmhist p s | S2 rmhist p s)
then ires s p
else if S3 rmhist p s
- then if rmhist s p = histA
+ then if rmhist s p = histA
then ires s p else MemFailure
else if S4 rmhist p s
then if (rmhist s p = histB & ires s p = NotAResult)
@@ -167,11 +170,13 @@
then MemFailure else res (crCh s p)
else NotAResult)" (* dummy value *)
-rules
+axioms
(* the "base" variables: everything except resbar and hist (for any index) *)
- MI_base "basevars (caller memCh!p,
- (rtrner memCh!p, caller crCh!p, cst!p),
- (rtrner crCh!p, caller rmCh!p, rst!p),
- (mm!l, rtrner rmCh!p, ires!p))"
+ MI_base: "basevars (caller memCh!p,
+ (rtrner memCh!p, caller crCh!p, cst!p),
+ (rtrner crCh!p, caller rmCh!p, rst!p),
+ (mm!l, rtrner rmCh!p, ires!p))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/TLA/Memory/MemoryParameters.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: MemoryParameters.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -8,10 +9,10 @@
Addsimps ([BadArgNoMemVal,MemFailNoMemVal,InitValMemVal,NotAResultNotVal,
NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]
- @ (map (fn x => x RS not_sym)
+ @ (map (fn x => x RS not_sym)
[NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]));
-val prems = goal thy "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P";
+val prems = goal (the_context ()) "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P";
by (resolve_tac prems 1);
by (cut_facts_tac (NotAResultNotVal::prems) 1);
by (Force_tac 1);
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MemoryParameters.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,32 +10,37 @@
RPC-Memory example: Memory parameters
*)
-MemoryParameters = Datatype + RPCMemoryParams +
+theory MemoryParameters
+imports RPCMemoryParams
+begin
(* the memory operations *)
datatype memOp = read Locs | write Locs Vals
consts
(* memory locations and contents *)
- MemLoc :: Locs set
- MemVal :: Vals set
+ MemLoc :: "Locs set"
+ MemVal :: "Vals set"
(* some particular values *)
OK :: "Vals"
BadArg :: "Vals"
MemFailure :: "Vals"
NotAResult :: "Vals" (* defined here for simplicity *)
-
+
(* the initial value stored in each memory cell *)
InitVal :: "Vals"
-rules
+axioms
(* basic assumptions about the above constants and predicates *)
- BadArgNoMemVal "BadArg ~: MemVal"
- MemFailNoMemVal "MemFailure ~: MemVal"
- InitValMemVal "InitVal : MemVal"
- NotAResultNotVal "NotAResult ~: MemVal"
- NotAResultNotOK "NotAResult ~= OK"
- NotAResultNotBA "NotAResult ~= BadArg"
- NotAResultNotMF "NotAResult ~= MemFailure"
+ BadArgNoMemVal: "BadArg ~: MemVal"
+ MemFailNoMemVal: "MemFailure ~: MemVal"
+ InitValMemVal: "InitVal : MemVal"
+ NotAResultNotVal: "NotAResult ~: MemVal"
+ NotAResultNotOK: "NotAResult ~= OK"
+ NotAResultNotBA: "NotAResult ~= BadArg"
+ NotAResultNotMF: "NotAResult ~= MemFailure"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/Memory/ProcedureInterface.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: ProcedureInterface.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -11,10 +12,10 @@
(* ---------------------------------------------------------------------------- *)
-val Procedure_defs = [caller_def, rtrner_def, Calling_def,
+val Procedure_defs = [caller_def, rtrner_def, Calling_def,
Call_def, Return_def,
- PLegalCaller_def, LegalCaller_def,
- PLegalReturner_def, LegalReturner_def];
+ PLegalCaller_def, LegalCaller_def,
+ PLegalReturner_def, LegalReturner_def];
(* Calls and returns change their subchannel *)
Goal "|- Call ch p v --> <Call ch p v>_((caller ch)!p)";
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: ProcedureInterface.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,28 +10,29 @@
Procedure interface for RPC-Memory components.
*)
-ProcedureInterface = TLA + RPCMemoryParams +
+theory ProcedureInterface
+imports TLA RPCMemoryParams
+begin
-types
+typedecl
(* type of channels with argument type 'a and return type 'r.
- we model a channel as an array of variables (of type chan)
- rather than a single array-valued variable because the
+ we model a channel as an array of variables (of type chan)
+ rather than a single array-valued variable because the
notation gets a little simpler.
*)
('a,'r) chan
- ('a,'r) channel = (PrIds => ('a,'r) chan) stfun
-
-arities
- chan :: (type,type) type
+types
+ ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
consts
(* data-level functions *)
- cbit,rbit :: "('a,'r) chan => bit"
+ cbit :: "('a,'r) chan => bit"
+ rbit :: "('a,'r) chan => bit"
arg :: "('a,'r) chan => 'a"
res :: "('a,'r) chan => 'r"
(* state functions *)
- caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
+ caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
(* state predicates *)
@@ -50,10 +52,10 @@
slice :: "('a => 'b) stfun => 'a => 'b stfun"
syntax
- "_slice" :: [lift, 'a] => lift ("(_!_)" [70,70] 70)
+ "_slice" :: "[lift, 'a] => lift" ("(_!_)" [70,70] 70)
- "_Call" :: ['a, 'b, lift] => lift ("(Call _ _ _)" [90,90,90] 90)
- "_Return" :: ['a, 'b, lift] => lift ("(Return _ _ _)" [90,90,90] 90)
+ "_Call" :: "['a, 'b, lift] => lift" ("(Call _ _ _)" [90,90,90] 90)
+ "_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90)
translations
"_slice" == "slice"
@@ -61,25 +63,27 @@
"_Call" == "ACall"
"_Return" == "AReturn"
-rules
- slice_def "(PRED (x!i)) s == x s i"
+defs
+ slice_def: "(PRED (x!i)) s == x s i"
- caller_def "caller ch == %s p. (cbit (ch s p), arg (ch s p))"
- rtrner_def "rtrner ch == %s p. (rbit (ch s p), res (ch s p))"
+ caller_def: "caller ch == %s p. (cbit (ch s p), arg (ch s p))"
+ rtrner_def: "rtrner ch == %s p. (rbit (ch s p), res (ch s p))"
- Calling_def "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >"
- Call_def "(ACT Call ch p v) == ACT ~ $Calling ch p
+ Calling_def: "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >"
+ Call_def: "(ACT Call ch p v) == ACT ~ $Calling ch p
& (cbit<ch!p>$ ~= $rbit<ch!p>)
& (arg<ch!p>$ = $v)"
- Return_def "(ACT Return ch p v) == ACT $Calling ch p
+ Return_def: "(ACT Return ch p v) == ACT $Calling ch p
& (rbit<ch!p>$ = $cbit<ch!p>)
& (res<ch!p>$ = $v)"
- PLegalCaller_def "PLegalCaller ch p == TEMP
+ PLegalCaller_def: "PLegalCaller ch p == TEMP
Init(~ Calling ch p)
& [][ ? a. Call ch p a ]_((caller ch)!p)"
- LegalCaller_def "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
- PLegalReturner_def "PLegalReturner ch p == TEMP
+ LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
+ PLegalReturner_def: "PLegalReturner ch p == TEMP
[][ ? v. Return ch p v ]_((rtrner ch)!p)"
- LegalReturner_def "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
+ LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/TLA/Memory/ROOT.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/ROOT.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,2 +1,4 @@
+
+(* $Id$ *)
time_use_thy "MemoryImplementation";
--- a/src/HOL/TLA/Memory/RPC.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/RPC.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,12 +1,13 @@
-(*
+(*
File: RPC.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
RPC-Memory example: RPC specification (theorems and proofs)
*)
-val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def,
+val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def,
RPCReply_def, RPCNext_def];
val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def];
@@ -29,7 +30,7 @@
Goal "|- RPCFail send rcv rst p --> \
\ <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)";
by (auto_tac (claset() addSDs [Return_changed],
- simpset() addsimps [angle_def,RPCNext_def,RPCFail_def]));
+ simpset() addsimps [angle_def,RPCNext_def,RPCFail_def]));
qed "RPCFail_vis";
Goal "|- Enabled (RPCFail send rcv rst p) --> \
--- a/src/HOL/TLA/Memory/RPC.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: RPC.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,7 +10,9 @@
RPC-Memory example: RPC specification
*)
-RPC = RPCParameters + ProcedureInterface + Memory +
+theory RPC
+imports RPCParameters ProcedureInterface Memory
+begin
types
rpcSndChType = "(rpcOp,Vals) channel"
@@ -31,10 +34,10 @@
RPCIPSpec :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
-rules
- RPCInit_def "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
+defs
+ RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
- RPCFwd_def "RPCFwd send rcv rst p == ACT
+ RPCFwd_def: "RPCFwd send rcv rst p == ACT
$(Calling send p)
& $(rst!p) = # rpcA
& IsLegalRcvArg<arg<$(send!p)>>
@@ -42,36 +45,38 @@
& (rst!p)$ = # rpcB
& unchanged (rtrner send!p)"
- RPCReject_def "RPCReject send rcv rst p == ACT
+ RPCReject_def: "RPCReject send rcv rst p == ACT
$(rst!p) = # rpcA
& ~IsLegalRcvArg<arg<$(send!p)>>
& Return send p #BadCall
& unchanged ((rst!p), (caller rcv!p))"
- RPCFail_def "RPCFail send rcv rst p == ACT
+ RPCFail_def: "RPCFail send rcv rst p == ACT
~$(Calling rcv p)
& Return send p #RPCFailure
& (rst!p)$ = #rpcA
& unchanged (caller rcv!p)"
- RPCReply_def "RPCReply send rcv rst p == ACT
+ RPCReply_def: "RPCReply send rcv rst p == ACT
~$(Calling rcv p)
& $(rst!p) = #rpcB
- & Return send p res<rcv!p>
+ & Return send p res<rcv!p>
& (rst!p)$ = #rpcA
& unchanged (caller rcv!p)"
- RPCNext_def "RPCNext send rcv rst p == ACT
+ RPCNext_def: "RPCNext send rcv rst p == ACT
( RPCFwd send rcv rst p
| RPCReject send rcv rst p
| RPCFail send rcv rst p
| RPCReply send rcv rst p)"
- RPCIPSpec_def "RPCIPSpec send rcv rst p == TEMP
+ RPCIPSpec_def: "RPCIPSpec send rcv rst p == TEMP
Init RPCInit rcv rst p
& [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
& WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
- RPCISpec_def "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
+ RPCISpec_def: "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: RPCMemoryParams.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,7 +10,9 @@
Basic declarations for the RPC-memory example.
*)
-theory RPCMemoryParams imports Main begin
+theory RPCMemoryParams
+imports Main
+begin
types
bit = "bool" (* Signal wires for the procedure interface.
--- a/src/HOL/TLA/Memory/RPCParameters.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,11 +1,11 @@
-(*
+(*
File: RPCParameters.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
RPC-Memory example: RPC parameters (theorems and proofs)
*)
-
Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF]
@ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF]));
--- a/src/HOL/TLA/Memory/RPCParameters.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: RPCParameters.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -11,10 +12,12 @@
memory implementation.
*)
-RPCParameters = MemoryParameters +
+theory RPCParameters
+imports MemoryParameters
+begin
-datatype rpcOp = memcall memOp | othercall Vals
-datatype rpcState = rpcA | rpcB
+datatype rpcOp = memcall memOp | othercall Vals
+datatype rpcState = rpcA | rpcB
consts
(* some particular return values *)
@@ -25,21 +28,24 @@
is legal for the receiver (i.e., the memory). This can now be a little
simpler than for the generic RPC component. RelayArg returns an arbitrary
memory call for illegal arguments. *)
- IsLegalRcvArg :: rpcOp => bool
- RPCRelayArg :: rpcOp => memOp
+ IsLegalRcvArg :: "rpcOp => bool"
+ RPCRelayArg :: "rpcOp => memOp"
-rules
+axioms
(* RPCFailure is different from MemVals and exceptions *)
- RFNoMemVal "RPCFailure ~: MemVal"
- NotAResultNotRF "NotAResult ~= RPCFailure"
- OKNotRF "OK ~= RPCFailure"
- BANotRF "BadArg ~= RPCFailure"
+ RFNoMemVal: "RPCFailure ~: MemVal"
+ NotAResultNotRF: "NotAResult ~= RPCFailure"
+ OKNotRF: "OK ~= RPCFailure"
+ BANotRF: "BadArg ~= RPCFailure"
defs
- IsLegalRcvArg_def "IsLegalRcvArg ra ==
+ IsLegalRcvArg_def: "IsLegalRcvArg ra ==
case ra of (memcall m) => True
| (othercall v) => False"
- RPCRelayArg_def "RPCRelayArg ra ==
+ RPCRelayArg_def: "RPCRelayArg ra ==
case ra of (memcall m) => m
| (othercall v) => arbitrary"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/HOL/TLA/ROOT.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/ROOT.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,4 +1,5 @@
(* Title: TLA/ROOT.ML
+ ID: $Id$
Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
*)
--- a/src/HOL/TLA/Stfun.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Stfun.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: Stfun.ML
+(*
+ File: Stfun.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -51,7 +52,7 @@
Goal "!!v. basevars (v::bool stfun, v) ==> False";
by (etac baseE 1);
-by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1);
+by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1);
by (atac 2);
by (Asm_full_simp_tac 1);
--- a/src/HOL/TLA/Stfun.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Stfun.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/Stfun.thy
+(*
+ File: TLA/Stfun.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -9,18 +10,18 @@
States and state functions for TLA as an "intensional" logic.
*)
-Stfun = Intensional +
+theory Stfun
+imports Intensional
+begin
+
+typedecl state
+
+instance state :: world ..
types
- state
- 'a stfun = "state => 'a"
- stpred = "bool stfun"
+ 'a stfun = "state => 'a"
+ stpred = "bool stfun"
-arities
- state :: type
-
-instance
- state :: world
consts
(* Formalizing type "state" would require formulas to be tagged with
@@ -39,20 +40,22 @@
stvars :: "'a stfun => bool"
syntax
- "PRED" :: lift => 'a ("PRED _")
- "_stvars" :: lift => bool ("basevars _")
+ "PRED" :: "lift => 'a" ("PRED _")
+ "_stvars" :: "lift => bool" ("basevars _")
translations
"PRED P" => "(P::state => _)"
"_stvars" == "stvars"
defs
- (* Base variables may be assigned arbitrary (type-correct) values.
+ (* Base variables may be assigned arbitrary (type-correct) values.
Note that vs may be a tuple of variables. The correct identification
of base variables is up to the user who must take care not to
introduce an inconsistency. For example, "basevars (x,x)" would
definitely be inconsistent.
*)
- basevars_def "stvars vs == range vs = UNIV"
+ basevars_def: "stvars vs == range vs = UNIV"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/TLA/TLA.ML Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/TLA.ML Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
- File: TLA/TLA.ML
+(*
+ File: TLA/TLA.ML
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -8,11 +9,11 @@
(* Specialize intensional introduction/elimination rules for temporal formulas *)
-val [prem] = goal thy "(!!sigma. sigma |= (F::temporal)) ==> |- F";
+val [prem] = goal (the_context ()) "(!!sigma. sigma |= (F::temporal)) ==> |- F";
by (REPEAT (resolve_tac [prem,intI] 1));
qed "tempI";
-val [prem] = goal thy "|- (F::temporal) ==> sigma |= F";
+val [prem] = goal (the_context ()) "|- (F::temporal) ==> sigma |= F";
by (rtac (prem RS intD) 1);
qed "tempD";
@@ -23,14 +24,14 @@
functions defined in Intensional.ML in that they introduce a
"world" parameter of type "behavior".
*)
-fun temp_unlift th =
+fun temp_unlift th =
(rewrite_rule action_rews (th RS tempD))
handle _ => action_unlift th;
(* Turn |- F = G into meta-level rewrite rule F == G *)
val temp_rewrite = int_rewrite;
-fun temp_use th =
+fun temp_use th =
case (concl_of th) of
Const _ $ (Const ("Intensional.Valid", _) $ _) =>
((flatten (temp_unlift th)) handle _ => th)
@@ -77,7 +78,7 @@
section "Simple temporal logic";
(* []~F == []~Init F *)
-bind_thm("boxNotInit",
+bind_thm("boxNotInit",
rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] boxInit));
Goalw [dmd_def] "TEMP <>F == TEMP <> Init F";
@@ -85,7 +86,7 @@
by (simp_tac (simpset() addsimps Init_simps) 1);
qed "dmdInit";
-bind_thm("dmdNotInit",
+bind_thm("dmdNotInit",
rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] dmdInit));
(* boxInit and dmdInit cannot be used as rewrites, because they loop.
@@ -133,7 +134,7 @@
by (force_tac (temp_css addEs2 [transT,STL2]) 1);
qed "STL3";
-(* corresponding elimination rule introduces double boxes:
+(* corresponding elimination rule introduces double boxes:
[| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
*)
bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2));
@@ -148,7 +149,7 @@
(* ------------------------ STL4 ------------------------------------------- *)
-val [prem] = goal thy "|- F --> G ==> |- []F --> []G";
+val [prem] = goal (the_context ()) "|- F --> G ==> |- []F --> []G";
by (Clarsimp_tac 1);
by (rtac (temp_use normalT) 1);
by (rtac (temp_use (prem RS necT)) 1);
@@ -156,15 +157,15 @@
qed "STL4";
(* Unlifted version as an elimination rule *)
-val prems = goal thy "[| sigma |= []F; |- F --> G |] ==> sigma |= []G";
+val prems = goal (the_context ()) "[| sigma |= []F; |- F --> G |] ==> sigma |= []G";
by (REPEAT (resolve_tac (prems @ [temp_use STL4]) 1));
qed "STL4E";
-val [prem] = goal thy "|- Init F --> Init G ==> |- []F --> []G";
+val [prem] = goal (the_context ()) "|- Init F --> Init G ==> |- []F --> []G";
by (rtac (rewrite_rule [boxInitD] (prem RS STL4)) 1);
qed "STL4_gen";
-val prems = goal thy
+val prems = goal (the_context ())
"[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G";
by (REPEAT (resolve_tac (prems @ [temp_use STL4_gen]) 1));
qed "STL4E_gen";
@@ -176,12 +177,12 @@
*)
(* The dual versions for <> *)
-val [prem] = goalw thy [dmd_def]
+val [prem] = goalw (the_context ()) [dmd_def]
"|- F --> G ==> |- <>F --> <>G";
by (fast_tac (temp_cs addSIs [prem] addSEs [STL4E]) 1);
qed "DmdImpl";
-val prems = goal thy "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G";
+val prems = goal (the_context ()) "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G";
by (REPEAT (resolve_tac (prems @ [temp_use DmdImpl]) 1));
qed "DmdImplE";
@@ -201,7 +202,7 @@
(NB: F and G must have the same type, i.e., both actions or temporals.)
Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
*)
-val prems = goal thy
+val prems = goal (the_context ())
"[| sigma |= []F; sigma |= []G; sigma |= [](F&G) ==> PROP R |] ==> PROP R";
by (REPEAT (resolve_tac (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1));
qed "box_conjE";
@@ -225,15 +226,15 @@
REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]);
fun merge_temp_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i,
+ REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i,
eres_inst_tac [("'a","behavior")] box_thin i]);
fun merge_stp_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i,
+ REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i,
eres_inst_tac [("'a","state")] box_thin i]);
fun merge_act_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i,
+ REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i,
eres_inst_tac [("'a","state * state")] box_thin i]);
@@ -245,8 +246,8 @@
Goal "|- (<>(F | G)) = (<>F | <>G)";
by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]));
-by (ALLGOALS (EVERY' [etac contrapos_np,
- merge_box_tac,
+by (ALLGOALS (EVERY' [etac contrapos_np,
+ merge_box_tac,
fast_tac (temp_cs addSEs [STL4E])]));
qed "DmdOr";
@@ -255,7 +256,7 @@
qed "exT";
bind_thm("ex_dmd", standard((temp_unlift exT) RS sym));
-
+
Goal "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G";
by (etac dup_boxE 1);
@@ -272,7 +273,7 @@
by (fast_tac (temp_cs addSEs [STL4E]) 1);
qed "DmdImpl2";
-val [prem1,prem2,prem3] = goal thy
+val [prem1,prem2,prem3] = goal (the_context ())
"[| sigma |= []<>F; sigma |= []G; |- F & G --> H |] ==> sigma |= []<>H";
by (cut_facts_tac [prem1,prem2] 1);
by (eres_inst_tac [("F","G")] dup_boxE 1);
@@ -303,7 +304,7 @@
by (fast_tac (temp_cs addSEs [notE,STL4E]) 1);
qed "BoxDmd2_simple";
-val [p1,p2,p3] = goal thy
+val [p1,p2,p3] = goal (the_context ())
"[| sigma |= []A; sigma |= <>F; |- []A & F --> G |] ==> sigma |= <>G";
by (rtac ((p2 RS (p1 RS (temp_use BoxDmd))) RS DmdImplE) 1);
by (rtac p3 1);
@@ -312,7 +313,7 @@
Goal "|- <>[]F & <>[]G --> <>[](F & G)";
by (auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]));
by (dtac (temp_use linT) 1);
-by (atac 1);
+by (atac 1);
by (etac thin_rl 1);
by (rtac ((temp_unlift DmdDmd) RS iffD1) 1);
by (etac disjE 1);
@@ -320,8 +321,8 @@
by (rtac BoxDmd 1);
by (etac DmdImplE 1);
by Auto_tac;
-by (dtac (temp_use BoxDmd) 1);
-by (atac 1);
+by (dtac (temp_use BoxDmd) 1);
+by (atac 1);
by (etac thin_rl 1);
by (fast_tac (temp_cs addSEs [DmdImplE]) 1);
qed "STL6";
@@ -333,7 +334,7 @@
Goal "|- ([]#P) = #P";
by (rtac tempI 1);
by (case_tac "P" 1);
-by (auto_tac (temp_css addSIs2 [necT] addDs2 [STL2_gen]
+by (auto_tac (temp_css addSIs2 [necT] addDs2 [STL2_gen]
addsimps2 Init_simps));
qed "BoxConst";
@@ -365,7 +366,7 @@
e.g. []F & ~[]F becomes []F & <>~F !! *)
val more_temp_simps = (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd])
@ (map (fn th => (temp_unlift th) RS eq_reflection)
- [NotBox, NotDmd]);
+ [NotBox, NotDmd]);
Goal "|- ([]<>[]F) = (<>[]F)";
by (auto_tac (temp_css addSDs2 [STL2]));
@@ -373,7 +374,7 @@
by (subgoal_tac "sigma |= <>[][]F & <>[]~[]F" 1);
by (etac thin_rl 1);
by Auto_tac;
-by (dtac (temp_use STL6) 1);
+by (dtac (temp_use STL6) 1);
by (atac 1);
by (Asm_full_simp_tac 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps)));
@@ -397,7 +398,7 @@
by (Clarsimp_tac 1);
by (rtac ccontr 1);
by (asm_full_simp_tac (simpset() addsimps more_temp_simps) 1);
-by (dtac (temp_use STL6) 1);
+by (dtac (temp_use STL6) 1);
by (atac 1);
by (Asm_full_simp_tac 1);
qed "DBImplBD";
@@ -433,14 +434,14 @@
by (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_pr]));
qed "BoxPrime";
-val prems = goal thy "|- $P & P$ --> A ==> |- []P --> []A";
+val prems = goal (the_context ()) "|- $P & P$ --> A ==> |- []P --> []A";
by (Clarsimp_tac 1);
by (dtac (temp_use BoxPrime) 1);
-by (auto_tac (temp_css addsimps2 [Init_stp_act_rev]
+by (auto_tac (temp_css addsimps2 [Init_stp_act_rev]
addSIs2 prems addSEs2 [STL4E]));
qed "TLA2";
-val prems = goal thy
+val prems = goal (the_context ())
"[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A";
by (REPEAT (resolve_tac (prems @ (prems RL [temp_use TLA2])) 1));
qed "TLA2E";
@@ -454,7 +455,7 @@
(* ------------------------ INV1, stable --------------------------------------- *)
section "stable, invariant";
-val prems = goal thy
+val prems = goal (the_context ())
"[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |] \
\ ==> sigma |= []F";
by (rtac (temp_use indT) 1);
@@ -469,7 +470,7 @@
val more_temp_simps = (temp_rewrite box_stp_act)::more_temp_simps;
-Goalw [stable_def,boxInit_stp,boxInit_act]
+Goalw [stable_def,boxInit_stp,boxInit_act]
"|- (Init P) --> (stable P) --> []P";
by (Clarsimp_tac 1);
by (etac ind_rule 1);
@@ -481,7 +482,7 @@
by (fast_tac (temp_cs addSEs [STL4E]) 1);
qed "StableT";
-val prems = goal thy
+val prems = goal (the_context ())
"[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P";
by (REPEAT (resolve_tac (prems @ [temp_use StableT]) 1));
qed "Stable";
@@ -560,7 +561,7 @@
by (fast_tac (temp_cs addIs [DmdPrime] addSEs [STL4E]) 1);
qed "InfinitePrime";
-val prems = goalw thy [temp_rewrite InfinitePrime]
+val prems = goalw (the_context ()) [temp_rewrite InfinitePrime]
"[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P";
by (rtac InfImpl 1);
by (REPEAT (resolve_tac prems 1));
@@ -570,7 +571,7 @@
section "fairness";
(* alternative definitions of fairness *)
-Goalw [WF_def,dmd_def]
+Goalw [WF_def,dmd_def]
"|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)";
by (fast_tac temp_cs 1);
qed "WF_alt";
@@ -582,7 +583,7 @@
(* theorems to "box" fairness conditions *)
Goal "|- WF(A)_v --> []WF(A)_v";
-by (auto_tac (temp_css addsimps2 (WF_alt::more_temp_simps)
+by (auto_tac (temp_css addsimps2 (WF_alt::more_temp_simps)
addSIs2 [BoxOr]));
qed "BoxWFI";
@@ -591,7 +592,7 @@
qed "WF_Box";
Goal "|- SF(A)_v --> []SF(A)_v";
-by (auto_tac (temp_css addsimps2 (SF_alt::more_temp_simps)
+by (auto_tac (temp_css addsimps2 (SF_alt::more_temp_simps)
addSIs2 [BoxOr]));
qed "BoxSFI";
@@ -618,7 +619,7 @@
qed "leadsto_init";
(* |- F & (F ~> G) --> <>G *)
-bind_thm("leadsto_init_temp",
+bind_thm("leadsto_init_temp",
rewrite_rule Init_simps (read_instantiate [("'a","behavior")] leadsto_init));
Goalw [leadsto_def] "|- ([]<>Init F --> []<>G) = (<>(F ~> G))";
@@ -628,14 +629,14 @@
by (fast_tac (temp_cs addSIs [InitDmd] addSEs [STL4E]) 1);
by (subgoal_tac "sigma |= []<><>G" 1);
by (asm_full_simp_tac (simpset() addsimps more_temp_simps) 1);
-by (dtac (temp_use BoxDmdDmdBox) 1);
+by (dtac (temp_use BoxDmdDmdBox) 1);
by (atac 1);
by (fast_tac (temp_cs addSEs [DmdImplE,STL4E]) 1);
qed "streett_leadsto";
Goal "|- []<>F & (F ~> G) --> []<>G";
by (Clarsimp_tac 1);
-by (etac ((temp_use InitDmd) RS
+by (etac ((temp_use InitDmd) RS
((temp_unlift streett_leadsto) RS iffD2 RS mp)) 1);
by (asm_simp_tac (simpset() addsimps [dmdInitD]) 1);
qed "leadsto_infinite";
@@ -656,7 +657,7 @@
*)
Goalw [leadsto_def] "|- []I & (P & I ~> Q) --> (P ~> Q)";
by (Clarsimp_tac 1);
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_gen]));
qed "INV_leadsto";
@@ -682,17 +683,17 @@
qed "ImplLeadsto_gen";
bind_thm("ImplLeadsto",
- rewrite_rule Init_simps
+ rewrite_rule Init_simps
(read_instantiate [("'a","behavior"), ("'b","behavior")] ImplLeadsto_gen));
Goal "!!F G. |- F --> G ==> |- F ~> G";
-by (auto_tac (temp_css addsimps2 [Init_def]
+by (auto_tac (temp_css addsimps2 [Init_def]
addSIs2 [ImplLeadsto_gen,necT]));
qed "ImplLeadsto_simple";
-val [prem] = goalw thy [leadsto_def]
+val [prem] = goalw (the_context ()) [leadsto_def]
"|- A & $P --> Q` ==> |- []A --> (P ~> Q)";
-by (clarsimp_tac (temp_css addSEs2 [INV_leadsto]) 1);
+by (clarsimp_tac (temp_css addSEs2 [INV_leadsto]) 1);
by (etac STL4E_gen 1);
by (auto_tac (temp_css addsimps2 Init_defs addSIs2 [PrimeDmd,prem]));
qed "EnsuresLeadsto";
@@ -703,12 +704,12 @@
by (auto_tac (temp_css addsimps2 Init_simps addSIs2 [PrimeDmd]));
qed "EnsuresLeadsto2";
-val [p1,p2] = goalw thy [leadsto_def]
+val [p1,p2] = goalw (the_context ()) [leadsto_def]
"[| |- $P & N --> P` | Q`; \
\ |- ($P & N) & A --> Q` \
\ |] ==> |- []N & []([]P --> <>A) --> (P ~> Q)";
by (Clarsimp_tac 1);
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (Clarsimp_tac 1);
by (subgoal_tac "sigmaa |= []($P --> P` | Q`)" 1);
@@ -720,7 +721,7 @@
by (force_tac (temp_css addEs2 [STL4E] addDs2 [p1]) 1);
qed "ensures";
-val prems = goal thy
+val prems = goal (the_context ())
"[| |- $P & N --> P` | Q`; \
\ |- ($P & N) & A --> Q` \
\ |] ==> |- []N & []<>A --> (P ~> Q)";
@@ -730,9 +731,9 @@
by (force_tac (temp_css addSEs2 [STL4E]) 1);
qed "ensures_simple";
-val prems = goal thy
+val prems = goal (the_context ())
"[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q";
-by (REPEAT (resolve_tac (prems @
+by (REPEAT (resolve_tac (prems @
(map temp_use [leadsto_infinite, EnsuresLeadsto])) 1));
qed "EnsuresInfinite";
@@ -751,7 +752,7 @@
by (clarsimp_tac (temp_css addSEs2 [STL4E]) 1);
by (rtac dup_dmdD 1);
by (subgoal_tac "sigmaa |= <>Init G" 1);
- by (etac DmdImpl2 1);
+ by (etac DmdImpl2 1);
by (atac 1);
by (asm_simp_tac (simpset() addsimps [dmdInitD]) 1);
qed "LatticeTransitivity";
@@ -785,7 +786,7 @@
Goal "|- (A ~> D | B) & (B ~> D) --> (A ~> D)";
by (Clarsimp_tac 1);
by (subgoal_tac "sigma |= (D | B) ~> D" 1);
-by (eres_inst_tac [("G", "LIFT (D | B)")] (temp_use LatticeTransitivity) 1);
+by (eres_inst_tac [("G", "LIFT (D | B)")] (temp_use LatticeTransitivity) 1);
by (atac 1);
by (auto_tac (temp_css addIs2 [LatticeDisjunctionIntro,LatticeReflexivity]));
qed "LatticeTriangle";
@@ -793,7 +794,7 @@
Goal "|- (A ~> B | D) & (B ~> D) --> (A ~> D)";
by (Clarsimp_tac 1);
by (subgoal_tac "sigma |= B | D ~> D" 1);
-by (eres_inst_tac [("G", "LIFT (B | D)")] (temp_use LatticeTransitivity) 1);
+by (eres_inst_tac [("G", "LIFT (B | D)")] (temp_use LatticeTransitivity) 1);
by (atac 1);
by (auto_tac (temp_css addIs2 [LatticeDisjunctionIntro,LatticeReflexivity]));
qed "LatticeTriangle2";
@@ -801,7 +802,7 @@
(*** Lamport's fairness rules ***)
section "Fairness rules";
-val prems = goal thy
+val prems = goal (the_context ())
"[| |- $P & N --> P` | Q`; \
\ |- ($P & N) & <A>_v --> Q`; \
\ |- $P & N --> $(Enabled(<A>_v)) |] \
@@ -809,7 +810,7 @@
by (clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1);
by (rtac (temp_use ensures) 1);
by (TRYALL (ares_tac prems));
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (clarsimp_tac (temp_css addsimps2 [WF_def]) 1);
by (rtac (temp_use STL2) 1);
@@ -819,17 +820,17 @@
qed "WF1";
(* Sometimes easier to use; designed for action B rather than state predicate Q *)
-val [prem1,prem2,prem3] = goalw thy [leadsto_def]
+val [prem1,prem2,prem3] = goalw (the_context ()) [leadsto_def]
"[| |- N & $P --> $Enabled (<A>_v); \
-\ |- N & <A>_v --> B; \
+\ |- N & <A>_v --> B; \
\ |- [](N & [~A]_v) --> stable P |] \
\ ==> |- []N & WF(A)_v --> (P ~> B)";
by (clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1);
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (Clarsimp_tac 1);
by (rtac (temp_use (prem2 RS DmdImpl)) 1);
-by (rtac (temp_use BoxDmd_simple) 1);
+by (rtac (temp_use BoxDmd_simple) 1);
by (atac 1);
by (rtac classical 1);
by (rtac (temp_use STL2) 1);
@@ -841,7 +842,7 @@
by (asm_full_simp_tac (simpset() addsimps [split_box_conj,temp_use NotDmd,not_angle]) 1);
qed "WF_leadsto";
-val prems = goal thy
+val prems = goal (the_context ())
"[| |- $P & N --> P` | Q`; \
\ |- ($P & N) & <A>_v --> Q`; \
\ |- []P & []N & []F --> <>Enabled(<A>_v) |] \
@@ -851,26 +852,26 @@
by (TRYALL (ares_tac prems));
by (eres_inst_tac [("F","F")] dup_boxE 1);
by (merge_temp_box_tac 1);
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (clarsimp_tac (temp_css addsimps2 [SF_def]) 1);
-by (rtac (temp_use STL2) 1);
+by (rtac (temp_use STL2) 1);
by (etac mp 1);
by (resolve_tac (map temp_use (prems RL [STL4])) 1);
by (asm_simp_tac (simpset() addsimps [split_box_conj, STL3]) 1);
qed "SF1";
-val [prem1,prem2,prem3,prem4] = goal thy
+val [prem1,prem2,prem3,prem4] = goal (the_context ())
"[| |- N & <B>_f --> <M>_g; \
\ |- $P & P` & <N & A>_f --> B; \
\ |- P & Enabled(<M>_g) --> Enabled(<A>_f); \
\ |- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P |] \
\ ==> |- []N & WF(A)_f & []F --> WF(M)_g";
-by (clarsimp_tac (temp_css addSDs2 [BoxWFI, (temp_use BoxDmdBox) RS iffD2]
+by (clarsimp_tac (temp_css addSDs2 [BoxWFI, (temp_use BoxDmdBox) RS iffD2]
addsimps2 [read_instantiate [("A","M")] WF_def]) 1);
by (eres_inst_tac [("F","F")] dup_boxE 1);
by (merge_temp_box_tac 1);
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (clarsimp_tac (temp_css addSIs2
[(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1);
@@ -880,36 +881,36 @@
by (rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1);
by (asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1);
by (merge_act_box_tac 1);
-by (forward_tac [temp_use prem4] 1);
+by (forward_tac [temp_use prem4] 1);
by (TRYALL atac);
-by (dtac (temp_use STL6) 1);
+by (dtac (temp_use STL6) 1);
by (atac 1);
by (eres_inst_tac [("V","sigmaa |= <>[]P")] thin_rl 1);
by (eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1);
by (dtac (temp_use BoxWFI) 1);
by (eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1);
by (merge_temp_box_tac 1);
-by (etac DmdImpldup 1);
+by (etac DmdImpldup 1);
by (atac 1);
by (auto_tac (temp_css addsimps2 [split_box_conj,STL3,WF_Box,box_stp_act]));
by (force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1);
by (rtac (temp_use STL2) 1);
-by (force_tac (temp_css addsimps2 [WF_def,split_box_conj] addSEs2 [mp]
+by (force_tac (temp_css addsimps2 [WF_def,split_box_conj] addSEs2 [mp]
addSIs2 [InitDmd, prem3 RS STL4]) 1);
qed "WF2";
-val [prem1,prem2,prem3,prem4] = goal thy
+val [prem1,prem2,prem3,prem4] = goal (the_context ())
"[| |- N & <B>_f --> <M>_g; \
\ |- $P & P` & <N & A>_f --> B; \
\ |- P & Enabled(<M>_g) --> Enabled(<A>_f); \
\ |- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P |] \
\ ==> |- []N & SF(A)_f & []F --> SF(M)_g";
-by (clarsimp_tac (temp_css addSDs2 [BoxSFI]
+by (clarsimp_tac (temp_css addSDs2 [BoxSFI]
addsimps2 [read_instantiate [("A","M")] SF_def]) 1);
by (eres_inst_tac [("F","F")] dup_boxE 1);
by (eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1);
by (merge_temp_box_tac 1);
-by (etac STL4Edup 1);
+by (etac STL4Edup 1);
by (atac 1);
by (clarsimp_tac (temp_css addSIs2
[(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1);
@@ -919,19 +920,19 @@
by (rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1);
by (asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1);
by (merge_act_box_tac 1);
-by (forward_tac [temp_use prem4] 1);
+by (forward_tac [temp_use prem4] 1);
by (TRYALL atac);
by (eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1);
by (dtac (temp_use BoxSFI) 1);
by (eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1);
by (eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1);
by (merge_temp_box_tac 1);
-by (etac DmdImpldup 1);
+by (etac DmdImpldup 1);
by (atac 1);
by (auto_tac (temp_css addsimps2 [split_box_conj,STL3,SF_Box,box_stp_act]));
by (force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1);
by (rtac (temp_use STL2) 1);
-by (force_tac (temp_css addsimps2 [SF_def,split_box_conj] addSEs2 [mp,InfImpl]
+by (force_tac (temp_css addsimps2 [SF_def,split_box_conj] addSEs2 [mp,InfImpl]
addSIs2 [prem3]) 1);
qed "SF2";
@@ -940,7 +941,7 @@
(* ------------------------------------------------------------------------- *)
section "Well-founded orderings";
-val p1::prems = goal thy
+val p1::prems = goal (the_context ())
"[| wf r; \
\ !!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y)) \
\ |] ==> sigma |= F x ~> G";
@@ -962,7 +963,7 @@
by (force_tac (temp_css addsimps2 Init_defs) 1);
by (clarsimp_tac (temp_css addsimps2 [leadsto_exists,not_square]@more_temp_simps) 1);
by (etac wf_leadsto 1);
-by (rtac (temp_use ensures_simple) 1);
+by (rtac (temp_use ensures_simple) 1);
by (TRYALL atac);
by (auto_tac (temp_css addsimps2 [square_def,angle_def]));
qed "wf_not_box_decrease";
@@ -974,13 +975,13 @@
(* If there are infinitely many steps where v decreases, then there
have to be infinitely many non-stuttering steps where v doesn't decrease.
*)
-val [prem] = goal thy
+val [prem] = goal (the_context ())
"wf r ==> |- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v";
by (Clarsimp_tac 1);
by (rtac ccontr 1);
by (asm_full_simp_tac (simpset() addsimps not_angle::more_temp_simps) 1);
by (dtac (prem RS (temp_use wf_not_dmd_box_decrease)) 1);
-by (dtac (temp_use BoxDmdDmdBox) 1);
+by (dtac (temp_use BoxDmdDmdBox) 1);
by (atac 1);
by (subgoal_tac "sigma |= []<>((#False)::action)" 1);
by (Force_tac 1);
@@ -995,8 +996,8 @@
Goal "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)";
by (Clarsimp_tac 1);
by (subgoal_tac "sigma |= []<><~( (n`,$n) : #less_than )>_n" 1);
- by (etac thin_rl 1);
- by (etac STL4E 1);
+ by (etac thin_rl 1);
+ by (etac STL4E 1);
by (rtac DmdImpl 1);
by (clarsimp_tac (temp_css addsimps2 [angle_def]) 1);
by (rtac (temp_use wf_box_dmd_decrease) 1);
@@ -1009,10 +1010,10 @@
(* ------------------------------------------------------------------------- *)
section "Flexible quantification";
-val [prem1,prem2] = goal thy
+val [prem1,prem2] = goal (the_context ())
"[| basevars vs; (!!x. basevars (x,vs) ==> sigma |= F x) |]\
\ ==> sigma |= (AALL x. F x)";
-by (auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE]
+by (auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE]
addSIs2 [prem1] addSDs2 [prem2]));
qed "aallI";
@@ -1023,14 +1024,14 @@
qed "aallE";
(* monotonicity of quantification *)
-val [min,maj] = goal thy
+val [min,maj] = goal (the_context ())
"[| sigma |= EEX x. F x; !!x. sigma |= F x --> G x |] ==> sigma |= EEX x. G x";
by (rtac (unit_base RS (min RS eexE)) 1);
by (rtac (temp_use eexI) 1);
by (etac ((rewrite_rule intensional_rews maj) RS mp) 1);
qed "eex_mono";
-val [min,maj] = goal thy
+val [min,maj] = goal (the_context ())
"[| sigma |= AALL x. F(x); !!x. sigma |= F(x) --> G(x) |] ==> sigma |= AALL x. G(x)";
by (rtac (unit_base RS aallI) 1);
by (rtac ((rewrite_rule intensional_rews maj) RS mp) 1);
@@ -1038,7 +1039,7 @@
qed "aall_mono";
(* Derived history introduction rule *)
-val [p1,p2,p3,p4,p5] = goal thy
+val [p1,p2,p3,p4,p5] = goal (the_context ())
"[| sigma |= Init I; sigma |= []N; basevars vs; \
\ (!!h. basevars(h,vs) ==> |- I & h = ha --> HI h); \
\ (!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)) \
@@ -1046,7 +1047,7 @@
by (rtac ((temp_use history) RS eexE) 1);
by (rtac p3 1);
by (rtac (temp_use eexI) 1);
-by (Clarsimp_tac 1);
+by (Clarsimp_tac 1);
by (rtac conjI 1);
by (cut_facts_tac [p2] 2);
by (merge_box_tac 2);
--- a/src/HOL/TLA/TLA.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/TLA.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(*
+(*
File: TLA/TLA.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
@@ -9,32 +10,34 @@
The temporal level of TLA.
*)
-TLA = Init +
+theory TLA
+imports Init
+begin
consts
(** abstract syntax **)
- Box :: ('w::world) form => temporal
- Dmd :: ('w::world) form => temporal
- leadsto :: ['w::world form, 'v::world form] => temporal
- Stable :: stpred => temporal
- WF :: [action, 'a stfun] => temporal
- SF :: [action, 'a stfun] => temporal
+ Box :: "('w::world) form => temporal"
+ Dmd :: "('w::world) form => temporal"
+ leadsto :: "['w::world form, 'v::world form] => temporal"
+ Stable :: "stpred => temporal"
+ WF :: "[action, 'a stfun] => temporal"
+ SF :: "[action, 'a stfun] => temporal"
(* Quantification over (flexible) state variables *)
- EEx :: ('a stfun => temporal) => temporal (binder "Eex " 10)
- AAll :: ('a stfun => temporal) => temporal (binder "Aall " 10)
+ EEx :: "('a stfun => temporal) => temporal" (binder "Eex " 10)
+ AAll :: "('a stfun => temporal) => temporal" (binder "Aall " 10)
(** concrete syntax **)
syntax
- "_Box" :: lift => lift ("([]_)" [40] 40)
- "_Dmd" :: lift => lift ("(<>_)" [40] 40)
- "_leadsto" :: [lift,lift] => lift ("(_ ~> _)" [23,22] 22)
- "_stable" :: lift => lift ("(stable/ _)")
- "_WF" :: [lift,lift] => lift ("(WF'(_')'_(_))" [0,60] 55)
- "_SF" :: [lift,lift] => lift ("(SF'(_')'_(_))" [0,60] 55)
+ "_Box" :: "lift => lift" ("([]_)" [40] 40)
+ "_Dmd" :: "lift => lift" ("(<>_)" [40] 40)
+ "_leadsto" :: "[lift,lift] => lift" ("(_ ~> _)" [23,22] 22)
+ "_stable" :: "lift => lift" ("(stable/ _)")
+ "_WF" :: "[lift,lift] => lift" ("(WF'(_')'_(_))" [0,60] 55)
+ "_SF" :: "[lift,lift] => lift" ("(SF'(_')'_(_))" [0,60] 55)
- "_EEx" :: [idts, lift] => lift ("(3EEX _./ _)" [0,10] 10)
- "_AAll" :: [idts, lift] => lift ("(3AALL _./ _)" [0,10] 10)
+ "_EEx" :: "[idts, lift] => lift" ("(3EEX _./ _)" [0,10] 10)
+ "_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10)
translations
"_Box" == "Box"
@@ -56,43 +59,46 @@
"sigma |= AALL x. F" <= "_AAll x F sigma"
syntax (xsymbols)
- "_Box" :: lift => lift ("(\\<box>_)" [40] 40)
- "_Dmd" :: lift => lift ("(\\<diamond>_)" [40] 40)
- "_leadsto" :: [lift,lift] => lift ("(_ \\<leadsto> _)" [23,22] 22)
- "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
- "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+ "_Box" :: "lift => lift" ("(\<box>_)" [40] 40)
+ "_Dmd" :: "lift => lift" ("(\<diamond>_)" [40] 40)
+ "_leadsto" :: "[lift,lift] => lift" ("(_ \<leadsto> _)" [23,22] 22)
+ "_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
+ "_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
syntax (HTML output)
- "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
- "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+ "_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
+ "_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
-rules
+axioms
(* Definitions of derived operators *)
- dmd_def "TEMP <>F == TEMP ~[]~F"
- boxInit "TEMP []F == TEMP []Init F"
- leadsto_def "TEMP F ~> G == TEMP [](Init F --> <>G)"
- stable_def "TEMP stable P == TEMP []($P --> P$)"
- WF_def "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
- SF_def "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v"
- aall_def "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
+ dmd_def: "TEMP <>F == TEMP ~[]~F"
+ boxInit: "TEMP []F == TEMP []Init F"
+ leadsto_def: "TEMP F ~> G == TEMP [](Init F --> <>G)"
+ stable_def: "TEMP stable P == TEMP []($P --> P$)"
+ WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
+ SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v"
+ aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
(* Base axioms for raw TLA. *)
- normalT "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *)
- reflT "|- []F --> F" (* F::temporal *)
- transT "|- []F --> [][]F" (* polymorphic *)
- linT "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
- discT "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
- primeI "|- []P --> Init P`"
- primeE "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
- indT "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
- allT "|- (ALL x. [](F x)) = ([](ALL x. F x))"
+ normalT: "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *)
+ reflT: "|- []F --> F" (* F::temporal *)
+ transT: "|- []F --> [][]F" (* polymorphic *)
+ linT: "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
+ discT: "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
+ primeI: "|- []P --> Init P`"
+ primeE: "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
+ indT: "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
+ allT: "|- (ALL x. [](F x)) = ([](ALL x. F x))"
- necT "|- F ==> |- []F" (* polymorphic *)
+ necT: "|- F ==> |- []F" (* polymorphic *)
(* Flexible quantification: refinement mappings, history variables *)
- eexI "|- F x --> (EEX x. F x)"
- eexE "[| sigma |= (EEX x. F x); basevars vs;
- (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
- |] ==> G sigma"
- history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
+ eexI: "|- F x --> (EEX x. F x)"
+ eexE: "[| sigma |= (EEX x. F x); basevars vs;
+ (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
+ |] ==> G sigma"
+ history: "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end