1.1 --- a/src/HOLCF/ex/Hoare.thy Sat Nov 27 14:34:54 2010 -0800
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,425 +0,0 @@
1.4 -(* Title: HOLCF/ex/hoare.thy
1.5 - Author: Franz Regensburger
1.6 -
1.7 -Theory for an example by C.A.R. Hoare
1.8 -
1.9 -p x = if b1 x
1.10 - then p (g x)
1.11 - else x fi
1.12 -
1.13 -q x = if b1 x orelse b2 x
1.14 - then q (g x)
1.15 - else x fi
1.16 -
1.17 -Prove: for all b1 b2 g .
1.18 - q o p = q
1.19 -
1.20 -In order to get a nice notation we fix the functions b1,b2 and g in the
1.21 -signature of this example
1.22 -
1.23 -*)
1.24 -
1.25 -theory Hoare
1.26 -imports HOLCF
1.27 -begin
1.28 -
1.29 -axiomatization
1.30 - b1 :: "'a -> tr" and
1.31 - b2 :: "'a -> tr" and
1.32 - g :: "'a -> 'a"
1.33 -
1.34 -definition
1.35 - p :: "'a -> 'a" where
1.36 - "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)"
1.37 -
1.38 -definition
1.39 - q :: "'a -> 'a" where
1.40 - "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)"
1.41 -
1.42 -
1.43 -(* --------- pure HOLCF logic, some little lemmas ------ *)
1.44 -
1.45 -lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU"
1.46 -apply (rule Exh_tr [THEN disjE])
1.47 -apply blast+
1.48 -done
1.49 -
1.50 -lemma hoare_lemma3: " (ALL k. b1$(iterate k$g$x) = TT) | (EX k. b1$(iterate k$g$x)~=TT)"
1.51 -apply blast
1.52 -done
1.53 -
1.54 -lemma hoare_lemma4: "(EX k. b1$(iterate k$g$x) ~= TT) ==>
1.55 - EX k. b1$(iterate k$g$x) = FF | b1$(iterate k$g$x) = UU"
1.56 -apply (erule exE)
1.57 -apply (rule exI)
1.58 -apply (rule hoare_lemma2)
1.59 -apply assumption
1.60 -done
1.61 -
1.62 -lemma hoare_lemma5: "[|(EX k. b1$(iterate k$g$x) ~= TT);
1.63 - k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==>
1.64 - b1$(iterate k$g$x)=FF | b1$(iterate k$g$x)=UU"
1.65 -apply hypsubst
1.66 -apply (rule hoare_lemma2)
1.67 -apply (erule exE)
1.68 -apply (erule LeastI)
1.69 -done
1.70 -
1.71 -lemma hoare_lemma6: "b=UU ==> b~=TT"
1.72 -apply hypsubst
1.73 -apply (rule dist_eq_tr)
1.74 -done
1.75 -
1.76 -lemma hoare_lemma7: "b=FF ==> b~=TT"
1.77 -apply hypsubst
1.78 -apply (rule dist_eq_tr)
1.79 -done
1.80 -
1.81 -lemma hoare_lemma8: "[|(EX k. b1$(iterate k$g$x) ~= TT);
1.82 - k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==>
1.83 - ALL m. m < k --> b1$(iterate m$g$x)=TT"
1.84 -apply hypsubst
1.85 -apply (erule exE)
1.86 -apply (intro strip)
1.87 -apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
1.88 -prefer 2 apply (assumption)
1.89 -apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
1.90 -prefer 2 apply (assumption)
1.91 -apply (rule Least_le)
1.92 -apply (erule hoare_lemma6)
1.93 -apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
1.94 -prefer 2 apply (assumption)
1.95 -apply (rule Least_le)
1.96 -apply (erule hoare_lemma7)
1.97 -done
1.98 -
1.99 -
1.100 -lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
1.101 -by (rule strictI)
1.102 -
1.103 -
1.104 -(* ----- access to definitions ----- *)
1.105 -
1.106 -lemma p_def3: "p$x = If b1$x then p$(g$x) else x"
1.107 -apply (rule trans)
1.108 -apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
1.109 -apply simp
1.110 -done
1.111 -
1.112 -lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x"
1.113 -apply (rule trans)
1.114 -apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
1.115 -apply simp
1.116 -done
1.117 -
1.118 -(** --------- proofs about iterations of p and q ---------- **)
1.119 -
1.120 -lemma hoare_lemma9: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->
1.121 - p$(iterate k$g$x)=p$x"
1.122 -apply (induct_tac k)
1.123 -apply (simp (no_asm))
1.124 -apply (simp (no_asm))
1.125 -apply (intro strip)
1.126 -apply (rule_tac s = "p$ (iterate n$g$x) " in trans)
1.127 -apply (rule trans)
1.128 -apply (rule_tac [2] p_def3 [symmetric])
1.129 -apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
1.130 -apply (rule mp)
1.131 -apply (erule spec)
1.132 -apply (simp (no_asm) add: less_Suc_eq)
1.133 -apply simp
1.134 -apply (erule mp)
1.135 -apply (intro strip)
1.136 -apply (rule mp)
1.137 -apply (erule spec)
1.138 -apply (erule less_trans)
1.139 -apply simp
1.140 -done
1.141 -
1.142 -lemma hoare_lemma24: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->
1.143 - q$(iterate k$g$x)=q$x"
1.144 -apply (induct_tac k)
1.145 -apply (simp (no_asm))
1.146 -apply (simp (no_asm) add: less_Suc_eq)
1.147 -apply (intro strip)
1.148 -apply (rule_tac s = "q$ (iterate n$g$x) " in trans)
1.149 -apply (rule trans)
1.150 -apply (rule_tac [2] q_def3 [symmetric])
1.151 -apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
1.152 -apply blast
1.153 -apply simp
1.154 -apply (erule mp)
1.155 -apply (intro strip)
1.156 -apply (fast dest!: less_Suc_eq [THEN iffD1])
1.157 -done
1.158 -
1.159 -(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
1.160 -
1.161 -thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
1.162 -
1.163 -lemma hoare_lemma10:
1.164 - "EX k. b1$(iterate k$g$x) ~= TT
1.165 - ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"
1.166 - by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]])
1.167 -
1.168 -lemma hoare_lemma11: "(EX n. b1$(iterate n$g$x) ~= TT) ==>
1.169 - k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF
1.170 - --> p$x = iterate k$g$x"
1.171 -apply (case_tac "k")
1.172 -apply hypsubst
1.173 -apply (simp (no_asm))
1.174 -apply (intro strip)
1.175 -apply (erule conjE)
1.176 -apply (rule trans)
1.177 -apply (rule p_def3)
1.178 -apply simp
1.179 -apply hypsubst
1.180 -apply (intro strip)
1.181 -apply (erule conjE)
1.182 -apply (rule trans)
1.183 -apply (erule hoare_lemma10 [symmetric])
1.184 -apply assumption
1.185 -apply (rule trans)
1.186 -apply (rule p_def3)
1.187 -apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
1.188 -apply (rule hoare_lemma8 [THEN spec, THEN mp])
1.189 -apply assumption
1.190 -apply assumption
1.191 -apply (simp (no_asm))
1.192 -apply (simp (no_asm))
1.193 -apply (rule trans)
1.194 -apply (rule p_def3)
1.195 -apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
1.196 -apply (erule_tac s = "FF" in ssubst)
1.197 -apply simp
1.198 -done
1.199 -
1.200 -lemma hoare_lemma12: "(EX n. b1$(iterate n$g$x) ~= TT) ==>
1.201 - k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU
1.202 - --> p$x = UU"
1.203 -apply (case_tac "k")
1.204 -apply hypsubst
1.205 -apply (simp (no_asm))
1.206 -apply (intro strip)
1.207 -apply (erule conjE)
1.208 -apply (rule trans)
1.209 -apply (rule p_def3)
1.210 -apply simp
1.211 -apply hypsubst
1.212 -apply (simp (no_asm))
1.213 -apply (intro strip)
1.214 -apply (erule conjE)
1.215 -apply (rule trans)
1.216 -apply (rule hoare_lemma10 [symmetric])
1.217 -apply assumption
1.218 -apply assumption
1.219 -apply (rule trans)
1.220 -apply (rule p_def3)
1.221 -apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
1.222 -apply (rule hoare_lemma8 [THEN spec, THEN mp])
1.223 -apply assumption
1.224 -apply assumption
1.225 -apply (simp (no_asm))
1.226 -apply (simp)
1.227 -apply (rule trans)
1.228 -apply (rule p_def3)
1.229 -apply simp
1.230 -done
1.231 -
1.232 -(* -------- results about p for case (ALL k. b1$(iterate k$g$x)=TT) ------- *)
1.233 -
1.234 -lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
1.235 -apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
1.236 -apply simp
1.237 -apply simp
1.238 -apply (simp (no_asm))
1.239 -apply (rule allI)
1.240 -apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
1.241 -apply (erule spec)
1.242 -apply (simp)
1.243 -apply (rule iterate_Suc [THEN subst])
1.244 -apply (erule spec)
1.245 -done
1.246 -
1.247 -lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU"
1.248 -apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
1.249 -apply (erule fernpass_lemma [THEN spec])
1.250 -done
1.251 -
1.252 -(* -------- results about q for case (ALL k. b1$(iterate k$g$x)=TT) ------- *)
1.253 -
1.254 -lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
1.255 -apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
1.256 -apply simp
1.257 -apply simp
1.258 -apply (rule allI)
1.259 -apply (simp (no_asm))
1.260 -apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
1.261 -apply (erule spec)
1.262 -apply (simp)
1.263 -apply (rule iterate_Suc [THEN subst])
1.264 -apply (erule spec)
1.265 -done
1.266 -
1.267 -lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU"
1.268 -apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
1.269 -apply (erule hoare_lemma17 [THEN spec])
1.270 -done
1.271 -
1.272 -lemma hoare_lemma19:
1.273 - "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"
1.274 -apply (rule flat_codom)
1.275 -apply (rule_tac t = "x1" in iterate_0 [THEN subst])
1.276 -apply (erule spec)
1.277 -done
1.278 -
1.279 -lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
1.280 -apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
1.281 -apply simp
1.282 -apply simp
1.283 -apply (rule allI)
1.284 -apply (simp (no_asm))
1.285 -apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
1.286 -apply (erule spec)
1.287 -apply (simp)
1.288 -apply (rule iterate_Suc [THEN subst])
1.289 -apply (erule spec)
1.290 -done
1.291 -
1.292 -lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"
1.293 -apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
1.294 -apply (erule hoare_lemma20 [THEN spec])
1.295 -done
1.296 -
1.297 -lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"
1.298 -apply (subst q_def3)
1.299 -apply simp
1.300 -done
1.301 -
1.302 -(* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
1.303 -
1.304 -lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT
1.305 - ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x"
1.306 - by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]])
1.307 -
1.308 -lemma hoare_lemma26: "(EX n. b1$(iterate n$g$x)~=TT) ==>
1.309 - k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF
1.310 - --> q$x = q$(iterate k$g$x)"
1.311 -apply (case_tac "k")
1.312 -apply hypsubst
1.313 -apply (intro strip)
1.314 -apply (simp (no_asm))
1.315 -apply hypsubst
1.316 -apply (intro strip)
1.317 -apply (erule conjE)
1.318 -apply (rule trans)
1.319 -apply (rule hoare_lemma25 [symmetric])
1.320 -apply assumption
1.321 -apply assumption
1.322 -apply (rule trans)
1.323 -apply (rule q_def3)
1.324 -apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
1.325 -apply (rule hoare_lemma8 [THEN spec, THEN mp])
1.326 -apply assumption
1.327 -apply assumption
1.328 -apply (simp (no_asm))
1.329 -apply (simp (no_asm))
1.330 -done
1.331 -
1.332 -
1.333 -lemma hoare_lemma27: "(EX n. b1$(iterate n$g$x) ~= TT) ==>
1.334 - k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU
1.335 - --> q$x = UU"
1.336 -apply (case_tac "k")
1.337 -apply hypsubst
1.338 -apply (simp (no_asm))
1.339 -apply (intro strip)
1.340 -apply (erule conjE)
1.341 -apply (subst q_def3)
1.342 -apply (simp)
1.343 -apply hypsubst
1.344 -apply (simp (no_asm))
1.345 -apply (intro strip)
1.346 -apply (erule conjE)
1.347 -apply (rule trans)
1.348 -apply (rule hoare_lemma25 [symmetric])
1.349 -apply assumption
1.350 -apply assumption
1.351 -apply (rule trans)
1.352 -apply (rule q_def3)
1.353 -apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
1.354 -apply (rule hoare_lemma8 [THEN spec, THEN mp])
1.355 -apply assumption
1.356 -apply assumption
1.357 -apply (simp (no_asm))
1.358 -apply (simp)
1.359 -apply (rule trans)
1.360 -apply (rule q_def3)
1.361 -apply (simp)
1.362 -done
1.363 -
1.364 -(* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q ----- *)
1.365 -
1.366 -lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x"
1.367 -apply (subst hoare_lemma16)
1.368 -apply assumption
1.369 -apply (rule hoare_lemma19 [THEN disjE])
1.370 -apply assumption
1.371 -apply (simplesubst hoare_lemma18)
1.372 -apply assumption
1.373 -apply (simplesubst hoare_lemma22)
1.374 -apply assumption
1.375 -apply (rule refl)
1.376 -apply (simplesubst hoare_lemma21)
1.377 -apply assumption
1.378 -apply (simplesubst hoare_lemma21)
1.379 -apply assumption
1.380 -apply (rule refl)
1.381 -done
1.382 -
1.383 -(* ------------ EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q ----- *)
1.384 -
1.385 -lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x"
1.386 -apply (rule hoare_lemma5 [THEN disjE])
1.387 -apply assumption
1.388 -apply (rule refl)
1.389 -apply (subst hoare_lemma11 [THEN mp])
1.390 -apply assumption
1.391 -apply (rule conjI)
1.392 -apply (rule refl)
1.393 -apply assumption
1.394 -apply (rule hoare_lemma26 [THEN mp, THEN subst])
1.395 -apply assumption
1.396 -apply (rule conjI)
1.397 -apply (rule refl)
1.398 -apply assumption
1.399 -apply (rule refl)
1.400 -apply (subst hoare_lemma12 [THEN mp])
1.401 -apply assumption
1.402 -apply (rule conjI)
1.403 -apply (rule refl)
1.404 -apply assumption
1.405 -apply (subst hoare_lemma22)
1.406 -apply (subst hoare_lemma28)
1.407 -apply assumption
1.408 -apply (rule refl)
1.409 -apply (rule sym)
1.410 -apply (subst hoare_lemma27 [THEN mp])
1.411 -apply assumption
1.412 -apply (rule conjI)
1.413 -apply (rule refl)
1.414 -apply assumption
1.415 -apply (rule refl)
1.416 -done
1.417 -
1.418 -(* ------ the main proof q o p = q ------ *)
1.419 -
1.420 -theorem hoare_main: "q oo p = q"
1.421 -apply (rule cfun_eqI)
1.422 -apply (subst cfcomp2)
1.423 -apply (rule hoare_lemma3 [THEN disjE])
1.424 -apply (erule hoare_lemma23)
1.425 -apply (erule hoare_lemma29)
1.426 -done
1.427 -
1.428 -end