Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Memory/MIlive.ML
changeset 6255 db63752140c7
parent 4477 b3e5857d8d99
equal deleted inserted replaced
6254:f6335d319e9f 6255:db63752140c7 
    12 *)
 
    12 *)
 
    13 
    13 
    14 (* ------------------------------ State S1 ------------------------------ *)
 
    14 (* ------------------------------ State S1 ------------------------------ *)
 
    15 
    15 
    16 qed_goal "S1_successors" MemoryImplementation.thy
 
    16 qed_goal "S1_successors" MemoryImplementation.thy
 
    17    "$(S1 rmhist p) .& ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>  \
 
    17    "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)  \
 
    18 \   .-> $(S1 rmhist p)` .| $(S2 rmhist p)`"
 
    18 \      --> (S1 rmhist p)` | (S2 rmhist p)`"
 
    19    (fn _ => [split_idle_tac [] 1,
 
    19    (fn _ => [split_idle_tac [] 1,
 
    20 	     auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_1])
 
    20 	     auto_tac (MI_css addSDs2 [Step1_2_1])
 
    21 	    ]);
 
    21 	    ]);
 
    22 
    22 
    23 (* Show that the implementation can satisfy the high-level fairness requirements
 
    23 (* Show that the implementation can satisfy the high-level fairness requirements
 
    24    by entering the state S1 infinitely often.
 
    24    by entering the state S1 infinitely often.
 
    25 *)
 
    25 *)
 
    26 
    26 
    27 qed_goal "S1_RNextdisabled" MemoryImplementation.thy
 
    27 qed_goal "S1_RNextdisabled" MemoryImplementation.thy
 
    28    "$(S1 rmhist p) .-> \
 
    28    "|- S1 rmhist p --> \
 
    29 \   .~$(Enabled (<RNext memCh mem (resbar rmhist) p>_<rtrner memCh @ p, resbar 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])
 
    30    (fn _ => [action_simp_tac (simpset() addsimps [angle_def,S_def,S1_def])
 
    31 	                     [notI] [enabledE,MemoryidleE] 1,
 
    31 	                     [notI] [enabledE,temp_elim Memoryidle] 1,
 
    32 	     auto_tac MI_fast_css
 
    32 	     Force_tac 1
 
    33 	    ]);
 
    33 	    ]);
 
    34 
    34 
    35 qed_goal "S1_Returndisabled" MemoryImplementation.thy
 
    35 qed_goal "S1_Returndisabled" MemoryImplementation.thy
 
    36    "$(S1 rmhist p) .-> \
 
    36    "|- S1 rmhist p --> \
 
    37 \   .~$(Enabled (<MemReturn memCh (resbar rmhist) p>_<rtrner memCh @ p, resbar 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])
 
    38    (fn _ => [action_simp_tac (simpset() addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def])
 
    39 	                     [notI] [enabledE] 1
 
    39 	                     [notI] [enabledE] 1
 
    40 	    ]);
 
    40 	    ]);
 
    41 
    41 
    42 qed_goal "RNext_fair" MemoryImplementation.thy
 
    42 qed_goal "RNext_fair" MemoryImplementation.thy
 
    43    "!!sigma. (sigma |= []<>($(S1 rmhist p)))   \
 
    43    "|- []<>S1 rmhist p   \
 
    44 \     ==> (sigma |= WF(RNext memCh mem (resbar rmhist) p)_<rtrner memCh @ p, resbar rmhist @ p>)"
 
    44 \      --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
 
    45    (fn _ => [auto_tac (MI_css addsimps2 [temp_rewrite WF_alt]
 
    45    (fn _ => [auto_tac (MI_css addsimps2 [WF_alt]
 
    46 			      addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE])
 
    46 			      addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE])
 
    47 	    ]);
 
    47 	    ]);
 
    48 
    48 
    49 qed_goal "Return_fair" MemoryImplementation.thy
 
    49 qed_goal "Return_fair" MemoryImplementation.thy
 
    50    "!!sigma. (sigma |= []<>($(S1 rmhist p)))   \
 
    50    "|- []<>S1 rmhist p   \
 
    51 \     ==> (sigma |= WF(MemReturn memCh (resbar rmhist) p)_<rtrner memCh @ p, resbar rmhist @ p>)"
 
    51 \      --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
 
    52    (fn _ => [auto_tac (MI_css addsimps2 [temp_rewrite WF_alt]
 
    52    (fn _ => [auto_tac (MI_css addsimps2 [WF_alt]
 
    53 			      addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE])
 
    53 			      addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE])
 
    54 	    ]);
 
    54 	    ]);
 
    55 
    55 
    56 (* ------------------------------ State S2 ------------------------------ *)
 
    56 (* ------------------------------ State S2 ------------------------------ *)
 
    57 
    57 
    58 qed_goal "S2_successors" MemoryImplementation.thy
 
    58 qed_goal "S2_successors" MemoryImplementation.thy
 
    59    "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)   \
 
    59    "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
 
    60 \   .-> $(S2 rmhist p)` .| $(S3 rmhist p)`"
 
    60 \      --> (S2 rmhist p)` | (S3 rmhist p)`"
 
    61    (fn _ => [split_idle_tac [] 1,
 
    61    (fn _ => [split_idle_tac [] 1,
 
    62 	     auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_2])
 
    62 	     auto_tac (MI_css addSDs2 [Step1_2_2])
 
    63 	    ]);
 
    63 	    ]);
 
    64 
    64 
    65 qed_goal "S2MClkFwd_successors" MemoryImplementation.thy
 
    65 qed_goal "S2MClkFwd_successors" MemoryImplementation.thy
 
    66    "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)    \
 
    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) \
 
    67 \      & <MClkFwd memCh crCh cst p>_(c p) \
 
    68 \   .-> $(S3 rmhist p)`"
 
    68 \      --> (S3 rmhist p)`"
 
    69    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_2]) ]);
 
    69    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_2]) ]);
 
    70 
    70 
    71 qed_goal "S2MClkFwd_enabled" MemoryImplementation.thy
 
    71 qed_goal "S2MClkFwd_enabled" MemoryImplementation.thy
 
    72    "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)   \
 
    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)))"
 
    73 \      --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
 
    74    (fn _ => [cut_facts_tac [MI_base] 1,
 
    74    (fn _ => [auto_tac (MI_css addsimps2 [c_def] addSIs2 [MClkFwd_ch_enabled,MClkFwd_enabled]),
 
    75 	     auto_tac (MI_css addsimps2 [c_def,base_pair]
 
    75              cut_facts_tac [MI_base] 1,
 
    76 		              addSIs2 [MClkFwd_ch_enabled,action_mp MClkFwd_enabled]),
 
    76              blast_tac (claset() addDs [base_pair]) 1,
 
    77 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S2_def]) [] [])
 
    77              ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S2_def]))
 
    78 	    ]);
 
    78 	    ]);
 
    79 
    79 
    80 qed_goal "S2_live" MemoryImplementation.thy
 
    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) \
 
    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))"
 
    82 \      --> (S2 rmhist p ~> S3 rmhist p)"
 
    83    (fn _ => [REPEAT (resolve_tac [WF1,S2_successors,
 
    83    (fn _ => [REPEAT (resolve_tac [WF1,S2_successors,
 
    84 				  S2MClkFwd_successors,S2MClkFwd_enabled] 1)
 
    84 				  S2MClkFwd_successors,S2MClkFwd_enabled] 1)
 
    85 	    ]);
 
    85 	    ]);
 
    86 
    86 
    87 
    87 
    88 (* ------------------------------ State S3 ------------------------------ *)
 
    88 (* ------------------------------ State S3 ------------------------------ *)
 
    89 
    89 
    90 qed_goal "S3_successors" MemoryImplementation.thy
 
    90 qed_goal "S3_successors" MemoryImplementation.thy
 
    91    "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)   \
 
    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))`"
 
    92 \      --> (S3 rmhist p)` | (S4 rmhist p | S6 rmhist p)`"
 
    93    (fn _ => [split_idle_tac [] 1,
 
    93    (fn _ => [split_idle_tac [] 1,
 
    94 	     auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_3])
 
    94 	     auto_tac (MI_css addSDs2 [Step1_2_3])
 
    95 	    ]);
 
    95 	    ]);
 
    96 
    96 
    97 qed_goal "S3RPC_successors" MemoryImplementation.thy
 
    97 qed_goal "S3RPC_successors" MemoryImplementation.thy
 
    98    "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)   \
 
    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) \
 
    99 \      & <RPCNext crCh rmCh rst p>_(r p) \
 
   100 \   .-> ($(S4 rmhist p) .| $(S6 rmhist p))`"
 
   100 \      --> (S4 rmhist p | S6 rmhist p)`"
 
   101    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_3]) ]);
 
   101    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_3]) ]);
 
   102 
   102 
   103 qed_goal "S3RPC_enabled" MemoryImplementation.thy
 
   103 qed_goal "S3RPC_enabled" MemoryImplementation.thy
 
   104    "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)   \
 
   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)))"
 
   105 \      --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
 
   106    (fn _ => [cut_facts_tac [MI_base] 1,
 
   106    (fn _ => [auto_tac (MI_css addsimps2 [r_def]
 
   107 	     auto_tac (MI_css addsimps2 [r_def,base_pair]
 
   107 		              addSIs2 [RPCFail_Next_enabled,RPCFail_enabled]),
 
   108 		              addSIs2 [RPCFail_Next_enabled,action_mp RPCFail_enabled]),
 
   108 	     cut_facts_tac [MI_base] 1,
 
   109 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S3_def]) [] [])
 
   109 	     blast_tac (claset() addDs [base_pair]) 1,
 
       
   110              ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S3_def]))
 
   110 	    ]);
 
   111 	    ]);
 
   111 
   112 
   112 qed_goal "S3_live" MemoryImplementation.thy
 
   113 qed_goal "S3_live" MemoryImplementation.thy
 
   113    "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)  \
 
   114    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) & WF(RPCNext crCh rmCh rst p)_(r p) \
 
   114 \        .& WF(RPCNext crCh rmCh rst p)_(r p) \
 
   115 \   --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
 
   115 \   .-> ($(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p)))"
 
       
   116    (fn _ => [REPEAT (resolve_tac [WF1,S3_successors,S3RPC_successors,S3RPC_enabled] 1)]);
 
   116    (fn _ => [REPEAT (resolve_tac [WF1,S3_successors,S3RPC_successors,S3RPC_enabled] 1)]);
 
   117 
   117 
   118 (* ------------- State S4 -------------------------------------------------- *)
 
   118 (* ------------- State S4 -------------------------------------------------- *)
 
   119 
   119 
   120 qed_goal "S4_successors" MemoryImplementation.thy
 
   120 qed_goal "S4_successors" MemoryImplementation.thy
 
   121    "$(S4 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \
 
   121    "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
 
   122 \                                .& (RALL l. $(MemInv mem l)))  \
 
   122 \                   & (!l. $MemInv mm l)  \
 
   123 \   .-> $(S4 rmhist p)` .| $(S5 rmhist p)`"
 
   123 \      --> (S4 rmhist p)` | (S5 rmhist p)`"
 
   124    (fn _ => [split_idle_tac [] 1,
 
   124    (fn _ => [split_idle_tac [] 1,
 
   125 	     auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_4])
 
   125 	     auto_tac (MI_css addSDs2 [Step1_2_4])
 
   126 	    ]);
 
   126 	    ]);
 
   127 
   127 
   128 (* ------------- State S4a: S4 /\ (ires p = NotAResult) ------------------------------ *)
 
   128 (* ------------- State S4a: S4 /\ (ires p = NotAResult) ------------------------------ *)
 
   129 
   129 
   130 qed_goal "S4a_successors" MemoryImplementation.thy
 
   130 qed_goal "S4a_successors" MemoryImplementation.thy
 
   131    "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \
 
   131    "|- $(S4 rmhist p & ires!p = #NotAResult) \
 
   132 \                   .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \
 
   132 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l) \
 
   133 \                                 .& (RALL l. $(MemInv mem l))) \
 
   133 \      --> (S4 rmhist p & ires!p = #NotAResult)`  \
 
   134 \   .-> ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult))`  \
 
   134 \        | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)`"
 
   135 \       .| (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))`"
 
       
   136    (fn _ => [split_idle_tac [m_def] 1,
 
   135    (fn _ => [split_idle_tac [m_def] 1,
 
   137 	     auto_tac (MI_css addsimps2 [m_def] addSEs2 [action_conjimpE Step1_2_4])
 
   136 	     auto_tac (MI_css addSDs2 [Step1_2_4])
 
   138 	    ]);
 
   137 	    ]);
 
   139 
   138 
   140 qed_goal "S4aRNext_successors" MemoryImplementation.thy
 
   139 qed_goal "S4aRNext_successors" MemoryImplementation.thy
 
   141    "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult))  \
 
   140    "|- ($(S4 rmhist p & ires!p = #NotAResult)  \
 
   142 \   .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>   \
 
   141 \       & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))  \
 
   143 \                 .& (RALL l. $(MemInv mem l)))  \
 
   142 \      & <RNext rmCh mm ires p>_(m p) \
 
   144 \   .& <RNext rmCh mem ires p>_(m p) \
 
   143 \      --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)`"
 
   145 \   .-> (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))`"
 
       
   146    (fn _ => [auto_tac (MI_css addsimps2 [angle_def]
 
   144    (fn _ => [auto_tac (MI_css addsimps2 [angle_def]
 
   147 		              addSEs2 [action_conjimpE Step1_2_4,
 
   145 		              addSDs2 [Step1_2_4, ReadResult, WriteResult])
 
   148 				       action_conjimpE ReadResult, action_impE WriteResult])
 
       
   149 	    ]);
 
   146 	    ]);
 
   150 
   147 
   151 qed_goal "S4aRNext_enabled" MemoryImplementation.thy
 
   148 qed_goal "S4aRNext_enabled" MemoryImplementation.thy
 
   152    "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \
 
   149    "|- $(S4 rmhist p & ires!p = #NotAResult) \
 
   153 \   .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>   \
 
   150 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)  \
 
   154 \                 .& (RALL l. $(MemInv mem l)))  \
 
   151 \   --> $Enabled (<RNext rmCh mm ires p>_(m p))"
 
   155 \   .-> $(Enabled (<RNext rmCh mem ires p>_(m p)))"
 
   152    (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [RNext_enabled]),
 
   156    (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [action_mp RNext_enabled]),
 
   153 	     cut_facts_tac [MI_base] 1,
 
   157 	     ALLGOALS (cut_facts_tac [MI_base]),
 
   154 	     blast_tac (claset() addDs [base_pair]) 1,
 
   158 	     auto_tac (MI_css addsimps2 [base_pair]),
 
   155 	     asm_full_simp_tac (simpset() addsimps [S_def,S4_def]) 1
 
   159 	        (* it's faster to expand S4 only where necessary *)
 
       
   160 	     action_simp_tac (simpset() addsimps [S_def,S4_def]) [] [] 1
 
       
   161 	    ]);
 
   156 	    ]);
 
   162 
   157 
   163 qed_goal "S4a_live" MemoryImplementation.thy
 
   158 qed_goal "S4a_live" MemoryImplementation.thy
 
   164   "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& (RALL l. $(MemInv mem l))) \
 
   159   "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)) \
 
   165 \  .& WF(RNext rmCh mem ires p)_(m p) \
 
   160 \     & WF(RNext rmCh mm ires p)_(m p) \
 
   166 \  .-> (($(S4 rmhist p) .& ($(ires@p) .= #NotAResult))  \
 
   161 \     --> (S4 rmhist p & ires!p = #NotAResult  \
 
   167 \        ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))"
 
   162 \          ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
 
   168    (fn _ => [rtac WF1 1,
 
   163    (K [REPEAT (resolve_tac [WF1, S4a_successors, S4aRNext_successors, S4aRNext_enabled] 1)]);
 
   169 	     ALLGOALS (action_simp_tac (simpset())
 
       
   170 		                       (map ((rewrite_rule [slice_def]) o action_mp) 
       
   171                                             [S4a_successors,S4aRNext_successors,S4aRNext_enabled])
 
       
   172 				       [])
 
       
   173 	    ]);
 
       
   174 
   164 
   175 (* ------------- State S4b: S4 /\ (ires p # NotAResult) ------------------------------ *)
 
   165 (* ------------- State S4b: S4 /\ (ires p # NotAResult) ------------------------------ *)
 
   176 
   166 
   177 qed_goal "S4b_successors" MemoryImplementation.thy
 
   167 qed_goal "S4b_successors" MemoryImplementation.thy
 
   178    "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult))  \
 
   168    "|- $(S4 rmhist p & ires!p ~= #NotAResult)  \
 
   179 \                   .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \
 
   169 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l) \
 
   180 \                                 .& (RALL l. $(MemInv mem l))) \
 
   170 \      --> (S4 rmhist p & ires!p ~= #NotAResult)` | (S5 rmhist p)`"
 
   181 \   .-> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult))` .| $(S5 rmhist p)`"
 
       
   182    (fn _ => [split_idle_tac [m_def] 1,
 
   171    (fn _ => [split_idle_tac [m_def] 1,
 
   183 	     auto_tac (MI_css addSEs2 (action_impE WriteResult
 
   172 	     auto_tac (MI_css addSDs2 [WriteResult,Step1_2_4,ReadResult])
 
   184 				       :: map action_conjimpE [Step1_2_4,ReadResult]))
 
       
   185 	    ]);
 
   173 	    ]);
 
   186 
   174 
   187 qed_goal "S4bReturn_successors" MemoryImplementation.thy
 
   175 qed_goal "S4bReturn_successors" MemoryImplementation.thy
 
   188    "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult))  \
 
   176    "|- ($(S4 rmhist p & ires!p ~= #NotAResult)  \
 
   189 \   .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \
 
   177 \       & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))   \
 
   190 \                 .& (RALL l. $(MemInv mem l)))   \
 
   178 \      & <MemReturn rmCh ires p>_(m p) \
 
   191 \   .& <MemReturn rmCh ires p>_(m p) \
 
   179 \      --> (S5 rmhist p)`"
 
   192 \   .-> ($(S5 rmhist p))`"
 
   180    (fn _ => [force_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_4]
 
   193    (fn _ => [auto_tac (MI_css addsimps2 [angle_def]
 
   181                                addDs2 [ReturnNotReadWrite]) 1
 
   194 	                      addSEs2 [action_conjimpE Step1_2_4]
 
       
   195 		              addEs2 [action_conjimpE ReturnNotReadWrite])
 
       
   196 	    ]);
 
   182 	    ]);
 
   197 
   183 
   198 qed_goal "S4bReturn_enabled" MemoryImplementation.thy
 
   184 qed_goal "S4bReturn_enabled" MemoryImplementation.thy
 
   199    "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult))  \
 
   185    "|- $(S4 rmhist p & ires!p ~= #NotAResult)  \
 
   200 \   .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \
 
   186 \      & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)  \
 
   201 \                 .& (RALL l. $(MemInv mem l)))  \
 
   187 \      --> $Enabled (<MemReturn rmCh ires p>_(m p))"
 
   202 \   .-> $(Enabled (<MemReturn rmCh ires p>_(m p)))"
 
   188    (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [MemReturn_enabled]),
 
   203    (fn _ => [cut_facts_tac [MI_base] 1,
 
   189 	     cut_facts_tac [MI_base] 1,
 
   204              auto_tac (MI_css addsimps2 [m_def,base_pair]
 
   190              blast_tac (claset() addDs [base_pair]) 1,
 
   205 		              addSIs2 [action_mp MemReturn_enabled]),
 
   191 	     asm_full_simp_tac (simpset() addsimps [S_def,S4_def]) 1
 
   206 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S4_def]) [] [])
 
       
   207 	    ]);
 
   192 	    ]);
 
   208 
   193 
   209 qed_goal "S4b_live" MemoryImplementation.thy
 
   194 qed_goal "S4b_live" MemoryImplementation.thy
 
   210   "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& (RALL l. $(MemInv mem l))) \
 
   195   "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)) \
 
   211 \  .& WF(MemReturn rmCh ires p)_(m p) \
 
   196 \     & WF(MemReturn rmCh ires p)_(m p) \
 
   212 \  .-> (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p))"
 
   197 \     --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
 
   213    (fn _ => [rtac WF1 1,
 
   198    (K [REPEAT (resolve_tac [WF1, S4b_successors,S4bReturn_successors, S4bReturn_enabled] 1)]);
 
   214 	     ALLGOALS (action_simp_tac (simpset())
 
       
   215 		                       (map ((rewrite_rule [slice_def]) o action_mp) 
       
   216                                             [S4b_successors,S4bReturn_successors,S4bReturn_enabled])
 
       
   217 				       [allE])
 
       
   218 	    ]);
 
       
   219 
   199 
   220 (* ------------------------------ State S5 ------------------------------ *)
 
   200 (* ------------------------------ State S5 ------------------------------ *)
 
   221 
   201 
   222 qed_goal "S5_successors" MemoryImplementation.thy
 
   202 qed_goal "S5_successors" MemoryImplementation.thy
 
   223    "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \
 
   203    "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
 
   224 \   .-> $(S5 rmhist p)` .| $(S6 rmhist p)`"
 
   204 \      --> (S5 rmhist p)` | (S6 rmhist p)`"
 
   225    (fn _ => [split_idle_tac [] 1,
 
   205    (fn _ => [split_idle_tac [] 1,
 
   226 	     auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_5])
 
   206 	     auto_tac (MI_css addSDs2 [Step1_2_5])
 
   227 	    ]);
 
   207 	    ]);
 
   228 
   208 
   229 qed_goal "S5RPC_successors" MemoryImplementation.thy
 
   209 qed_goal "S5RPC_successors" MemoryImplementation.thy
 
   230    "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \
 
   210    "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) \
 
   231 \   .& <RPCNext crCh rmCh rst p>_(r p) \
 
   211 \     & <RPCNext crCh rmCh rst p>_(r p) \
 
   232 \   .-> $(S6 rmhist p)`"
 
   212 \     --> (S6 rmhist p)`"
 
   233    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_5]) ]);
 
   213    (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_5]) ]);
 
   234 
   214 
   235 qed_goal "S5RPC_enabled" MemoryImplementation.thy
 
   215 qed_goal "S5RPC_enabled" MemoryImplementation.thy
 
   236    "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \
 
   216    "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
 
   237 \   .-> $(Enabled (<RPCNext crCh rmCh rst p>_(r p)))"
 
   217 \      --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
 
   238    (fn _ => [cut_facts_tac [MI_base] 1,
 
   218    (fn _ => [auto_tac (MI_css addsimps2 [r_def]
 
   239 	     auto_tac (MI_css addsimps2 [r_def,base_pair]
 
   219 		              addSIs2 [RPCFail_Next_enabled, RPCFail_enabled]),
 
   240 		              addSIs2 [RPCFail_Next_enabled,action_mp RPCFail_enabled]),
 
   220 	     cut_facts_tac [MI_base] 1,
 
   241 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S5_def]) [] [])
 
   221 	     blast_tac (claset() addDs [base_pair]) 1,
 
       
   222 	     ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S5_def]))
 
   242 	    ]);
 
   223 	    ]);
 
   243 
   224 
   244 qed_goal "S5_live" MemoryImplementation.thy
 
   225 qed_goal "S5_live" MemoryImplementation.thy
 
   245    "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>)   \
 
   226    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))   \
 
   246 \   .& WF(RPCNext crCh rmCh rst p)_(r p) \
 
   227 \      & WF(RPCNext crCh rmCh rst p)_(r p) \
 
   247 \   .-> ($(S5 rmhist p) ~> $(S6 rmhist p))"
 
   228 \      --> (S5 rmhist p ~> S6 rmhist p)"
 
   248    (fn _ => [REPEAT (resolve_tac [WF1,S5_successors,S5RPC_successors,S5RPC_enabled] 1)]);
 
   229    (fn _ => [REPEAT (resolve_tac [WF1,S5_successors,S5RPC_successors,S5RPC_enabled] 1)]);
 
   249 
   230 
   250 
   231 
   251 (* ------------------------------ State S6 ------------------------------ *)
 
   232 (* ------------------------------ State S6 ------------------------------ *)
 
   252 
   233 
   253 qed_goal "S6_successors" MemoryImplementation.thy
 
   234 qed_goal "S6_successors" MemoryImplementation.thy
 
   254    "$(S6 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \
 
   235    "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \
 
   255 \   .-> $(S1 rmhist p)` .| $(S3 rmhist p)` .| $(S6 rmhist p)`"
 
   236 \      --> (S1 rmhist p)` | (S3 rmhist p)` | (S6 rmhist p)`"
 
   256    (fn _ => [split_idle_tac [] 1,
 
   237    (fn _ => [split_idle_tac [] 1,
 
   257 	     auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_6])
 
   238 	     auto_tac (MI_css addSDs2 [Step1_2_6])
 
   258 	    ]);
 
   239 	    ]);
 
   259 
   240 
   260 qed_goal "S6MClkReply_successors" MemoryImplementation.thy
 
   241 qed_goal "S6MClkReply_successors" MemoryImplementation.thy
 
   261    "$(S6 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \
 
   242    "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) \
 
   262 \   .& <MClkReply memCh crCh cst p>_(c p) \
 
   243 \      & <MClkReply memCh crCh cst p>_(c p) \
 
   263 \   .-> $(S1 rmhist p)`"
 
   244 \      --> (S1 rmhist p)`"
 
   264    (fn _ => [auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_6,
 
   245    (fn _ => [auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_6, MClkReplyNotRetry])
 
   265 							     action_impE MClkReplyNotRetry])
 
       
   266 	    ]);
 
   246 	    ]);
 
   267 
   247 
   268 qed_goal "MClkReplyS6" MemoryImplementation.thy
 
   248 qed_goal "MClkReplyS6" MemoryImplementation.thy
 
   269    "$(ImpInv rmhist p) .& <MClkReply memCh crCh cst p>_(c p) .-> $(S6 rmhist p)"
 
   249    "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
 
   270    (fn _ => [action_simp_tac
 
   250    (fn _ => [action_simp_tac
 
   271 	        (simpset() addsimps
 
   251 	        (simpset() addsimps
 
   272 		    [angle_def,MClkReply_def,Return_def,
 
   252 		    [angle_def,MClkReply_def,Return_def,
 
   273 		     ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
 
   253 		     ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def])
 
   274 		[] [] 1
 
   254 		[] [] 1
 
   275 	    ]);
 
   255 	    ]);
 
   276 
   256 
   277 qed_goal "S6MClkReply_enabled" MemoryImplementation.thy
 
   257 qed_goal "S6MClkReply_enabled" MemoryImplementation.thy
 
   278    "$(S6 rmhist p) .-> $(Enabled (<MClkReply memCh crCh cst p>_(c p)))"
 
   258    "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
 
   279    (fn _ => [cut_facts_tac [MI_base] 1,
 
   259    (fn _ => [auto_tac (MI_css addsimps2 [c_def] addSIs2 [MClkReply_enabled]),
 
   280 	     auto_tac (MI_css addsimps2 [c_def,base_pair]
 
   260 	     cut_facts_tac [MI_base] 1,
 
   281 		              addSIs2 [action_mp MClkReply_enabled]),
 
   261 	     blast_tac (claset() addDs [base_pair]) 1,
 
   282 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S6_def]) [] [])
 
   262 	     ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S6_def]) [] [])
 
   283 	    ]);
 
   263 	    ]);
 
   284 
   264 
   285 qed_goal "S6_live" MemoryImplementation.thy
 
   265 qed_goal "S6_live" MemoryImplementation.thy
 
   286    "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& $(ImpInv rmhist p)) \
 
   266    "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p)) \
 
   287 \   .& SF(MClkReply memCh crCh cst p)_(c p) .& []<>($(S6 rmhist p))  \
 
   267 \      & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)  \
 
   288 \   .-> []<>($(S1 rmhist p))"
 
   268 \      --> []<>(S1 rmhist p)"
 
   289    (fn _ => [Auto_tac,
 
   269    (fn _ => [Clarsimp_tac 1,
 
   290 	     subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1,
 
   270 	     subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1,
 
   291 	     eres_inst_tac [("P","<MClkReply memCh crCh cst p>_(c p)")]
 
   271              etac InfiniteEnsures 1, atac 1,
 
   292 	                   EnsuresInfinite 1, atac 1,
 
       
   293 	     action_simp_tac (simpset()) []
 
   272 	     action_simp_tac (simpset()) []
 
   294 	                     (map action_conjimpE [MClkReplyS6,S6MClkReply_successors]) 1,
 
   273 	                     (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1,
 
   295 	     auto_tac (MI_css addsimps2 [SF_def]),
 
   274 	     auto_tac (MI_css addsimps2 [SF_def]),
 
   296 	     etac swap 1,
 
   275 	     etac swap 1,
 
   297 	     auto_tac (MI_css addSIs2 [action_mp S6MClkReply_enabled]
 
   276 	     auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE])
 
   298 		              addSEs2 [STL4E,DmdImplE])
 
       
   299 	    ]);
 
   277 	    ]);
 
   300 
   278 
   301 (* ------------------------------ complex leadsto properties ------------------------------ *)
 
   279 (* ------------------------------ complex leadsto properties ------------------------------ *)
 
   302 
   280 
   303 qed_goal "S5S6LeadstoS6" MemoryImplementation.thy
 
   281 qed_goal "S5S6LeadstoS6" MemoryImplementation.thy
 
   304    "!!sigma. (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) \
 
   282    "!!sigma. sigma |= S5 rmhist p ~> S6 rmhist p \
 
   305 \      ==> (sigma |= ($(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))"
 
   283 \      ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
 
   306    (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,
 
   284    (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro, LatticeReflexivity])
 
   307 				       temp_unlift LatticeReflexivity])
 
       
   308 	    ]);
 
   285 	    ]);
 
   309 
   286 
   310 qed_goal "S4bS5S6LeadstoS6" MemoryImplementation.thy
 
   287 qed_goal "S4bS5S6LeadstoS6" MemoryImplementation.thy
 
   311    "!!sigma. [| (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p));  \
 
   288    "!!sigma. [| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
 
   312 \               (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |]  \
 
   289 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
 
   313 \      ==> (sigma |= (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))"
 
   290 \      ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p \
 
       
   291 \                   ~> S6 rmhist p"
 
   314    (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6]
 
   292    (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6]
 
   315 		              addIs2 [LatticeTransitivity])
 
   293 		              addIs2 [LatticeTransitivity])
 
   316             ]);
 
   294             ]);
 
   317 
   295 
   318 qed_goal "S4S5S6LeadstoS6" MemoryImplementation.thy
 
   296 qed_goal "S4S5S6LeadstoS6" MemoryImplementation.thy
 
   319    "!!sigma. [| (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \
 
   297    "!!sigma. [| sigma |= S4 rmhist p & ires!p = #NotAResult \
 
   320 \                             ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \
 
   298 \                        ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; \
 
   321 \               (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p));  \
 
   299 \               sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
 
   322 \               (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |]  \
 
   300 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
 
   323 \      ==> (sigma |= ($(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))"
 
   301 \      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
 
   324    (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,
 
   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,
 
   325 	     eres_inst_tac [("G", "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) .| ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)")] LatticeTransitivity 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,
 
   326 	     SELECT_GOAL (auto_tac (MI_css addSIs2 [ImplLeadsto, temp_unlift necT])) 1,
 
   304 	     force_tac (MI_css addsimps2 Init_defs addSIs2 [ImplLeadsto_gen, necT]) 1,
 
   327 	     rtac LatticeDisjunctionIntro 1,
 
   305 	     rtac (temp_use LatticeDisjunctionIntro) 1,
 
   328 	     etac LatticeTransitivity 1,
 
   306 	     etac (temp_use LatticeTransitivity) 1,
 
   329 	     etac LatticeTriangle 1, atac 1,
 
   307 	     etac (temp_use LatticeTriangle2) 1, atac 1,
 
   330 	     auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6])
 
   308 	     auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6])
 
   331 	    ]);
 
   309 	    ]);
 
   332 
   310 
   333 qed_goal "S3S4S5S6LeadstoS6" MemoryImplementation.thy
 
   311 qed_goal "S3S4S5S6LeadstoS6" MemoryImplementation.thy
 
   334    "!!sigma. [| (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p)));   \
 
   312    "!!sigma. [| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;   \
 
   335 \               (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \
 
   313 \               sigma |= S4 rmhist p & ires!p = #NotAResult \
 
   336 \                         ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \
 
   314 \                         ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; \
 
   337 \               (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p));  \
 
   315 \               sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
 
   338 \               (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |]  \
 
   316 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
 
   339 \      ==> (sigma |= ($(S3 rmhist p) .| $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))"
 
   317 \      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
 
   340    (fn _ => [rtac LatticeDisjunctionIntro 1,
 
   318    (fn _ => [rtac (temp_use LatticeDisjunctionIntro) 1,
 
   341 	     rtac LatticeTriangle 1, atac 2,
 
   319 	     etac (temp_use LatticeTriangle2) 1,
 
   342 	     rtac (S4S5S6LeadstoS6 RS LatticeTransitivity) 1,
 
   320 	     rtac (S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1,
 
   343 	     auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,temp_unlift necT]
 
   321 	     auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,necT]
 
   344 			      addIs2 [ImplLeadsto])
 
   322 			      addIs2 [ImplLeadsto_gen] addsimps2 Init_defs)
 
   345 	    ]);
 
   323 	    ]);
 
   346 
   324 
   347 qed_goal "S2S3S4S5S6LeadstoS6" MemoryImplementation.thy
 
   325 qed_goal "S2S3S4S5S6LeadstoS6" MemoryImplementation.thy
 
   348    "!!sigma. [| (sigma |= $(S2 rmhist p) ~> $(S3 rmhist p)); \
 
   326    "!!sigma. [| sigma |= S2 rmhist p ~> S3 rmhist p; \
 
   349 \               (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p)));   \
 
   327 \               sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;   \
 
   350 \               (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \
 
   328 \               sigma |= S4 rmhist p & ires!p = #NotAResult \
 
   351 \                         ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \
 
   329 \                         ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; \
 
   352 \               (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p));  \
 
   330 \               sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
 
   353 \               (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |]  \
 
   331 \               sigma |= S5 rmhist p ~> S6 rmhist p |]  \
 
   354 \      ==> (sigma |= ($(S2 rmhist p) .| $(S3 rmhist p) .| $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))"
 
   332 \      ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \
 
   355    (fn _ => [rtac LatticeDisjunctionIntro 1,
 
   333 \                   ~> S6 rmhist p"
 
   356 	     rtac LatticeTransitivity 1, atac 2,
 
   334    (fn _ => [rtac (temp_use LatticeDisjunctionIntro) 1,
 
   357 	     rtac (S3S4S5S6LeadstoS6 RS LatticeTransitivity) 1,
 
   335 	     rtac (temp_use LatticeTransitivity) 1, atac 2,
 
   358 	     auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,temp_unlift necT]
 
   336 	     rtac (S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1,
 
   359 			      addIs2 [ImplLeadsto])
 
   337 	     auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,necT]
 
       
   338 			      addIs2 [ImplLeadsto_gen] addsimps2 Init_defs)
 
   360 	    ]);
 
   339 	    ]);
 
   361 
   340 
   362 qed_goal "NotS1LeadstoS6" MemoryImplementation.thy
 
   341 qed_goal "NotS1LeadstoS6" MemoryImplementation.thy
 
   363    "!!sigma. [| (sigma |= []($(ImpInv rmhist p))); \
 
   342    "!!sigma. [| sigma |= []ImpInv rmhist p; \
 
   364 \        (sigma |= $(S2 rmhist p) ~> $(S3 rmhist p)); \
 
   343 \        sigma |= S2 rmhist p ~> S3 rmhist p; \
 
   365 \        (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \
 
   344 \        sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; \
 
   366 \        (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \
 
   345 \        sigma |= S4 rmhist p & ires!p = #NotAResult \
 
   367 \                  ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \
 
   346 \                 ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; \
 
   368 \        (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p));  \
 
   347 \        sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;  \
 
   369 \        (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \
 
   348 \        sigma |= S5 rmhist p ~> S6 rmhist p |] \
 
   370 \        ==> (sigma |= .~$(S1 rmhist p) ~> $(S6 rmhist p))"
 
   349 \        ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
 
   371    (fn _ => [rtac (S2S3S4S5S6LeadstoS6 RS LatticeTransitivity) 1,
 
   350    (fn _ => [rtac (S2S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1,
 
   372 	     auto_tac (MI_css addsimps2 [ImpInv_def] addIs2 [ImplLeadsto] addSEs2 [STL4E])
 
   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])
 
   373 	    ]);
 
   356 	    ]);
 
   374 
   357 
   375 qed_goal "S1Infinite" MemoryImplementation.thy
 
   358 qed_goal "S1Infinite" MemoryImplementation.thy
 
   376    "!!sigma. [| (sigma |= .~$(S1 rmhist p) ~> $(S6 rmhist p)); \
 
   359    "!!sigma. [| sigma |= ~S1 rmhist p ~> S6 rmhist p; \
 
   377 \               (sigma |= []<>($(S6 rmhist p)) .-> []<>($(S1 rmhist p))) |] \
 
   360 \               sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |] \
 
   378 \            ==> (sigma |= []<>($(S1 rmhist p)))"
 
   361 \            ==> sigma |= []<>S1 rmhist p"
 
   379    (fn _ => [rtac classical 1,
 
   362    (fn _ => [rtac classical 1,
 
   380 	     asm_full_simp_tac (simpset() addsimps [NotBox, temp_rewrite NotDmd]) 1,
 
   363 	     asm_full_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1,
 
   381 	     auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [temp_mp DBImplBDAct])
 
   364 	     auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [DBImplBD])
 
   382 	    ]);
 
   365 	    ]);
isabelle