src/HOL/TLA/Memory/MemClerk.ML
changeset 6255 db63752140c7
parent 4089 96fba19bcbe2
child 7881 1b1db39a110b
     1.1 --- a/src/HOL/TLA/Memory/MemClerk.ML	Mon Feb 08 13:02:42 1999 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerk.ML	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -3,69 +3,60 @@
     1.4      Author:      Stephan Merz
     1.5      Copyright:   1997 University of Munich
     1.6  
     1.7 -    RPC-Memory example: Memory clerk specification (ML file)
     1.8 +    RPC-Memory example: Memory clerk specification (theorems and proofs)
     1.9  *)
    1.10  
    1.11  val MC_action_defs = 
    1.12 -   [MClkInit_def RS inteq_reflection]
    1.13 -   @ [MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
    1.14 +   [MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
    1.15  
    1.16  val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
    1.17  
    1.18 +val mem_css = (claset(), simpset());
    1.19 +
    1.20  (* The Clerk engages in an action for process p only if there is an outstanding,
    1.21     unanswered call for that process.
    1.22  *)
    1.23  
    1.24  qed_goal "MClkidle" MemClerk.thy
    1.25 -   ".~ $(Calling send p) .& ($(cst@p) .= #clkA) .-> .~ MClkNext send rcv cst p"
    1.26 -   (fn _ => [ auto_tac (claset(),
    1.27 -                        simpset() addsimps (MC_action_defs @ [Return_def]))
    1.28 -            ]);
    1.29 +   "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"
    1.30 +   (fn _ => [ auto_tac (mem_css addsimps2 (Return_def::MC_action_defs)) ]);
    1.31  
    1.32  qed_goal "MClkbusy" MemClerk.thy
    1.33 -   "$(Calling rcv p) .-> .~ MClkNext send rcv cst p"
    1.34 -   (fn _ => [ auto_tac (claset(),
    1.35 -                        simpset() addsimps (MC_action_defs @ [Call_def]))
    1.36 -            ]);
    1.37 -
    1.38 -(* unlifted versions as introduction rules *)
    1.39 -
    1.40 -bind_thm("MClkidleI", action_mp MClkidle);
    1.41 -bind_thm("MClkbusyI", action_mp MClkbusy);
    1.42 +   "|- $Calling rcv p --> ~MClkNext send rcv cst p"
    1.43 +   (fn _ => [ auto_tac (mem_css addsimps2 (MC_action_defs @ [Call_def])) ]);
    1.44  
    1.45  (* Enabledness of actions *)
    1.46  
    1.47  qed_goal "MClkFwd_enabled" MemClerk.thy
    1.48 -   "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
    1.49 -\        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkA)  \
    1.50 -\        .-> $(Enabled (MClkFwd send rcv cst p))"
    1.51 +   "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \
    1.52 +\        |- Calling send p & ~Calling rcv p & cst!p = #clkA  \
    1.53 +\           --> Enabled (MClkFwd send rcv cst p)"
    1.54     (fn _ => [action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
    1.55                               [] [base_enabled,Pair_inject] 1]);
    1.56  
    1.57  qed_goal "MClkFwd_ch_enabled" MemClerk.thy
    1.58 -   "Enabled (MClkFwd send rcv cst p) s  \
    1.59 -\   ==> Enabled (<MClkFwd send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>) s"
    1.60 -   (fn [prem] => [auto_tac (claset() addSIs [prem RS enabled_mono],
    1.61 -			    simpset() addsimps [angle_def,MClkFwd_def])
    1.62 -		 ]);
    1.63 +   "|- Enabled (MClkFwd send rcv cst p)  -->  \
    1.64 +\      Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
    1.65 +   (fn _ => [auto_tac (mem_css addSEs2 [enabled_mono]
    1.66 +	                       addsimps2 [angle_def,MClkFwd_def])
    1.67 +  	    ]);
    1.68  
    1.69  qed_goal "MClkReply_change" MemClerk.thy
    1.70 -   "MClkReply send rcv cst p .-> <MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>"
    1.71 -   (fn _ => [auto_tac (action_css addsimps2 [angle_def,MClkReply_def]
    1.72 -			          addEs2 [Return_changedE])
    1.73 +   "|- MClkReply send rcv cst p --> <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
    1.74 +   (fn _ => [auto_tac (mem_css addsimps2 [angle_def,MClkReply_def]
    1.75 +			       addEs2 [Return_changed])
    1.76              ]);
    1.77  
    1.78  qed_goal "MClkReply_enabled" MemClerk.thy
    1.79 -   "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
    1.80 -\        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkB)  \
    1.81 -\        .-> $(Enabled (<MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>))"
    1.82 +   "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \
    1.83 +\        |- Calling send p & ~Calling rcv p & cst!p = #clkB  \
    1.84 +\           --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
    1.85     (fn _ => [action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1,
    1.86  	     action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
    1.87                               [] [base_enabled,Pair_inject] 1
    1.88  	    ]);
    1.89  
    1.90  qed_goal "MClkReplyNotRetry" MemClerk.thy
    1.91 -   "MClkReply send rcv cst p .-> .~(MClkRetry send rcv cst p)"
    1.92 -   (fn _ => [ auto_tac (claset(),
    1.93 -			simpset() addsimps [MClkReply_def,MClkRetry_def]) 
    1.94 -	    ]);
    1.95 +   "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
    1.96 +   (fn _ => [ auto_tac (mem_css addsimps2 [MClkReply_def,MClkRetry_def]) ]);
    1.97 +