src/HOL/TLA/Memory/MIsafe.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:        MIsafe.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 about memory implementation (safety)
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
(* ========================= Lemmas about values ========================= *)
wenzelm@3807
    10
wenzelm@3807
    11
(* RPCFailure notin MemVals U {OK,BadArg} *)
wenzelm@3807
    12
wenzelm@6255
    13
qed_goalw "MVOKBAnotRF" MemoryImplementation.thy [MVOKBA_def]
wenzelm@3807
    14
   "!!x. MVOKBA x ==> x ~= RPCFailure"
wenzelm@6255
    15
   (fn _ => [ Auto_tac ]);
wenzelm@3807
    16
wenzelm@3807
    17
(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
wenzelm@3807
    18
wenzelm@6255
    19
qed_goalw "MVOKBARFnotNR" MemoryImplementation.thy [MVOKBARF_def]
wenzelm@3807
    20
   "!!x. MVOKBARF x ==> x ~= NotAResult"
wenzelm@6255
    21
   (fn _ => [ Auto_tac ]);
wenzelm@3807
    22
wenzelm@3807
    23
(* ========================= Si's are mutually exclusive ==================================== *)
wenzelm@3807
    24
(* Si and Sj are mutually exclusive for i # j. This helps to simplify the big
wenzelm@3807
    25
   conditional in the definition of resbar when doing the step-simulation proof.
wenzelm@3807
    26
   We prove a weaker result, which suffices for our purposes: 
wenzelm@3807
    27
   Si implies (not Sj), for j<i.
wenzelm@3807
    28
*)
wenzelm@3807
    29
wenzelm@3807
    30
(* --- not used ---
wenzelm@3807
    31
qed_goal "S1_excl" MemoryImplementation.thy 
wenzelm@6255
    32
     "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p & \
wenzelm@6255
    33
\                        ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
wenzelm@3807
    34
   (fn _ => [ auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def,
wenzelm@3807
    35
                                          S3_def, S4_def, S5_def, S6_def])
wenzelm@3807
    36
            ]);
wenzelm@3807
    37
*)
wenzelm@3807
    38
wenzelm@3807
    39
qed_goal "S2_excl" MemoryImplementation.thy 
wenzelm@6255
    40
     "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p"
wenzelm@3807
    41
   (fn _ => [ auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def]) ]);
wenzelm@3807
    42
wenzelm@3807
    43
qed_goal "S3_excl" MemoryImplementation.thy 
wenzelm@6255
    44
     "|- S3 rmhist p --> S3 rmhist p & ~S1 rmhist p & ~S2 rmhist p"
wenzelm@3807
    45
   (fn _ => [ auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def, S3_def]) ]);
wenzelm@3807
    46
wenzelm@3807
    47
qed_goal "S4_excl" MemoryImplementation.thy 
wenzelm@6255
    48
     "|- S4 rmhist p --> S4 rmhist p & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p"
wenzelm@3807
    49
   (fn _ => [ auto_tac (MI_css addsimps2 [S_def,S1_def,S2_def,S3_def,S4_def]) ]);
wenzelm@3807
    50
wenzelm@3807
    51
qed_goal "S5_excl" MemoryImplementation.thy 
wenzelm@6255
    52
     "|- S5 rmhist p --> S5 rmhist p & ~S1 rmhist p & ~S2 rmhist p \
wenzelm@6255
    53
\                        & ~S3 rmhist p & ~S4 rmhist p"
wenzelm@3807
    54
   (fn _ => [ auto_tac (MI_css addsimps2 [S_def,S1_def,S2_def,S3_def,S4_def,S5_def]) ]);
wenzelm@3807
    55
wenzelm@3807
    56
qed_goal "S6_excl" MemoryImplementation.thy 
wenzelm@6255
    57
     "|- S6 rmhist p --> S6 rmhist p & ~S1 rmhist p & ~S2 rmhist p  \
wenzelm@6255
    58
