src/HOL/TLA/Memory/Memory.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 7881 1b1db39a110b
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:        Memory.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     RPC-Memory example: Memory specification (theorems and proofs)
     7 *)
     8 
     9 val RM_action_defs = 
    10    [MInit_def, PInit_def, RdRequest_def, WrRequest_def, MemInv_def,
    11     GoodRead_def, BadRead_def, ReadInner_def, Read_def,
    12     GoodWrite_def, BadWrite_def, WriteInner_def, Write_def,
    13     MemReturn_def, RNext_def];
    14 
    15 val UM_action_defs = RM_action_defs @ [MemFail_def, UNext_def];
    16 
    17 val RM_temp_defs = [RPSpec_def, MSpec_def, IRSpec_def];
    18 val UM_temp_defs = [UPSpec_def, MSpec_def, IUSpec_def];
    19 
    20 val mem_css = (claset(), simpset());
    21 
    22 (* -------------------- Proofs ---------------------------------------------- *)
    23 
    24 (* The reliable memory is an implementation of the unreliable one *)
    25 qed_goal "ReliableImplementsUnReliable" Memory.thy 
    26    "|- IRSpec ch mm rs --> IUSpec ch mm rs"
    27    (K [force_tac (temp_css addsimps2 ([UNext_def,UPSpec_def,IUSpec_def] @ RM_temp_defs)
    28 			   addSEs2 [STL4E,squareE]) 1]);
    29 
    30 (* The memory spec implies the memory invariant *)
    31 qed_goal "MemoryInvariant" Memory.thy 
    32    "|- MSpec ch mm rs l --> [](MemInv mm l)"
    33    (fn _ => [ auto_inv_tac (simpset() addsimps RM_temp_defs @ RM_action_defs) 1 ]);
    34 
    35 (* The invariant is trivial for non-locations *)
    36 qed_goal "NonMemLocInvariant" Memory.thy
    37    "|- #l ~: #MemLoc --> [](MemInv mm l)"
    38    (K [ auto_tac (temp_css addsimps2 [MemInv_def] addSIs2 [necT]) ]);
    39 
    40 qed_goal "MemoryInvariantAll" Memory.thy
    41    "|- (!l. #l : #MemLoc --> MSpec ch mm rs l) --> (!l. [](MemInv mm l))"
    42     (K [step_tac temp_cs 1,
    43 	case_tac "l : MemLoc" 1,
    44 	auto_tac (temp_css addSEs2 [MemoryInvariant,NonMemLocInvariant]) ]);
    45 
    46 (* The memory engages in an action for process p only if there is an 
    47    unanswered call from p.
    48    We need this only for the reliable memory.
    49 *)
    50 
    51 qed_goal "Memoryidle" Memory.thy
    52    "|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
    53    (K [ auto_tac (mem_css addsimps2 (Return_def::RM_action_defs)) ]);
    54 
    55 (* Enabledness conditions *)
    56 
    57 qed_goal "MemReturn_change" Memory.thy
    58    "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
    59    (K [ force_tac (mem_css addsimps2 [MemReturn_def,angle_def]) 1]);
    60 
    61 qed_goal "MemReturn_enabled" Memory.thy
    62    "!!p. basevars (rtrner ch ! p, rs!p) ==> \
    63 \        |- Calling ch p & (rs!p ~= #NotAResult) \
    64 \           --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
    65   (K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1,
    66       action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def])
    67                              [] [base_enabled,Pair_inject] 1
    68 	    ]);
    69 
    70 qed_goal "ReadInner_enabled" Memory.thy
    71  "!!p. basevars (rtrner ch ! p, rs!p) ==> \
    72 \      |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
    73    (fn _ => [case_tac "l : MemLoc" 1,
    74              ALLGOALS
    75 	        (action_simp_tac 
    76                     (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,
    77 					RdRequest_def])
    78                     [] [base_enabled,Pair_inject])
    79             ]);
    80 
    81 qed_goal "WriteInner_enabled" Memory.thy
    82    "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==> \
    83 \        |- Calling ch p & (arg<ch!p> = #(write l v)) \
    84 \           --> Enabled (WriteInner ch mm rs p l v)"
    85    (fn _ => [case_tac "l:MemLoc & v:MemVal" 1,
    86              ALLGOALS (action_simp_tac 
    87                  (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
    88 					WrRequest_def] delsimps [disj_not1])
    89                     [] [base_enabled,Pair_inject])
    90             ]);
    91 
    92 qed_goal "ReadResult" Memory.thy
    93    "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
    94    (fn _ => [force_tac (mem_css addsimps2 
    95                             [Read_def,ReadInner_def,GoodRead_def,BadRead_def,MemInv_def]) 1]);
    96 
    97 qed_goal "WriteResult" Memory.thy
    98    "|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult"
    99    (fn _ => [auto_tac (mem_css addsimps2 ([Write_def,WriteInner_def,GoodWrite_def,BadWrite_def]))
   100 	    ]);
   101 
   102 qed_goal "ReturnNotReadWrite" Memory.thy
   103    "|- (!l. $MemInv mm l) & MemReturn ch rs p \
   104 \      --> ~ Read ch mm rs p & (!l. ~ Write ch mm rs p l)"
   105    (fn _ => [auto_tac
   106 	       (mem_css addsimps2 [MemReturn_def] addSDs2 [WriteResult, ReadResult])
   107 	    ]);
   108 
   109 qed_goal "RWRNext_enabled" Memory.thy
   110    "|- (rs!p = #NotAResult) & (!l. MemInv mm l)  \
   111 \          & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l)) \
   112 \      --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   113    (K [force_tac (mem_css addsimps2 [RNext_def,angle_def]
   114 	     addSEs2 [enabled_mono2]
   115 	     addDs2 [ReadResult, WriteResult]) 1]);
   116 
   117 
   118 (* Combine previous lemmas: the memory can make a visible step if there is an
   119    outstanding call for which no result has been produced.
   120 *)
   121 qed_goal "RNext_enabled" Memory.thy
   122 "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==> \
   123 \     |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l)  \
   124 \        --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" (K [
   125 	     auto_tac (mem_css addsimps2 [enabled_disj]
   126 		                  addSIs2 [RWRNext_enabled]),
   127              exhaust_tac "arg(ch w p)" 1,
   128  	      action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
   129 	                      [ReadInner_enabled,exI] [] 1,
   130               force_tac (mem_css addDs2 [base_pair]) 1,
   131 	     etac swap 1,
   132 	     action_simp_tac (simpset() addsimps [Write_def,enabled_ex])
   133 	                     [WriteInner_enabled,exI] [] 1]);
   134