src/HOLCF/ex/Hoare.thy
author huffman
Sat Oct 16 17:09:57 2010 -0700 (2010-10-16)
changeset 40028 9ee4e0ab2964
parent 40002 c5b5f7a3a3b1
child 40322 707eb30e8a53
permissions -rw-r--r--
remove old uses of 'simp_tac HOLCF_ss'
clasohm@1479
     1
(*  Title:      HOLCF/ex/hoare.thy
clasohm@1479
     2
    Author:     Franz Regensburger
nipkow@244
     3
wenzelm@12036
     4
Theory for an example by C.A.R. Hoare
nipkow@244
     5
wenzelm@17291
     6
p x = if b1 x
regensbu@1168
     7
         then p (g x)
nipkow@244
     8
         else x fi
nipkow@244
     9
wenzelm@17291
    10
q x = if b1 x orelse b2 x
regensbu@1168
    11
         then q (g x)
nipkow@244
    12
         else x fi
nipkow@244
    13
wenzelm@17291
    14
Prove: for all b1 b2 g .
wenzelm@17291
    15
            q o p  = q
nipkow@244
    16
nipkow@244
    17
In order to get a nice notation we fix the functions b1,b2 and g in the
nipkow@244
    18
signature of this example
nipkow@244
    19
nipkow@244
    20
*)
nipkow@244
    21
wenzelm@17291
    22
theory Hoare
wenzelm@17291
    23
imports HOLCF
wenzelm@17291
    24
begin
nipkow@244
    25
wenzelm@25135
    26
axiomatization
wenzelm@25135
    27
  b1 :: "'a -> tr" and
wenzelm@25135
    28
  b2 :: "'a -> tr" and
wenzelm@17291
    29
  g :: "'a -> 'a"
nipkow@244
    30
wenzelm@19763
    31
definition
wenzelm@21404
    32
  p :: "'a -> 'a" where
wenzelm@19763
    33
  "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)"
nipkow@244
    34
wenzelm@21404
    35
definition
wenzelm@21404
    36
  q :: "'a -> 'a" where
wenzelm@19763
    37
  "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"
nipkow@244
    38
wenzelm@19742
    39
wenzelm@19742
    40
(* --------- pure HOLCF logic, some little lemmas ------ *)
wenzelm@19742
    41
wenzelm@19742
    42
lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU"
wenzelm@19742
    43
apply (rule Exh_tr [THEN disjE])
wenzelm@19742
    44
apply blast+
wenzelm@19742
    45
done
wenzelm@19742
    46
wenzelm@19742
    47
lemma hoare_lemma3: " (ALL k. b1$(iterate k$g$x) = TT) | (EX k. b1$(iterate k$g$x)~=TT)"
wenzelm@19742
    48
apply blast
wenzelm@19742
    49
done
wenzelm@19742
    50
wenzelm@19742
    51
lemma hoare_lemma4: "(EX k. b1$(iterate k$g$x) ~= TT) ==>  
wenzelm@19742
    52
  EX k. b1$(iterate k$g$x) = FF | b1$(iterate k$g$x) = UU"
wenzelm@19742
    53
apply (erule exE)
wenzelm@19742
    54
apply (rule exI)
wenzelm@19742
    55
apply (rule hoare_lemma2)
wenzelm@19742
    56
apply assumption
wenzelm@19742
    57
done
wenzelm@19742
    58
wenzelm@19742
    59
lemma hoare_lemma5: "[|(EX k. b1$(iterate k$g$x) ~= TT); 
wenzelm@19742
    60
    k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==>  
wenzelm@19742
    61
  b1$(iterate k$g$x)=FF | b1$(iterate k$g$x)=UU"
wenzelm@19742
    62
apply hypsubst
wenzelm@19742
    63
apply (rule hoare_lemma2)
wenzelm@19742
    64
apply (erule exE)
wenzelm@19742
    65
apply (erule LeastI)
wenzelm@19742
    66
done
wenzelm@19742
    67
wenzelm@19742
    68
lemma hoare_lemma6: "b=UU ==> b~=TT"
wenzelm@19742
    69
apply hypsubst
wenzelm@19742
    70
apply (rule dist_eq_tr)
wenzelm@19742
    71
done
wenzelm@19742
    72
wenzelm@19742
    73
lemma hoare_lemma7: "b=FF ==> b~=TT"
wenzelm@19742
    74
apply hypsubst
wenzelm@19742
    75
apply (rule dist_eq_tr)
wenzelm@19742
    76
done
wenzelm@19742
    77
wenzelm@19742
    78
