src/HOL/TLA/Memory/MemClerk.ML
author wenzelm
Mon Feb 08 13:02:56 1999 +0100 (1999-02-08)
changeset 6255 db63752140c7
parent 4089 96fba19bcbe2
child 7881 1b1db39a110b
permissions -rw-r--r--
updated (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@6255
     6
    RPC-Memory example: Memory clerk specification (theorems and proofs)
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
val MC_action_defs = 
wenzelm@6255
    10
   [MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
wenzelm@3807
    11
wenzelm@3807
    12
val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
wenzelm@3807
    13
wenzelm@6255
    14
val mem_css = (claset(), simpset());
wenzelm@6255
    15
wenzelm@3807
    16
(* The Clerk engages in an action for process p only if there is an outstanding,
wenzelm@3807
    17
   unanswered call for that process.
wenzelm@3807
    18
*)
wenzelm@3807
    19
wenzelm@3807
    20
qed_goal "MClkidle" MemClerk.thy
wenzelm@6255
    21
   "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"
wenzelm@6255
    22
   (fn _ => [ auto_tac (mem_css addsimps2 (Return_def::MC_action_defs)) ]);
wenzelm@3807
    23
wenzelm@3807
    24
qed_goal "MClkbusy" MemClerk.thy
wenzelm@6255
    25
   "|- $Calling rcv p --> ~MClkNext send rcv cst p"
wenzelm@6255
    26
   (fn _ => [ auto_tac (mem_css addsimps2 (MC_action_defs @ [Call_def])) ]);
wenzelm@3807
    27
wenzelm@3807
    28
(* Enabledness of actions *)
wenzelm@3807
    29
wenzelm@3807
    30
qed_goal "MClkFwd_enabled" MemClerk.thy
wenzelm@6255
    31
   "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \
wenzelm@6255
    32
\        |- Calling send p & ~Calling rcv p & cst!p = #clkA  \
wenzelm@6255
    33
\           --> Enabled (MClkFwd send rcv cst p)"
wenzelm@4089
    34
   (fn _ => [action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
wenzelm@3807
    35
                             [] [base_enabled,Pair_inject] 1]);
wenzelm@3807
    36
wenzelm@3807
    37
qed_goal "MClkFwd_ch_enabled" MemClerk.thy
wenzelm@6255
    38
   "|- Enabled (MClkFwd send rcv cst p)  -->  \
wenzelm@6255
    39
\      Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
wenzelm@6255
    40
   (fn _ => [auto_tac (mem_css addSEs2 [enabled_mono]
wenzelm@6255
    41
	                       addsimps2 [angle_def,MClkFwd_def])
wenzelm@6255
    42
  	    ]);
wenzelm@3807
    43
wenzelm@3807
    44
qed_goal "MClkReply_change" MemClerk.thy
wenzelm@6255
    45
   "|- MClkReply send rcv cst p --> <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
wenzelm@6255
    46
   (fn _ => [auto_tac (mem_css addsimps2 [angle_def,MClkReply_def]
wenzelm@6255
    47
			       addEs2 [Return_changed])
wenzelm@3807
    48
            ]);
wenzelm@3807
    49
wenzelm@3807
    50
qed_goal "MClkReply_enabled" MemClerk.thy
wenzelm@6255
    51
   "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \
wenzelm@6255
    52
\        |- Calling send p & ~Calling rcv p & cst!p = #clkB  \
wenzelm@6255
    53
\           --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
wenzelm@4089
    54
   (fn _ => [action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1,
wenzelm@4089
    55
	     action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
wenzelm@3807
    56
                             [] [base_enabled,Pair_inject] 1
wenzelm@3807
    57
	    ]);
wenzelm@3807
    58
wenzelm@3807
    59
qed_goal "MClkReplyNotRetry" MemClerk.thy
wenzelm@6255
    60
   "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
wenzelm@6255
    61
   (fn _ => [ auto_tac (mem_css addsimps2 [MClkReply_def,MClkRetry_def]) ]);
wenzelm@6255
    62