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