lemma hoare_lemma8: "[|(EX k. b1$(iterate k$g$x) ~= TT); 
wenzelm@19742
    79
    k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==>  
wenzelm@19742
    80
  ALL m. m < k --> b1$(iterate m$g$x)=TT"
wenzelm@19742
    81
apply hypsubst
wenzelm@19742
    82
apply (erule exE)
wenzelm@19742
    83
apply (intro strip)
wenzelm@19742
    84
apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
wenzelm@19742
    85
prefer 2 apply (assumption)
wenzelm@26334
    86
apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
wenzelm@19742
    87
prefer 2 apply (assumption)
wenzelm@19742
    88
apply (rule Least_le)
wenzelm@19742
    89
apply (erule hoare_lemma6)
wenzelm@26334
    90
apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
wenzelm@19742
    91
prefer 2 apply (assumption)
wenzelm@19742
    92
apply (rule Least_le)
wenzelm@19742
    93
apply (erule hoare_lemma7)
wenzelm@19742
    94
done
wenzelm@19742
    95
wenzelm@19742
    96
wenzelm@19742
    97
lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
wenzelm@19742
    98
apply (erule flat_codom [THEN disjE])
wenzelm@19742
    99
apply auto
wenzelm@19742
   100
done
wenzelm@19742
   101
wenzelm@19742
   102
wenzelm@19742
   103
(* ----- access to definitions ----- *)
wenzelm@19742
   104
wenzelm@19742
   105
lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
wenzelm@19742
   106
apply (rule trans)
wenzelm@19763
   107
apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
wenzelm@19742
   108
apply simp
wenzelm@19742
   109
done
wenzelm@19742
   110
wenzelm@19742
   111
lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
wenzelm@19742
   112
apply (rule trans)
wenzelm@19763
   113
apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
wenzelm@19742
   114
apply simp
wenzelm@19742
   115
done
wenzelm@19742
   116
wenzelm@19742
   117
(** --------- proofs about iterations of p and q ---------- **)
wenzelm@19742
   118
wenzelm@19742
   119
lemma hoare_lemma9: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) --> 
wenzelm@19742
   120
   p$(iterate k$g$x)=p$x"
wenzelm@19742
   121
apply (induct_tac k)
wenzelm@19742
   122
apply (simp (no_asm))
wenzelm@19742
   123
apply (simp (no_asm))
wenzelm@19742
   124
apply (intro strip)
wenzelm@19742
   125
apply (rule_tac s = "p$ (iterate n$g$x) " in trans)
wenzelm@19742
   126
apply (rule trans)
wenzelm@19742
   127
apply (rule_tac [2] p_def3 [symmetric])
wenzelm@19742
   128
apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
wenzelm@19742
   129
apply (rule mp)
wenzelm@19742
   130
apply (erule spec)
wenzelm@19742
   131
apply (simp (no_asm) add: less_Suc_eq)
wenzelm@19742
   132
apply simp
wenzelm@19742
   133
apply (erule mp)
wenzelm@19742
   134
apply (intro strip)
wenzelm@19742
   135
apply (rule mp)
wenzelm@19742
   136
apply (erule spec)
wenzelm@19742
   137
apply (erule less_trans)
wenzelm@19742
   138
apply simp
wenzelm@19742
   139
done
wenzelm@19742
   140
wenzelm@19742
   141
lemma hoare_lemma24: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->  
wenzelm@19742
   142
  q$(iterate k$g$x)=q$x"
wenzelm@19742
   143
apply (induct_tac k)
wenzelm@19742
   144
apply (simp (no_asm))
wenzelm@19742
   145
apply (simp (no_asm) add: less_Suc_eq)
wenzelm@19742
   146
apply (intro strip)
wenzelm@19742
   147
apply (rule_tac s = "q$ (iterate n$g$x) " in trans)
wenzelm@19742
   148
apply (rule trans)
wenzelm@19742
   149
apply (rule_tac [2] q_def3 [symmetric])
wenzelm@19742
   150
apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
wenzelm@19742
   151
apply blast
wenzelm@19742
   152
apply simp
wenzelm@19742
   153
apply (erule mp)
wenzelm@19742
   154
apply (intro strip)
wenzelm@19742
   155
apply (fast dest!: less_Suc_eq [THEN iffD1])
wenzelm@19742
   156
done
wenzelm@19742
   157
wenzelm@19742
   158
(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
wenzelm@19742
   159
wenzelm@26936
   160
thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
wenzelm@19742
   161
wenzelm@19742
   162
lemma hoare_lemma10:
wenzelm@19742
   163
  "EX k. b1$(iterate k$g$x) ~= TT
wenzelm@19742
   164
    ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"
wenzelm@19742
   165
  by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]])
