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