src/HOLCF/ex/Hoare.ML
author berghofe
Mon Aug 05 14:32:56 2002 +0200 (2002-08-05)
changeset 13454 01e2496dee05
parent 10835 f4745d77e620
child 16218 ea49a9c7ff7c
permissions -rw-r--r--
Replaced nat_ind_tac by induct_tac.
clasohm@1461
     1
(*  Title:      HOLCF/ex/hoare.ML
nipkow@244
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
clasohm@1461
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@244
     5
*)
nipkow@244
     6
nipkow@244
     7
(* --------- pure HOLCF logic, some little lemmas ------ *)
nipkow@244
     8
paulson@9265
     9
Goal "b~=TT ==> b=FF | b=UU";
paulson@9265
    10
by (rtac (Exh_tr RS disjE) 1);
paulson@9265
    11
by (fast_tac HOL_cs 1);
paulson@9265
    12
by (etac disjE 1);
paulson@9265
    13
by (contr_tac 1);
paulson@9265
    14
by (fast_tac HOL_cs 1);
paulson@9265
    15
qed "hoare_lemma2";
nipkow@244
    16
nipkow@10835
    17
Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)";
paulson@9265
    18
by (fast_tac HOL_cs 1);
paulson@9265
    19
qed "hoare_lemma3";
nipkow@244
    20
nipkow@10835
    21
Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \
nipkow@10835
    22
\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU";
paulson@9265
    23
by (etac exE 1);
paulson@9265
    24
by (rtac exI 1);
paulson@9265
    25
by (rtac hoare_lemma2 1);
paulson@9265
    26
by (atac 1);
paulson@9265
    27
qed "hoare_lemma4";
nipkow@244
    28
nipkow@10835
    29
Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
nipkow@10835
    30
\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
nipkow@10835
    31
\ b1$(iterate k g x)=FF | b1$(iterate k g x)=UU";
paulson@9265
    32
by (hyp_subst_tac 1);
paulson@9265
    33
by (rtac hoare_lemma2 1);
paulson@9265
    34
by (etac exE 1);
paulson@9265
    35
by (etac LeastI 1);
paulson@9265
    36
qed "hoare_lemma5";
nipkow@244
    37
paulson@9265
    38
Goal "b=UU ==> b~=TT";
paulson@9265
    39
by (hyp_subst_tac 1);
paulson@9265
    40
by (resolve_tac dist_eq_tr 1);
paulson@9265
    41
qed "hoare_lemma6";
paulson@9265
    42
paulson@9265
    43
Goal "b=FF ==> b~=TT";
paulson@9265
    44
by (hyp_subst_tac 1);
paulson@9265
    45
by (resolve_tac dist_eq_tr 1);
paulson@9265
    46
qed "hoare_lemma7";
nipkow@244
    47
nipkow@10835
    48
Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
nipkow@10835
    49
\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
nipkow@10835
    50
\ ALL m. m < k --> b1$(iterate m g x)=TT";
paulson@9265
    51
by (hyp_subst_tac 1);
paulson@9265
    52
by (etac exE 1);
paulson@9265
    53
by (strip_tac 1);
nipkow@10835
    54
by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1);
paulson@9265
    55
by (atac 2);
paulson@9265
    56
by (rtac (le_less_trans RS less_irrefl) 1);
paulson@9265
    57
by (atac 2);
paulson@9265
    58
by (rtac Least_le 1);
paulson@9265
    59
by (etac hoare_lemma6 1);
paulson@9265
    60
by (rtac (le_less_trans RS less_irrefl) 1);
paulson@9265
    61
by (atac 2);
paulson@9265
    62
by (rtac Least_le 1);
paulson@9265
    63
by (etac hoare_lemma7 1);
paulson@9265
    64
qed "hoare_lemma8";
nipkow@244
    65
regensbu@1168
    66
nipkow@10835
    67
Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU";
paulson@9265
    68
by (etac (flat_codom RS disjE) 1);
paulson@9265
    69
by Auto_tac;  
paulson@9265
    70
qed "hoare_lemma28";
nipkow@244
    71
nipkow@244
    72
nipkow@244
    73
(* ----- access to definitions ----- *)
nipkow@244
    74
nipkow@10835
    75
Goal "p$x = If b1$x then p$(g$x) else x fi";
paulson@9265
    76
by (fix_tac3 p_def 1);
paulson@9265
    77
