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