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