by (Simp_tac 1);
paulson@9265
    78
qed "p_def3";
nipkow@244
    79
nipkow@10835
    80
Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi";
paulson@9265
    81
by (fix_tac3 q_def 1);
paulson@9265
    82
by (Simp_tac 1);
paulson@9265
    83
qed "q_def3";
nipkow@244
    84
nipkow@244
    85
(** --------- proves about iterations of p and q ---------- **)
nipkow@244
    86
nipkow@10835
    87
Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
nipkow@10835
    88
\  p$(iterate k g x)=p$x";
berghofe@13454
    89
by (induct_tac "k" 1);
paulson@9265
    90
by (Simp_tac 1);
paulson@9265
    91
by (Simp_tac 1);
paulson@9265
    92
by (strip_tac 1);
berghofe@13454
    93
by (res_inst_tac [("s","p$(iterate n g x)")] trans 1);
paulson@9265
    94
by (rtac trans 1);
paulson@9265
    95
by (rtac (p_def3 RS sym) 2);
berghofe@13454
    96
by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
paulson@9265
    97
by (rtac mp 1);
paulson@9265
    98
by (etac spec 1);
paulson@9265
    99
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
paulson@9265
   100
by (simp_tac HOLCF_ss 1);
paulson@9265
   101
by (etac mp 1);
paulson@9265
   102
by (strip_tac 1);
paulson@9265
   103
by (rtac mp 1);
paulson@9265
   104
by (etac spec 1);
paulson@9265
   105
by (etac less_trans 1);
paulson@9265
   106
by (Simp_tac 1);
paulson@9265
   107
qed "hoare_lemma9";
nipkow@3044
   108
nipkow@10835
   109
Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
nipkow@10835
   110
\ q$(iterate k g x)=q$x";
berghofe@13454
   111
by (induct_tac "k" 1);
paulson@9265
   112
by (Simp_tac 1);
paulson@9265
   113
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
paulson@9265
   114
by (strip_tac 1);
berghofe@13454
   115
by (res_inst_tac [("s","q$(iterate n g x)")] trans 1);
paulson@9265
   116
by (rtac trans 1);
paulson@9265
   117
by (rtac (q_def3 RS sym) 2);
berghofe@13454
   118
by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
paulson@9265
   119
by (fast_tac HOL_cs 1);
paulson@9265
   120
by (simp_tac HOLCF_ss 1);
paulson@9265
   121
by (etac mp 1);
paulson@9265
   122
by (strip_tac 1);
paulson@9265
   123
by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1);
paulson@9265
   124
qed "hoare_lemma24";
nipkow@244
   125
nipkow@10835
   126
(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *)
nipkow@244
   127
nipkow@244
   128
nipkow@244
   129
val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
nipkow@244
   130
(* 
nipkow@10835
   131
val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
nipkow@10835
   132
    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
nipkow@10835
   133
 p$(iterate ?k3 g ?x1) = p$?x1" : thm
regensbu@1168
   134
nipkow@244
   135
*)
nipkow@244
   136
nipkow@10835
   137
Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
nipkow@10835
   138
\ k=(LEAST n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x)=FF \
nipkow@10835
   139
\ --> p$x = iterate k g x";
paulson@9265
   140
by (case_tac "k" 1);
paulson@9265
   141
by (hyp_subst_tac 1);
paulson@9265
   142
by (Simp_tac 1);
paulson@9265
   143
by (strip_tac 1);
paulson@9265
   144
by (etac conjE 1);
paulson@9265
   145
by (rtac trans 1);
paulson@9265
   146
by (rtac p_def3 1);
paulson@9265
   147
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   148
by (hyp_subst_tac 1);
paulson@9265
   149
by (strip_tac 1);
paulson@9265
   150
by (etac conjE 1);
paulson@9265
   151
by (rtac trans 1);
paulson@9265
   152
by (etac (hoare_lemma10 RS sym) 1);
paulson@9265
   153
by (atac 1);
paulson@9265
   154
by (rtac trans 1);
paulson@9265
   155
by (rtac p_def3 1);
nipkow@10835
   156
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
paulson@9265
   157
by (rtac (hoare_lemma8 RS spec RS mp) 1);
paulson@9265
   158
by (atac 1);
paulson@9265
   159
by (atac 1);
paulson@9265
   160
by (Simp_tac 1);
paulson@9265
   161
by (simp_tac HOLCF_ss 1);
paulson@9265
   162