wenzelm@19742
   166
wenzelm@19742
   167
lemma hoare_lemma11: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 
wenzelm@19742
   168
  k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF  
wenzelm@19742
   169
  --> p$x = iterate k$g$x"
wenzelm@19742
   170
apply (case_tac "k")
wenzelm@19742
   171
apply hypsubst
wenzelm@19742
   172
apply (simp (no_asm))
wenzelm@19742
   173
apply (intro strip)
wenzelm@19742
   174
apply (erule conjE)
wenzelm@19742
   175
apply (rule trans)
wenzelm@19742
   176
apply (rule p_def3)
wenzelm@19742
   177
apply simp
wenzelm@19742
   178
apply hypsubst
wenzelm@19742
   179
apply (intro strip)
wenzelm@19742
   180
apply (erule conjE)
wenzelm@19742
   181
apply (rule trans)
wenzelm@19742
   182
apply (erule hoare_lemma10 [symmetric])
wenzelm@19742
   183
apply assumption
wenzelm@19742
   184
apply (rule trans)
wenzelm@19742
   185
apply (rule p_def3)
wenzelm@19742
   186
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
wenzelm@19742
   187
apply (rule hoare_lemma8 [THEN spec, THEN mp])
wenzelm@19742
   188
apply assumption
wenzelm@19742
   189
apply assumption
wenzelm@19742
   190
apply (simp (no_asm))
huffman@40028
   191
apply (simp (no_asm))
wenzelm@19742
   192
apply (rule trans)
wenzelm@19742
   193
apply (rule p_def3)
wenzelm@19742
   194
apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
wenzelm@19742
   195
apply (erule_tac s = "FF" in ssubst)
wenzelm@19742
   196
apply simp
wenzelm@19742
   197
done
wenzelm@19742
   198
wenzelm@19742
   199
lemma hoare_lemma12: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 
wenzelm@19742
   200
  k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU  
wenzelm@19742
   201
  --> p$x = UU"
wenzelm@19742
   202
apply (case_tac "k")
wenzelm@19742
   203
apply hypsubst
wenzelm@19742
   204
apply (simp (no_asm))
wenzelm@19742
   205
apply (intro strip)
wenzelm@19742
   206
apply (erule conjE)
wenzelm@19742
   207
apply (rule trans)
wenzelm@19742
   208
apply (rule p_def3)
wenzelm@19742
   209
apply simp
wenzelm@19742
   210
apply hypsubst
wenzelm@19742
   211
apply (simp (no_asm))
wenzelm@19742
   212
apply (intro strip)
wenzelm@19742
   213
apply (erule conjE)
wenzelm@19742
   214
apply (rule trans)
wenzelm@19742
   215
apply (rule hoare_lemma10 [symmetric])
wenzelm@19742
   216
apply assumption
wenzelm@19742
   217
apply assumption
wenzelm@19742
   218
apply (rule trans)
wenzelm@19742
   219
apply (rule p_def3)
wenzelm@19742
   220
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
wenzelm@19742
   221
apply (rule hoare_lemma8 [THEN spec, THEN mp])
wenzelm@19742
   222
apply assumption
wenzelm@19742
   223
apply assumption
wenzelm@19742
   224
apply (simp (no_asm))
huffman@40028
   225
apply (simp)
wenzelm@19742
   226
apply (rule trans)
wenzelm@19742
   227
apply (rule p_def3)
wenzelm@19742
   228
apply simp
wenzelm@19742
   229
done
wenzelm@19742
   230
wenzelm@19742
   231
