haftmann@22803: (* Title: HOL/Library/While_Combinator.thy wenzelm@10251: Author: Tobias Nipkow krauss@37757: Author: Alexander Krauss wenzelm@10251: Copyright 2000 TU Muenchen wenzelm@10251: *) wenzelm@10251: wenzelm@14706: header {* A general ``while'' combinator *} wenzelm@10251: nipkow@15131: theory While_Combinator haftmann@30738: imports Main nipkow@15131: begin wenzelm@10251: krauss@37760: subsection {* Partial version *} krauss@37757: krauss@37757: definition while_option :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a option" where krauss@37757: "while_option b c s = (if (\k. ~ b ((c ^^ k) s)) krauss@37757: 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 krauss@37757: proof (cases "\k. ~ b ((c ^^ k) s)") krauss@37757: case True krauss@37757: then obtain k where 1: "~ b ((c ^^ k) s)" .. krauss@37757: with `b s` obtain l where "k = Suc l" by (cases k) auto krauss@37757: with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1) krauss@37757: then have 2: "\l. ~ b ((c ^^ l) (c s))" .. krauss@37757: from 1 krauss@37757: have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))" krauss@37757: by (rule Least_Suc) (simp add: `b s`) krauss@37757: also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))" krauss@37757: by (simp add: funpow_swap1) krauss@37757: finally krauss@37757: show ?thesis krauss@37757: using True 2 `b s` by (simp add: funpow_swap1 while_option_def) krauss@37757: next krauss@37757: case False krauss@37757: then have "~ (\l. ~ b ((c ^^ Suc l) s))" by blast krauss@37757: then have "~ (\l. ~ b ((c ^^ l) (c s)))" krauss@37757: by (simp add: funpow_swap1) krauss@37757: with False `b s` show ?thesis by (simp add: while_option_def) krauss@37757: qed krauss@37757: next krauss@37757: assume [simp]: "~ b s" krauss@37757: have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0" krauss@37757: by (rule Least_equality) auto krauss@37757: moreover krauss@37757: 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: nipkow@45834: "while_option b c s = Some t \ EX 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: nipkow@45834: 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: krauss@37757: assumes step: "!!s. P s ==> b s ==> P (c s)" krauss@37757: and result: "while_option b c s = Some t" krauss@37757: and init: "P s" krauss@37757: shows "P t" krauss@37757: proof - krauss@37757: def 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 bool) \ ('a \ 'a) \ 'a \ 'a" krauss@37757: where "while b c s = the (while_option b c s)" krauss@37757: krauss@37757: lemma while_unfold: 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@10251: text {* wenzelm@10251: The proof rule for @{term while}, where @{term P} is the invariant. wenzelm@10251: *} 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: nipkow@41720: 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}" nipkow@41764: and "!!s. P s \ b s \ P(c s)" and "P s" nipkow@41720: shows "EX t. while_option b c s = Some t" nipkow@41764: using assms(1,3) nipkow@41720: apply (induct s) nipkow@41764: using assms(2) nipkow@41720: apply (subst while_option_unfold) nipkow@41720: apply simp nipkow@41720: done nipkow@41720: nipkow@41720: theorem measure_while_option_Some: fixes f :: "'s \ nat" nipkow@41764: shows "(!!s. P s \ b s \ P(c s) \ f(c s) < f s) nipkow@41764: \ P s \ EX 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: nipkow@45834: text{* Kleene iteration starting from the empty set and assuming some finite nipkow@45834: 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 nipkow@45834: 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: wenzelm@10251: end