src/HOL/TLA/Memory/MIlive.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:        MIlive.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     RPC-Memory example: Lower-level lemmas for the liveness proof
     7 *)
     8 
     9 (* Liveness assertions for the different implementation states, based on the
    10    fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas
    11    for readability. Reuse action proofs from safety part.
    12 *)
    13 
    14 (* ------------------------------ State S1 ------------------------------ *)
    15 
    16 qed_goal "S1_successors" MemoryImplementation.thy
    17    "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)  \
    18 \      --> (S1 rmhist p)` | (S2 rmhist p)`"
    19    (fn _ => [split_idle_tac [] 1,
    20 	     auto_tac (MI_css addSDs2 [Step1_2_1])
    21 	    ]);
    22 
    23 (* Show that the implementation can satisfy the high-level fairness requirements
    24    by entering the state S1 infinitely often.
    25 *)
    26 
    27 qed_goal "S1_RNextdisabled" MemoryImplementation.thy
    28    "|- S1 rmhist p --> \
    29 \      ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
    30    (fn _ => [action_simp_tac (simpset() addsimps [angle_def,S_def,S1_def])
    31 	                     [notI] [enabledE,temp_elim Memoryidle] 1,
    32 	     Force_tac 1
    33 	    ]);
    34 
    35 qed_goal "S1_Returndisabled" MemoryImplementation.thy
    36    "|- S1 rmhist p --> \
    37 \      ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
    38    (fn _ => [action_simp_tac (simpset() addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def])
    39 	                     [notI] [enabledE] 1
    40 	    ]);
    41 
    42 qed_goal "RNext_fair" MemoryImplementation.thy
    43    "|- []<>S1 rmhist p   \
    44 \      --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
    45    (fn _ => [auto_tac (MI_css addsimps2 [WF_alt]
    46 			      addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE])
    47 	    ]);
    48 
    49 qed_goal "Return_fair" MemoryImplementation.thy
    50    "|- []<>S1 rmhist p   \
    51 \      --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
    52    (fn _ => [auto_tac (MI_css addsimps2 [WF_alt]
    53 			      addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE])
    54 	    ]);
    55 
    56 (* ------------------------------ State S2 ------------------------------ *)
    57 
    58 qed_goal "S2_successors" MemoryImplementation.thy
    59    "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
    60 \      --> (S2 rmhist p)` | (S3 rmhist p)`"
    61    (fn _ => [split_idle_tac [] 1,
    62 	     auto_tac (MI_css addSDs2 [Step1_2_2])
    63 	    ]);
    64 
    65 qed_goal "S2MClkFwd_successors" MemoryImplementation.thy
    66    "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))    \
    67 \      & <MClkFwd memCh crCh cst p>_(c p) \
    68 \      --> (S3 rmhist p)`"
    69    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_2]) ]);
    70 
    71 qed_goal "S2MClkFwd_enabled" MemoryImplementation.thy
    72    "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)    \
    73 \      --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
    74    (fn _ => [auto_tac (MI_css addsimps2 [c_def] addSIs2 [MClkFwd_ch_enabled,MClkFwd_enabled]),
    75              cut_facts_tac [MI_base] 1,
    76              blast_tac (claset() addDs [base_pair]) 1,
    77              ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S2_def]))
    78 	    ]);
    79 
    80 qed_goal "S2_live" MemoryImplementation.thy
    81    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) & WF(MClkFwd memCh crCh cst p)_(c p) \
    82 \      --> (S2 rmhist p ~> S3 rmhist p)"
    83    (fn _ => [REPEAT (resolve_tac [WF1,S2_successors,
    84 				  S2MClkFwd_successors,S2MClkFwd_enabled] 1)
    85 	    ]);
    86 
    87 
    88 (* ------------------------------ State S3 ------------------------------ *)
    89 
    90 qed_goal "S3_successors" MemoryImplementation.thy
    91    "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
    92 \      --> (S3 rmhist p)` | (S4 rmhist p | S6 rmhist p)`"
    93    (fn _ => [split_idle_tac [] 1,
    94 	     auto_tac (MI_css addSDs2 [Step1_2_3])
    95 	    ]);
    96 
    97 qed_goal "S3RPC_successors" MemoryImplementation.thy
    98    "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))   \
    99 \      & <RPCNext crCh rmCh rst p>_(r p) \
   100 \      --> (S4 rmhist p | S6 rmhist p)`"
   101    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_3]) ]);
   102 
   103 qed_goal "S3RPC_enabled" MemoryImplementation.thy
   104    "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   105 \      --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
   106    (fn _ => [auto_tac (MI_css addsimps2 [r_def]
   107 		              addSIs2 [RPCFail_Next_enabled,RPCFail_enabled]),
   108 	     cut_facts_tac [MI_base] 1,
   109 	     blast_tac (claset() addDs [base_pair]) 1,
   110              ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S3_def]))
   111 	    ]);
   112 
   113 qed_goal "S3_live" MemoryImplementation.thy
   114    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) & WF(RPCNext crCh rmCh rst p)_(r p) \
   115 \   --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
   116    (fn _ => [REPEAT (resolve_tac [WF1,S3_successors,S3RPC_successors,S3RPC_enabled] 1)]);
   117 
   118 (* ------------- State S4 -------------------------------------------------- *)
   119 
   120 qed_goal "S4_successors" MemoryImplementation.thy
   121    "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
   122 \                   & (!l. $MemInv mm l)  \
   123 \      --> (S4 rmhist p)` | (S5 rmhist p)`"
   124    (fn _ => [split_idle_tac [] 1,
   125 	     auto_tac (MI_css addSDs2 [Step1_2_4])
   126 	    ]);
   127 
   128 (* ------------- State S4a: S4 /\ (ires p = NotAResult) ------------------------------ *)
   129 
   130 qed_goal "S4a_successors" MemoryImplementation.thy
   131    "|- $(S4 rmhist p & ires!p = #NotAResult) \
   132 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l) \
   133 \      --> (S4 rmhist p & ires!p = #NotAResult)`  \
   134 \        | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)`"
   135    (fn _ => [split_idle_tac [m_def] 1,
   136 	     auto_tac (MI_css addSDs2 [Step1_2_4])
   137 	    ]);
   138 
   139 qed_goal "S4aRNext_successors" MemoryImplementation.thy
   140    "|- ($(S4 rmhist p & ires!p = #NotAResult)  \
   141 \       & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))  \
   142 \      & <RNext rmCh mm ires p>_(m p) \
   143 \      --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)`"
   144    (fn _ => [auto_tac (MI_css addsimps2 [angle_def]
   145 		              addSDs2 [Step1_2_4, ReadResult, WriteResult])
   146 	    ]);
   147 
   148 qed_goal "S4aRNext_enabled" MemoryImplementation.thy
   149    "|- $(S4 rmhist p & ires!p = #NotAResult) \
   150 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)  \
   151 \   --> $Enabled (<RNext rmCh mm ires p>_(m p))"
   152    (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [RNext_enabled]),
   153 	     cut_facts_tac [MI_base] 1,
   154 	     blast_tac (claset() addDs [base_pair]) 1,
   155 	     asm_full_simp_tac (simpset() addsimps [S_def,S4_def]) 1
   156 	    ]);
   157 
   158 qed_goal "S4a_live" MemoryImplementation.thy
   159   "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)) \
   160 \     & WF(RNext rmCh mm ires p)_(m p) \
   161 \     --> (S4 rmhist p & ires!p = #NotAResult  \
   162 \          ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
   163    (K [REPEAT (resolve_tac [WF1, S4a_successors, S4aRNext_successors, S4aRNext_enabled] 1)]);
   164 
   165 (* ------------- State S4b: S4 /\ (ires p # NotAResult) ------------------------------ *)
   166 
   167 qed_goal "S4b_successors" MemoryImplementation.thy
   168    "|- $(S4 rmhist p & ires!p ~= #NotAResult)  \
   169 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l) \
   170 \      --> (S4 rmhist p & ires!p ~= #NotAResult)` | (S5 rmhist p)`"
   171    (fn _ => [split_idle_tac [m_def] 1,
   172 	     auto_tac (MI_css addSDs2 [WriteResult,Step1_2_4,ReadResult])
   173 	    ]);
   174 
   175 qed_goal "S4bReturn_successors" MemoryImplementation.thy
   176    "|- ($(S4 rmhist p & ires!p ~= #NotAResult)  \
   177 \       & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))   \
   178 \      & <MemReturn rmCh ires p>_(m p) \
   179 \      --> (S5 rmhist p)`"
   180    (fn _ => [force_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_4]
   181                                addDs2 [ReturnNotReadWrite]) 1
   182 	    ]);
   183 
   184 qed_goal "S4bReturn_enabled" MemoryImplementation.thy
   185    "|- $(S4 rmhist p & ires!p ~= #NotAResult)  \
   186 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)  \
   187 \      --> $Enabled (<MemReturn rmCh ires p>_(m p))"
   188    (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [MemReturn_enabled]),
   189 	     cut_facts_tac [MI_base] 1,
   190              blast_tac (claset() addDs [base_pair]) 1,
   191 	     asm_full_simp_tac (simpset() addsimps [S_def,S4_def]) 1
   192 	    ]);
   193 
   194 qed_goal "S4b_live" MemoryImplementation.thy
   195   "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)) \
   196 \     & WF(MemReturn rmCh ires p)_(m p) \
   197 \     --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
   198    (K [REPEAT (resolve_tac [WF1, S4b_successors,S4bReturn_successors, S4bReturn_enabled] 1)]);
   199 
   200 (* ------------------------------ State S5 ------------------------------ *)
   201 
   202 qed_goal "S5_successors" MemoryImplementation.thy
   203    "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
   204 \      --> (S5 rmhist p)` | (S6 rmhist p)`"
   205    (fn _ => [split_idle_tac [] 1,
   206 	     auto_tac (MI_css addSDs2 [Step1_2_5])
   207 	    ]);
   208 
   209 qed_goal "S5RPC_successors" MemoryImplementation.thy
   210    "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) \
   211 \     & <RPCNext crCh rmCh rst p>_(r p) \
   212 \     --> (S6 rmhist p)`"
   213    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_5]) ]);
   214 
   215 qed_goal "S5RPC_enabled" MemoryImplementation.thy
   216    "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
   217 \      --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
   218    (fn _ => [auto_tac (MI_css addsimps2 [r_def]
   219 		              addSIs2 [RPCFail_Next_enabled, RPCFail_enabled]),
   220 	     cut_facts_tac [MI_base] 1,
   221 	     blast_tac (claset() addDs [base_pair]) 1,
   222 	     ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S5_def]))
   223 	    ]);
   224 
   225 qed_goal "S5_live" MemoryImplementation.thy
   226    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))   \
   227 \      & WF(RPCNext crCh rmCh rst p)_(r p) \
   228 \      --> (S5 rmhist p ~> S6 rmhist p)"
   229    (fn _ => [REPEAT (resolve_tac [WF1,S5_successors,S5RPC_successors,S5RPC_enabled] 1)]);
   230 
   231 
   232 (* ------------------------------ State S6 ------------------------------ *)
   233 
   234 qed_goal "S6_successors" MemoryImplementation.thy
   235    "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
   236 \      --> (S1 rmhist p)` | (S3 rmhist p)` | (S6 rmhist p)`"
   237    (fn _ => [split_idle_tac [] 1,
   238 	     auto_tac (MI_css addSDs2 [Step1_2_6])
   239 	    ]);
   240 
   241 qed_goal "S6MClkReply_successors" MemoryImplementation.thy
   242    "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) \
   243 \      & <MClkReply memCh crCh cst p>_(c p) \
   244 \      --> (S1 rmhist p)`"
   245    (fn _ => [auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_6, MClkReplyNotRetry])
   246 	    ]);
   247 
   248 qed_goal "MClkReplyS6" MemoryImplementation.thy
   249    "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
   250    (fn _ => [action_simp_tac
   251 	        (simpset() addsimps
   252 		    [angle_def,MClkReply_def,Return_def,
   253 		     ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
   254 		[] [] 1
   255 	    ]);
   256 
   257 qed_goal "S6MClkReply_enabled" MemoryImplementation.thy
   258    "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
   259    (fn _ => [auto_tac (MI_css addsimps2 [c_def] addSIs2 [MClkReply_enabled]),
   260 	     cut_facts_tac [MI_base] 1,
   261 	     blast_tac (claset() addDs [base_pair]) 1,
   262 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S6_def]) [] [])
   263 	    ]);
   264 
   265 qed_goal "S6_live" MemoryImplementation.thy
   266    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p)) \
   267 \      & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)  \
   268 \      --> []<>(S1 rmhist p)"
   269    (fn _ => [Clarsimp_tac 1,
   270 	     subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1,
   271              etac InfiniteEnsures 1, atac 1,
   272 	     action_simp_tac (simpset()) []
   273 	                     (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1,
   274 	     auto_tac (MI_css addsimps2 [SF_def]),
   275 	     etac swap 1,
   276 	     auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE])
   277 	    ]);
   278 
   279 (* ------------------------------ complex leadsto properties ------------------------------ *)
   280 
   281 qed_goal "S5S6LeadstoS6" MemoryImplementation.thy
   282    "!!sigma. sigma |= S5 rmhist p ~> S6 rmhist p \
   283 \      ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
   284    (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro, LatticeReflexivity])
   285 	    ]);
   286 
   287 qed_goal "S4bS5S6LeadstoS6" MemoryImplementation.thy
   288    "!!sigma. [| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
   289 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
   290 \      ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p \
   291 \                   ~> S6 rmhist p"
   292    (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6]
   293 		              addIs2 [LatticeTransitivity])
   294             ]);
   295 
   296 qed_goal "S4S5S6LeadstoS6" MemoryImplementation.thy
   297    "!!sigma. [| sigma |= S4 rmhist p & ires!p = #NotAResult \
   298 \                        ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; \
   299 \               sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
   300 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
   301 \      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
   302    (fn _ => [subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) | (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p" 1,
   303 	     eres_inst_tac [("G", "PRED ((S4 rmhist p & ires!p = #NotAResult) | (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p)")] (temp_use LatticeTransitivity) 1,
   304 	     force_tac (MI_css addsimps2 Init_defs addSIs2 [ImplLeadsto_gen, necT]) 1,
   305 	     rtac (temp_use LatticeDisjunctionIntro) 1,
   306 	     etac (temp_use LatticeTransitivity) 1,
   307 	     etac (temp_use LatticeTriangle2) 1, atac 1,
   308 	     auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6])
   309 	    ]);
   310 
   311 qed_goal "S3S4S5S6LeadstoS6" MemoryImplementation.thy
   312    "!!sigma. [| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;   \
   313 \               sigma |= S4 rmhist p & ires!p = #NotAResult \
   314 \                         ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; \
   315 \               sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
   316 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
   317 \      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
   318    (fn _ => [rtac (temp_use LatticeDisjunctionIntro) 1,
   319 	     etac (temp_use LatticeTriangle2) 1,
   320 	     rtac (S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1,
   321 	     auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,necT]
   322 			      addIs2 [ImplLeadsto_gen] addsimps2 Init_defs)
   323 	    ]);
   324 
   325 qed_goal "S2S3S4S5S6LeadstoS6" MemoryImplementation.thy
   326    "!!sigma. [| sigma |= S2 rmhist p ~> S3 rmhist p; \
   327 \               sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;   \
   328 \               sigma |= S4 rmhist p & ires!p = #NotAResult \
   329 \                         ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; \
   330 \               sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
   331 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
   332 \      ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \
   333 \                   ~> S6 rmhist p"
   334    (fn _ => [rtac (temp_use LatticeDisjunctionIntro) 1,
   335 	     rtac (temp_use LatticeTransitivity) 1, atac 2,
   336 	     rtac (S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1,
   337 	     auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,necT]
   338 			      addIs2 [ImplLeadsto_gen] addsimps2 Init_defs)
   339 	    ]);
   340 
   341 qed_goal "NotS1LeadstoS6" MemoryImplementation.thy
   342    "!!sigma. [| sigma |= []ImpInv rmhist p; \
   343 \        sigma |= S2 rmhist p ~> S3 rmhist p; \
   344 \        sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; \
   345 \        sigma |= S4 rmhist p & ires!p = #NotAResult \
   346 \                 ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; \
   347 \        sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
   348 \        sigma |= S5 rmhist p ~> S6 rmhist p |] \
   349 \        ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
   350    (fn _ => [rtac (S2S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1,
   351              TRYALL atac,
   352              etac (temp_use INV_leadsto) 1,
   353              rtac (temp_use ImplLeadsto_gen) 1,
   354              rtac (temp_use necT) 1,
   355 	     auto_tac (MI_css addsimps2 ImpInv_def::Init_defs addSIs2 [necT])
   356 	    ]);
   357 
   358 qed_goal "S1Infinite" MemoryImplementation.thy
   359    "!!sigma. [| sigma |= ~S1 rmhist p ~> S6 rmhist p; \
   360 \               sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |] \
   361 \            ==> sigma |= []<>S1 rmhist p"
   362    (fn _ => [rtac classical 1,
   363 	     asm_full_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1,
   364 	     auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [DBImplBD])
   365 	    ]);