src/HOLCF/ex/Hoare.ML
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 1043 ffa68eb2730b
child 1267 bca91b4e1710
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
nipkow@244
     1
(*  Title:	HOLCF/ex/hoare.ML
nipkow@244
     2
    ID:         $Id$
nipkow@244
     3
    Author: 	Franz Regensburger
nipkow@244
     4
    Copyright	1993 Technische Universitaet Muenchen
nipkow@244
     5
*)
nipkow@244
     6
nipkow@244
     7
open Hoare;
nipkow@244
     8
nipkow@244
     9
(* --------- pure HOLCF logic, some little lemmas ------ *)
nipkow@244
    10
regensbu@1168
    11
val hoare_lemma2 = prove_goal HOLCF.thy "b~=TT ==> b=FF | b=UU"
nipkow@244
    12
 (fn prems =>
nipkow@244
    13
	[
nipkow@244
    14
	(cut_facts_tac prems 1),
nipkow@244
    15
	(rtac (Exh_tr RS disjE) 1),
nipkow@244
    16
	(fast_tac HOL_cs 1),
nipkow@244
    17
	(etac disjE 1),
nipkow@244
    18
	(contr_tac 1),
nipkow@244
    19
	(fast_tac HOL_cs 1)
nipkow@244
    20
	]);
nipkow@244
    21
regensbu@1043
    22
val hoare_lemma3 = prove_goal HOLCF.thy 
regensbu@1168
    23
" (!k.b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
nipkow@244
    24
 (fn prems =>
nipkow@244
    25
	[
nipkow@244
    26
	(fast_tac HOL_cs 1)
nipkow@244
    27
	]);
nipkow@244
    28
regensbu@1043
    29
val hoare_lemma4 = prove_goal HOLCF.thy 
regensbu@1168
    30
"(? k. b1`(iterate k g x) ~= TT) ==> \
regensbu@1168
    31
\ ? k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU"
nipkow@244
    32
 (fn prems =>
nipkow@244
    33
	[
nipkow@244
    34
	(cut_facts_tac prems 1),
nipkow@244
    35
	(etac exE 1),
nipkow@244
    36
	(rtac exI 1),
nipkow@244
    37
	(rtac hoare_lemma2 1),
nipkow@244
    38
	(atac 1)
nipkow@244
    39
	]);
nipkow@244
    40
regensbu@1043
    41
val hoare_lemma5 = prove_goal HOLCF.thy 
regensbu@1168
    42
"[|(? k. b1`(iterate k g x) ~= TT);\
regensbu@1168
    43
\   k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
regensbu@1168
    44
\ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU"
nipkow@244
    45
 (fn prems =>
nipkow@244
    46
	[
nipkow@244
    47
	(cut_facts_tac prems 1),
nipkow@244
    48
	(hyp_subst_tac 1),
nipkow@244
    49
	(rtac hoare_lemma2 1),
nipkow@244
    50
	(etac exE 1),
nipkow@244
    51
	(etac theleast1 1)
nipkow@244
    52
	]);
nipkow@244
    53
regensbu@1168
    54
val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> b~=TT"
nipkow@244
    55
 (fn prems =>
nipkow@244
    56
	[
nipkow@244
    57
	(cut_facts_tac prems 1),
nipkow@244
    58
	(hyp_subst_tac 1),
nipkow@244
    59
	(resolve_tac dist_eq_tr 1)
nipkow@244
    60
	]);
nipkow@244
    61
regensbu@1168
    62
val hoare_lemma7 = prove_goal HOLCF.thy "b=FF ==> b~=TT"
nipkow@244
    63
 (fn prems =>
nipkow@244
    64
	[
nipkow@244
    65
	(cut_facts_tac prems 1),
nipkow@244
    66
	(hyp_subst_tac 1),
nipkow@244
    67
	(resolve_tac dist_eq_tr 1)
nipkow@244
    68
	]);
nipkow@244
    69
regensbu@1043
    70
