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