\                        & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p"
wenzelm@3807
    59
   (fn _ => [ auto_tac (MI_css addsimps2 [S_def,S1_def,S2_def,S3_def,S4_def,S5_def,S6_def]) ]);
wenzelm@3807
    60
wenzelm@3807
    61
wenzelm@3807
    62
(* ==================== Lemmas about the environment ============================== *)
wenzelm@3807
    63
wenzelm@3807
    64
qed_goal "Envbusy" MemoryImplementation.thy
wenzelm@6255
    65
   "|- $(Calling memCh p) --> ~ENext p"
wenzelm@3807
    66
   (fn _ => [ auto_tac (MI_css addsimps2 [ENext_def,Call_def]) ]);
wenzelm@3807
    67
wenzelm@3807
    68
(* ==================== Lemmas about the implementation's states ==================== *)
wenzelm@3807
    69
wenzelm@3807
    70
(* The following series of lemmas are used in establishing the implementation's
wenzelm@3807
    71
   next-state relation (Step 1.2 of the proof in the paper). For each state Si, we
wenzelm@6255
    72
   determine which component actions are possible and what state they result in.
wenzelm@3807
    73
*)
wenzelm@3807
    74
wenzelm@3807
    75
(* ------------------------------ State S1 ---------------------------------------- *) 
wenzelm@3807
    76
wenzelm@3807
    77
qed_goal "S1Env" MemoryImplementation.thy
wenzelm@6255
    78
   "|- ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p) --> (S2 rmhist p)$"
wenzelm@6255
    79
   (fn _ => [force_tac (MI_css
wenzelm@6255
    80
		        addsimps2 [ENext_def,Call_def,c_def,r_def,m_def,
wenzelm@6255
    81
			   	   caller_def,rtrner_def,MVNROKBA_def,
wenzelm@6255
    82
                                   S_def,S1_def,S2_def,Calling_def]) 1
wenzelm@3807
    83
	    ]);
wenzelm@3807
    84
wenzelm@3807
    85
qed_goal "S1ClerkUnch" MemoryImplementation.thy 
wenzelm@6255
    86
   "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
wenzelm@6255
    87
   (fn _ => [auto_tac (MI_fast_css addSDs2 [MClkidle] addsimps2 [S_def,S1_def]) ]);
wenzelm@3807
    88
wenzelm@3807
    89
qed_goal "S1RPCUnch" MemoryImplementation.thy
wenzelm@6255
    90
   "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
wenzelm@6255
    91
   (fn _ => [auto_tac (MI_fast_css addSDs2 [RPCidle] addsimps2 [S_def,S1_def]) ]);
wenzelm@3807
    92
wenzelm@3807
    93
qed_goal "S1MemUnch" MemoryImplementation.thy
wenzelm@6255
    94
   "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
wenzelm@6255
    95
   (fn _ => [auto_tac (MI_fast_css addSDs2 [Memoryidle] addsimps2 [S_def,S1_def]) ]);
wenzelm@3807
    96
wenzelm@3807
    97
qed_goal "S1Hist" MemoryImplementation.thy
wenzelm@6255
    98
   "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p) --> unchanged (rmhist!p)"
wenzelm@6255
    99
   (fn _ => [action_simp_tac (simpset() addsimps [HNext_def, S_def, S1_def, MemReturn_def, 
wenzelm@6255
   100
                                                  RPCFail_def,MClkReply_def,Return_def])
wenzelm@6255
   101
                             [] [squareE] 1
wenzelm@3807
   102
	    ]);
wenzelm@3807
   103
wenzelm@3807
   104
(* ------------------------------ State S2 ---------------------------------------- *)
wenzelm@3807
   105
wenzelm@3807
   106
qed_goal "S2EnvUnch" MemoryImplementation.thy
wenzelm@6255
   107
   "|- [ENext p]_(e p) & $(S2 rmhist p) --> unchanged (e p)"
wenzelm@6255
   108
   (fn _ => [auto_tac (MI_css addSDs2 [Envbusy] addsimps2 [S_def,S2_def]) ]);
wenzelm@3807
   109
wenzelm@3807
   110
qed_goal "S2Clerk" MemoryImplementation.thy
wenzelm@6255
   111
   "|- MClkNext memCh crCh cst p & $(S2 rmhist p) --> MClkFwd memCh crCh cst p"
wenzelm@6255
   112
   (fn _ => [auto_tac (MI_css addsimps2 [MClkNext_def,MClkRetry_def,MClkReply_def,
wenzelm@6255
   113
					 S_def,S2_def])
wenzelm@3807
   114
	    ]);
wenzelm@3807
   115
wenzelm@3807
   116
qed_goal "S2Forward" MemoryImplementation.thy
wenzelm@6255
   117
   "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p & unchanged (e p, r p, m p, rmhist!p) \
wenzelm@6255
   118
\      --> (S3 rmhist p)$"
wenzelm@4089
   119
   (fn _ => [action_simp_tac (simpset() addsimps
wenzelm@3807
   120
                [MClkFwd_def,Call_def,e_def,r_def,m_def,caller_def,rtrner_def,
wenzelm@3807
   121
                 S_def,S2_def,S3_def,Calling_def])
wenzelm@3807
   122
               [] [] 1
wenzelm@3807
   123
	     ]);
wenzelm@3807
   124
wenzelm@3807
   125
qed_goal "S2RPCUnch" MemoryImplementation.thy
wenzelm@6255
   126
   "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
wenzelm@6255
   127
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S2_def] addSDs2 [RPCidle]) ]);
wenzelm@3807
   128
