src/HOL/Library/While_Combinator.thy
 author nipkow Fri Nov 23 23:07:38 2012 +0100 (2012-11-23) changeset 50180 c6626861c31a parent 50008 eb7f574d0303 child 50577 cfbad2d08412 permissions -rw-r--r--
moved lemma
 haftmann@22803 1 (* Title: HOL/Library/While_Combinator.thy wenzelm@10251 2 Author: Tobias Nipkow krauss@37757 3 Author: Alexander Krauss wenzelm@10251 4 Copyright 2000 TU Muenchen wenzelm@10251 5 *) wenzelm@10251 6 wenzelm@14706 7 header {* A general ``while'' combinator *} wenzelm@10251 8 nipkow@15131 9 theory While_Combinator haftmann@30738 10 imports Main nipkow@15131 11 begin wenzelm@10251 12 krauss@37760 13 subsection {* Partial version *} krauss@37757 14 krauss@37757 15 definition while_option :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a option" where krauss@37757 16 "while_option b c s = (if (\k. ~ b ((c ^^ k) s)) krauss@37757 17 then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s) krauss@37757 18 else None)" wenzelm@10251 19 krauss@37757 20 theorem while_option_unfold[code]: krauss@37757 21 "while_option b c s = (if b s then while_option b c (c s) else Some s)" krauss@37757 22 proof cases krauss@37757 23 assume "b s" krauss@37757 24 show ?thesis krauss@37757 25 proof (cases "\k. ~ b ((c ^^ k) s)") krauss@37757 26 case True krauss@37757 27 then obtain k where 1: "~ b ((c ^^ k) s)" .. krauss@37757 28 with `b s` obtain l where "k = Suc l" by (cases k) auto krauss@37757 29 with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1) krauss@37757 30 then have 2: "\l. ~ b ((c ^^ l) (c s))" .. krauss@37757 31 from 1 krauss@37757 32 have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))" krauss@37757 33 by (rule Least_Suc) (simp add: `b s`) krauss@37757 34 also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))" krauss@37757 35 by (simp add: funpow_swap1) krauss@37757 36 finally krauss@37757 37 show ?thesis krauss@37757 38 using True 2 `b s` by (simp add: funpow_swap1 while_option_def) krauss@37757 39 next krauss@37757 40 case False krauss@37757 41 then have "~ (\l. ~ b ((c ^^ Suc l) s))" by blast krauss@37757 42 then have "~ (\l. ~ b ((c ^^ l) (c s)))" krauss@37757 43 by (simp add: funpow_swap1) krauss@37757 44 with False `b s` show ?thesis by (simp add: while_option_def) krauss@37757 45 qed krauss@37757 46 next krauss@37757 47 assume [simp]: "~ b s" krauss@37757 48 have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0" krauss@37757 49 by (rule Least_equality) auto krauss@37757 50 moreover krauss@37757 51 have "\k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto krauss@37757 52 ultimately show ?thesis unfolding while_option_def by auto krauss@37757 53 qed wenzelm@10251 54 nipkow@45834 55 lemma while_option_stop2: nipkow@45834 56 "while_option b c s = Some t \ EX k. t = (c^^k) s \ \ b t" nipkow@45834 57 apply(simp add: while_option_def split: if_splits) blanchet@46365 58 by (metis (lifting) LeastI_ex) nipkow@45834 59 nipkow@45834 60 lemma while_option_stop: "while_option b c s = Some t \ ~ b t" nipkow@45834 61 by(metis while_option_stop2) krauss@37757 62 krauss@37757 63 theorem while_option_rule: krauss@37757 64 assumes step: "!!s. P s ==> b s ==> P (c s)" krauss@37757 65 and result: "while_option b c s = Some t" krauss@37757 66 and init: "P s" krauss@37757 67 shows "P t" krauss@37757 68 proof - krauss@37757 69 def k == "LEAST k. ~ b ((c ^^ k) s)" krauss@37757 70 from assms have t: "t = (c ^^ k) s" krauss@37757 71 by (simp add: while_option_def k_def split: if_splits) krauss@37757 72 have 1: "ALL i bool) \ ('a \ 'a) \ 'a \ 'a" krauss@37757 84 where "while b c s = the (while_option b c s)" krauss@37757 85 nipkow@50008 86 lemma while_unfold [code]: krauss@37757 87 "while b c s = (if b s then while b c (c s) else s)" krauss@37757 88 unfolding while_def by (subst while_option_unfold) simp nipkow@10984 89 wenzelm@18372 90 lemma def_while_unfold: wenzelm@18372 91 assumes fdef: "f == while test do" wenzelm@18372 92 shows "f x = (if test x then f(do x) else x)" krauss@37757 93 unfolding fdef by (fact while_unfold) nipkow@14300 94 nipkow@14300 95 wenzelm@10251 96 text {* wenzelm@10251 97 The proof rule for @{term while}, where @{term P} is the invariant. wenzelm@10251 98 *} wenzelm@10251 99 wenzelm@18372 100 theorem while_rule_lemma: wenzelm@18372 101 assumes invariant: "!!s. P s ==> b s ==> P (c s)" wenzelm@18372 102 and terminate: "!!s. P s ==> \ b s ==> Q s" wenzelm@18372 103 and wf: "wf {(t, s). P s \ b s \ t = c s}" wenzelm@18372 104 shows "P s \ Q (while b c s)" wenzelm@19736 105 using wf wenzelm@19736 106 apply (induct s) wenzelm@18372 107 apply simp wenzelm@18372 108 apply (subst while_unfold) wenzelm@18372 109 apply (simp add: invariant terminate) wenzelm@18372 110 done wenzelm@10251 111 nipkow@10653 112 theorem while_rule: nipkow@10984 113 "[| P s; nipkow@10984 114 !!s. [| P s; b s |] ==> P (c s); nipkow@10984 115 !!s. [| P s; \ b s |] ==> Q s; wenzelm@10997 116 wf r; nipkow@10984 117 !!s. [| P s; b s |] ==> (c s, s) \ r |] ==> nipkow@10984 118 Q (while b c s)" wenzelm@19736 119 apply (rule while_rule_lemma) wenzelm@19736 120 prefer 4 apply assumption wenzelm@19736 121 apply blast wenzelm@19736 122 apply blast wenzelm@19736 123 apply (erule wf_subset) wenzelm@19736 124 apply blast wenzelm@19736 125 done nipkow@10653 126 nipkow@41720 127 text{* Proving termination: *} nipkow@41720 128 nipkow@41720 129 theorem wf_while_option_Some: nipkow@41764 130 assumes "wf {(t, s). (P s \ b s) \ t = c s}" nipkow@41764 131 and "!!s. P s \ b s \ P(c s)" and "P s" nipkow@41720 132 shows "EX t. while_option b c s = Some t" nipkow@41764 133 using assms(1,3) nipkow@41720 134 apply (induct s) nipkow@41764 135 using assms(2) nipkow@41720 136 apply (subst while_option_unfold) nipkow@41720 137 apply simp nipkow@41720 138 done nipkow@41720 139 nipkow@41720 140 theorem measure_while_option_Some: fixes f :: "'s \ nat" nipkow@41764 141 shows "(!!s. P s \ b s \ P(c s) \ f(c s) < f s) nipkow@41764 142 \ P s \ EX t. while_option b c s = Some t" nipkow@41764 143 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f]) wenzelm@10251 144 nipkow@45834 145 text{* Kleene iteration starting from the empty set and assuming some finite nipkow@45834 146 bounding set: *} nipkow@45834 147 nipkow@45834 148 lemma while_option_finite_subset_Some: fixes C :: "'a set" nipkow@45834 149 assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" nipkow@45834 150 shows "\P. while_option (\A. f A \ A) f {} = Some P" nipkow@45834 151 proof(rule measure_while_option_Some[where nipkow@45834 152 f= "%A::'a set. card C - card A" and P= "%A. A \ C \ A \ f A" and s= "{}"]) nipkow@45834 153 fix A assume A: "A \ C \ A \ f A" "f A \ A" nipkow@45834 154 show "(f A \ C \ f A \ f (f A)) \ card C - card (f A) < card C - card A" nipkow@45834 155 (is "?L \ ?R") nipkow@45834 156 proof nipkow@45834 157 show ?L by(metis A(1) assms(2) monoD[OF `mono f`]) nipkow@45834 158 show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset) nipkow@45834 159 qed nipkow@45834 160 qed simp nipkow@45834 161 nipkow@45834 162 lemma lfp_the_while_option: nipkow@45834 163 assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" nipkow@45834 164 shows "lfp f = the(while_option (\A. f A \ A) f {})" nipkow@45834 165 proof- nipkow@45834 166 obtain P where "while_option (\A. f A \ A) f {} = Some P" nipkow@45834 167 using while_option_finite_subset_Some[OF assms] by blast nipkow@45834 168 with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)] nipkow@45834 169 show ?thesis by auto nipkow@45834 170 qed nipkow@45834 171 nipkow@50180 172 lemma lfp_while: nipkow@50180 173 assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" nipkow@50180 174 shows "lfp f = while (\A. f A \ A) f {}" nipkow@50180 175 unfolding while_def using assms by (rule lfp_the_while_option) blast nipkow@50180 176 wenzelm@10251 177 end