(* -------- results about p for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
wenzelm@19742
   232
wenzelm@19742
   233
lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
wenzelm@19763
   234
apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
huffman@35948
   235
apply simp
huffman@35948
   236
apply simp
wenzelm@19742
   237
apply (simp (no_asm))
wenzelm@19742
   238
apply (rule allI)
wenzelm@19742
   239
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
wenzelm@19742
   240
apply (erule spec)
huffman@40028
   241
apply (simp)
wenzelm@19742
   242
apply (rule iterate_Suc [THEN subst])
wenzelm@19742
   243
apply (erule spec)
wenzelm@19742
   244
done
wenzelm@19742
   245
wenzelm@19742
   246
lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU"
wenzelm@19742
   247
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
wenzelm@19742
   248
apply (erule fernpass_lemma [THEN spec])
wenzelm@19742
   249
done
wenzelm@19742
   250
wenzelm@19742
   251
(* -------- results about q for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
wenzelm@19742
   252
wenzelm@19742
   253
lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
wenzelm@19763
   254
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
huffman@35948
   255
apply simp
huffman@35948
   256
apply simp
wenzelm@19742
   257
apply (rule allI)
wenzelm@19742
   258
apply (simp (no_asm))
wenzelm@19742
   259
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
wenzelm@19742
   260
apply (erule spec)
huffman@40028
   261
apply (simp)
wenzelm@19742
   262
apply (rule iterate_Suc [THEN subst])
wenzelm@19742
   263
apply (erule spec)
wenzelm@19742
   264
done
wenzelm@19742
   265
wenzelm@19742
   266
lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU"
wenzelm@19742
   267
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
wenzelm@19742
   268
apply (erule hoare_lemma17 [THEN spec])
wenzelm@19742
   269
done
wenzelm@19742
   270
wenzelm@19742
   271
lemma hoare_lemma19:
wenzelm@19742
   272
  "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"
wenzelm@19742
   273
apply (rule flat_codom)
wenzelm@19742
   274
apply (rule_tac t = "x1" in iterate_0 [THEN subst])
wenzelm@19742
   275
apply (erule spec)
wenzelm@19742
   276
done
wenzelm@19742
   277
wenzelm@19742
   278
lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
wenzelm@19763
   279
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
huffman@35948
   280
apply simp
huffman@35948
   281
apply simp
wenzelm@19742
   282
apply (rule allI)
wenzelm@19742
   283
apply (simp (no_asm))
wenzelm@19742
   284
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
wenzelm@19742
   285
apply (erule spec)
huffman@40028
   286
apply (simp)
wenzelm@19742
   287
apply (rule iterate_Suc [THEN subst])
wenzelm@19742
   288
apply (erule spec)
wenzelm@19742
   289
done
wenzelm@19742
   290
wenzelm@19742
   291
lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"
wenzelm@19742
   292
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
wenzelm@19742
   293
apply (erule hoare_lemma20 [THEN spec])
wenzelm@19742
   294
done
wenzelm@19742
   295
wenzelm@19742
   296
lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"
wenzelm@19742
   297
apply (subst q_def3)
wenzelm@19742
   298
apply simp
wenzelm@19742
   299
done
wenzelm@19742
   300
wenzelm@19742
   301
(* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
wenzelm@19742
   302
wenzelm@19742
   303
lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT
wenzelm@19742
   304
  ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x"
wenzelm@19742
   305
  by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]])
wenzelm@19742
   306
wenzelm@19742
   307
lemma hoare_lemma26: "(EX n. b1$(iterate n$g$x)~=TT) ==> 
wenzelm@19742
   308
  k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF  
wenzelm@19742
   309
  --> q$x = q$(iterate k$g$x)"
wenzelm@19742
   310
apply (case_tac "k")
wenzelm@19742
   311
apply hypsubst
wenzelm@19742
   312
apply (intro strip)
wenzelm@19742
   313
apply (simp (no_asm))
wenzelm@19742
   314
apply hypsubst
wenzelm@19742
   315
apply (intro strip)
wenzelm@19742
   316
apply (erule conjE)
wenzelm@19742
   317
apply (rule trans)
wenzelm@19742
   318
apply (rule hoare_lemma25 [symmetric])
wenzelm@19742
   319
apply assumption
wenzelm@19742
   320
apply assumption
wenzelm@19742
   321
apply (rule trans)
wenzelm@19742
   322
apply (rule q_def3)
wenzelm@19742
   323
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
wenzelm@19742
   324
apply (rule hoare_lemma8 [THEN spec, THEN mp])
wenzelm@19742
   325
apply assumption
wenzelm@19742
   326
apply assumption
wenzelm@19742
   327
apply (simp (no_asm))
wenzelm@19742
   328
apply (simp (no_asm))
wenzelm@19742
   329
done
wenzelm@19742
   330
wenzelm@19742
   331
wenzelm@19742
   332
lemma hoare_lemma27: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 
wenzelm@19742
   333
  k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU  
wenzelm@19742
   334
  --> q$x = UU"
wenzelm@19742
   335
apply (case_tac "k")
wenzelm@19742
   336
apply hypsubst
wenzelm@19742
   337
apply (simp (no_asm))
wenzelm@19742
   338
apply (intro strip)
wenzelm@19742
   339
apply (erule conjE)
wenzelm@19742
   340
apply (subst q_def3)
huffman@40028
   341
apply (simp)
wenzelm@19742
   342
apply hypsubst
wenzelm@19742
   343
apply (simp (no_asm))
wenzelm@19742
   344