wenzelm@3807
   129
qed_goal "S2MemUnch" MemoryImplementation.thy
wenzelm@6255
   130
   "|- [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) --> unchanged (m p)"
wenzelm@6255
   131
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S2_def] addSDs2 [Memoryidle]) ]);
wenzelm@3807
   132
wenzelm@3807
   133
qed_goal "S2Hist" MemoryImplementation.thy
wenzelm@6255
   134
   "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p) --> unchanged (rmhist!p)"
wenzelm@3807
   135
   (fn _ => [auto_tac (MI_fast_css
wenzelm@6255
   136
		       addsimps2 [HNext_def,MemReturn_def,
wenzelm@3807
   137
				  RPCFail_def,MClkReply_def,Return_def,S_def,S2_def])
wenzelm@3807
   138
	    ]);
wenzelm@3807
   139
wenzelm@3807
   140
(* ------------------------------ State S3 ---------------------------------------- *)
wenzelm@3807
   141
wenzelm@3807
   142
qed_goal "S3EnvUnch" MemoryImplementation.thy
wenzelm@6255
   143
   "|- [ENext p]_(e p) & $(S3 rmhist p) --> unchanged (e p)"
wenzelm@6255
   144
   (fn _ => [auto_tac (MI_css addSDs2 [Envbusy] addsimps2 [S_def,S3_def]) ]);
wenzelm@3807
   145
wenzelm@3807
   146
qed_goal "S3ClerkUnch" MemoryImplementation.thy 
wenzelm@6255
   147
   "|- [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) --> unchanged (c p)"
wenzelm@6255
   148
   (fn _ => [auto_tac (MI_css addSDs2 [MClkbusy] addsimps2 [square_def,S_def,S3_def]) ]);
wenzelm@3807
   149
wenzelm@3807
   150
qed_goal "S3LegalRcvArg" MemoryImplementation.thy
wenzelm@6255
   151
   "|- S3 rmhist p --> IsLegalRcvArg<arg<crCh!p>>"
wenzelm@6255
   152
   (fn _ => [auto_tac (MI_css addsimps2 [IsLegalRcvArg_def,MClkRelayArg_def,S_def,S3_def]) ]);
wenzelm@3807
   153
wenzelm@3807
   154