val hoare_lemma8 = prove_goal HOLCF.thy 
regensbu@1168
    71
"[|(? k. b1`(iterate k g x) ~= TT);\
regensbu@1168
    72
\   k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
regensbu@1168
    73
\ !m. m < k --> b1`(iterate m g x)=TT"
nipkow@244
    74
 (fn prems =>
nipkow@244
    75
	[
nipkow@244
    76
	(cut_facts_tac prems 1),
nipkow@244
    77
	(hyp_subst_tac 1),
nipkow@244
    78
	(etac exE 1),
nipkow@244
    79
	(strip_tac 1),
regensbu@1168
    80
	(res_inst_tac [("p","b1`(iterate m g x)")] trE 1),
nipkow@244
    81
	(atac 2),
nipkow@244
    82
	(rtac (le_less_trans RS less_anti_refl) 1),
nipkow@244
    83
	(atac 2),
nipkow@244
    84
	(rtac theleast2 1),
nipkow@244
    85
	(etac hoare_lemma6 1),
nipkow@244
    86
	(rtac (le_less_trans RS less_anti_refl) 1),
nipkow@244
    87
	(atac 2),
nipkow@244
    88
	(rtac theleast2 1),
nipkow@244
    89
	(etac hoare_lemma7 1)
nipkow@244
    90
	]);
nipkow@244
    91
regensbu@1168
    92
regensbu@1043
    93
val hoare_lemma28 = prove_goal HOLCF.thy 
regensbu@1168
    94
"b1`(y::'a)=(UU::tr) ==> b1`UU = UU"
nipkow@244
    95
 (fn prems =>
nipkow@244
    96
	[
nipkow@244
    97
	(cut_facts_tac prems 1),
nipkow@244
    98
	(etac (flat_tr RS flat_codom RS disjE) 1),
nipkow@244
    99
	(atac 1),
nipkow@244
   100
	(etac spec 1)
nipkow@244
   101
	]);
nipkow@244
   102
nipkow@244
   103
nipkow@244
   104
(* ----- access to definitions ----- *)
nipkow@244
   105
regensbu@1043
   106
val p_def2 = prove_goalw Hoare.thy [p_def]
regensbu@1168
   107
"p = fix`(LAM f x. If b1`x then f`(g`x) else x fi)"
nipkow@244
   108
 (fn prems =>
nipkow@244
   109
	[
nipkow@244
   110
	(rtac refl 1)
nipkow@244
   111
	]);
nipkow@244
   112
regensbu@1043
   113
val q_def2 = prove_goalw Hoare.thy [q_def]
regensbu@1168
   114
"q = fix`(LAM f x. If b1`x orelse b2`x then \
regensbu@1168
   115
\     f`(g`x) else x fi)"
nipkow@244
   116
 (fn prems =>
nipkow@244
   117
	[
nipkow@244
   118
	(rtac refl 1)
nipkow@244
   119
	]);
nipkow@244
   120
nipkow@244
   121
regensbu@1043
   122
val p_def3 = prove_goal Hoare.thy 
regensbu@1168
   123
"p`x = If b1`x then p`(g`x) else x fi"
nipkow@244
   124
 (fn prems =>
nipkow@244
   125
	[
nipkow@244
   126
	(fix_tac3 p_def 1),
nipkow@244
   127
	(simp_tac HOLCF_ss 1)
nipkow@244
   128
	]);
nipkow@244
   129
regensbu@1043
   130
val q_def3 = prove_goal Hoare.thy 
regensbu@1168
   131
"q`x = If b1`x orelse b2`x then q`(g`x) else x fi"
nipkow@244
   132
 (fn prems =>
nipkow@244
   133
	[
nipkow@244
   134
	(fix_tac3 q_def 1),
nipkow@244
   135
	(simp_tac HOLCF_ss 1)
nipkow@244
   136
	]);
nipkow@244
   137
nipkow@244
   138
(** --------- proves about iterations of p and q ---------- **)
nipkow@244
   139
