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