apply (intro strip)
wenzelm@19742
   345
apply (erule conjE)
wenzelm@19742
   346
apply (rule trans)
wenzelm@19742
   347
apply (rule hoare_lemma25 [symmetric])
wenzelm@19742
   348
apply assumption
wenzelm@19742
   349
apply assumption
wenzelm@19742
   350
apply (rule trans)
wenzelm@19742
   351
apply (rule q_def3)
wenzelm@19742
   352
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
wenzelm@19742
   353
apply (rule hoare_lemma8 [THEN spec, THEN mp])
wenzelm@19742
   354
apply assumption
wenzelm@19742
   355
apply assumption
wenzelm@19742
   356
apply (simp (no_asm))
huffman@40028
   357
apply (simp)
wenzelm@19742
   358
apply (rule trans)
wenzelm@19742
   359
apply (rule q_def3)
huffman@40028
   360
apply (simp)
wenzelm@19742
   361
done
wenzelm@19742
   362
wenzelm@19742
   363
(* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q   ----- *)
wenzelm@19742
   364
wenzelm@19742
   365
lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x"
wenzelm@19742
   366
apply (subst hoare_lemma16)
wenzelm@19742
   367
apply assumption
wenzelm@19742
   368
apply (rule hoare_lemma19 [THEN disjE])
wenzelm@19742
   369
apply assumption
wenzelm@19742
   370
apply (simplesubst hoare_lemma18)
wenzelm@19742
   371
apply assumption
wenzelm@19742
   372
apply (simplesubst hoare_lemma22)
wenzelm@19742
   373
apply assumption
wenzelm@19742
   374
apply (rule refl)
wenzelm@19742
   375
apply (simplesubst hoare_lemma21)
wenzelm@19742
   376
apply assumption
wenzelm@19742
   377
apply (simplesubst hoare_lemma21)
wenzelm@19742
   378
apply assumption
wenzelm@19742
   379
apply (rule refl)
wenzelm@19742
   380
done
wenzelm@19742
   381
wenzelm@19742
   382
(* ------------  EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q   ----- *)
wenzelm@19742
   383
wenzelm@19742
   384
lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x"
wenzelm@19742
   385
apply (rule hoare_lemma5 [THEN disjE])
wenzelm@19742
   386
apply assumption
wenzelm@19742
   387
apply (rule refl)
wenzelm@19742
   388
apply (subst hoare_lemma11 [THEN mp])
wenzelm@19742
   389
apply assumption
wenzelm@19742
   390
apply (rule conjI)
wenzelm@19742
   391
apply (rule refl)
wenzelm@19742
   392
apply assumption
wenzelm@19742
   393
apply (rule hoare_lemma26 [THEN mp, THEN subst])
wenzelm@19742
   394
apply assumption
wenzelm@19742
   395
apply (rule conjI)
wenzelm@19742
   396
apply (rule refl)
wenzelm@19742
   397
apply assumption
wenzelm@19742
   398
apply (rule refl)
wenzelm@19742
   399
apply (subst hoare_lemma12 [THEN mp])
wenzelm@19742
   400
apply assumption
wenzelm@19742
   401
apply (rule conjI)
wenzelm@19742
   402
apply (rule refl)
wenzelm@19742
   403
apply assumption
wenzelm@19742
   404
apply (subst hoare_lemma22)
wenzelm@19742
   405
apply (subst hoare_lemma28)
wenzelm@19742
   406
apply assumption
wenzelm@19742
   407
apply (rule refl)
wenzelm@19742
   408
apply (rule sym)
wenzelm@19742
   409
apply (subst hoare_lemma27 [THEN mp])
wenzelm@19742
   410
apply assumption
wenzelm@19742
   411
apply (rule conjI)
wenzelm@19742
   412
apply (rule refl)
wenzelm@19742
   413
apply assumption
wenzelm@19742
   414
apply (rule refl)
wenzelm@19742
   415
done
wenzelm@19742
   416
wenzelm@19742
   417
(* ------ the main proof q o p = q ------ *)
wenzelm@19742
   418
wenzelm@19742
   419
theorem hoare_main: "q oo p = q"
huffman@40002
   420
apply (rule cfun_eqI)
wenzelm@19742
   421
apply (subst cfcomp2)
wenzelm@19742
   422
apply (rule hoare_lemma3 [THEN disjE])
wenzelm@19742
   423
apply (erule hoare_lemma23)
wenzelm@19742
   424
apply (erule hoare_lemma29)
wenzelm@19742
   425
done
wenzelm@17291
   426
nipkow@244
   427
end