src/HOL/Library/While_Combinator.thy
 author haftmann Fri Mar 27 10:05:11 2009 +0100 (2009-03-27) changeset 30738 0842e906300c parent 27487 c8a6ce181805 child 37757 dc78d2d9e90a permissions -rw-r--r--
normalized imports
 haftmann@22803 1 (* Title: HOL/Library/While_Combinator.thy wenzelm@10251 2 Author: Tobias Nipkow wenzelm@10251 3 Copyright 2000 TU Muenchen wenzelm@10251 4 *) wenzelm@10251 5 wenzelm@14706 6 header {* A general ``while'' combinator *} wenzelm@10251 7 nipkow@15131 8 theory While_Combinator haftmann@30738 9 imports Main nipkow@15131 10 begin wenzelm@10251 11 krauss@23821 12 text {* krauss@23821 13 We define the while combinator as the "mother of all tail recursive functions". wenzelm@10251 14 *} wenzelm@10251 15 krauss@23821 16 function (tailrec) while :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a" krauss@23821 17 where krauss@23821 18 while_unfold[simp del]: "while b c s = (if b s then while b c (c s) else s)" krauss@23821 19 by auto wenzelm@10251 20 krauss@23821 21 declare while_unfold[code] nipkow@10984 22 wenzelm@18372 23 lemma def_while_unfold: wenzelm@18372 24 assumes fdef: "f == while test do" wenzelm@18372 25 shows "f x = (if test x then f(do x) else x)" nipkow@14300 26 proof - nipkow@14300 27 have "f x = while test do x" using fdef by simp nipkow@14300 28 also have "\ = (if test x then while test do (do x) else x)" nipkow@14300 29 by(rule while_unfold) nipkow@14300 30 also have "\ = (if test x then f(do x) else x)" by(simp add:fdef[symmetric]) nipkow@14300 31 finally show ?thesis . nipkow@14300 32 qed nipkow@14300 33 nipkow@14300 34 wenzelm@10251 35 text {* wenzelm@10251 36 The proof rule for @{term while}, where @{term P} is the invariant. wenzelm@10251 37 *} wenzelm@10251 38 wenzelm@18372 39 theorem while_rule_lemma: wenzelm@18372 40 assumes invariant: "!!s. P s ==> b s ==> P (c s)" wenzelm@18372 41 and terminate: "!!s. P s ==> \ b s ==> Q s" wenzelm@18372 42 and wf: "wf {(t, s). P s \ b s \ t = c s}" wenzelm@18372 43 shows "P s \ Q (while b c s)" wenzelm@19736 44 using wf wenzelm@19736 45 apply (induct s) wenzelm@18372 46 apply simp wenzelm@18372 47 apply (subst while_unfold) wenzelm@18372 48 apply (simp add: invariant terminate) wenzelm@18372 49 done wenzelm@10251 50 nipkow@10653 51 theorem while_rule: nipkow@10984 52 "[| P s; nipkow@10984 53 !!s. [| P s; b s |] ==> P (c s); nipkow@10984 54 !!s. [| P s; \ b s |] ==> Q s; wenzelm@10997 55 wf r; nipkow@10984 56 !!s. [| P s; b s |] ==> (c s, s) \ r |] ==> nipkow@10984 57 Q (while b c s)" wenzelm@19736 58 apply (rule while_rule_lemma) wenzelm@19736 59 prefer 4 apply assumption wenzelm@19736 60 apply blast wenzelm@19736 61 apply blast wenzelm@19736 62 apply (erule wf_subset) wenzelm@19736 63 apply blast wenzelm@19736 64 done nipkow@10653 65 nipkow@10984 66 text {* nipkow@10984 67 \medskip An application: computation of the @{term lfp} on finite nipkow@10984 68 sets via iteration. nipkow@10984 69 *} nipkow@10984 70 nipkow@10984 71 theorem lfp_conv_while: nipkow@10984 72 "[| mono f; finite U; f U = U |] ==> nipkow@10984 73 lfp f = fst (while (\(A, fA). A \ fA) (\(A, fA). (fA, f fA)) ({}, f {}))" nipkow@10984 74 apply (rule_tac P = "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" and wenzelm@11047 75 r = "((Pow U \ UNIV) \ (Pow U \ UNIV)) \ nipkow@10984 76 inv_image finite_psubset (op - U o fst)" in while_rule) nipkow@10984 77 apply (subst lfp_unfold) nipkow@10984 78 apply assumption nipkow@10984 79 apply (simp add: monoD) nipkow@10984 80 apply (subst lfp_unfold) nipkow@10984 81 apply assumption nipkow@10984 82 apply clarsimp nipkow@10984 83 apply (blast dest: monoD) nipkow@10984 84 apply (fastsimp intro!: lfp_lowerbound) nipkow@10984 85 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) krauss@19769 86 apply (clarsimp simp add: finite_psubset_def order_less_le) nipkow@10984 87 apply (blast intro!: finite_Diff dest: monoD) nipkow@10984 88 done nipkow@10984 89 nipkow@10984 90 nipkow@10984 91 text {* wenzelm@14589 92 An example of using the @{term while} combinator. nipkow@10984 93 *} nipkow@10984 94 nipkow@15197 95 text{* Cannot use @{thm[source]set_eq_subset} because it leads to nipkow@15197 96 looping because the antisymmetry simproc turns the subset relationship nipkow@15197 97 back into equality. *} nipkow@15197 98 wenzelm@14589 99 theorem "P (lfp (\N::int set. {0} \ {(n + 2) mod 6 | n. n \ N})) = wenzelm@14589 100 P {0, 4, 2}" wenzelm@10997 101 proof - wenzelm@19736 102 have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))" wenzelm@19736 103 by blast wenzelm@10997 104 have aux: "!!f A B. {f n | n. A n \ B n} = {f n | n. A n} \ {f n | n. B n}" nipkow@10984 105 apply blast wenzelm@10997 106 done wenzelm@10997 107 show ?thesis wenzelm@11914 108 apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) wenzelm@10997 109 apply (rule monoI) wenzelm@10997 110 apply blast wenzelm@10997 111 apply simp wenzelm@10997 112 apply (simp add: aux set_eq_subset) wenzelm@10997 113 txt {* The fixpoint computation is performed purely by rewriting: *} nipkow@15197 114 apply (simp add: while_unfold aux seteq del: subset_empty) wenzelm@10997 115 done wenzelm@10997 116 qed wenzelm@10251 117 wenzelm@10251 118 end