--- a/src/HOL/TLA/Action.ML Mon Oct 18 16:16:03 1999 +0200
+++ b/src/HOL/TLA/Action.ML Mon Oct 18 18:38:21 1999 +0200
@@ -201,11 +201,20 @@
(* A rule that combines enabledI and baseE, but generates fewer possible instantiations *)
qed_goal "base_enabled" Action.thy
+ "[| basevars vs; ? c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
+ (fn prems => [cut_facts_tac prems 1,
+ etac exE 1, etac baseE 1,
+ rtac (action_use enabledI) 1,
+ etac allE 1, etac mp 1, atac 1
+ ]);
+
+(*** old version immediately generates schematic variable
+qed_goal "base_enabled" Action.thy
"[| basevars vs; !!u. vs u = c s ==> A (s,u) |] ==> s |= Enabled A"
(fn prems => [cut_facts_tac prems 1,
etac baseE 1, rtac (action_use enabledI) 1,
REPEAT (ares_tac prems 1)]);
-
+***)
(* ================================ action_simp_tac ================================== *)
--- a/src/HOL/TLA/Inc/Inc.ML Mon Oct 18 16:16:03 1999 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML Mon Oct 18 18:38:21 1999 +0200
@@ -91,7 +91,8 @@
(fn _ => [Clarsimp_tac 1,
res_inst_tac [("F","gamma1")] enabled_mono 1,
enabled_tac Inc_base 1,
- auto_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def])
+ force_tac (Inc_css addsimps2 [gamma1_def]) 1,
+ force_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def]) 1
]);
qed_goal "g1_leadsto_a1" Inc.thy
@@ -112,7 +113,8 @@
(fn _ => [Clarsimp_tac 1,
res_inst_tac [("F","gamma2")] enabled_mono 1,
enabled_tac Inc_base 1,
- auto_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def])
+ force_tac (Inc_css addsimps2 [gamma2_def]) 1,
+ force_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def]) 1
]);
qed_goal "g2_leadsto_a2" Inc.thy
@@ -131,7 +133,8 @@
(fn _ => [Clarsimp_tac 1,
res_inst_tac [("F","beta2")] enabled_mono 1,
enabled_tac Inc_base 1,
- auto_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def])
+ force_tac (Inc_css addsimps2 [beta2_def]) 1,
+ force_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def]) 1
]);
qed_goal "b2_leadsto_g2" Inc.thy
@@ -173,8 +176,8 @@
(fn _ => [Clarsimp_tac 1,
res_inst_tac [("F","alpha1")] enabled_mono 1,
enabled_tac Inc_base 1,
- auto_tac (Inc_css addIs2 [sym]
- addsimps2 [angle_def,alpha1_def,N1_def] @ PsiInv_defs)
+ force_tac (Inc_css addsimps2 (alpha1_def::PsiInv_defs)) 1,
+ force_tac (Inc_css addsimps2 [angle_def,alpha1_def,N1_def]) 1
]);
qed_goal "a1_leadsto_b1" Inc.thy
@@ -218,7 +221,8 @@
(fn _ => [Clarsimp_tac 1,
res_inst_tac [("F","beta1")] enabled_mono 1,
enabled_tac Inc_base 1,
- auto_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def])
+ force_tac (Inc_css addsimps2 [beta1_def]) 1,
+ force_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def]) 1
]);
(* Now assemble the bits and pieces to prove that Psi is fair. *)
--- a/src/HOL/TLA/Memory/MemClerk.ML Mon Oct 18 16:16:03 1999 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.ML Mon Oct 18 18:38:21 1999 +0200
@@ -32,7 +32,7 @@
\ |- Calling send p & ~Calling rcv p & cst!p = #clkA \
\ --> Enabled (MClkFwd send rcv cst p)"
(fn _ => [action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
- [] [base_enabled,Pair_inject] 1]);
+ [exI] [base_enabled,Pair_inject] 1]);
qed_goal "MClkFwd_ch_enabled" MemClerk.thy
"|- Enabled (MClkFwd send rcv cst p) --> \
@@ -53,7 +53,7 @@
\ --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
(fn _ => [action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1,
action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
- [] [base_enabled,Pair_inject] 1
+ [exI] [base_enabled,Pair_inject] 1
]);
qed_goal "MClkReplyNotRetry" MemClerk.thy
--- a/src/HOL/TLA/Memory/Memory.ML Mon Oct 18 16:16:03 1999 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML Mon Oct 18 18:38:21 1999 +0200
@@ -64,18 +64,17 @@
\ --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
(K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1,
action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def])
- [] [base_enabled,Pair_inject] 1
- ]);
+ [exI] [base_enabled,Pair_inject] 1
+ ]);
qed_goal "ReadInner_enabled" Memory.thy
"!!p. basevars (rtrner ch ! p, rs!p) ==> \
\ |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
(fn _ => [case_tac "l : MemLoc" 1,
ALLGOALS
- (action_simp_tac
- (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,
- RdRequest_def])
- [] [base_enabled,Pair_inject])
+ (force_tac (mem_css addsimps2 [ReadInner_def,GoodRead_def,
+ BadRead_def,RdRequest_def]
+ addSIs2 [exI] addSEs2 [base_enabled]))
]);
qed_goal "WriteInner_enabled" Memory.thy
@@ -83,10 +82,10 @@
\ |- Calling ch p & (arg<ch!p> = #(write l v)) \
\ --> Enabled (WriteInner ch mm rs p l v)"
(fn _ => [case_tac "l:MemLoc & v:MemVal" 1,
- ALLGOALS (action_simp_tac
- (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
- WrRequest_def] delsimps [disj_not1])
- [] [base_enabled,Pair_inject])
+ ALLGOALS
+ (force_tac (mem_css addsimps2 [WriteInner_def,GoodWrite_def,
+ BadWrite_def,WrRequest_def]
+ addSIs2 [exI] addSEs2 [base_enabled]))
]);
qed_goal "ReadResult" Memory.thy
--- a/src/HOL/TLA/Memory/RPC.ML Mon Oct 18 16:16:03 1999 +0200
+++ b/src/HOL/TLA/Memory/RPC.ML Mon Oct 18 18:38:21 1999 +0200
@@ -44,7 +44,7 @@
"!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> \
\ |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
(fn _ => [action_simp_tac (simpset() addsimps [RPCFail_def,Return_def,caller_def,rtrner_def])
- [] [base_enabled,Pair_inject] 1
+ [exI] [base_enabled,Pair_inject] 1
]);
qed_goal "RPCReply_enabled" RPC.thy
@@ -52,5 +52,5 @@
\ |- ~Calling rcv p & Calling send p & rst!p = #rpcB \
\ --> Enabled (RPCReply send rcv rst p)"
(fn _ => [action_simp_tac (simpset() addsimps [RPCReply_def,Return_def,caller_def,rtrner_def])
- [] [base_enabled,Pair_inject] 1]);
+ [exI] [base_enabled,Pair_inject] 1]);
--- a/src/HOL/TLA/README.html Mon Oct 18 16:16:03 1999 +0200
+++ b/src/HOL/TLA/README.html Mon Oct 18 18:38:21 1999 +0200
@@ -28,7 +28,7 @@
</UL>
Please consult the
-<A HREF="http://www4.in.tum.de/~merz/papers/IsaTLADesign.ps">design notes</A>
+<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
for further information regarding the setup and use of this encoding
of TLA.
@@ -44,7 +44,7 @@
<LI><A HREF="Memory/index.html">Memory</A>: a verification of (the
untimed part of) Broy and Lamport's <em>RPC-Memory</em> case study,
more fully explained in LNCS 1169 (the
- <A HREF="http://www4.in.tum.de/~merz/papers/RPCMemory.html">TLA
+ <A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
solution</A> is available separately).
</UL>