regensbu@1043
   140
val hoare_lemma9 = prove_goal Hoare.thy 
regensbu@1168
   141
"(! m. m< Suc k --> b1`(iterate m g x)=TT) -->\
regensbu@1168
   142
\  p`(iterate k g x)=p`x"
nipkow@244
   143
 (fn prems =>
nipkow@244
   144
	[
nipkow@244
   145
	(nat_ind_tac "k" 1),
nipkow@244
   146
	(simp_tac iterate_ss 1),
nipkow@244
   147
	(simp_tac iterate_ss 1),
nipkow@244
   148
	(strip_tac 1),
regensbu@1168
   149
	(res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
nipkow@244
   150
	(rtac trans 1),
nipkow@244
   151
	(rtac (p_def3 RS sym) 2),
regensbu@1168
   152
	(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
nipkow@244
   153
	(rtac mp 1),
nipkow@244
   154
	(etac spec 1),
nipkow@244
   155
	(simp_tac nat_ss 1),
nipkow@244
   156
	(simp_tac HOLCF_ss 1),
nipkow@244
   157
	(etac mp 1),
nipkow@244
   158
	(strip_tac 1),
nipkow@244
   159
	(rtac mp 1),
nipkow@244
   160
	(etac spec 1),
nipkow@244
   161
	(etac less_trans 1),
nipkow@244
   162
	(simp_tac nat_ss 1)
nipkow@244
   163
	]);
nipkow@244
   164
regensbu@1043
   165
val hoare_lemma24 = prove_goal Hoare.thy 
regensbu@1168
   166
"(! m. m< Suc k --> b1`(iterate m g x)=TT) --> \
regensbu@1168
   167
\ q`(iterate k g x)=q`x"
nipkow@244
   168
 (fn prems =>
nipkow@244
   169
	[
nipkow@244
   170
	(nat_ind_tac "k" 1),
nipkow@244
   171
	(simp_tac iterate_ss 1),
nipkow@244
   172
	(simp_tac iterate_ss 1),
nipkow@244
   173
	(strip_tac 1),
regensbu@1168
   174
	(res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
nipkow@244
   175
	(rtac trans 1),
nipkow@244
   176
	(rtac (q_def3 RS sym) 2),
regensbu@1168
   177
	(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
nipkow@244
   178
	(rtac mp 1),
nipkow@244
   179
	(etac spec 1),
nipkow@244
   180
	(simp_tac nat_ss 1),
nipkow@244
   181
	(simp_tac HOLCF_ss 1),
nipkow@244
   182
	(etac mp 1),
nipkow@244
   183
	(strip_tac 1),
nipkow@244
   184
	(rtac mp 1),
nipkow@244
   185
	(etac spec 1),
nipkow@244
   186
	(etac less_trans 1),
nipkow@244
   187
	(simp_tac nat_ss 1)
nipkow@244
   188
	]);
nipkow@244
   189
regensbu@1168
   190
(* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
nipkow@244
   191
nipkow@244
   192
nipkow@244
   193
val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
nipkow@244
   194
(* 
regensbu@1168
   195
val hoare_lemma10 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
regensbu@1168
   196
    Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
regensbu@1168
   197
 p`(iterate ?k3 g ?x1) = p`?x1" : thm
regensbu@1168
   198
nipkow@244
   199
*)
nipkow@244
   200
regensbu@1043
   201
val hoare_lemma11 = prove_goal Hoare.thy 
regensbu@1168
   202
"(? n.b1`(iterate n g x) ~= TT) ==>\
regensbu@1168
   203
\ k=theleast(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
regensbu@1168
   204
\ --> p`x = iterate k g x"
nipkow@244
   205
 (fn prems =>
nipkow@244
   206
	[
nipkow@244
   207
	(cut_facts_tac prems 1),
nipkow@244
   208
	(res_inst_tac [("n","k")] natE 1),
nipkow@244
   209
	(hyp_subst_tac 1),
nipkow@244
   210
	(simp_tac iterate_ss 1),
nipkow@244
   211
	(strip_tac 1),
nipkow@244
   212
	(etac conjE 1),
nipkow@244
   213
	(rtac trans 1),
nipkow@244
   214
	(rtac p_def3 1),
nipkow@244
   215
	(asm_simp_tac HOLCF_ss  1),
regensbu@1168
   216
	(eres_inst_tac [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")]
nipkow@244
   217
	subst 1),
nipkow@244
   218
	(simp_tac iterate_ss 1),
nipkow@244
   219
	(hyp_subst_tac 1),
nipkow@244
   220
	(strip_tac 1),
nipkow@244
   221
	(etac conjE 1),
nipkow@244
   222
	(rtac trans 1),
nipkow@244
   223
	(etac (hoare_lemma10 RS sym) 1),
nipkow@244
   224
	(atac 1),
nipkow@244
   225
	(rtac trans 1),
nipkow@244
   226
	(rtac p_def3 1),
regensbu@1168
   227
	(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
nipkow@244
   228
	(rtac (hoare_lemma8 RS spec RS mp) 1),
nipkow@244
   229
	(atac 1),
nipkow@244
   230
	(atac 1),
nipkow@244
   231
	(simp_tac nat_ss 1),
nipkow@244
   232
	(simp_tac HOLCF_ss 1),
nipkow@244
   233
	(rtac trans 1),
nipkow@244
   234
	(rtac p_def3 1),
nipkow@244
   235
	(simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1),
nipkow@244
   236
	(eres_inst_tac [("s","FF")]	ssubst 1),
nipkow@244
   237
	(simp_tac HOLCF_ss 1)
nipkow@244
   238
	]);
nipkow@244
   239
regensbu@1043
   240
val hoare_lemma12 = prove_goal Hoare.thy 
regensbu@1168
   241
"(? n. b1`(iterate n g x) ~= TT) ==>\
regensbu@1168
   242
\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
regensbu@1168
   243
\ --> p`x = UU"
nipkow@244
   244
 (fn prems =>
nipkow@244
   245
	[
nipkow@244
   246
	(cut_facts_tac prems 1),
nipkow@244
   247
	(res_inst_tac [("n","k")] natE 1),
nipkow@244
   248
	(hyp_subst_tac 1),
nipkow@244
   249
	(simp_tac iterate_ss 1),
nipkow@244
   250
	(strip_tac 1),
nipkow@244
   251
	(etac conjE 1),
nipkow@244
   252
	(rtac trans 1),
nipkow@244
   253
	(rtac p_def3 1),
nipkow@244
   254
	(asm_simp_tac HOLCF_ss  1),
nipkow@244
   255
	(hyp_subst_tac 1),
nipkow@244
   256
	(simp_tac iterate_ss 1),
nipkow@244
   257
	(strip_tac 1),
nipkow@244
   258
	(etac conjE 1),
nipkow@244
   259
	(rtac trans 1),
nipkow@244
   260
	(rtac (hoare_lemma10 RS sym) 1),
nipkow@244
   261
	(atac 1),
nipkow@244
   262
	(atac 1),
nipkow@244
   263
	(rtac trans 1),
nipkow@244
   264
	(rtac p_def3 1),
regensbu@1168
   265
	(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
nipkow@244
   266
	(rtac (hoare_lemma8 RS spec RS mp) 1),
nipkow@244
   267
	(atac 1),
nipkow@244
   268
	(atac 1),
nipkow@244
   269
	(simp_tac nat_ss 1),
nipkow@244
   270
	(asm_simp_tac HOLCF_ss  1),
nipkow@244
   271
	(rtac trans 1),
nipkow@244
   272
	(rtac p_def3 1),
nipkow@244
   273
	(asm_simp_tac HOLCF_ss  1)
nipkow@244
   274
	]);
nipkow@244
   275
regensbu@1168
   276
(* -------- results about p for case  (! k. b1`(iterate k g x)=TT) ------- *)
nipkow@244
   277
regensbu@1043
   278
val fernpass_lemma = prove_goal Hoare.thy 
regensbu@1168
   279
"(! k. b1`(iterate k g x)=TT) ==> !k.p`(iterate k g x) = UU"
nipkow@244
   280
 (fn prems =>
nipkow@244
   281
	[
nipkow@244
   282
	(cut_facts_tac prems 1),
nipkow@244
   283
	(rtac (p_def2 RS ssubst) 1),
nipkow@244
   284
	(rtac fix_ind 1),
nipkow@244
   285
	(rtac adm_all 1),
nipkow@244
   286
	(rtac allI 1),
nipkow@244
   287
	(rtac adm_eq 1),
regensbu@1168
   288
	(cont_tacR 1),
nipkow@244
   289
	(rtac allI 1),
nipkow@244
   290
	(rtac (strict_fapp1 RS ssubst) 1),
nipkow@244
   291
	(rtac refl 1),
nipkow@244
   292
	(simp_tac iterate_ss 1),
nipkow@244
   293
	(rtac allI 1),
regensbu@1168
   294
	(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
nipkow@244
   295
	(etac spec 1),
nipkow@244
   296
	(asm_simp_tac HOLCF_ss 1),
nipkow@244
   297
	(rtac (iterate_Suc RS subst) 1),
nipkow@244
   298
	(etac spec 1)
nipkow@244
   299
	]);
nipkow@244
   300
regensbu@1043
   301
val hoare_lemma16 = prove_goal Hoare.thy 
regensbu@1168
   302
"(! k. b1`(iterate k g x)=TT) ==> p`x = UU"
nipkow@244
   303
 (fn prems =>
nipkow@244
   304
	[
nipkow@244
   305
	(cut_facts_tac prems 1),
nipkow@244
   306
	(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1),
nipkow@244
   307
	(etac (fernpass_lemma RS spec) 1)
nipkow@244
   308
	]);
nipkow@244
   309
regensbu@1168
   310
(* -------- results about q for case  (! k. b1`(iterate k g x)=TT) ------- *)
nipkow@244
   311
regensbu@1043
   312
val hoare_lemma17 = prove_goal Hoare.thy 
regensbu@1168
   313
"(! k. b1`(iterate k g x)=TT) ==> !k.q`(iterate k g x) = UU"
nipkow@244
   314
 (fn prems =>
nipkow@244
   315
	[
nipkow@244
   316
	(cut_facts_tac prems 1),
nipkow@244
   317
	(rtac (q_def2 RS ssubst) 1),
nipkow@244
   318
	(rtac fix_ind 1),
nipkow@244
   319
	(rtac adm_all 1),
nipkow@244
   320
	(rtac allI 1),
nipkow@244
   321
	(rtac adm_eq 1),
regensbu@1168
   322
	(cont_tacR 1),
nipkow@244
   323
	(rtac allI 1),
nipkow@244
   324
	(rtac (strict_fapp1 RS ssubst) 1),
nipkow@244
   325
	(rtac refl 1),
nipkow@244
   326
	(rtac allI 1),
nipkow@244
   327
	(simp_tac iterate_ss 1),
regensbu@1168
   328
	(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
nipkow@244
   329
	(etac spec 1),
nipkow@244
   330
	(asm_simp_tac HOLCF_ss  1),
nipkow@244
   331
	(rtac (iterate_Suc RS subst) 1),
nipkow@244
   332
	(etac spec 1)
nipkow@244
   333
	]);
nipkow@244
   334
regensbu@1043
   335
val hoare_lemma18 = prove_goal Hoare.thy 
regensbu@1168
   336
"(! k. b1`(iterate k g x)=TT) ==> q`x = UU"
nipkow@244
   337
 (fn prems =>
nipkow@244
   338
	[
nipkow@244
   339
	(cut_facts_tac prems 1),
nipkow@244
   340
	(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1),
nipkow@244
   341
	(etac (hoare_lemma17 RS spec) 1)
nipkow@244
   342
	]);
nipkow@244
   343
regensbu@1043
   344
val hoare_lemma19 = prove_goal Hoare.thy 
regensbu@1168
   345
"(!k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (!y.b1`(y::'a)=TT)"
nipkow@244
   346
 (fn prems =>
nipkow@244
   347
	[
nipkow@244
   348
	(cut_facts_tac prems 1),
nipkow@244
   349
	(rtac (flat_tr RS flat_codom) 1),
nipkow@244
   350
	(res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
nipkow@244
   351
	(etac spec 1)
nipkow@244
   352
	]);
nipkow@244
   353
regensbu@1043
   354
val hoare_lemma20 = prove_goal Hoare.thy 
regensbu@1168
   355
"(! y. b1`(y::'a)=TT) ==> !k.q`(iterate k g (x::'a)) = UU"
nipkow@244
   356
 (fn prems =>
nipkow@244
   357
	[
nipkow@244
   358
	(cut_facts_tac prems 1),
nipkow@244
   359
	(rtac (q_def2 RS ssubst) 1),
nipkow@244
   360
	(rtac fix_ind 1),
nipkow@244
   361
	(rtac adm_all 1),
nipkow@244
   362
	(rtac allI 1),
nipkow@244
   363
	(rtac adm_eq 1),
regensbu@1168
   364
	(cont_tacR 1),
nipkow@244
   365
	(rtac allI 1),
nipkow@244
   366
	(rtac (strict_fapp1 RS ssubst) 1),
nipkow@244
   367
	(rtac refl 1),
nipkow@244
   368
	(rtac allI 1),
nipkow@244
   369
	(simp_tac iterate_ss 1),
regensbu@1168
   370
	(res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1),
nipkow@244
   371
	(etac spec 1),
nipkow@244
   372
	(asm_simp_tac HOLCF_ss  1),
nipkow@244
   373
	(rtac (iterate_Suc RS subst) 1),
nipkow@244
   374
	(etac spec 1)
nipkow@244
   375
	]);
nipkow@244
   376
regensbu@1043
   377
val hoare_lemma21 = prove_goal Hoare.thy 
regensbu@1168
   378
"(! y. b1`(y::'a)=TT) ==> q`(x::'a) = UU"
nipkow@244
   379
 (fn prems =>
nipkow@244
   380
	[
nipkow@244
   381
	(cut_facts_tac prems 1),
nipkow@244
   382
	(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1),
nipkow@244
   383
	(etac (hoare_lemma20 RS spec) 1)
nipkow@244
   384
	]);
nipkow@244
   385
regensbu@1043
   386
val hoare_lemma22 = prove_goal Hoare.thy 
regensbu@1168
   387
"b1`(UU::'a)=UU ==> q`(UU::'a) = UU"
nipkow@244
   388
 (fn prems =>
nipkow@244
   389
	[
nipkow@244
   390
	(cut_facts_tac prems 1),
nipkow@244
   391
	(rtac (q_def3 RS ssubst) 1),
nipkow@244
   392
	(asm_simp_tac HOLCF_ss  1)
nipkow@244
   393
	]);
nipkow@244
   394
regensbu@1168
   395
(* -------- results about q for case (? k. b1`(iterate k g x) ~= TT) ------- *)
nipkow@244
   396
nipkow@244
   397
val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
nipkow@244
   398
(* 
regensbu@1168
   399
val hoare_lemma25 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
regensbu@1168
   400
    Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
regensbu@1168
   401
 q`(iterate ?k3 g ?x1) = q`?x1" : thm
nipkow@244
   402
*)
nipkow@244
   403
regensbu@1043
   404
val hoare_lemma26 = prove_goal Hoare.thy 
regensbu@1168
   405
"(? n. b1`(iterate n g x)~=TT) ==>\
regensbu@1168
   406
\ k=theleast(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
regensbu@1168
   407
\ --> q`x = q`(iterate k g x)"
nipkow@244
   408
 (fn prems =>
nipkow@244
   409
	[
nipkow@244
   410
	(cut_facts_tac prems 1),
nipkow@244
   411
	(res_inst_tac [("n","k")] natE 1),
nipkow@244
   412
	(hyp_subst_tac 1),
nipkow@244
   413
	(strip_tac 1),
nipkow@244
   414
	(simp_tac iterate_ss 1),
nipkow@244
   415
	(hyp_subst_tac 1),
nipkow@244
   416
	(strip_tac 1),
nipkow@244
   417
	(etac conjE 1),
nipkow@244
   418
	(rtac trans 1),
nipkow@244
   419
	(rtac (hoare_lemma25 RS sym) 1),
nipkow@244
   420
	(atac 1),
nipkow@244
   421
	(atac 1),
nipkow@244
   422
	(rtac trans 1),
nipkow@244
   423
	(rtac q_def3 1),
regensbu@1168
   424
	(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
nipkow@244
   425
	(rtac (hoare_lemma8 RS spec RS mp) 1),
nipkow@244
   426
	(atac 1),
nipkow@244
   427
	(atac 1),
nipkow@244
   428
	(simp_tac nat_ss 1),
nipkow@244
   429
	(simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1)
nipkow@244
   430
	]);
nipkow@244
   431
nipkow@244
   432
regensbu@1043
   433
val hoare_lemma27 = prove_goal Hoare.thy 
regensbu@1168
   434
"(? n. b1`(iterate n g x) ~= TT) ==>\
regensbu@1168
   435
\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
regensbu@1168
   436
\ --> q`x = UU"
nipkow@244
   437
 (fn prems =>
nipkow@244
   438
	[
nipkow@244
   439
	(cut_facts_tac prems 1),
nipkow@244
   440
	(res_inst_tac [("n","k")] natE 1),
nipkow@244
   441
	(hyp_subst_tac 1),
nipkow@244
   442
	(simp_tac iterate_ss 1),
nipkow@244
   443
	(strip_tac 1),
nipkow@244
   444
	(etac conjE 1),
nipkow@244
   445
	(rtac (q_def3 RS ssubst) 1),
nipkow@244
   446
	(asm_simp_tac HOLCF_ss  1),
nipkow@244
   447
	(hyp_subst_tac 1),
nipkow@244
   448
	(simp_tac iterate_ss 1),
nipkow@244
   449
	(strip_tac 1),
nipkow@244
   450
	(etac conjE 1),
nipkow@244
   451
	(rtac trans 1),
nipkow@244
   452
	(rtac (hoare_lemma25 RS sym) 1),
nipkow@244
   453
	(atac 1),
nipkow@244
   454
	(atac 1),
nipkow@244
   455
	(rtac trans 1),
nipkow@244
   456
	(rtac q_def3 1),
regensbu@1168
   457
	(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
nipkow@244
   458
	(rtac (hoare_lemma8 RS spec RS mp) 1),
nipkow@244
   459
	(atac 1),
nipkow@244
   460
	(atac 1),
nipkow@244
   461
	(simp_tac nat_ss 1),
nipkow@244
   462
	(asm_simp_tac HOLCF_ss 1),
nipkow@244
   463
	(rtac trans 1),
nipkow@244
   464
	(rtac q_def3 1),
nipkow@244
   465
	(asm_simp_tac HOLCF_ss  1)
nipkow@244
   466
	]);
nipkow@244
   467
regensbu@1168
   468
(* ------- (! k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
nipkow@244
   469
regensbu@1043
   470
val hoare_lemma23 = prove_goal Hoare.thy 
regensbu@1168
   471
"(! k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x"
nipkow@244
   472
 (fn prems =>
nipkow@244
   473
	[
nipkow@244
   474
	(cut_facts_tac prems 1),
nipkow@244
   475
	(rtac (hoare_lemma16 RS ssubst) 1),
nipkow@244
   476
	(atac 1),
nipkow@244
   477
	(rtac (hoare_lemma19 RS disjE) 1),
nipkow@244
   478
	(atac 1),
nipkow@244
   479
	(rtac (hoare_lemma18 RS ssubst) 1),
nipkow@244
   480
	(atac 1),
nipkow@244
   481
	(rtac (hoare_lemma22 RS ssubst) 1),
nipkow@244
   482
	(atac 1),
nipkow@244
   483
	(rtac refl 1),
nipkow@244
   484
	(rtac (hoare_lemma21 RS ssubst) 1),
nipkow@244
   485
	(atac 1),
nipkow@244
   486
	(rtac (hoare_lemma21 RS ssubst) 1),
nipkow@244
   487
	(atac 1),
nipkow@244
   488
	(rtac refl 1)
nipkow@244
   489
	]);
nipkow@244
   490
regensbu@1168
   491
(* ------------  ? k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
nipkow@244
   492
regensbu@1043
   493
val hoare_lemma29 = prove_goal Hoare.thy 
regensbu@1168
   494
"? k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x"
nipkow@244
   495
 (fn prems =>
nipkow@244
   496
	[
nipkow@244
   497
	(cut_facts_tac prems 1),
nipkow@244
   498
	(rtac (hoare_lemma5 RS disjE) 1),
nipkow@244
   499
	(atac 1),
nipkow@244
   500
	(rtac refl 1),
nipkow@244
   501
	(rtac (hoare_lemma11 RS mp RS ssubst) 1),
nipkow@244
   502
	(atac 1),
nipkow@244
   503
	(rtac conjI 1),
nipkow@244
   504
	(rtac refl 1),
nipkow@244
   505
	(atac 1),
nipkow@244
   506
	(rtac (hoare_lemma26 RS mp RS subst) 1),
nipkow@244
   507
	(atac 1),
nipkow@244
   508
	(rtac conjI 1),
nipkow@244
   509
	(rtac refl 1),
nipkow@244
   510
	(atac 1),
nipkow@244
   511
	(rtac refl 1),
nipkow@244
   512
	(rtac (hoare_lemma12 RS mp RS ssubst) 1),
nipkow@244
   513
	(atac 1),
nipkow@244
   514
	(rtac conjI 1),
nipkow@244
   515
	(rtac refl 1),
nipkow@244
   516
	(atac 1),
nipkow@244
   517
	(rtac (hoare_lemma22 RS ssubst) 1),
nipkow@244
   518
	(rtac (hoare_lemma28 RS ssubst) 1),
nipkow@244
   519
	(atac 1),
nipkow@244
   520
	(rtac refl 1),
nipkow@244
   521
	(rtac sym 1),
nipkow@244
   522
	(rtac (hoare_lemma27 RS mp RS ssubst) 1),
nipkow@244
   523
	(atac 1),
nipkow@244
   524
	(rtac conjI 1),
nipkow@244
   525
	(rtac refl 1),
nipkow@244
   526
	(atac 1),
nipkow@244
   527
	(rtac refl 1)
nipkow@244
   528
	]);
nipkow@244
   529
nipkow@244
   530
(* ------ the main prove q o p = q ------ *)
nipkow@244
   531
regensbu@1043
   532
val hoare_main = prove_goal Hoare.thy "q oo p = q"
nipkow@244
   533
 (fn prems =>
nipkow@244
   534
	[
nipkow@244
   535
	(rtac ext_cfun 1),
nipkow@244
   536
	(rtac (cfcomp2 RS ssubst) 1),
nipkow@244
   537
	(rtac (hoare_lemma3 RS disjE) 1),
nipkow@244
   538
	(etac hoare_lemma23 1),
nipkow@244
   539
	(etac hoare_lemma29 1)
nipkow@244
   540
	]);
nipkow@244
   541
nipkow@244
   542