src/HOL/TLA/Memory/MemClerk.ML
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 4089 96fba19bcbe2
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:        MemClerk.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    RPC-Memory example: Memory clerk specification (ML file)
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
val MC_action_defs = 
wenzelm@3807
    10
   [MClkInit_def RS inteq_reflection]
wenzelm@3807
    11
   @ [MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
wenzelm@3807
    12
wenzelm@3807
    13
val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
wenzelm@3807
    14
wenzelm@3807
    15
(* The Clerk engages in an action for process p only if there is an outstanding,
wenzelm@3807
    16
   unanswered call for that process.
wenzelm@3807
    17
*)
wenzelm@3807
    18
wenzelm@3807
    19
qed_goal "MClkidle" MemClerk.thy
wenzelm@3807
    20
   ".~ $(Calling send p) .& ($(cst@p) .= #clkA) .-> .~ MClkNext send rcv cst p"
wenzelm@3807
    21
   (fn _ => [ auto_tac (!claset,
wenzelm@3807
    22
                        !simpset addsimps (MC_action_defs @ [Return_def]))
wenzelm@3807
    23
            ]);
wenzelm@3807
    24
wenzelm@3807
    25
qed_goal "MClkbusy" MemClerk.thy
wenzelm@3807
    26
   "$(Calling rcv p) .-> .~ MClkNext send rcv cst p"
wenzelm@3807
    27
   (fn _ => [ auto_tac (!claset,
wenzelm@3807
    28
                        !simpset addsimps (MC_action_defs @ [Call_def]))
wenzelm@3807
    29
            ]);
wenzelm@3807
    30
wenzelm@3807
    31
(* unlifted versions as introduction rules *)
wenzelm@3807
    32
wenzelm@3807
    33
bind_thm("MClkidleI", action_mp MClkidle);
wenzelm@3807
    34
bind_thm("MClkbusyI", action_mp MClkbusy);
wenzelm@3807
    35
wenzelm@3807
    36
(* Enabledness of actions *)
wenzelm@3807
    37
wenzelm@3807
    38
qed_goal "MClkFwd_enabled" MemClerk.thy
wenzelm@3807
    39
   "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
wenzelm@3807
    40
\        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkA)  \
wenzelm@3807
    41
\        .-> $(Enabled (MClkFwd send rcv cst p))"
wenzelm@3807
    42
   (fn _ => [action_simp_tac (!simpset addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
wenzelm@3807
    43
                             [] [base_enabled,Pair_inject] 1]);
wenzelm@3807
    44
wenzelm@3807
    45
qed_goal "MClkFwd_ch_enabled" MemClerk.thy
wenzelm@3807
    46
   "Enabled (MClkFwd send rcv cst p) s  \
wenzelm@3807
    47
\   ==> Enabled (<MClkFwd send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>) s"
wenzelm@3807
    48
   (fn [prem] => [auto_tac (!claset addSIs [prem RS enabled_mono],
wenzelm@3807
    49
			    !simpset addsimps [angle_def,MClkFwd_def])
wenzelm@3807
    50
		 ]);
wenzelm@3807
    51
wenzelm@3807
    52
qed_goal "MClkReply_change" MemClerk.thy
wenzelm@3807
    53
   "MClkReply send rcv cst p .-> <MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>"
wenzelm@3807
    54
   (fn _ => [auto_tac (action_css addsimps2 [angle_def,MClkReply_def]
wenzelm@3807
    55
			          addEs2 [Return_changedE])
wenzelm@3807
    56
            ]);
wenzelm@3807
    57
wenzelm@3807
    58
qed_goal "MClkReply_enabled" MemClerk.thy
wenzelm@3807
    59
   "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
wenzelm@3807
    60
\        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkB)  \
wenzelm@3807
    61
\        .-> $(Enabled (<MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>))"
wenzelm@3807
    62
   (fn _ => [action_simp_tac (!simpset) [MClkReply_change RSN (2,enabled_mono)] [] 1,
wenzelm@3807
    63
	     action_simp_tac (!simpset addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
wenzelm@3807
    64
                             [] [base_enabled,Pair_inject] 1
wenzelm@3807
    65
	    ]);
wenzelm@3807
    66
wenzelm@3807
    67
qed_goal "MClkReplyNotRetry" MemClerk.thy
wenzelm@3807
    68
   "MClkReply send rcv cst p .-> .~(MClkRetry send rcv cst p)"
wenzelm@3807
    69
   (fn _ => [ auto_tac (!claset,
wenzelm@3807
    70
			!simpset addsimps [MClkReply_def,MClkRetry_def]) 
wenzelm@3807
    71
	    ]);