qed_goal "S3RPC" MemoryImplementation.thy
wenzelm@6255
   155
   "|- RPCNext crCh rmCh rst p & $(S3 rmhist p) \
wenzelm@6255
   156
\      --> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
wenzelm@6255
   157
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   158
             forward_tac [action_use S3LegalRcvArg] 1,
wenzelm@3807
   159
	     auto_tac (MI_css addsimps2 [RPCNext_def,RPCReject_def,RPCReply_def,S_def,S3_def])
wenzelm@3807
   160
	    ]);
wenzelm@3807
   161
wenzelm@3807
   162
qed_goal "S3Forward" MemoryImplementation.thy
wenzelm@6255
   163
   "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p) & unchanged (e p, c p, m p) \
wenzelm@6255
   164
\      --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@3807
   165
   (fn _ => [action_simp_tac 
wenzelm@4089
   166
               (simpset() addsimps [RPCFwd_def,HNext_def,MemReturn_def,RPCFail_def,MClkReply_def,
wenzelm@3807
   167
				   Return_def,Call_def,e_def,c_def,m_def,caller_def,rtrner_def, 
wenzelm@3807
   168
				   S_def,S3_def,S4_def,Calling_def])
wenzelm@3807
   169
	       [] [] 1
wenzelm@3807
   170
	    ]);
wenzelm@3807
   171
wenzelm@3807
   172
qed_goal "S3Fail" MemoryImplementation.thy
wenzelm@6255
   173
   "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p & unchanged (e p, c p, m p) \
wenzelm@6255
   174
\      --> (S6 rmhist p)$"
wenzelm@3807
   175
   (fn _ => [action_simp_tac 
wenzelm@4089
   176
               (simpset() addsimps [HNext_def,RPCFail_def,Return_def,e_def,c_def,m_def,
wenzelm@3807
   177
				   caller_def,rtrner_def,MVOKBARF_def,
wenzelm@3807
   178
				   S_def,S3_def,S6_def,Calling_def])
wenzelm@3807
   179
               [] [] 1
wenzelm@3807
   180
	    ]);
wenzelm@3807
   181
wenzelm@3807
   182
qed_goal "S3MemUnch" MemoryImplementation.thy
wenzelm@6255
   183
   "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
wenzelm@6255
   184
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S3_def] addSDs2 [Memoryidle]) ]);
wenzelm@3807
   185
wenzelm@3807
   186
qed_goal "S3Hist" MemoryImplementation.thy
wenzelm@6255
   187
   "|- HNext rmhist p & $(S3 rmhist p) & unchanged (r p) --> unchanged (rmhist!p)"
wenzelm@6255
   188
   (fn _ => [auto_tac (MI_css
wenzelm@3807
   189
		       addsimps2 [HNext_def,MemReturn_def,RPCFail_def,MClkReply_def,
wenzelm@3807
   190
				  Return_def,r_def,rtrner_def,S_def,S3_def,Calling_def])
wenzelm@3807
   191
	    ]);
wenzelm@3807
   192
wenzelm@3807
   193
wenzelm@3807
   194
(* ------------------------------ State S4 ---------------------------------------- *)
wenzelm@3807
   195
wenzelm@3807
   196
qed_goal "S4EnvUnch" MemoryImplementation.thy
wenzelm@6255
   197
   "|- [ENext p]_(e p) & $(S4 rmhist p) --> unchanged (e p)"
wenzelm@6255
   198
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S4_def] addSDs2 [Envbusy]) ]);
wenzelm@3807
   199
wenzelm@3807
   200
qed_goal "S4ClerkUnch" MemoryImplementation.thy
wenzelm@6255
   201
   "|- [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) --> unchanged (c p)"
wenzelm@6255
   202
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S4_def] addSDs2 [MClkbusy]) ]);
wenzelm@3807
   203
wenzelm@3807
   204
qed_goal "S4RPCUnch" MemoryImplementation.thy
wenzelm@6255
   205
   "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