by (rtac trans 1);
paulson@9265
   163
by (rtac p_def3 1);
paulson@9265
   164
by (simp_tac (simpset() delsimps [iterate_Suc] addsimps [iterate_Suc RS sym]) 1);
paulson@9265
   165
by (eres_inst_tac [("s","FF")] ssubst 1);
paulson@9265
   166
by (simp_tac HOLCF_ss 1);
paulson@9265
   167
qed "hoare_lemma11";
nipkow@244
   168
nipkow@10835
   169
Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
nipkow@10835
   170
\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
nipkow@10835
   171
\ --> p$x = UU";
paulson@9265
   172
by (case_tac "k" 1);
paulson@9265
   173
by (hyp_subst_tac 1);
paulson@9265
   174
by (Simp_tac 1);
paulson@9265
   175
by (strip_tac 1);
paulson@9265
   176
by (etac conjE 1);
paulson@9265
   177
by (rtac trans 1);
paulson@9265
   178
by (rtac p_def3 1);
paulson@9265
   179
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   180
by (hyp_subst_tac 1);
paulson@9265
   181
by (Simp_tac 1);
paulson@9265
   182
by (strip_tac 1);
paulson@9265
   183
by (etac conjE 1);
paulson@9265
   184
by (rtac trans 1);
paulson@9265
   185
by (rtac (hoare_lemma10 RS sym) 1);
paulson@9265
   186
by (atac 1);
paulson@9265
   187
by (atac 1);
paulson@9265
   188
by (rtac trans 1);
paulson@9265
   189
by (rtac p_def3 1);
nipkow@10835
   190
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
paulson@9265
   191
by (rtac (hoare_lemma8 RS spec RS mp) 1);
paulson@9265
   192
by (atac 1);
paulson@9265
   193
by (atac 1);
paulson@9265
   194
by (Simp_tac 1);
paulson@9265
   195
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   196
by (rtac trans 1);
paulson@9265
   197
by (rtac p_def3 1);
paulson@9265
   198
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   199
qed "hoare_lemma12";
nipkow@244
   200
nipkow@10835
   201
(* -------- results about p for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
nipkow@244
   202
nipkow@10835
   203
Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU";
paulson@9265
   204
by (rtac (p_def RS def_fix_ind) 1);
paulson@9265
   205
by (rtac adm_all 1);
paulson@9265
   206
by (rtac allI 1);
paulson@9265
   207
by (rtac adm_eq 1);
paulson@9265
   208
by (cont_tacR 1);
paulson@9265
   209
by (rtac allI 1);
paulson@9265
   210
by (stac strict_Rep_CFun1 1);
paulson@9265
   211
by (rtac refl 1);
paulson@9265
   212
by (Simp_tac 1);
paulson@9265
   213
by (rtac allI 1);
nipkow@10835
   214
by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
paulson@9265
   215
by (etac spec 1);
paulson@9265
   216
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   217
by (rtac (iterate_Suc RS subst) 1);
paulson@9265
   218
by (etac spec 1);
paulson@9265
   219
qed "fernpass_lemma";
nipkow@244
   220
nipkow@10835
   221
Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU";
paulson@9265
   222
by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
paulson@9265
   223
by (etac (fernpass_lemma RS spec) 1);
paulson@9265
   224
qed "hoare_lemma16";
nipkow@244
   225
nipkow@10835
   226
(* -------- results about q for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
nipkow@244
   227
nipkow@10835
   228
Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU";
paulson@9265
   229
by (rtac (q_def RS def_fix_ind) 1);
paulson@9265
   230
by (rtac adm_all 1);
paulson@9265
   231
by (rtac allI 1);
paulson@9265
   232
by (rtac adm_eq 1);
paulson@9265
   233
by (cont_tacR 1);
paulson@9265
   234
by (rtac allI 1);
paulson@9265
   235
by (stac strict_Rep_CFun1 1);
paulson@9265
   236
by (rtac refl 1);
paulson@9265
   237
by (rtac allI 1);
paulson@9265
   238
by (Simp_tac 1);
nipkow@10835
   239
by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
paulson@9265
   240
by (etac spec 1);
paulson@9265
   241
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   242
by (rtac (iterate_Suc RS subst) 1);
paulson@9265
   243
by (etac spec 1);
paulson@9265
   244
qed "hoare_lemma17";
nipkow@244
   245
nipkow@10835
   246
Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU";
paulson@9265
   247
by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
paulson@9265
   248
by (etac (hoare_lemma17 RS spec) 1);
paulson@9265
   249
qed "hoare_lemma18";
paulson@9265
   250
nipkow@10835
   251
Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)";
paulson@9265
   252
by (rtac (flat_codom) 1);
paulson@9265
   253
by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1);
paulson@9265
   254
