src/HOL/Library/While_Combinator.thy
 author wenzelm Thu May 06 14:14:18 2004 +0200 (2004-05-06) changeset 14706 71590b7733b7 parent 14589 feae7b5fd425 child 15131 c69542757a4d permissions -rw-r--r--
tuned document;
 wenzelm@10251 1 (* Title: HOL/Library/While.thy wenzelm@10251 2 ID: \$Id\$ wenzelm@10251 3 Author: Tobias Nipkow wenzelm@10251 4 Copyright 2000 TU Muenchen wenzelm@10251 5 *) wenzelm@10251 6 wenzelm@14706 7 header {* A general ``while'' combinator *} wenzelm@10251 8 wenzelm@10251 9 theory While_Combinator = Main: wenzelm@10251 10 wenzelm@10251 11 text {* wenzelm@10251 12 We define a while-combinator @{term while} and prove: (a) an wenzelm@10251 13 unrestricted unfolding law (even if while diverges!) (I got this wenzelm@10251 14 idea from Wolfgang Goerigk), and (b) the invariant rule for reasoning wenzelm@10251 15 about @{term while}. wenzelm@10251 16 *} wenzelm@10251 17 wenzelm@10251 18 consts while_aux :: "('a => bool) \ ('a => 'a) \ 'a => 'a" wenzelm@11626 19 recdef (permissive) while_aux wenzelm@10251 20 "same_fst (\b. True) (\b. same_fst (\c. True) (\c. wenzelm@10251 21 {(t, s). b s \ c s = t \ wenzelm@11701 22 \ (\f. f (0::nat) = s \ (\i. b (f i) \ c (f i) = f (i + 1)))}))" wenzelm@10251 23 "while_aux (b, c, s) = wenzelm@11701 24 (if (\f. f (0::nat) = s \ (\i. b (f i) \ c (f i) = f (i + 1))) wenzelm@10251 25 then arbitrary wenzelm@10251 26 else if b s then while_aux (b, c, c s) wenzelm@10251 27 else s)" wenzelm@10251 28 wenzelm@10774 29 recdef_tc while_aux_tc: while_aux wenzelm@10774 30 apply (rule wf_same_fst) wenzelm@10774 31 apply (rule wf_same_fst) wenzelm@10774 32 apply (simp add: wf_iff_no_infinite_down_chain) wenzelm@10774 33 apply blast wenzelm@10774 34 done wenzelm@10774 35 wenzelm@10251 36 constdefs wenzelm@10251 37 while :: "('a => bool) => ('a => 'a) => 'a => 'a" wenzelm@10251 38 "while b c s == while_aux (b, c, s)" wenzelm@10251 39 wenzelm@10251 40 lemma while_aux_unfold: wenzelm@10251 41 "while_aux (b, c, s) = wenzelm@11701 42 (if \f. f (0::nat) = s \ (\i. b (f i) \ c (f i) = f (i + 1)) wenzelm@10251 43 then arbitrary wenzelm@10251 44 else if b s then while_aux (b, c, c s) wenzelm@10251 45 else s)" wenzelm@10251 46 apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]]) wenzelm@10251 47 apply (rule refl) wenzelm@10251 48 done wenzelm@10251 49 wenzelm@10251 50 text {* wenzelm@10251 51 The recursion equation for @{term while}: directly executable! wenzelm@10251 52 *} wenzelm@10251 53 kleing@12791 54 theorem while_unfold [code]: wenzelm@10251 55 "while b c s = (if b s then while b c (c s) else s)" wenzelm@10251 56 apply (unfold while_def) wenzelm@10251 57 apply (rule while_aux_unfold [THEN trans]) wenzelm@10251 58 apply auto wenzelm@10251 59 apply (subst while_aux_unfold) wenzelm@10251 60 apply simp wenzelm@10251 61 apply clarify wenzelm@10251 62 apply (erule_tac x = "\i. f (Suc i)" in allE) wenzelm@10251 63 apply blast wenzelm@10251 64 done wenzelm@10251 65 nipkow@10984 66 hide const while_aux nipkow@10984 67 nipkow@14300 68 lemma def_while_unfold: assumes fdef: "f == while test do" nipkow@14300 69 shows "f x = (if test x then f(do x) else x)" nipkow@14300 70 proof - nipkow@14300 71 have "f x = while test do x" using fdef by simp nipkow@14300 72 also have "\ = (if test x then while test do (do x) else x)" nipkow@14300 73 by(rule while_unfold) nipkow@14300 74 also have "\ = (if test x then f(do x) else x)" by(simp add:fdef[symmetric]) nipkow@14300 75 finally show ?thesis . nipkow@14300 76 qed nipkow@14300 77 nipkow@14300 78 wenzelm@10251 79 text {* wenzelm@10251 80 The proof rule for @{term while}, where @{term P} is the invariant. wenzelm@10251 81 *} wenzelm@10251 82 nipkow@10653 83 theorem while_rule_lemma[rule_format]: nipkow@10984 84 "[| !!s. P s ==> b s ==> P (c s); nipkow@10984 85 !!s. P s ==> \ b s ==> Q s; nipkow@10984 86 wf {(t, s). P s \ b s \ t = c s} |] ==> wenzelm@10251 87 P s --> Q (while b c s)" wenzelm@10251 88 proof - wenzelm@11549 89 case rule_context wenzelm@10251 90 assume wf: "wf {(t, s). P s \ b s \ t = c s}" wenzelm@10251 91 show ?thesis wenzelm@10251 92 apply (induct s rule: wf [THEN wf_induct]) wenzelm@10251 93 apply simp wenzelm@10251 94 apply clarify wenzelm@10251 95 apply (subst while_unfold) wenzelm@11549 96 apply (simp add: rule_context) wenzelm@10251 97 done wenzelm@10251 98 qed wenzelm@10251 99 nipkow@10653 100 theorem while_rule: nipkow@10984 101 "[| P s; nipkow@10984 102 !!s. [| P s; b s |] ==> P (c s); nipkow@10984 103 !!s. [| P s; \ b s |] ==> Q s; wenzelm@10997 104 wf r; nipkow@10984 105 !!s. [| P s; b s |] ==> (c s, s) \ r |] ==> nipkow@10984 106 Q (while b c s)" nipkow@10653 107 apply (rule while_rule_lemma) nipkow@10653 108 prefer 4 apply assumption nipkow@10653 109 apply blast nipkow@10653 110 apply blast nipkow@10653 111 apply(erule wf_subset) nipkow@10653 112 apply blast nipkow@10653 113 done nipkow@10653 114 nipkow@10984 115 text {* nipkow@10984 116 \medskip An application: computation of the @{term lfp} on finite nipkow@10984 117 sets via iteration. nipkow@10984 118 *} nipkow@10984 119 nipkow@10984 120 theorem lfp_conv_while: nipkow@10984 121 "[| mono f; finite U; f U = U |] ==> nipkow@10984 122 lfp f = fst (while (\(A, fA). A \ fA) (\(A, fA). (fA, f fA)) ({}, f {}))" nipkow@10984 123 apply (rule_tac P = "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" and wenzelm@11047 124 r = "((Pow U \ UNIV) \ (Pow U \ UNIV)) \ nipkow@10984 125 inv_image finite_psubset (op - U o fst)" in while_rule) nipkow@10984 126 apply (subst lfp_unfold) nipkow@10984 127 apply assumption nipkow@10984 128 apply (simp add: monoD) nipkow@10984 129 apply (subst lfp_unfold) nipkow@10984 130 apply assumption nipkow@10984 131 apply clarsimp nipkow@10984 132 apply (blast dest: monoD) nipkow@10984 133 apply (fastsimp intro!: lfp_lowerbound) nipkow@10984 134 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) nipkow@10984 135 apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le) nipkow@10984 136 apply (blast intro!: finite_Diff dest: monoD) nipkow@10984 137 done nipkow@10984 138 nipkow@10984 139 nipkow@10984 140 text {* wenzelm@14589 141 An example of using the @{term while} combinator. nipkow@10984 142 *} nipkow@10984 143 wenzelm@14589 144 theorem "P (lfp (\N::int set. {0} \ {(n + 2) mod 6 | n. n \ N})) = wenzelm@14589 145 P {0, 4, 2}" wenzelm@10997 146 proof - wenzelm@10997 147 have aux: "!!f A B. {f n | n. A n \ B n} = {f n | n. A n} \ {f n | n. B n}" nipkow@10984 148 apply blast wenzelm@10997 149 done wenzelm@10997 150 show ?thesis wenzelm@11914 151 apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) wenzelm@10997 152 apply (rule monoI) wenzelm@10997 153 apply blast wenzelm@10997 154 apply simp wenzelm@10997 155 apply (simp add: aux set_eq_subset) wenzelm@10997 156 txt {* The fixpoint computation is performed purely by rewriting: *} wenzelm@10997 157 apply (simp add: while_unfold aux set_eq_subset del: subset_empty) wenzelm@10997 158 done wenzelm@10997 159 qed wenzelm@10251 160 wenzelm@10251 161 end