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