src/HOL/TLA/Memory/MemClerk.ML
changeset 3807 82a99b090d9d
child 4089 96fba19bcbe2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TLA/Memory/MemClerk.ML	Wed Oct 08 11:50:33 1997 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(* 
     1.5 +    File:        MemClerk.ML
     1.6 +    Author:      Stephan Merz
     1.7 +    Copyright:   1997 University of Munich
     1.8 +
     1.9 +    RPC-Memory example: Memory clerk specification (ML file)
    1.10 +*)
    1.11 +
    1.12 +val MC_action_defs = 
    1.13 +   [MClkInit_def RS inteq_reflection]
    1.14 +   @ [MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
    1.15 +
    1.16 +val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
    1.17 +
    1.18 +(* The Clerk engages in an action for process p only if there is an outstanding,
    1.19 +   unanswered call for that process.
    1.20 +*)
    1.21 +
    1.22 +qed_goal "MClkidle" MemClerk.thy
    1.23 +   ".~ $(Calling send p) .& ($(cst@p) .= #clkA) .-> .~ MClkNext send rcv cst p"
    1.24 +   (fn _ => [ auto_tac (!claset,
    1.25 +                        !simpset addsimps (MC_action_defs @ [Return_def]))
    1.26 +            ]);
    1.27 +
    1.28 +qed_goal "MClkbusy" MemClerk.thy
    1.29 +   "$(Calling rcv p) .-> .~ MClkNext send rcv cst p"
    1.30 +   (fn _ => [ auto_tac (!claset,
    1.31 +                        !simpset addsimps (MC_action_defs @ [Call_def]))
    1.32 +            ]);
    1.33 +
    1.34 +(* unlifted versions as introduction rules *)
    1.35 +
    1.36 +bind_thm("MClkidleI", action_mp MClkidle);
    1.37 +bind_thm("MClkbusyI", action_mp MClkbusy);
    1.38 +
    1.39 +(* Enabledness of actions *)
    1.40 +
    1.41 +qed_goal "MClkFwd_enabled" MemClerk.thy
    1.42 +   "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
    1.43 +\        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkA)  \
    1.44 +\        .-> $(Enabled (MClkFwd send rcv cst p))"
    1.45 +   (fn _ => [action_simp_tac (!simpset addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
    1.46 +                             [] [base_enabled,Pair_inject] 1]);
    1.47 +
    1.48 +qed_goal "MClkFwd_ch_enabled" MemClerk.thy
    1.49 +   "Enabled (MClkFwd send rcv cst p) s  \
    1.50 +\   ==> Enabled (<MClkFwd send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>) s"
    1.51 +   (fn [prem] => [auto_tac (!claset addSIs [prem RS enabled_mono],
    1.52 +			    !simpset addsimps [angle_def,MClkFwd_def])
    1.53 +		 ]);
    1.54 +
    1.55 +qed_goal "MClkReply_change" MemClerk.thy
    1.56 +   "MClkReply send rcv cst p .-> <MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>"
    1.57 +   (fn _ => [auto_tac (action_css addsimps2 [angle_def,MClkReply_def]
    1.58 +			          addEs2 [Return_changedE])
    1.59 +            ]);
    1.60 +
    1.61 +qed_goal "MClkReply_enabled" MemClerk.thy
    1.62 +   "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
    1.63 +\        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkB)  \
    1.64 +\        .-> $(Enabled (<MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>))"
    1.65 +   (fn _ => [action_simp_tac (!simpset) [MClkReply_change RSN (2,enabled_mono)] [] 1,
    1.66 +	     action_simp_tac (!simpset addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
    1.67 +                             [] [base_enabled,Pair_inject] 1
    1.68 +	    ]);
    1.69 +
    1.70 +qed_goal "MClkReplyNotRetry" MemClerk.thy
    1.71 +   "MClkReply send rcv cst p .-> .~(MClkRetry send rcv cst p)"
    1.72 +   (fn _ => [ auto_tac (!claset,
    1.73 +			!simpset addsimps [MClkReply_def,MClkRetry_def]) 
    1.74 +	    ]);