src/HOL/IMP/Live_True.thy
changeset 46365 547d1a1dcaf6
parent 45812 0b02adadf384
child 47818 151d137f1095
equal deleted inserted replaced
46364:abab10d1f4a3 46365:547d1a1dcaf6
   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