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