wenzelm@6255
   206
   (fn _ => [auto_tac (MI_fast_css addsimps2 [S_def,S4_def] addSDs2 [RPCbusy]) ]);
wenzelm@3807
   207
wenzelm@3807
   208
qed_goal "S4ReadInner" MemoryImplementation.thy
wenzelm@6255
   209
   "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p) \
wenzelm@6255
   210
\           & HNext rmhist p & $(MemInv mm l) \
wenzelm@6255
   211
\      --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@3807
   212
   (fn _ => [action_simp_tac 
wenzelm@4089
   213
               (simpset() addsimps [ReadInner_def,GoodRead_def, BadRead_def,HNext_def,
wenzelm@3807
   214
				   MemReturn_def, RPCFail_def,MClkReply_def,Return_def,
wenzelm@3807
   215
				   e_def,c_def,r_def,rtrner_def,caller_def,MVNROKBA_def,
wenzelm@3807
   216
				   S_def,S4_def,RdRequest_def,Calling_def,MemInv_def])
wenzelm@3807
   217
               [] [] 1
wenzelm@3807
   218
	    ]);
wenzelm@3807
   219
wenzelm@3807
   220
qed_goal "S4Read" MemoryImplementation.thy
wenzelm@6255
   221
   "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p) \
wenzelm@6255
   222
\           & HNext rmhist p & (!l. $MemInv mm l) \
wenzelm@6255
   223
\      --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@6255
   224
   (fn _ => [auto_tac (MI_css addsimps2 [Read_def] addSDs2 [S4ReadInner]) ]);
wenzelm@3807
   225
wenzelm@3807
   226
qed_goal "S4WriteInner" MemoryImplementation.thy
wenzelm@6255
   227
   "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) \
wenzelm@6255
   228
\           & HNext rmhist p \
wenzelm@6255
   229
\      --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@3807
   230
   (fn _ => [action_simp_tac 
wenzelm@4089
   231
               (simpset() addsimps [WriteInner_def,GoodWrite_def, BadWrite_def,HNext_def,
wenzelm@3807
   232
				   MemReturn_def,RPCFail_def,MClkReply_def,Return_def,
wenzelm@3807
   233
				   e_def,c_def,r_def,rtrner_def,caller_def,MVNROKBA_def, 
wenzelm@3807
   234
				   S_def,S4_def,WrRequest_def,Calling_def])
wenzelm@3807
   235
               [] [] 1
wenzelm@3807
   236
	    ]);
wenzelm@3807
   237
wenzelm@3807
   238
qed_goal "S4Write" MemoryImplementation.thy
wenzelm@6255
   239
   "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p) & (HNext rmhist p) \
wenzelm@6255
   240
\      --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@6255
   241
   (fn _ => [ auto_tac (MI_css addsimps2 [Write_def] addSDs2 [S4WriteInner]) ]);
wenzelm@3807
   242
wenzelm@3807
   243
qed_goal "WriteS4" MemoryImplementation.thy
wenzelm@6255
   244
   "|- $ImpInv rmhist p & Write rmCh mm ires p l --> $S4 rmhist p"
wenzelm@6255
   245
   (fn _ => [auto_tac (MI_css
wenzelm@3807
   246
		       addsimps2 [Write_def,WriteInner_def,ImpInv_def,WrRequest_def,
wenzelm@3807
   247
				  S_def,S1_def,S2_def,S3_def,S4_def,S5_def,S6_def])
wenzelm@3807
   248
            ]);
wenzelm@3807
   249
wenzelm@3807
   250
qed_goal "S4Return" MemoryImplementation.thy
wenzelm@6255
   251
   "|- MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p) & HNext rmhist p \
wenzelm@6255
   252
\      --> (S5 rmhist p)$"
wenzelm@6255
   253
   (fn _ => [auto_tac (MI_css
wenzelm@3807
   254
		       addsimps2 [HNext_def,MemReturn_def,Return_def,e_def,c_def,r_def,
wenzelm@3807
   255
				  rtrner_def,caller_def,MVNROKBA_def,MVOKBA_def,
wenzelm@3807
   256
		                  S_def,S4_def,S5_def,Calling_def])
wenzelm@3807
   257
	    ]);