by (etac spec 1);
paulson@9265
   255
qed "hoare_lemma19";
nipkow@244
   256
nipkow@10835
   257
Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU";
paulson@9265
   258
by (rtac (q_def RS def_fix_ind) 1);
paulson@9265
   259
by (rtac adm_all 1);
paulson@9265
   260
by (rtac allI 1);
paulson@9265
   261
by (rtac adm_eq 1);
paulson@9265
   262
by (cont_tacR 1);
paulson@9265
   263
by (rtac allI 1);
paulson@9265
   264
by (stac strict_Rep_CFun1 1);
paulson@9265
   265
by (rtac refl 1);
paulson@9265
   266
by (rtac allI 1);
paulson@9265
   267
by (Simp_tac 1);
nipkow@10835
   268
by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1);
paulson@9265
   269
by (etac spec 1);
paulson@9265
   270
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   271
by (rtac (iterate_Suc RS subst) 1);
paulson@9265
   272
by (etac spec 1);
paulson@9265
   273
qed "hoare_lemma20";
nipkow@244
   274
nipkow@10835
   275
Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU";
paulson@9265
   276
by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
paulson@9265
   277
by (etac (hoare_lemma20 RS spec) 1);
paulson@9265
   278
qed "hoare_lemma21";
nipkow@244
   279
nipkow@10835
   280
Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU";
paulson@9265
   281
by (stac q_def3 1);
paulson@9265
   282
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   283
qed "hoare_lemma22";
nipkow@244
   284
nipkow@10835
   285
(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *)
nipkow@244
   286
nipkow@244
   287
val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
nipkow@244
   288
(* 
nipkow@10835
   289
val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
nipkow@10835
   290
    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
nipkow@10835
   291
 q$(iterate ?k3 g ?x1) = q$?x1" : thm
nipkow@244
   292
*)
nipkow@244
   293
nipkow@10835
   294
Goal "(EX n. b1$(iterate n g x)~=TT) ==>\
nipkow@10835
   295
\ k=Least(%n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x) =FF \
nipkow@10835
   296
\ --> q$x = q$(iterate k g x)";
paulson@9265
   297
by (case_tac "k" 1);
paulson@9265
   298
by (hyp_subst_tac 1);
paulson@9265
   299
by (strip_tac 1);
paulson@9265
   300
by (Simp_tac 1);
paulson@9265
   301
by (hyp_subst_tac 1);
paulson@9265
   302
by (strip_tac 1);
paulson@9265
   303
by (etac conjE 1);
paulson@9265
   304
by (rtac trans 1);
paulson@9265
   305
by (rtac (hoare_lemma25 RS sym) 1);
paulson@9265
   306
by (atac 1);
paulson@9265
   307
by (atac 1);
paulson@9265
   308
by (rtac trans 1);
paulson@9265
   309
by (rtac q_def3 1);
nipkow@10835
   310
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
paulson@9265
   311
by (rtac (hoare_lemma8 RS spec RS mp) 1);
paulson@9265
   312
by (atac 1);
paulson@9265
   313
by (atac 1);
paulson@9265
   314
by (Simp_tac 1);
paulson@9265
   315
by (simp_tac HOLCF_ss 1);
paulson@9265
   316
qed "hoare_lemma26";
nipkow@244
   317
nipkow@244
   318
nipkow@10835
   319
Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
nipkow@10835
   320
\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
nipkow@10835
   321
\ --> q$x = UU";
paulson@9265
   322
by (case_tac "k" 1);
paulson@9265
   323
by (hyp_subst_tac 1);
paulson@9265
   324
by (Simp_tac 1);
paulson@9265
   325
by (strip_tac 1);
paulson@9265
   326
by (etac conjE 1);
paulson@9265
   327
by (stac q_def3 1);
paulson@9265
   328
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   329
by (hyp_subst_tac 1);
paulson@9265
   330
by (Simp_tac 1);
paulson@9265
   331
by (strip_tac 1);
paulson@9265
   332
by (etac conjE 1);
paulson@9265
   333
