src/HOL/Library/While_Combinator.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (19 months ago) changeset 67951 655aa11359dc parent 67717 5a1b299fe4af child 69593 3dda49e08b9d permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
1 (*  Title:      HOL/Library/While_Combinator.thy
2     Author:     Tobias Nipkow
3     Author:     Alexander Krauss
4 *)
6 section \<open>A general ``while'' combinator\<close>
8 theory While_Combinator
9 imports Main
10 begin
12 subsection \<open>Partial version\<close>
14 definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
15 "while_option b c s = (if (\<exists>k. \<not> b ((c ^^ k) s))
16    then Some ((c ^^ (LEAST k. \<not> b ((c ^^ k) s))) s)
17    else None)"
19 theorem while_option_unfold[code]:
20 "while_option b c s = (if b s then while_option b c (c s) else Some s)"
21 proof cases
22   assume "b s"
23   show ?thesis
24   proof (cases "\<exists>k. \<not> b ((c ^^ k) s)")
25     case True
26     then obtain k where 1: "\<not> b ((c ^^ k) s)" ..
27     with \<open>b s\<close> obtain l where "k = Suc l" by (cases k) auto
28     with 1 have "\<not> b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
29     then have 2: "\<exists>l. \<not> b ((c ^^ l) (c s))" ..
30     from 1
31     have "(LEAST k. \<not> b ((c ^^ k) s)) = Suc (LEAST l. \<not> b ((c ^^ Suc l) s))"
32       by (rule Least_Suc) (simp add: \<open>b s\<close>)
33     also have "... = Suc (LEAST l. \<not> b ((c ^^ l) (c s)))"
34       by (simp add: funpow_swap1)
35     finally
36     show ?thesis
37       using True 2 \<open>b s\<close> by (simp add: funpow_swap1 while_option_def)
38   next
39     case False
40     then have "\<not> (\<exists>l. \<not> b ((c ^^ Suc l) s))" by blast
41     then have "\<not> (\<exists>l. \<not> b ((c ^^ l) (c s)))"
42       by (simp add: funpow_swap1)
43     with False  \<open>b s\<close> show ?thesis by (simp add: while_option_def)
44   qed
45 next
46   assume [simp]: "\<not> b s"
47   have least: "(LEAST k. \<not> b ((c ^^ k) s)) = 0"
48     by (rule Least_equality) auto
49   moreover
50   have "\<exists>k. \<not> b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
51   ultimately show ?thesis unfolding while_option_def by auto
52 qed
54 lemma while_option_stop2:
55  "while_option b c s = Some t \<Longrightarrow> \<exists>k. t = (c^^k) s \<and> \<not> b t"
56 apply(simp add: while_option_def split: if_splits)
57 by (metis (lifting) LeastI_ex)
59 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> \<not> b t"
60 by(metis while_option_stop2)
62 theorem while_option_rule:
63   assumes step: "!!s. P s ==> b s ==> P (c s)"
64     and result: "while_option b c s = Some t"
65     and init: "P s"
66   shows "P t"
67 proof -
68   define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
69   from assms have t: "t = (c ^^ k) s"
70     by (simp add: while_option_def k_def split: if_splits)
71   have 1: "\<forall>i<k. b ((c ^^ i) s)"
72     by (auto simp: k_def dest: not_less_Least)
74   { fix i assume "i \<le> k" then have "P ((c ^^ i) s)"
75       by (induct i) (auto simp: init step 1) }
76   thus "P t" by (auto simp: t)
77 qed
79 lemma funpow_commute:
80   "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
81 by (induct k arbitrary: s) auto
83 lemma while_option_commute_invariant:
84 assumes Invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
85 assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
86 assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
87 assumes Initial: "P s"
88 shows "map_option f (while_option b c s) = while_option b' c' (f s)"
89 unfolding while_option_def
90 proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
91   fix k
92   assume "\<not> b ((c ^^ k) s)"
93   with Initial show "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
94   proof (induction k arbitrary: s)
95     case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
96   next
97     case (Suc k) thus ?case
98     proof (cases "b s")
99       assume "b s"
100       with Suc.IH[of "c s"] Suc.prems show ?thesis
101         by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
102     next
103       assume "\<not> b s"
104       with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
105     qed
106   qed
107 next
108   fix k
109   assume "\<not> b' ((c' ^^ k) (f s))"
110   with Initial show "\<exists>k. \<not> b ((c ^^ k) s)"
111   proof (induction k arbitrary: s)
112     case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
113   next
114     case (Suc k) thus ?case
115     proof (cases "b s")
116        assume "b s"
117       with Suc.IH[of "c s"] Suc.prems show ?thesis
118         by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
119     next
120       assume "\<not> b s"
121       with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
122     qed
123   qed
124 next
125   fix k
126   assume k: "\<not> b' ((c' ^^ k) (f s))"
127   have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))"
128           (is "?k' = ?k")
129   proof (cases ?k')
130     case 0
131     have "\<not> b' ((c' ^^ 0) (f s))"
132       unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
133     hence "\<not> b s" by (auto simp: TestCommute Initial)
134     hence "?k = 0" by (intro Least_equality) auto
135     with 0 show ?thesis by auto
136   next
137     case (Suc k')
138     have "\<not> b' ((c' ^^ Suc k') (f s))"
139       unfolding Suc[symmetric] by (rule LeastI) (rule k)
140     moreover
141     { fix k assume "k \<le> k'"
142       hence "k < ?k'" unfolding Suc by simp
143       hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
144     }
145     note b' = this
146     { fix k assume "k \<le> k'"
147       hence "f ((c ^^ k) s) = (c' ^^ k) (f s)"
148       and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
149       and "P ((c ^^ k) s)"
150         by (induct k) (auto simp: b' assms)
151       with \<open>k \<le> k'\<close>
152       have "b ((c ^^ k) s)"
153       and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
154       and "P ((c ^^ k) s)"
155         by (auto simp: b')
156     }
157     note b = this(1) and body = this(2) and inv = this(3)
158     hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
159     ultimately show ?thesis unfolding Suc using b
160     proof (intro Least_equality[symmetric], goal_cases)
161       case 1
162       hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
163         by (auto simp: BodyCommute inv b)
164       have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
165       with Test show ?case by (auto simp: TestCommute)
166     next
167       case 2
168       thus ?case by (metis not_less_eq_eq)
169     qed
170   qed
171   have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
172   proof (rule funpow_commute, clarify)
173     fix k assume "k < ?k"
174     hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least)
175     from \<open>k < ?k\<close> have "P ((c ^^ k) s)"
176     proof (induct k)
177       case 0 thus ?case by (auto simp: assms)
178     next
179       case (Suc h)
180       hence "P ((c ^^ h) s)" by auto
181       with Suc show ?case
182         by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
183     qed
184     with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))"
185       by (metis BodyCommute)
186   qed
187   thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
188 qed
190 lemma while_option_commute:
191   assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)"
192   shows "map_option f (while_option b c s) = while_option b' c' (f s)"
193 by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
194   (auto simp add: assms)
196 subsection \<open>Total version\<close>
198 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
199 where "while b c s = the (while_option b c s)"
201 lemma while_unfold [code]:
202   "while b c s = (if b s then while b c (c s) else s)"
203 unfolding while_def by (subst while_option_unfold) simp
205 lemma def_while_unfold:
206   assumes fdef: "f == while test do"
207   shows "f x = (if test x then f(do x) else x)"
208 unfolding fdef by (fact while_unfold)
211 text \<open>
212  The proof rule for @{term while}, where @{term P} is the invariant.
213 \<close>
215 theorem while_rule_lemma:
216   assumes invariant: "!!s. P s ==> b s ==> P (c s)"
217     and terminate: "!!s. P s ==> \<not> b s ==> Q s"
218     and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
219   shows "P s \<Longrightarrow> Q (while b c s)"
220   using wf
221   apply (induct s)
222   apply simp
223   apply (subst while_unfold)
224   apply (simp add: invariant terminate)
225   done
227 theorem while_rule:
228   "[| P s;
229       !!s. [| P s; b s  |] ==> P (c s);
230       !!s. [| P s; \<not> b s  |] ==> Q s;
231       wf r;
232       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
233    Q (while b c s)"
234   apply (rule while_rule_lemma)
235      prefer 4 apply assumption
236     apply blast
237    apply blast
238   apply (erule wf_subset)
239   apply blast
240   done
242 text\<open>Proving termination:\<close>
244 theorem wf_while_option_Some:
245   assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
246   and "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
247   shows "\<exists>t. while_option b c s = Some t"
248 using assms(1,3)
249 proof (induction s)
250   case less thus ?case using assms(2)
251     by (subst while_option_unfold) simp
252 qed
254 lemma wf_rel_while_option_Some:
255 assumes wf: "wf R"
256 assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R"
257 assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)"
258 assumes init: "P s"
259 shows "\<exists>t. while_option b c s = Some t"
260 proof -
261  from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto
262  with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset)
263  with inv init show ?thesis by (auto simp: wf_while_option_Some)
264 qed
266 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
267 shows "(\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
268   \<Longrightarrow> P s \<Longrightarrow> \<exists>t. while_option b c s = Some t"
269 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
271 text\<open>Kleene iteration starting from the empty set and assuming some finite
272 bounding set:\<close>
274 lemma while_option_finite_subset_Some: fixes C :: "'a set"
275   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
276   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
277 proof(rule measure_while_option_Some[where
278     f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
279   fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
280   show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
281     (is "?L \<and> ?R")
282   proof
283     show ?L by(metis A(1) assms(2) monoD[OF \<open>mono f\<close>])
284     show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
285   qed
286 qed simp
288 lemma lfp_the_while_option:
289   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
290   shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
291 proof-
292   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
293     using while_option_finite_subset_Some[OF assms] by blast
294   with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
295   show ?thesis by auto
296 qed
298 lemma lfp_while:
299   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
300   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
301 unfolding while_def using assms by (rule lfp_the_while_option) blast
303 lemma wf_finite_less:
304   assumes "finite (C :: 'a::order set)"
305   shows "wf {(x, y). {x, y} \<subseteq> C \<and> x < y}"
306 by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> a < b}", THEN wf_subset])
307    (fastforce simp: less_eq assms intro: psubset_card_mono)
309 lemma wf_finite_greater:
310   assumes "finite (C :: 'a::order set)"
311   shows "wf {(x, y). {x, y} \<subseteq> C \<and> y < x}"
312 by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> b < a}", THEN wf_subset])
313    (fastforce simp: less_eq assms intro: psubset_card_mono)
315 lemma while_option_finite_increasing_Some:
316   fixes f :: "'a::order \<Rightarrow> 'a"
317   assumes "mono f" and "finite (UNIV :: 'a set)" and "s \<le> f s"
318   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
319 by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\<lambda>A. A \<le> f A" and s="s"])
320    (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified])
322 lemma lfp_the_while_option_lattice:
323   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
324   assumes "mono f" and "finite (UNIV :: 'a set)"
325   shows "lfp f = the (while_option (\<lambda>A. f A \<noteq> A) f bot)"
326 proof -
327   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f bot = Some P"
328     using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
329   with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
330   show ?thesis by auto
331 qed
333 lemma lfp_while_lattice:
334   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
335   assumes "mono f" and "finite (UNIV :: 'a set)"
336   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f bot"
337 unfolding while_def using assms by (rule lfp_the_while_option_lattice)
339 lemma while_option_finite_decreasing_Some:
340   fixes f :: "'a::order \<Rightarrow> 'a"
341   assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \<le> s"
342   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
343 by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\<lambda>A. f A \<le> A" and s="s"])
344    (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified])
346 lemma gfp_the_while_option_lattice:
347   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
348   assumes "mono f" and "finite (UNIV :: 'a set)"
349   shows "gfp f = the(while_option (\<lambda>A. f A \<noteq> A) f top)"
350 proof -
351   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f top = Some P"
352     using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
353   with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
354   show ?thesis by auto
355 qed
357 lemma gfp_while_lattice:
358   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
359   assumes "mono f" and "finite (UNIV :: 'a set)"
360   shows "gfp f = while (\<lambda>A. f A \<noteq> A) f top"
361 unfolding while_def using assms by (rule gfp_the_while_option_lattice)
363 text\<open>Computing the reflexive, transitive closure by iterating a successor
364 function. Stops when an element is found that dos not satisfy the test.
366 More refined (and hence more efficient) versions can be found in ITP 2011 paper
367 by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
368 and the AFP article Executable Transitive Closures by René Thiemann.\<close>
370 context
371 fixes p :: "'a \<Rightarrow> bool"
372 and f :: "'a \<Rightarrow> 'a list"
373 and x :: 'a
374 begin
376 qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
377 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
379 qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
380 where "rtrancl_while_step (ws, Z) =
381   (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
382   in (new @ tl ws, set new \<union> Z))"
384 definition rtrancl_while :: "('a list * 'a set) option"
385 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
387 qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
388 where "rtrancl_while_invariant (ws, Z) =
389    (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
390     Z \<subseteq> {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
392 qualified lemma rtrancl_while_invariant:
393   assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
394   shows   "rtrancl_while_invariant (rtrancl_while_step st)"
395 proof (cases st)
396   fix ws Z assume st: "st = (ws, Z)"
397   with test obtain h t where "ws = h # t" "p h" by (cases ws) auto
398   with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
399 qed
401 lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)"
402 shows "if ws = []
403        then Z = {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z. p z)
404        else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}\<^sup>* `` {x}"
405 proof -
406   have "rtrancl_while_invariant ([x],{x})" by simp
407   with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"
408     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
409   { assume "ws = []"
410     hence ?thesis using I
411       by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
412   } moreover
413   { assume "ws \<noteq> []"
414     hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
415       by (simp add: subset_iff)
416   }
417   ultimately show ?thesis by simp
418 qed
420 lemma rtrancl_while_finite_Some:
421   assumes "finite ({(x, y). y \<in> set (f x)}\<^sup>* `` {x})" (is "finite ?Cl")
422   shows "\<exists>y. rtrancl_while = Some y"
423 proof -
424   let ?R = "(\<lambda>(_, Z). card (?Cl - Z)) <*mlex*> (\<lambda>(ws, _). length ws) <*mlex*> {}"
425   have "wf ?R" by (blast intro: wf_mlex)
426   then show ?thesis unfolding rtrancl_while_def
427   proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
428     fix st assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
429     hence I: "rtrancl_while_invariant (rtrancl_while_step st)"
430       by (blast intro: rtrancl_while_invariant)
431     show "(rtrancl_while_step st, st) \<in> ?R"
432     proof (cases st)
433       fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)"
434       assume st: "st = (ws, Z)"
435       with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto
436       { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) \<noteq> []"
437         then obtain z where "z \<in> set (remdups (filter (\<lambda>y. y \<notin> Z) (f h)))" by fastforce
438         with st ws I have "Z \<subset> ?Z" "Z \<subseteq> ?Cl" "?Z \<subseteq> ?Cl" by auto
439         with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono)
440         with st ws have ?thesis unfolding mlex_prod_def by simp
441       }
442       moreover
443       { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []"
444         with st ws have "?Z = Z" "?ws = t"  by (auto simp: filter_empty_conv)
445         with st ws have ?thesis unfolding mlex_prod_def by simp
446       }
447       ultimately show ?thesis by blast
448     qed
449   qed (simp_all add: rtrancl_while_invariant)
450 qed
452 end
454 end