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'
     1 (*  Title:      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 fi)"
    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 fi)"
    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 apply (erule flat_codom [THEN disjE])
    99 apply auto
   100 done
   101 
   102 
   103 (* ----- access to definitions ----- *)
   104 
   105 lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
   106 apply (rule trans)
   107 apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
   108 apply simp
   109 done
   110 
   111 lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
   112 apply (rule trans)
   113 apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
   114 apply simp
   115 done
   116 
   117 (** --------- proofs about iterations of p and q ---------- **)
   118 
   119 lemma hoare_lemma9: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) --> 
   120    p$(iterate k$g$x)=p$x"
   121 apply (induct_tac k)
   122 apply (simp (no_asm))
   123 apply (simp (no_asm))
   124 apply (intro strip)
   125 apply (rule_tac s = "p$ (iterate n$g$x) " in trans)
   126 apply (rule trans)
   127 apply (rule_tac [2] p_def3 [symmetric])
   128 apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
   129 apply (rule mp)
   130 apply (erule spec)
   131 apply (simp (no_asm) add: less_Suc_eq)
   132 apply simp
   133 apply (erule mp)
   134 apply (intro strip)
   135 apply (rule mp)
   136 apply (erule spec)
   137 apply (erule less_trans)
   138 apply simp
   139 done
   140 
   141 lemma hoare_lemma24: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->  
   142   q$(iterate k$g$x)=q$x"
   143 apply (induct_tac k)
   144 apply (simp (no_asm))
   145 apply (simp (no_asm) add: less_Suc_eq)
   146 apply (intro strip)
   147 apply (rule_tac s = "q$ (iterate n$g$x) " in trans)
   148 apply (rule trans)
   149 apply (rule_tac [2] q_def3 [symmetric])
   150 apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
   151 apply blast
   152 apply simp
   153 apply (erule mp)
   154 apply (intro strip)
   155 apply (fast dest!: less_Suc_eq [THEN iffD1])
   156 done
   157 
   158 (* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
   159 
   160 thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
   161 
   162 lemma hoare_lemma10:
   163   "EX k. b1$(iterate k$g$x) ~= TT
   164     ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"
   165   by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]])
   166 
   167 lemma hoare_lemma11: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 
   168   k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF  
   169   --> p$x = iterate k$g$x"
   170 apply (case_tac "k")
   171 apply hypsubst
   172 apply (simp (no_asm))
   173 apply (intro strip)
   174 apply (erule conjE)
   175 apply (rule trans)
   176 apply (rule p_def3)
   177 apply simp
   178 apply hypsubst
   179 apply (intro strip)
   180 apply (erule conjE)
   181 apply (rule trans)
   182 apply (erule hoare_lemma10 [symmetric])
   183 apply assumption
   184 apply (rule trans)
   185 apply (rule p_def3)
   186 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
   187 apply (rule hoare_lemma8 [THEN spec, THEN mp])
   188 apply assumption
   189 apply assumption
   190 apply (simp (no_asm))
   191 apply (simp (no_asm))
   192 apply (rule trans)
   193 apply (rule p_def3)
   194 apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
   195 apply (erule_tac s = "FF" in ssubst)
   196 apply simp
   197 done
   198 
   199 lemma hoare_lemma12: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 
   200   k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU  
   201   --> p$x = UU"
   202 apply (case_tac "k")
   203 apply hypsubst
   204 apply (simp (no_asm))
   205 apply (intro strip)
   206 apply (erule conjE)
   207 apply (rule trans)
   208 apply (rule p_def3)
   209 apply simp
   210 apply hypsubst
   211 apply (simp (no_asm))
   212 apply (intro strip)
   213 apply (erule conjE)
   214 apply (rule trans)
   215 apply (rule hoare_lemma10 [symmetric])
   216 apply assumption
   217 apply assumption
   218 apply (rule trans)
   219 apply (rule p_def3)
   220 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
   221 apply (rule hoare_lemma8 [THEN spec, THEN mp])
   222 apply assumption
   223 apply assumption
   224 apply (simp (no_asm))
   225 apply (simp)
   226 apply (rule trans)
   227 apply (rule p_def3)
   228 apply simp
   229 done
   230 
   231 (* -------- results about p for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
   232 
   233 lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
   234 apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
   235 apply simp
   236 apply simp
   237 apply (simp (no_asm))
   238 apply (rule allI)
   239 apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
   240 apply (erule spec)
   241 apply (simp)
   242 apply (rule iterate_Suc [THEN subst])
   243 apply (erule spec)
   244 done
   245 
   246 lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU"
   247 apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
   248 apply (erule fernpass_lemma [THEN spec])
   249 done
   250 
   251 (* -------- results about q for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
   252 
   253 lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
   254 apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
   255 apply simp
   256 apply simp
   257 apply (rule allI)
   258 apply (simp (no_asm))
   259 apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
   260 apply (erule spec)
   261 apply (simp)
   262 apply (rule iterate_Suc [THEN subst])
   263 apply (erule spec)
   264 done
   265 
   266 lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU"
   267 apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
   268 apply (erule hoare_lemma17 [THEN spec])
   269 done
   270 
   271 lemma hoare_lemma19:
   272   "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"
   273 apply (rule flat_codom)
   274 apply (rule_tac t = "x1" in iterate_0 [THEN subst])
   275 apply (erule spec)
   276 done
   277 
   278 lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
   279 apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
   280 apply simp
   281 apply simp
   282 apply (rule allI)
   283 apply (simp (no_asm))
   284 apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
   285 apply (erule spec)
   286 apply (simp)
   287 apply (rule iterate_Suc [THEN subst])
   288 apply (erule spec)
   289 done
   290 
   291 lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"
   292 apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
   293 apply (erule hoare_lemma20 [THEN spec])
   294 done
   295 
   296 lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"
   297 apply (subst q_def3)
   298 apply simp
   299 done
   300 
   301 (* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
   302 
   303 lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT
   304   ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x"
   305   by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]])
   306 
   307 lemma hoare_lemma26: "(EX n. b1$(iterate n$g$x)~=TT) ==> 
   308   k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF  
   309   --> q$x = q$(iterate k$g$x)"
   310 apply (case_tac "k")
   311 apply hypsubst
   312 apply (intro strip)
   313 apply (simp (no_asm))
   314 apply hypsubst
   315 apply (intro strip)
   316 apply (erule conjE)
   317 apply (rule trans)
   318 apply (rule hoare_lemma25 [symmetric])
   319 apply assumption
   320 apply assumption
   321 apply (rule trans)
   322 apply (rule q_def3)
   323 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
   324 apply (rule hoare_lemma8 [THEN spec, THEN mp])
   325 apply assumption
   326 apply assumption
   327 apply (simp (no_asm))
   328 apply (simp (no_asm))
   329 done
   330 
   331 
   332 lemma hoare_lemma27: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 
   333   k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU  
   334   --> q$x = UU"
   335 apply (case_tac "k")
   336 apply hypsubst
   337 apply (simp (no_asm))
   338 apply (intro strip)
   339 apply (erule conjE)
   340 apply (subst q_def3)
   341 apply (simp)
   342 apply hypsubst
   343 apply (simp (no_asm))
   344 apply (intro strip)
   345 apply (erule conjE)
   346 apply (rule trans)
   347 apply (rule hoare_lemma25 [symmetric])
   348 apply assumption
   349 apply assumption
   350 apply (rule trans)
   351 apply (rule q_def3)
   352 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
   353 apply (rule hoare_lemma8 [THEN spec, THEN mp])
   354 apply assumption
   355 apply assumption
   356 apply (simp (no_asm))
   357 apply (simp)
   358 apply (rule trans)
   359 apply (rule q_def3)
   360 apply (simp)
   361 done
   362 
   363 (* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q   ----- *)
   364 
   365 lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x"
   366 apply (subst hoare_lemma16)
   367 apply assumption
   368 apply (rule hoare_lemma19 [THEN disjE])
   369 apply assumption
   370 apply (simplesubst hoare_lemma18)
   371 apply assumption
   372 apply (simplesubst hoare_lemma22)
   373 apply assumption
   374 apply (rule refl)
   375 apply (simplesubst hoare_lemma21)
   376 apply assumption
   377 apply (simplesubst hoare_lemma21)
   378 apply assumption
   379 apply (rule refl)
   380 done
   381 
   382 (* ------------  EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q   ----- *)
   383 
   384 lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x"
   385 apply (rule hoare_lemma5 [THEN disjE])
   386 apply assumption
   387 apply (rule refl)
   388 apply (subst hoare_lemma11 [THEN mp])
   389 apply assumption
   390 apply (rule conjI)
   391 apply (rule refl)
   392 apply assumption
   393 apply (rule hoare_lemma26 [THEN mp, THEN subst])
   394 apply assumption
   395 apply (rule conjI)
   396 apply (rule refl)
   397 apply assumption
   398 apply (rule refl)
   399 apply (subst hoare_lemma12 [THEN mp])
   400 apply assumption
   401 apply (rule conjI)
   402 apply (rule refl)
   403 apply assumption
   404 apply (subst hoare_lemma22)
   405 apply (subst hoare_lemma28)
   406 apply assumption
   407 apply (rule refl)
   408 apply (rule sym)
   409 apply (subst hoare_lemma27 [THEN mp])
   410 apply assumption
   411 apply (rule conjI)
   412 apply (rule refl)
   413 apply assumption
   414 apply (rule refl)
   415 done
   416 
   417 (* ------ the main proof q o p = q ------ *)
   418 
   419 theorem hoare_main: "q oo p = q"
   420 apply (rule cfun_eqI)
   421 apply (subst cfcomp2)
   422 apply (rule hoare_lemma3 [THEN disjE])
   423 apply (erule hoare_lemma23)
   424 apply (erule hoare_lemma29)
   425 done
   426 
   427 end