1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/HOLCF/ex/Hoare.thy Sat Nov 27 16:08:10 2010 -0800
1.3 @@ -0,0 +1,425 @@
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