haftmann@22803: (* Title: HOL/Library/While_Combinator.thy wenzelm@10251: Author: Tobias Nipkow krauss@37757: Author: Alexander Krauss wenzelm@10251: *) wenzelm@10251: wenzelm@60500: section \A general ``while'' combinator\ wenzelm@10251: nipkow@15131: theory While_Combinator haftmann@30738: imports Main nipkow@15131: begin wenzelm@10251: wenzelm@60500: subsection \Partial version\ krauss@37757: krauss@37757: definition while_option :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a option" where wenzelm@67091: "while_option b c s = (if (\k. \ b ((c ^^ k) s)) wenzelm@67091: then Some ((c ^^ (LEAST k. \ b ((c ^^ k) s))) s) krauss@37757: else None)" wenzelm@10251: krauss@37757: theorem while_option_unfold[code]: krauss@37757: "while_option b c s = (if b s then while_option b c (c s) else Some s)" krauss@37757: proof cases krauss@37757: assume "b s" krauss@37757: show ?thesis wenzelm@67091: proof (cases "\k. \ b ((c ^^ k) s)") krauss@37757: case True wenzelm@67091: then obtain k where 1: "\ b ((c ^^ k) s)" .. wenzelm@60500: with \b s\ obtain l where "k = Suc l" by (cases k) auto wenzelm@67091: with 1 have "\ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1) wenzelm@67091: then have 2: "\l. \ b ((c ^^ l) (c s))" .. krauss@37757: from 1 wenzelm@67091: have "(LEAST k. \ b ((c ^^ k) s)) = Suc (LEAST l. \ b ((c ^^ Suc l) s))" wenzelm@60500: by (rule Least_Suc) (simp add: \b s\) wenzelm@67091: also have "... = Suc (LEAST l. \ b ((c ^^ l) (c s)))" krauss@37757: by (simp add: funpow_swap1) krauss@37757: finally krauss@37757: show ?thesis wenzelm@60500: using True 2 \b s\ by (simp add: funpow_swap1 while_option_def) krauss@37757: next krauss@37757: case False wenzelm@67091: then have "\ (\l. \ b ((c ^^ Suc l) s))" by blast wenzelm@67091: then have "\ (\l. \ b ((c ^^ l) (c s)))" krauss@37757: by (simp add: funpow_swap1) wenzelm@60500: with False \b s\ show ?thesis by (simp add: while_option_def) krauss@37757: qed krauss@37757: next wenzelm@67091: assume [simp]: "\ b s" wenzelm@67091: have least: "(LEAST k. \ b ((c ^^ k) s)) = 0" krauss@37757: by (rule Least_equality) auto krauss@37757: moreover wenzelm@67091: have "\k. \ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto krauss@37757: ultimately show ?thesis unfolding while_option_def by auto krauss@37757: qed wenzelm@10251: nipkow@45834: lemma while_option_stop2: wenzelm@67091: "while_option b c s = Some t \ \k. t = (c^^k) s \ \ b t" nipkow@45834: apply(simp add: while_option_def split: if_splits) blanchet@46365: by (metis (lifting) LeastI_ex) nipkow@45834: wenzelm@67091: lemma while_option_stop: "while_option b c s = Some t \ \ b t" nipkow@45834: by(metis while_option_stop2) krauss@37757: krauss@37757: theorem while_option_rule: wenzelm@63040: assumes step: "!!s. P s ==> b s ==> P (c s)" wenzelm@63040: and result: "while_option b c s = Some t" wenzelm@63040: and init: "P s" wenzelm@63040: shows "P t" krauss@37757: proof - wenzelm@67091: define k where "k = (LEAST k. \ b ((c ^^ k) s))" krauss@37757: from assms have t: "t = (c ^^ k) s" krauss@37757: by (simp add: while_option_def k_def split: if_splits) krauss@37757: have 1: "ALL i k" then have "P ((c ^^ i) s)" krauss@37757: by (induct i) (auto simp: init step 1) } krauss@37757: thus "P t" by (auto simp: t) krauss@37757: qed krauss@37757: traytel@50577: lemma funpow_commute: traytel@50577: "\\k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\ \ f ((c^^k) s) = (c'^^k) (f s)" traytel@50577: by (induct k arbitrary: s) auto traytel@50577: nipkow@54050: lemma while_option_commute_invariant: nipkow@54050: assumes Invariant: "\s. P s \ b s \ P (c s)" nipkow@54050: assumes TestCommute: "\s. P s \ b s = b' (f s)" nipkow@54050: assumes BodyCommute: "\s. P s \ b s \ f (c s) = c' (f s)" nipkow@54050: assumes Initial: "P s" blanchet@55466: shows "map_option f (while_option b c s) = while_option b' c' (f s)" traytel@50577: unfolding while_option_def traytel@50577: proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject) nipkow@54050: fix k nipkow@54050: assume "\ b ((c ^^ k) s)" nipkow@54050: with Initial show "\k. \ b' ((c' ^^ k) (f s))" traytel@50577: proof (induction k arbitrary: s) nipkow@54050: case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0]) traytel@50577: next nipkow@54050: case (Suc k) thus ?case nipkow@54050: proof (cases "b s") nipkow@54050: assume "b s" nipkow@54050: with Suc.IH[of "c s"] Suc.prems show ?thesis nipkow@54050: by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1) nipkow@54050: next nipkow@54050: assume "\ b s" nipkow@54050: with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0]) nipkow@54050: qed traytel@50577: qed traytel@50577: next nipkow@54050: fix k nipkow@54050: assume "\ b' ((c' ^^ k) (f s))" nipkow@54050: with Initial show "\k. \ b ((c ^^ k) s)" traytel@50577: proof (induction k arbitrary: s) nipkow@54050: case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0]) traytel@50577: next nipkow@54050: case (Suc k) thus ?case traytel@50577: proof (cases "b s") nipkow@54050: assume "b s" nipkow@54050: with Suc.IH[of "c s"] Suc.prems show ?thesis nipkow@54050: by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1) nipkow@54050: next nipkow@54050: assume "\ b s" nipkow@54050: with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0]) nipkow@54050: qed traytel@50577: qed traytel@50577: next nipkow@54050: fix k nipkow@54050: assume k: "\ b' ((c' ^^ k) (f s))" nipkow@54050: have *: "(LEAST k. \ b' ((c' ^^ k) (f s))) = (LEAST k. \ b ((c ^^ k) s))" nipkow@54050: (is "?k' = ?k") traytel@50577: proof (cases ?k') traytel@50577: case 0 nipkow@54050: have "\ b' ((c' ^^ 0) (f s))" nipkow@54050: unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k) nipkow@54050: hence "\ b s" by (auto simp: TestCommute Initial) traytel@50577: hence "?k = 0" by (intro Least_equality) auto traytel@50577: with 0 show ?thesis by auto traytel@50577: next traytel@50577: case (Suc k') nipkow@54050: have "\ b' ((c' ^^ Suc k') (f s))" nipkow@54050: unfolding Suc[symmetric] by (rule LeastI) (rule k) traytel@50577: moreover traytel@50577: { fix k assume "k \ k'" traytel@50577: hence "k < ?k'" unfolding Suc by simp traytel@50577: hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least]) nipkow@54050: } nipkow@54050: note b' = this traytel@50577: { fix k assume "k \ k'" nipkow@54050: hence "f ((c ^^ k) s) = (c' ^^ k) (f s)" nipkow@54050: and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))" nipkow@54050: and "P ((c ^^ k) s)" nipkow@54050: by (induct k) (auto simp: b' assms) wenzelm@60500: with \k \ k'\ nipkow@54050: have "b ((c ^^ k) s)" nipkow@54050: and "f ((c ^^ k) s) = (c' ^^ k) (f s)" nipkow@54050: and "P ((c ^^ k) s)" nipkow@54050: by (auto simp: b') nipkow@54050: } nipkow@54050: note b = this(1) and body = this(2) and inv = this(3) nipkow@54050: hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto traytel@50577: ultimately show ?thesis unfolding Suc using b wenzelm@61166: proof (intro Least_equality[symmetric], goal_cases) wenzelm@60580: case 1 nipkow@54050: hence Test: "\ b' (f ((c ^^ Suc k') s))" nipkow@54050: by (auto simp: BodyCommute inv b) nipkow@54050: have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b) nipkow@54050: with Test show ?case by (auto simp: TestCommute) nipkow@54050: next wenzelm@60580: case 2 wenzelm@60580: thus ?case by (metis not_less_eq_eq) nipkow@54050: qed traytel@50577: qed traytel@50577: have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding * nipkow@54050: proof (rule funpow_commute, clarify) nipkow@54050: fix k assume "k < ?k" nipkow@54050: hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least) wenzelm@60500: from \k < ?k\ have "P ((c ^^ k) s)" nipkow@54050: proof (induct k) nipkow@54050: case 0 thus ?case by (auto simp: assms) nipkow@54050: next nipkow@54050: case (Suc h) nipkow@54050: hence "P ((c ^^ h) s)" by auto nipkow@54050: with Suc show ?case nipkow@54050: by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least) nipkow@54050: qed nipkow@54050: with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))" nipkow@54050: by (metis BodyCommute) nipkow@54050: qed traytel@50577: thus "\z. (c ^^ ?k) s = z \ f z = (c' ^^ ?k') (f s)" by blast traytel@50577: qed krauss@37757: nipkow@54050: lemma while_option_commute: nipkow@54050: assumes "\s. b s = b' (f s)" "\s. \b s\ \ f (c s) = c' (f s)" blanchet@55466: shows "map_option f (while_option b c s) = while_option b' c' (f s)" nipkow@54050: by(rule while_option_commute_invariant[where P = "\_. True"]) nipkow@54050: (auto simp add: assms) nipkow@54050: wenzelm@60500: subsection \Total version\ krauss@37757: krauss@37757: definition while :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a" krauss@37757: where "while b c s = the (while_option b c s)" krauss@37757: nipkow@50008: lemma while_unfold [code]: krauss@37757: "while b c s = (if b s then while b c (c s) else s)" krauss@37757: unfolding while_def by (subst while_option_unfold) simp nipkow@10984: wenzelm@18372: lemma def_while_unfold: wenzelm@18372: assumes fdef: "f == while test do" wenzelm@18372: shows "f x = (if test x then f(do x) else x)" krauss@37757: unfolding fdef by (fact while_unfold) nipkow@14300: nipkow@14300: wenzelm@60500: text \ wenzelm@10251: The proof rule for @{term while}, where @{term P} is the invariant. wenzelm@60500: \ wenzelm@10251: wenzelm@18372: theorem while_rule_lemma: wenzelm@18372: assumes invariant: "!!s. P s ==> b s ==> P (c s)" wenzelm@18372: and terminate: "!!s. P s ==> \ b s ==> Q s" wenzelm@18372: and wf: "wf {(t, s). P s \ b s \ t = c s}" wenzelm@18372: shows "P s \ Q (while b c s)" wenzelm@19736: using wf wenzelm@19736: apply (induct s) wenzelm@18372: apply simp wenzelm@18372: apply (subst while_unfold) wenzelm@18372: apply (simp add: invariant terminate) wenzelm@18372: done wenzelm@10251: nipkow@10653: theorem while_rule: nipkow@10984: "[| P s; nipkow@10984: !!s. [| P s; b s |] ==> P (c s); nipkow@10984: !!s. [| P s; \ b s |] ==> Q s; wenzelm@10997: wf r; nipkow@10984: !!s. [| P s; b s |] ==> (c s, s) \ r |] ==> nipkow@10984: Q (while b c s)" wenzelm@19736: apply (rule while_rule_lemma) wenzelm@19736: prefer 4 apply assumption wenzelm@19736: apply blast wenzelm@19736: apply blast wenzelm@19736: apply (erule wf_subset) wenzelm@19736: apply blast wenzelm@19736: done nipkow@10653: wenzelm@60500: text\Proving termination:\ nipkow@41720: nipkow@41720: theorem wf_while_option_Some: nipkow@41764: assumes "wf {(t, s). (P s \ b s) \ t = c s}" wenzelm@67091: and "\s. P s \ b s \ P(c s)" and "P s" wenzelm@67091: shows "\t. while_option b c s = Some t" nipkow@41764: using assms(1,3) nipkow@54050: proof (induction s) nipkow@54050: case less thus ?case using assms(2) nipkow@54050: by (subst while_option_unfold) simp nipkow@54050: qed nipkow@54050: nipkow@54050: lemma wf_rel_while_option_Some: nipkow@54050: assumes wf: "wf R" nipkow@54050: assumes smaller: "\s. P s \ b s \ (c s, s) \ R" nipkow@54050: assumes inv: "\s. P s \ b s \ P(c s)" nipkow@54050: assumes init: "P s" nipkow@54050: shows "\t. while_option b c s = Some t" nipkow@54050: proof - nipkow@54050: from smaller have "{(t,s). P s \ b s \ t = c s} \ R" by auto nipkow@54050: with wf have "wf {(t,s). P s \ b s \ t = c s}" by (auto simp: wf_subset) nipkow@54050: with inv init show ?thesis by (auto simp: wf_while_option_Some) nipkow@54050: qed nipkow@41720: nipkow@41720: theorem measure_while_option_Some: fixes f :: "'s \ nat" wenzelm@67091: shows "(\s. P s \ b s \ P(c s) \ f(c s) < f s) wenzelm@67091: \ P s \ \t. while_option b c s = Some t" nipkow@41764: by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f]) wenzelm@10251: wenzelm@60500: text\Kleene iteration starting from the empty set and assuming some finite wenzelm@60500: bounding set:\ nipkow@45834: nipkow@45834: lemma while_option_finite_subset_Some: fixes C :: "'a set" nipkow@45834: assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" nipkow@45834: shows "\P. while_option (\A. f A \ A) f {} = Some P" nipkow@45834: proof(rule measure_while_option_Some[where nipkow@45834: f= "%A::'a set. card C - card A" and P= "%A. A \ C \ A \ f A" and s= "{}"]) nipkow@45834: fix A assume A: "A \ C \ A \ f A" "f A \ A" nipkow@45834: show "(f A \ C \ f A \ f (f A)) \ card C - card (f A) < card C - card A" nipkow@45834: (is "?L \ ?R") nipkow@45834: proof wenzelm@60500: show ?L by(metis A(1) assms(2) monoD[OF \mono f\]) nipkow@45834: show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset) nipkow@45834: qed nipkow@45834: qed simp nipkow@45834: nipkow@45834: lemma lfp_the_while_option: nipkow@45834: assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" nipkow@45834: shows "lfp f = the(while_option (\A. f A \ A) f {})" nipkow@45834: proof- nipkow@45834: obtain P where "while_option (\A. f A \ A) f {} = Some P" nipkow@45834: using while_option_finite_subset_Some[OF assms] by blast nipkow@45834: with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)] nipkow@45834: show ?thesis by auto nipkow@45834: qed nipkow@45834: nipkow@50180: lemma lfp_while: nipkow@50180: assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" nipkow@50180: shows "lfp f = while (\A. f A \ A) f {}" nipkow@50180: unfolding while_def using assms by (rule lfp_the_while_option) blast nipkow@50180: Andreas@63561: lemma wf_finite_less: Andreas@63561: assumes "finite (C :: 'a::order set)" Andreas@63561: shows "wf {(x, y). {x, y} \ C \ x < y}" Andreas@63561: by (rule wf_measure[where f="\b. card {a. a \ C \ a < b}", THEN wf_subset]) Andreas@63561: (fastforce simp: less_eq assms intro: psubset_card_mono) Andreas@63561: Andreas@63561: lemma wf_finite_greater: Andreas@63561: assumes "finite (C :: 'a::order set)" Andreas@63561: shows "wf {(x, y). {x, y} \ C \ y < x}" Andreas@63561: by (rule wf_measure[where f="\b. card {a. a \ C \ b < a}", THEN wf_subset]) Andreas@63561: (fastforce simp: less_eq assms intro: psubset_card_mono) Andreas@63561: Andreas@63561: lemma while_option_finite_increasing_Some: Andreas@63561: fixes f :: "'a::order \ 'a" Andreas@63561: assumes "mono f" and "finite (UNIV :: 'a set)" and "s \ f s" Andreas@63561: shows "\P. while_option (\A. f A \ A) f s = Some P" Andreas@63561: by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\A. A \ f A" and s="s"]) Andreas@63561: (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified]) Andreas@63561: Andreas@63561: lemma lfp_the_while_option_lattice: Andreas@63561: fixes f :: "'a::complete_lattice \ 'a" Andreas@63561: assumes "mono f" and "finite (UNIV :: 'a set)" Andreas@63561: shows "lfp f = the (while_option (\A. f A \ A) f bot)" Andreas@63561: proof - Andreas@63561: obtain P where "while_option (\A. f A \ A) f bot = Some P" Andreas@63561: using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast Andreas@63561: with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)] Andreas@63561: show ?thesis by auto Andreas@63561: qed Andreas@63561: Andreas@63561: lemma lfp_while_lattice: Andreas@63561: fixes f :: "'a::complete_lattice \ 'a" Andreas@63561: assumes "mono f" and "finite (UNIV :: 'a set)" Andreas@63561: shows "lfp f = while (\A. f A \ A) f bot" Andreas@63561: unfolding while_def using assms by (rule lfp_the_while_option_lattice) Andreas@63561: Andreas@63561: lemma while_option_finite_decreasing_Some: Andreas@63561: fixes f :: "'a::order \ 'a" Andreas@63561: assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \ s" Andreas@63561: shows "\P. while_option (\A. f A \ A) f s = Some P" Andreas@63561: by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\A. f A \ A" and s="s"]) Andreas@63561: (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified]) Andreas@63561: Andreas@63561: lemma gfp_the_while_option_lattice: Andreas@63561: fixes f :: "'a::complete_lattice \ 'a" Andreas@63561: assumes "mono f" and "finite (UNIV :: 'a set)" Andreas@63561: shows "gfp f = the(while_option (\A. f A \ A) f top)" Andreas@63561: proof - Andreas@63561: obtain P where "while_option (\A. f A \ A) f top = Some P" Andreas@63561: using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast Andreas@63561: with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)] Andreas@63561: show ?thesis by auto Andreas@63561: qed Andreas@63561: Andreas@63561: lemma gfp_while_lattice: Andreas@63561: fixes f :: "'a::complete_lattice \ 'a" Andreas@63561: assumes "mono f" and "finite (UNIV :: 'a set)" Andreas@63561: shows "gfp f = while (\A. f A \ A) f top" Andreas@63561: unfolding while_def using assms by (rule gfp_the_while_option_lattice) nipkow@53217: wenzelm@60500: text\Computing the reflexive, transitive closure by iterating a successor nipkow@53217: function. Stops when an element is found that dos not satisfy the test. nipkow@53217: nipkow@53217: More refined (and hence more efficient) versions can be found in ITP 2011 paper nipkow@53217: by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow) wenzelm@60500: and the AFP article Executable Transitive Closures by RenĂ© Thiemann.\ nipkow@53217: traytel@54196: context traytel@54196: fixes p :: "'a \ bool" traytel@54196: and f :: "'a \ 'a list" traytel@54196: and x :: 'a traytel@54196: begin traytel@54196: wenzelm@61115: qualified fun rtrancl_while_test :: "'a list \ 'a set \ bool" traytel@54196: where "rtrancl_while_test (ws,_) = (ws \ [] \ p(hd ws))" traytel@54196: wenzelm@61115: qualified fun rtrancl_while_step :: "'a list \ 'a set \ 'a list \ 'a set" traytel@54196: where "rtrancl_while_step (ws, Z) = traytel@54196: (let x = hd ws; new = remdups (filter (\y. y \ Z) (f x)) traytel@54196: in (new @ tl ws, set new \ Z))" nipkow@53217: traytel@54196: definition rtrancl_while :: "('a list * 'a set) option" traytel@54196: where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})" traytel@54196: wenzelm@61115: qualified fun rtrancl_while_invariant :: "'a list \ 'a set \ bool" traytel@54196: where "rtrancl_while_invariant (ws, Z) = traytel@54196: (x \ Z \ set ws \ Z \ distinct ws \ {(x,y). y \ set(f x)} `` (Z - set ws) \ Z \ traytel@54196: Z \ {(x,y). y \ set(f x)}^* `` {x} \ (\z\Z - set ws. p z))" traytel@54196: wenzelm@61115: qualified lemma rtrancl_while_invariant: traytel@54196: assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st" traytel@54196: shows "rtrancl_while_invariant (rtrancl_while_step st)" traytel@54196: proof (cases st) traytel@54196: fix ws Z assume st: "st = (ws, Z)" traytel@54196: with test obtain h t where "ws = h # t" "p h" by (cases ws) auto traytel@54196: with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl) traytel@54196: qed traytel@54196: traytel@54196: lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)" nipkow@53217: shows "if ws = [] nipkow@53217: then Z = {(x,y). y \ set(f x)}^* `` {x} \ (\z\Z. p z) nipkow@53217: else \p(hd ws) \ hd ws \ {(x,y). y \ set(f x)}^* `` {x}" traytel@54196: proof - traytel@54196: have "rtrancl_while_invariant ([x],{x})" by simp traytel@54196: with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)" nipkow@53217: by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]]) nipkow@53217: { assume "ws = []" nipkow@53217: hence ?thesis using I haftmann@61424: by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl) nipkow@53217: } moreover nipkow@53217: { assume "ws \ []" nipkow@53217: hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]] nipkow@53217: by (simp add: subset_iff) nipkow@53217: } nipkow@53217: ultimately show ?thesis by simp nipkow@53217: qed nipkow@53217: traytel@54196: lemma rtrancl_while_finite_Some: traytel@54196: assumes "finite ({(x, y). y \ set (f x)}\<^sup>* `` {x})" (is "finite ?Cl") traytel@54196: shows "\y. rtrancl_while = Some y" traytel@54196: proof - traytel@54196: let ?R = "(\(_, Z). card (?Cl - Z)) <*mlex*> (\(ws, _). length ws) <*mlex*> {}" traytel@54196: have "wf ?R" by (blast intro: wf_mlex) traytel@54196: then show ?thesis unfolding rtrancl_while_def traytel@54196: proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant]) traytel@54196: fix st assume *: "rtrancl_while_invariant st \ rtrancl_while_test st" traytel@54196: hence I: "rtrancl_while_invariant (rtrancl_while_step st)" traytel@54196: by (blast intro: rtrancl_while_invariant) traytel@54196: show "(rtrancl_while_step st, st) \ ?R" traytel@54196: proof (cases st) traytel@54196: fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)" traytel@54196: assume st: "st = (ws, Z)" traytel@54196: with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto traytel@54196: { assume "remdups (filter (\y. y \ Z) (f h)) \ []" traytel@54196: then obtain z where "z \ set (remdups (filter (\y. y \ Z) (f h)))" by fastforce traytel@54196: with st ws I have "Z \ ?Z" "Z \ ?Cl" "?Z \ ?Cl" by auto traytel@54196: with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono) traytel@54196: with st ws have ?thesis unfolding mlex_prod_def by simp traytel@54196: } traytel@54196: moreover traytel@54196: { assume "remdups (filter (\y. y \ Z) (f h)) = []" traytel@54196: with st ws have "?Z = Z" "?ws = t" by (auto simp: filter_empty_conv) traytel@54196: with st ws have ?thesis unfolding mlex_prod_def by simp traytel@54196: } traytel@54196: ultimately show ?thesis by blast traytel@54196: qed traytel@54196: qed (simp_all add: rtrancl_while_invariant) traytel@54196: qed traytel@54196: wenzelm@10251: end traytel@54196: traytel@54196: end