by (rtac trans 1);
paulson@9265
   334
by (rtac (hoare_lemma25 RS sym) 1);
paulson@9265
   335
by (atac 1);
paulson@9265
   336
by (atac 1);
paulson@9265
   337
by (rtac trans 1);
paulson@9265
   338
by (rtac q_def3 1);
nipkow@10835
   339
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
paulson@9265
   340
by (rtac (hoare_lemma8 RS spec RS mp) 1);
paulson@9265
   341
by (atac 1);
paulson@9265
   342
by (atac 1);
paulson@9265
   343
by (Simp_tac 1);
paulson@9265
   344
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   345
by (rtac trans 1);
paulson@9265
   346
by (rtac q_def3 1);
paulson@9265
   347
by (asm_simp_tac HOLCF_ss 1);
paulson@9265
   348
qed "hoare_lemma27";
nipkow@244
   349
nipkow@10835
   350
(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q   ----- *)
nipkow@244
   351
nipkow@10835
   352
Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x";
paulson@9265
   353
by (stac hoare_lemma16 1);
paulson@9265
   354
by (atac 1);
paulson@9265
   355
by (rtac (hoare_lemma19 RS disjE) 1);
paulson@9265
   356
by (atac 1);
paulson@9265
   357
by (stac hoare_lemma18 1);
paulson@9265
   358
by (atac 1);
paulson@9265
   359
by (stac hoare_lemma22 1);
paulson@9265
   360
by (atac 1);
paulson@9265
   361
by (rtac refl 1);
paulson@9265
   362
by (stac hoare_lemma21 1);
paulson@9265
   363
by (atac 1);
paulson@9265
   364
by (stac hoare_lemma21 1);
paulson@9265
   365
by (atac 1);
paulson@9265
   366
by (rtac refl 1);
paulson@9265
   367
qed "hoare_lemma23";
nipkow@244
   368
paulson@9265
   369
(* ------------  EX k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
nipkow@244
   370
nipkow@10835
   371
Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x";
paulson@9265
   372
by (rtac (hoare_lemma5 RS disjE) 1);
paulson@9265
   373
by (atac 1);
paulson@9265
   374
by (rtac refl 1);
paulson@9265
   375
by (stac (hoare_lemma11 RS mp) 1);
paulson@9265
   376
by (atac 1);
paulson@9265
   377
by (rtac conjI 1);
paulson@9265
   378
by (rtac refl 1);
paulson@9265
   379
by (atac 1);
paulson@9265
   380
by (rtac (hoare_lemma26 RS mp RS subst) 1);
paulson@9265
   381
by (atac 1);
paulson@9265
   382
by (rtac conjI 1);
paulson@9265
   383
by (rtac refl 1);
paulson@9265
   384
by (atac 1);
paulson@9265
   385
by (rtac refl 1);
paulson@9265
   386
by (stac (hoare_lemma12 RS mp) 1);
paulson@9265
   387
by (atac 1);
paulson@9265
   388
by (rtac conjI 1);
paulson@9265
   389
by (rtac refl 1);
paulson@9265
   390
by (atac 1);
paulson@9265
   391
by (stac hoare_lemma22 1);
paulson@9265
   392
by (stac hoare_lemma28 1);
paulson@9265
   393
by (atac 1);
paulson@9265
   394
by (rtac refl 1);
paulson@9265
   395
by (rtac sym 1);
paulson@9265
   396
by (stac (hoare_lemma27 RS mp) 1);
paulson@9265
   397
by (atac 1);
paulson@9265
   398
by (rtac conjI 1);
paulson@9265
   399
by (rtac refl 1);
paulson@9265
   400
by (atac 1);
paulson@9265
   401
by (rtac refl 1);
paulson@9265
   402
qed "hoare_lemma29";
nipkow@244
   403
nipkow@244
   404
(* ------ the main prove q o p = q ------ *)
nipkow@244
   405
paulson@9265
   406
Goal "q oo p = q";
paulson@9265
   407
by (rtac ext_cfun 1);
paulson@9265
   408
by (stac cfcomp2 1);
paulson@9265
   409
by (rtac (hoare_lemma3 RS disjE) 1);
paulson@9265
   410
by (etac hoare_lemma23 1);
paulson@9265
   411
by (etac hoare_lemma29 1);
paulson@9265
   412
qed "hoare_main";
nipkow@244
   413
nipkow@244
   414