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