wenzelm@3807
   258
wenzelm@3807
   259
qed_goal "S4Hist" MemoryImplementation.thy
wenzelm@6255
   260
   "|- HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@6255
   261
   (fn _ => [auto_tac (MI_css
wenzelm@3807
   262
		       addsimps2 [HNext_def,MemReturn_def,RPCFail_def,MClkReply_def,
wenzelm@3807
   263
				  Return_def,m_def,rtrner_def,S_def,S4_def,Calling_def])
wenzelm@3807
   264
	    ]);
wenzelm@3807
   265
wenzelm@3807
   266
(* ------------------------------ State S5 ---------------------------------------- *)
wenzelm@3807
   267
wenzelm@3807
   268
qed_goal "S5EnvUnch" MemoryImplementation.thy
wenzelm@6255
   269
   "|- [ENext p]_(e p) & $(S5 rmhist p) --> unchanged (e p)"
wenzelm@6255
   270
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S5_def] addSDs2 [Envbusy]) ]);
wenzelm@3807
   271
wenzelm@3807
   272
qed_goal "S5ClerkUnch" MemoryImplementation.thy
wenzelm@6255
   273
   "|- [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) --> unchanged (c p)"
wenzelm@6255
   274
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S5_def] addSDs2 [MClkbusy]) ]);
wenzelm@3807
   275
wenzelm@3807
   276
qed_goal "S5RPC" MemoryImplementation.thy
wenzelm@6255
   277
   "|- RPCNext crCh rmCh rst p & $(S5 rmhist p)   \
wenzelm@6255
   278
\      --> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
wenzelm@6255
   279
   (fn _ => [auto_tac (MI_css
wenzelm@3807
   280
		       addsimps2 [RPCNext_def,RPCReject_def,RPCFwd_def,S_def,S5_def])
wenzelm@3807
   281
	    ]);
wenzelm@3807
   282
wenzelm@3807
   283
qed_goal "S5Reply" MemoryImplementation.thy
wenzelm@6255
   284
   "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p) \
wenzelm@6255
   285
\      --> (S6 rmhist p)$"
wenzelm@3807
   286
   (fn _ => [action_simp_tac 
wenzelm@4089
   287
               (simpset()
wenzelm@3807
   288
		addsimps [RPCReply_def,Return_def,e_def,c_def,m_def,
wenzelm@3807
   289
			  MVOKBA_def,MVOKBARF_def,caller_def,rtrner_def,
wenzelm@3807
   290
			  S_def,S5_def,S6_def,Calling_def])
wenzelm@3807
   291
               [] [] 1
wenzelm@3807
   292
	    ]);
wenzelm@3807
   293
wenzelm@3807
   294
qed_goal "S5Fail" MemoryImplementation.thy
wenzelm@6255
   295
   "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p) \
wenzelm@6255
   296
\      --> (S6 rmhist p)$"
wenzelm@3807
   297
   (fn _ => [action_simp_tac
wenzelm@4089
   298
	       (simpset()
wenzelm@3807
   299
		addsimps [RPCFail_def,Return_def,e_def,c_def,m_def,
wenzelm@3807
   300
			  MVOKBARF_def,caller_def,rtrner_def,
wenzelm@3807
   301
			  S_def,S5_def,S6_def,Calling_def])
wenzelm@3807
   302
               [] [] 1
wenzelm@3807
   303
	    ]);
wenzelm@3807
   304
wenzelm@3807
   305
qed_goal "S5MemUnch" MemoryImplementation.thy
wenzelm@6255
   306
   "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
wenzelm@6255
   307
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S5_def] addSDs2 [Memoryidle]) ]);
wenzelm@3807
   308
wenzelm@3807
   309
