equal
deleted
inserted
replaced
144 |
144 |
145 (* move to While_Combinator *) |
145 (* move to While_Combinator *) |
146 lemma while_option_stop2: |
146 lemma while_option_stop2: |
147 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" |
147 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" |
148 apply(simp add: while_option_def split: if_splits) |
148 apply(simp add: while_option_def split: if_splits) |
149 by (metis (lam_lifting) LeastI_ex) |
149 by (metis (lifting) LeastI_ex) |
150 (* move to While_Combinator *) |
150 (* move to While_Combinator *) |
151 lemma while_option_finite_subset_Some: fixes C :: "'a set" |
151 lemma while_option_finite_subset_Some: fixes C :: "'a set" |
152 assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
152 assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
153 shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P" |
153 shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P" |
154 proof(rule measure_while_option_Some[where |
154 proof(rule measure_while_option_Some[where |