# HG changeset patch # User wenzelm # Date 940264701 -7200 # Node ID 1b1db39a110bcbac12862c11e6b15e2835424f3c # Parent 62fb24e28e5ed8515bc40fa8dc9af16ae715b5b1 update by Stephan Merz; diff -r 62fb24e28e5e -r 1b1db39a110b src/HOL/TLA/Action.ML --- 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 ================================== *) diff -r 62fb24e28e5e -r 1b1db39a110b src/HOL/TLA/Inc/Inc.ML --- 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. *) diff -r 62fb24e28e5e -r 1b1db39a110b src/HOL/TLA/Memory/MemClerk.ML --- 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 (_(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 diff -r 62fb24e28e5e -r 1b1db39a110b src/HOL/TLA/Memory/Memory.ML --- 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 (_(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 = #(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 = #(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 diff -r 62fb24e28e5e -r 1b1db39a110b src/HOL/TLA/Memory/RPC.ML --- 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]); diff -r 62fb24e28e5e -r 1b1db39a110b src/HOL/TLA/README.html --- 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 @@ Please consult the -design notes +design notes for further information regarding the setup and use of this encoding of TLA. @@ -44,7 +44,7 @@
  • Memory: a verification of (the untimed part of) Broy and Lamport's RPC-Memory case study, more fully explained in LNCS 1169 (the - TLA + TLA solution is available separately).