qed_goal "S5Hist" MemoryImplementation.thy
wenzelm@6255
   310
   "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@3807
   311
   (fn _ => [auto_tac (MI_fast_css
wenzelm@6255
   312
		       addsimps2 [HNext_def,MemReturn_def,
wenzelm@3807
   313
				  RPCFail_def,MClkReply_def,Return_def,S_def,S5_def])
wenzelm@3807
   314
	    ]);
wenzelm@3807
   315
wenzelm@3807
   316
(* ------------------------------ State S6 ---------------------------------------- *)
wenzelm@3807
   317
wenzelm@3807
   318
qed_goal "S6EnvUnch" MemoryImplementation.thy
wenzelm@6255
   319
   "|- [ENext p]_(e p) & $(S6 rmhist p) --> unchanged (e p)"
wenzelm@6255
   320
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S6_def] addSDs2 [Envbusy]) ]);
wenzelm@3807
   321
wenzelm@3807
   322
qed_goal "S6Clerk" MemoryImplementation.thy
wenzelm@6255
   323
   "|- MClkNext memCh crCh cst p & $(S6 rmhist p) \
wenzelm@6255
   324
\      --> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
wenzelm@6255
   325
   (fn _ => [ auto_tac (MI_css addsimps2 [MClkNext_def,MClkFwd_def,S_def,S6_def]) ]);
wenzelm@3807
   326
wenzelm@3807
   327
qed_goal "S6Retry" MemoryImplementation.thy
wenzelm@6255
   328
   "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p & unchanged (e p,r p,m p) \
wenzelm@6255
   329
\      --> (S3 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@3807
   330
   (fn _ => [action_simp_tac
wenzelm@4089
   331
	        (simpset() addsimps [HNext_def,MClkReply_def,MClkRetry_def,Call_def,
wenzelm@3807
   332
				    Return_def,e_def,r_def,m_def,caller_def,rtrner_def,
wenzelm@3807
   333
		                    S_def,S6_def,S3_def,Calling_def])
wenzelm@3807
   334
                [] [] 1]);
wenzelm@3807
   335
wenzelm@3807
   336
qed_goal "S6Reply" MemoryImplementation.thy
wenzelm@6255
   337
   "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p & unchanged (e p,r p,m p) \
wenzelm@6255
   338
\      --> (S1 rmhist p)$"
wenzelm@4089
   339
   (fn _ => [action_simp_tac (simpset()
wenzelm@3807
   340
			      addsimps [HNext_def,MemReturn_def,RPCFail_def,Return_def,
wenzelm@3807
   341
					MClkReply_def,e_def,r_def,m_def,caller_def,rtrner_def,
wenzelm@3807
   342
					S_def,S6_def,S1_def,Calling_def])
wenzelm@3807
   343
	                     [] [] 1
wenzelm@3807
   344
	    ]);
wenzelm@3807
   345
wenzelm@3807
   346
qed_goal "S6RPCUnch" MemoryImplementation.thy
wenzelm@6255
   347
   "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
wenzelm@6255
   348
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S6_def] addSDs2 [RPCidle]) ]);
wenzelm@3807
   349
wenzelm@3807
   350
qed_goal "S6MemUnch" MemoryImplementation.thy
wenzelm@6255
   351
   "|- [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) --> unchanged (m p)"
wenzelm@6255
   352
   (fn _ => [auto_tac (MI_css addsimps2 [S_def,S6_def] addSDs2 [Memoryidle]) ]);
wenzelm@3807
   353
wenzelm@3807
   354
qed_goal "S6Hist" MemoryImplementation.thy
wenzelm@6255
   355
   "|- HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@6255
   356
   (fn _ => [auto_tac (MI_css
wenzelm@3807
   357
		       addsimps2 [HNext_def,MClkReply_def,Return_def,c_def,rtrner_def,
wenzelm@3807
   358
		                  S_def,S6_def,Calling_def])
wenzelm@3807
   359
	    ]);
wenzelm@6255
   360