diff -r 968602739b54 -r 5fa4fc4d721a src/HOL/IMP/Live_True.thy --- a/src/HOL/IMP/Live_True.thy Fri Jul 13 08:45:09 2012 +0200 +++ b/src/HOL/IMP/Live_True.thy Sat Jul 14 16:35:58 2012 +0200 @@ -123,55 +123,6 @@ lemma cfinite[simp]: "finite(vars(c::com))" by (induction c) auto -(* move to Inductive; call Kleene? *) -lemma lfp_finite_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot" -shows "lfp f = (f^^k) bot" -proof(rule antisym) - show "lfp f \ (f^^k) bot" - proof(rule lfp_lowerbound) - show "f ((f^^k) bot) \ (f^^k) bot" using assms(2) by simp - qed -next - show "(f^^k) bot \ lfp f" - proof(induction k) - case 0 show ?case by simp - next - case Suc - from monoD[OF assms(1) Suc] lfp_unfold[OF assms(1)] - show ?case by simp - qed -qed - -(* move to While_Combinator *) -lemma while_option_stop2: - "while_option b c s = Some t \ EX k. t = (c^^k) s \ \ b t" -apply(simp add: while_option_def split: if_splits) -by (metis (lifting) LeastI_ex) -(* move to While_Combinator *) -lemma while_option_finite_subset_Some: fixes C :: "'a set" - assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" - shows "\P. while_option (\A. f A \ A) f {} = Some P" -proof(rule measure_while_option_Some[where - f= "%A::'a set. card C - card A" and P= "%A. A \ C \ A \ f A" and s= "{}"]) - fix A assume A: "A \ C \ A \ f A" "f A \ A" - show "(f A \ C \ f A \ f (f A)) \ card C - card (f A) < card C - card A" - (is "?L \ ?R") - proof - show ?L by(metis A(1) assms(2) monoD[OF `mono f`]) - show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset) - qed -qed simp -(* move to While_Combinator *) -lemma lfp_eq_while_option: - assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" - shows "lfp f = the(while_option (\A. f A \ A) f {})" -proof- - obtain P where "while_option (\A. f A \ A) f {} = Some P" - using while_option_finite_subset_Some[OF assms] by blast - with while_option_stop2[OF this] lfp_finite_iter[OF assms(1)] - show ?thesis by auto -qed - text{* For code generation: *} lemma L_While: fixes b c X assumes "finite X" defines "f == \A. vars b \ X \ L c A" @@ -179,7 +130,7 @@ proof - let ?V = "vars b \ vars c \ X" have "lfp f = ?r" - proof(rule lfp_eq_while_option[where C = "?V"]) + proof(rule lfp_the_while_option[where C = "?V"]) show "mono f" by(simp add: f_def mono_union_L) next fix Y show "Y \ ?V \ f Y \ ?V"