src/HOL/TLA/Memory/MemoryImplementation.ML
author nipkow
Tue Sep 21 19:11:07 1999 +0200 (1999-09-21)
changeset 7570 a9391550eea1
parent 6919 7985b229806c
child 9517 f58863b1406a
permissions -rw-r--r--
Mod because of new solver interface.
     1 (* 
     2     File:        MemoryImplementation.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     RPC-Memory example: Memory implementation (ML file)
     7 
     8     The main theorem is theorem "Implementation" at the end of this file,
     9     which shows that the composition of a reliable memory, an RPC component, and
    10     a memory clerk implements an unreliable memory. The files "MIsafe.ML" and
    11     "MIlive.ML" contain lower-level lemmas for the safety and liveness parts.
    12 
    13     Steps are (roughly) numbered as in the hand proof.
    14 *)
    15 
    16 (* --------------------------- automatic prover --------------------------- *)
    17 
    18 Delcongs [if_weak_cong];
    19 
    20 val MI_css = (claset(), simpset());
    21 
    22 (* A more aggressive variant that tries to solve subgoals by assumption
    23    or contradiction during the simplification.
    24    THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
    25    (but it can be a lot faster than MI_css)
    26 *)
    27 val MI_fast_css =
    28   let 
    29     val (cs,ss) = MI_css
    30   in
    31     (cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
    32 end;
    33 
    34 val temp_elim = make_elim o temp_use;
    35 
    36 (****************************** The history variable ******************************)
    37 section "History variable";
    38 
    39 qed_goal "HistoryLemma" MemoryImplementation.thy
    40    "|- Init(!p. ImpInit p) & [](!p. ImpNext p)  \
    41 \      --> (EEX rmhist. Init(! p. HInit rmhist p) \
    42 \                     & [](!p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
    43    (fn _ => [Clarsimp_tac 1,
    44              rtac historyI 1, TRYALL atac, rtac MI_base 1,
    45              action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1,
    46              etac fun_cong 1,
    47              action_simp_tac (simpset() addsimps [HNext_def]) [busy_squareI] [] 1,
    48              etac fun_cong 1
    49             ]);
    50 
    51 qed_goal "History" MemoryImplementation.thy
    52    "|- Implementation --> (EEX rmhist. Hist rmhist)"
    53    (fn _ => [Clarsimp_tac 1,
    54              rtac ((temp_use HistoryLemma) RS eex_mono) 1,
    55              force_tac (MI_css 
    56                         addsimps2 [Hist_def,HistP_def,Init_def,all_box,split_box_conj]) 3,
    57              auto_tac (MI_css
    58                        addsimps2 [Implementation_def,MClkISpec_def,RPCISpec_def,IRSpec_def,
    59                                   MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
    60                                   ImpInit_def,Init_def,ImpNext_def,
    61                                   c_def,r_def,m_def,all_box,split_box_conj])
    62             ]);
    63 
    64 (******************************** The safety part *********************************)
    65 
    66 section "The safety part";
    67 
    68 (* ------------------------- Include lower-level lemmas ------------------------- *)
    69 use "MIsafe.ML";
    70 
    71 section "Correctness of predicate-action diagram";
    72 
    73 
    74 (* ========== Step 1.1 ================================================= *)
    75 (* The implementation's initial condition implies the state predicate S1 *)
    76 
    77 qed_goal "Step1_1" MemoryImplementation.thy
    78    "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
    79    (fn _ => [auto_tac (MI_fast_css
    80 		       addsimps2 [MVNROKBA_def,MClkInit_def,RPCInit_def,PInit_def,
    81 			          HInit_def,ImpInit_def,S_def,S1_def])
    82 	    ]);
    83 
    84 (* ========== Step 1.2 ================================================== *)
    85 (* Figure 16 is a predicate-action diagram for the implementation. *)
    86 
    87 qed_goal "Step1_2_1" MemoryImplementation.thy
    88    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
    89 \             & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p \
    90 \      --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
    91    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
    92                              (map temp_elim [S1ClerkUnch,S1RPCUnch,S1MemUnch,S1Hist]) 1,
    93              auto_tac (MI_fast_css addSIs2 [S1Env])
    94 	    ]);
    95 
    96 qed_goal "Step1_2_2" MemoryImplementation.thy
    97    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
    98 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p \
    99 \      --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p & unchanged (e p, r p, m p, rmhist!p)"
   100    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   101                              (map temp_elim [S2EnvUnch,S2RPCUnch,S2MemUnch,S2Hist]) 1,
   102 	     auto_tac (MI_fast_css addSIs2 [S2Clerk,S2Forward])
   103 	    ]);
   104 
   105 qed_goal "Step1_2_3" MemoryImplementation.thy
   106    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   107 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p \
   108 \      --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) \
   109 \        | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   110    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   111 	          (map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1,
   112              action_simp_tac (simpset()) [] 
   113                   (squareE::map temp_elim [S3RPC,S3Forward,S3Fail]) 1,
   114              auto_tac (MI_css addDs2 [S3Hist])
   115 	    ]);
   116 
   117 qed_goal "Step1_2_4" MemoryImplementation.thy
   118    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   119 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) \
   120 \             & $S4 rmhist p & (!l. $(MemInv mm l))     \
   121 \      --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p)) \
   122 \        | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p)) \
   123 \        | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   124    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   125                              (map temp_elim [S4EnvUnch,S4ClerkUnch,S4RPCUnch]) 1,
   126              action_simp_tac (simpset() addsimps [RNext_def]) []
   127                              (squareE::map temp_elim [S4Read,S4Write,S4Return]) 1,
   128              auto_tac (MI_css addDs2 [S4Hist])
   129             ]);
   130 
   131 qed_goal "Step1_2_5" MemoryImplementation.thy
   132    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   133 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p \
   134 \      --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p)) \
   135 \        | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   136    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   137                              (map temp_elim [S5EnvUnch,S5ClerkUnch,S5MemUnch,S5Hist]) 1,
   138 	     action_simp_tac (simpset()) [] [squareE, temp_elim S5RPC] 1,
   139 	     auto_tac (MI_fast_css addSDs2 [S5Reply,S5Fail])
   140 	    ]);
   141 
   142 qed_goal "Step1_2_6" MemoryImplementation.thy
   143    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   144 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p \
   145 \      --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))\
   146 \        | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   147    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   148                              (map temp_elim [S6EnvUnch,S6RPCUnch,S6MemUnch]) 1,
   149              action_simp_tac (simpset()) []
   150                              (squareE::map temp_elim [S6Clerk,S6Retry,S6Reply]) 1,
   151              auto_tac (MI_css addDs2 [S6Hist])
   152             ]);
   153 
   154 (* --------------------------------------------------------------------------
   155    Step 1.3: S1 implies the barred initial condition.
   156 *)
   157 
   158 section "Initialization (Step 1.3)";
   159 
   160 qed_goal "Step1_3" MemoryImplementation.thy 
   161    "|- S1 rmhist p --> PInit (resbar rmhist) p"
   162    (fn _ => [action_simp_tac (simpset() addsimps [resbar_def,PInit_def,S_def,S1_def])
   163                              [] [] 1
   164             ]);
   165 
   166 (* ----------------------------------------------------------------------
   167    Step 1.4: Implementation's next-state relation simulates specification's
   168              next-state relation (with appropriate substitutions)
   169 *)
   170 
   171 section "Step simulation (Step 1.4)";
   172 
   173 qed_goal "Step1_4_1" MemoryImplementation.thy
   174    "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p) \
   175 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   176   (fn _ => [ auto_tac (MI_fast_css addsimps2 [c_def,r_def,m_def,resbar_def]) ]);
   177 
   178 qed_goal "Step1_4_2" MemoryImplementation.thy
   179    "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$  \
   180 \                & unchanged (e p, r p, m p, rmhist!p) \
   181 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   182   (fn _ => [action_simp_tac
   183                 (simpset() addsimps [MClkFwd_def, e_def, r_def, m_def, resbar_def,
   184                                      S_def, S2_def, S3_def]) [] [] 1
   185            ]);
   186 
   187 qed_goal "Step1_4_3a" MemoryImplementation.thy
   188    "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$    \
   189 \                  & unchanged (e p, c p, m p, rmhist!p) \
   190 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   191   (fn _ => [Clarsimp_tac 1,
   192             REPEAT (dresolve_tac (map temp_use [S3_excl,S4_excl]) 1),
   193             action_simp_tac 
   194                  (simpset() addsimps [e_def,c_def,m_def,resbar_def,S_def, S3_def]) [] [] 1
   195            ]);
   196 
   197 qed_goal "Step1_4_3b" MemoryImplementation.thy
   198    "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$ & unchanged (e p, c p, m p) \
   199 \      --> MemFail memCh (resbar rmhist) p"
   200   (fn _ => [Clarsimp_tac 1,
   201             dtac (temp_use S6_excl) 1,
   202             auto_tac (MI_css addsimps2 [RPCFail_def,MemFail_def,e_def,c_def,m_def,
   203 		                        resbar_def]),
   204             force_tac (MI_css addsimps2 [S3_def,S_def]) 1,
   205             auto_tac (MI_css addsimps2 [Return_def])
   206            ]);
   207 
   208 
   209 qed_goal "Step1_4_4a1" MemoryImplementation.thy
   210    "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l \
   211 \             & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l \
   212 \      --> ReadInner memCh mm (resbar rmhist) p l"
   213   (fn _ => [Clarsimp_tac 1,
   214             REPEAT (dtac (temp_use S4_excl) 1),
   215             action_simp_tac 
   216                (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def]) 
   217                [] [] 1,
   218             auto_tac (MI_css addsimps2 [resbar_def]),
   219 	    ALLGOALS (action_simp_tac 
   220                         (simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
   221 		                            S_def,S4_def,RdRequest_def,MemInv_def])
   222 		      [] [impE,MemValNotAResultE])
   223            ]);
   224 
   225 qed_goal "Step1_4_4a" MemoryImplementation.thy
   226    "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ \
   227 \           & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l)) \
   228 \      --> Read memCh mm (resbar rmhist) p"
   229   (fn _ => [ force_tac (MI_css addsimps2 [Read_def] addSEs2 [Step1_4_4a1]) 1 ]);
   230 
   231 qed_goal "Step1_4_4b1" MemoryImplementation.thy
   232    "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v   \
   233 \                   & unchanged (e p, c p, r p, rmhist!p) \
   234 \      --> WriteInner memCh mm (resbar rmhist) p l v"
   235   (fn _ => [Clarsimp_tac 1,
   236             REPEAT (dtac (temp_use S4_excl) 1),
   237             action_simp_tac 
   238                (simpset() addsimps [WriteInner_def, GoodWrite_def, BadWrite_def,
   239 			           e_def, c_def, m_def])
   240                [] [] 1,
   241 	    auto_tac (MI_css addsimps2 [resbar_def]),
   242 	    ALLGOALS (action_simp_tac
   243                         (simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
   244 		                            S_def,S4_def,WrRequest_def])
   245 		      [] [])
   246            ]);
   247 
   248 qed_goal "Step1_4_4b" MemoryImplementation.thy
   249    "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$   \
   250 \                 & unchanged (e p, c p, r p, rmhist!p) \
   251 \      --> Write memCh mm (resbar rmhist) p l"
   252   (fn _ => [ force_tac (MI_css addsimps2 [Write_def] addSEs2 [Step1_4_4b1]) 1 ]);
   253 
   254 qed_goal "Step1_4_4c" MemoryImplementation.thy
   255    "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$ & unchanged (e p, c p, r p) \
   256 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   257   (fn _ => [action_simp_tac
   258 	       (simpset() addsimps [e_def,c_def,r_def,resbar_def]) [] [] 1,
   259 	    REPEAT (dresolve_tac [temp_use S4_excl, temp_use S5_excl] 1),
   260 	    auto_tac (MI_fast_css addsimps2 [MemReturn_def,Return_def])
   261            ]);
   262 
   263 qed_goal "Step1_4_5a" MemoryImplementation.thy
   264    "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$ & unchanged (e p, c p, m p) \
   265 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   266   (fn _ => [Clarsimp_tac 1,
   267             REPEAT (dresolve_tac [temp_use S5_excl, temp_use S6_excl] 1),
   268             auto_tac (MI_css addsimps2 [e_def,c_def,m_def, resbar_def]),
   269 	    auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def] 
   270                              addSDs2 [MVOKBAnotRF])
   271            ]);
   272 
   273 qed_goal "Step1_4_5b" MemoryImplementation.thy
   274    "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$ & unchanged (e p, c p, m p) \
   275 \      --> MemFail memCh (resbar rmhist) p"
   276   (fn _ => [Clarsimp_tac 1,
   277             dtac (temp_use S6_excl) 1,
   278             auto_tac (MI_css addsimps2 [e_def, c_def, m_def, RPCFail_def, Return_def,
   279 		 		        MemFail_def, resbar_def]),
   280 	    auto_tac (MI_css addsimps2 [S5_def,S_def])
   281            ]);
   282 
   283 qed_goal "Step1_4_6a" MemoryImplementation.thy
   284    "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$ & unchanged (e p, r p, m p) \
   285 \      --> MemReturn memCh (resbar rmhist) p"
   286   (fn _ => [Clarsimp_tac 1,
   287             dtac (temp_use S6_excl) 1,
   288             action_simp_tac
   289 	      (simpset() addsimps [e_def, r_def, m_def, MClkReply_def, MemReturn_def,
   290 				  Return_def, resbar_def]) [] [] 1,
   291 	    ALLGOALS Asm_full_simp_tac,  (* simplify if-then-else *)
   292 	    ALLGOALS (action_simp_tac
   293     	              (simpset() addsimps [MClkReplyVal_def,S6_def,S_def])
   294 		      [] [MVOKBARFnotNR])
   295            ]);
   296 
   297 qed_goal "Step1_4_6b" MemoryImplementation.thy
   298    "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$   \
   299 \                & unchanged (e p, r p, m p, rmhist!p) \
   300 \      --> MemFail memCh (resbar rmhist) p"
   301   (fn _ => [Clarsimp_tac 1,
   302             dtac (temp_use S3_excl) 1,
   303             action_simp_tac
   304 	       (simpset() addsimps [e_def, r_def, m_def, MClkRetry_def, MemFail_def, resbar_def])
   305 	       [] [] 1,
   306 	    auto_tac (MI_css addsimps2 [S6_def,S_def])
   307            ]);
   308 
   309 qed_goal "S_lemma" MemoryImplementation.thy
   310    "|- unchanged (e p, c p, r p, m p, rmhist!p) \
   311 \      --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
   312    (fn _ => [auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,caller_def,rtrner_def,
   313 					 S_def,Calling_def])
   314             ]);
   315 
   316 qed_goal "Step1_4_7H" MemoryImplementation.thy
   317    "|- unchanged (e p, c p, r p, m p, rmhist!p) \
   318 \      --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p, \
   319 \                     S4 rmhist p, S5 rmhist p, S6 rmhist p)"
   320    (fn _ => [Clarsimp_tac 1,
   321              rtac conjI 1,
   322              force_tac (MI_css addsimps2 [c_def]) 1,
   323              force_tac (MI_css addsimps2 [S1_def,S2_def,S3_def,S4_def,S5_def,S6_def]
   324                                addSIs2 [S_lemma]) 1
   325             ]);
   326 
   327 qed_goal "Step1_4_7" MemoryImplementation.thy
   328    "|- unchanged (e p, c p, r p, m p, rmhist!p) \
   329 \      --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p, S3 rmhist p, \
   330 \                     S4 rmhist p, S5 rmhist p, S6 rmhist p)"
   331   (fn _ => [rtac actionI 1,
   332             rewrite_goals_tac action_rews,
   333             rtac impI 1,
   334             forward_tac [temp_use Step1_4_7H] 1,
   335 	    auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,rtrner_def,resbar_def])
   336            ]);
   337 
   338 
   339 (* Frequently needed abbreviation: distinguish between idling and non-idling
   340    steps of the implementation, and try to solve the idling case by simplification
   341 *)
   342 fun split_idle_tac simps i = 
   343     EVERY [TRY (rtac actionI i),
   344 	   case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
   345 	   rewrite_goals_tac action_rews,
   346 	   forward_tac [temp_use Step1_4_7] i,
   347 	   asm_full_simp_tac (simpset() addsimps simps) i
   348 	  ];
   349 
   350 (* ----------------------------------------------------------------------
   351    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
   352    the specification's next-state relation.
   353 *)
   354 
   355 (* Steps that leave all variables unchanged are safe, so I may assume
   356    that some variable changes in the proof that a step is safe. *)
   357 qed_goal "unchanged_safe" MemoryImplementation.thy
   358    "|- (~unchanged (e p, c p, r p, m p, rmhist!p) \
   359 \        --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) \
   360 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   361    (fn _ => [split_idle_tac [square_def] 1,
   362              Force_tac 1
   363             ]);
   364 (* turn into (unsafe, looping!) introduction rule *)
   365 bind_thm("unchanged_safeI", impI RS (action_use unchanged_safe));
   366 
   367 qed_goal "S1safe" MemoryImplementation.thy
   368    "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   369 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   370    (fn _ => [Clarsimp_tac 1, 
   371              rtac unchanged_safeI 1,
   372              rtac idle_squareI 1,
   373 	     auto_tac (MI_css addSDs2 [Step1_2_1,Step1_4_1])
   374 	    ]);
   375 
   376 qed_goal "S2safe" MemoryImplementation.thy
   377    "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   378 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   379    (fn _ => [Clarsimp_tac 1, 
   380              rtac unchanged_safeI 1,
   381              rtac idle_squareI 1,
   382 	     auto_tac (MI_css addSDs2 [Step1_2_2,Step1_4_2])
   383 	    ]);
   384 
   385 qed_goal "S3safe" MemoryImplementation.thy
   386    "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   387 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   388    (fn _ => [Clarsimp_tac 1,
   389 	     rtac unchanged_safeI 1,
   390              auto_tac (MI_css addSDs2 [Step1_2_3]),
   391 	     auto_tac (MI_css addsimps2 [square_def,UNext_def]
   392 		              addSDs2 [Step1_4_3a,Step1_4_3b])
   393 	    ]);
   394 
   395 qed_goal "S4safe" MemoryImplementation.thy
   396    "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)  \
   397 \                   & (!l. $(MemInv mm l)) \
   398 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   399    (fn _ => [Clarsimp_tac 1,
   400 	     rtac unchanged_safeI 1,
   401              auto_tac (MI_css addSDs2 [Step1_2_4]),
   402 	     auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def]
   403                               addSDs2 [Step1_4_4a,Step1_4_4b,Step1_4_4c])
   404 	    ]);
   405 
   406 qed_goal "S5safe" MemoryImplementation.thy
   407    "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)  \
   408 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   409    (fn _ => [Clarsimp_tac 1,
   410 	     rtac unchanged_safeI 1,
   411              auto_tac (MI_css addSDs2 [Step1_2_5]),
   412 	     auto_tac (MI_css addsimps2 [square_def,UNext_def]
   413 		              addSDs2 [Step1_4_5a,Step1_4_5b])
   414 	    ]);
   415 
   416 qed_goal "S6safe" MemoryImplementation.thy
   417    "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   418 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   419    (fn _ => [Clarsimp_tac 1,
   420 	     rtac unchanged_safeI 1,
   421              auto_tac (MI_css addSDs2 [Step1_2_6]),
   422 	     auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def]
   423 		              addSDs2 [Step1_4_6a,Step1_4_6b])
   424 	    ]);
   425 
   426 (* ----------------------------------------------------------------------
   427    Step 1.5: Temporal refinement proof, based on previous steps.
   428 *)
   429 
   430 section "The liveness part";
   431 
   432 use "MIlive.ML";
   433 
   434 section "Refinement proof (step 1.5)";
   435 
   436 (* Prove invariants of the implementation:
   437    a. memory invariant
   438    b. "implementation invariant": always in states S1,...,S6
   439 *)
   440 qed_goal "Step1_5_1a" MemoryImplementation.thy 
   441    "|- IPImp p --> (!l. []$MemInv mm l)"
   442    (fn _ => [auto_tac (MI_css addsimps2 [IPImp_def,box_stp_act]
   443 			      addSIs2 [MemoryInvariantAll])
   444 	    ]);
   445 
   446 qed_goal "Step1_5_1b" MemoryImplementation.thy
   447    "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p) \
   448 \      & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](!l. $MemInv mm l) \
   449 \      --> []ImpInv rmhist p"
   450    (fn _ => [inv_tac MI_css 1,
   451 	     auto_tac (MI_css addsimps2 [Init_def, ImpInv_def, box_stp_act]
   452                               addSDs2 [Step1_1]
   453 		              addDs2 [S1_successors,S2_successors,S3_successors,
   454 			              S4_successors,S5_successors,S6_successors])
   455             ]);
   456 
   457 (*** Initialization ***)
   458 qed_goal "Step1_5_2a" MemoryImplementation.thy
   459    "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"
   460    (fn _ => [auto_tac (MI_css addsimps2 [Init_def]
   461                               addSIs2 [Step1_1,Step1_3])
   462             ]);
   463 
   464 (*** step simulation ***)
   465 qed_goal "Step1_5_2b" MemoryImplementation.thy
   466    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)   \
   467 \                   & $ImpInv rmhist p & (!l. $MemInv mm l))       \
   468 \      --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   469    (fn _ => [auto_tac (MI_css 
   470                           addsimps2 [ImpInv_def] addSEs2 [STL4E]
   471                           addSDs2 [S1safe,S2safe,S3safe,S4safe,S5safe,S6safe])
   472             ]);
   473 
   474 
   475 (*** Liveness ***)
   476 qed_goal "GoodImpl" MemoryImplementation.thy
   477    "|- IPImp p & HistP rmhist p  \
   478 \      -->   Init(ImpInit p & HInit rmhist p)   \
   479 \          & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   480 \          & [](!l. $MemInv mm l) & []($ImpInv rmhist p) \
   481 \          & ImpLive p"
   482    (fn _ => [Clarsimp_tac 1,
   483 	     subgoal_tac
   484 	       "sigma |= Init(ImpInit p & HInit rmhist p) \
   485 \                        & [](ImpNext p) \
   486 \                        & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) \
   487 \                        & [](!l. $MemInv mm l)" 1,
   488 	     auto_tac (MI_css addsimps2 [split_box_conj,box_stp_act] addSDs2 [Step1_5_1b]),
   489 	     force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
   490 					  ImpLive_def,c_def,r_def,m_def]) 1,
   491 	     force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
   492 					  HistP_def,Init_def,ImpInit_def]) 1,
   493 	     force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
   494 					  ImpNext_def,c_def,r_def,m_def,split_box_conj]) 1,
   495 	     force_tac (MI_css addsimps2 [HistP_def]) 1,
   496              force_tac (MI_css addsimps2 [temp_use allT] addSDs2 [Step1_5_1a]) 1
   497 	    ]);
   498 
   499 (* The implementation is infinitely often in state S1... *)
   500 qed_goal "Step1_5_3a" MemoryImplementation.thy
   501    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   502 \      & [](!l. $MemInv mm l)  \
   503 \      & []($ImpInv rmhist p) & ImpLive p  \
   504 \      --> []<>S1 rmhist p"
   505    (fn _ => [clarsimp_tac (MI_css addsimps2 [ImpLive_def]) 1,
   506              rtac S1Infinite 1,
   507 	     force_tac (MI_css
   508 			  addsimps2 [split_box_conj,box_stp_act]
   509 			  addSIs2 [NotS1LeadstoS6,S2_live,S3_live,S4a_live,S4b_live,S5_live]) 1,
   510              auto_tac (MI_css addsimps2 [split_box_conj] addSIs2 [S6_live])
   511             ]);
   512 
   513 (* ... which implies that it satisfies the fairness requirements of the specification *)
   514 qed_goal "Step1_5_3b" MemoryImplementation.thy
   515    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   516 \      & [](!l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p  \
   517 \      --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   518    (fn _ => [ auto_tac (MI_css addSIs2 [RNext_fair,Step1_5_3a]) ]);
   519 
   520 qed_goal "Step1_5_3c" MemoryImplementation.thy
   521    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   522 \      & [](!l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p  \
   523 \      --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   524    (fn _ => [ auto_tac (MI_css addSIs2 [Return_fair,Step1_5_3a]) ]);
   525 
   526 
   527 (* QED step of step 1 *)
   528 qed_goal "Step1" MemoryImplementation.thy
   529    "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
   530    (fn _ => [auto_tac
   531                (MI_css addsimps2 [UPSpec_def,split_box_conj]
   532 		       addSDs2 [GoodImpl]
   533                        addSIs2 [Step1_5_2a,Step1_5_2b,Step1_5_3b,Step1_5_3c])
   534             ]);
   535 
   536 
   537 (* ------------------------------ Step 2 ------------------------------ *)
   538 section "Step 2";
   539 
   540 qed_goal "Step2_2a" MemoryImplementation.thy
   541    "|- Write rmCh mm ires p l & ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p) \
   542 \      & $ImpInv rmhist p  \
   543 \      --> (S4 rmhist p)` & unchanged (e p, c p, r p, rmhist!p)"
   544    (fn _ => [Clarsimp_tac 1,
   545              dtac (action_use WriteS4) 1, atac 1,
   546              split_idle_tac [] 1,
   547              auto_tac (MI_css addsimps2 [ImpNext_def] 
   548                               addSDs2 [S4EnvUnch,S4ClerkUnch,S4RPCUnch]),
   549              auto_tac (MI_css addsimps2 [square_def] addDs2 [S4Write])
   550             ]);
   551 
   552 qed_goal "Step2_2" MemoryImplementation.thy
   553    "|-   (!p. ImpNext p) \
   554 \      & (!p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   555 \      & (!p. $ImpInv rmhist p) \
   556 \      & [? q. Write rmCh mm ires q l]_(mm!l) \
   557 \      --> [? q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   558    (fn _ => [auto_tac (MI_css addSIs2 [squareCI] addSEs2 [squareE]),
   559              REPEAT (ares_tac [exI, action_use Step1_4_4b] 1),
   560              force_tac (MI_css addSIs2 [WriteS4]) 1,
   561              auto_tac (MI_css addSDs2 [Step2_2a])
   562             ]);
   563 
   564 qed_goal "Step2_lemma" MemoryImplementation.thy
   565    "|-  [](  (!p. ImpNext p) \
   566 \          & (!p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   567 \          & (!p. $ImpInv rmhist p) \
   568 \          & [? q. Write rmCh mm ires q l]_(mm!l)) \
   569 \       --> [][? q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   570    (fn _ => [ force_tac (MI_css addSEs2 [STL4E] addSDs2 [Step2_2]) 1 ]);
   571 
   572 qed_goal "Step2" MemoryImplementation.thy
   573    "|- #l : #MemLoc & (!p. IPImp p & HistP rmhist p)  \
   574 \      --> MSpec memCh mm (resbar rmhist) l"
   575    (fn _ => [auto_tac (MI_css addsimps2 [MSpec_def]),
   576 	     force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 1,
   577 	     auto_tac (MI_css addSIs2 [Step2_lemma]
   578 		              addsimps2 [split_box_conj,all_box]),
   579 	     force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 4,
   580              auto_tac (MI_css addsimps2 [split_box_conj] addSEs2 [allE] addSDs2 [GoodImpl])
   581 	    ]);
   582 
   583 (* ----------------------------- Main theorem --------------------------------- *)
   584 section "Memory implementation";
   585 
   586 (* The combination of a legal caller, the memory clerk, the RPC component,
   587    and a reliable memory implement the unreliable memory.
   588 *)
   589 
   590 (* Implementation of internal specification by combination of implementation
   591    and history variable with explicit refinement mapping
   592 *)
   593 qed_goal "Impl_IUSpec" MemoryImplementation.thy
   594    "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"
   595    (fn _ => [auto_tac (MI_css addsimps2 [IUSpec_def,Implementation_def,IPImp_def,
   596 					 MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def]
   597 		              addSIs2 [Step1,Step2])
   598 	    ]);
   599 
   600 (* The main theorem: introduce hiding and eliminate history variable. *)
   601 qed_goal "Implementation" MemoryImplementation.thy
   602    "|- Implementation --> USpec memCh"
   603    (fn _ => [Clarsimp_tac 1,
   604              forward_tac [temp_use History] 1,
   605              auto_tac (MI_css addsimps2 [USpec_def] 
   606                               addIs2 [eexI, Impl_IUSpec, MI_base]
   607                               addSEs2 [eexE])
   608             ]);
   609 
   610