# HG changeset patch
# User nipkow
# Date 1366224806 -7200
# Node ID f692657e0f71cfca820699eef76e0cbf07c7319c
# Parent  19b47bfac6ef4d278868aaaa441a2b61bc9a880f
moved leastness lemma

diff -r 19b47bfac6ef -r f692657e0f71 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Apr 17 20:53:26 2013 +0200
@@ -120,6 +120,14 @@
                         where P = "%x. x \<in> L \<and> x \<le> q"]
 by (metis assms(1-6) order_trans)
 
+lemma pfp_bot_least:
+assumes "\<forall>x\<in>{C. strip C = c}.\<forall>y\<in>{C. strip C = c}. x \<le> y \<longrightarrow> f x \<le> f y"
+and "\<forall>C. C \<in> {C. strip C = c} \<longrightarrow> f C \<in> {C. strip C = c}"
+and "f C' \<le> C'" "strip C' = c" "pfp f (bot c) = Some C"
+shows "C \<le> C'"
+by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(5)[unfolded pfp_def]])
+  (simp_all add: assms(4) bot_least)
+
 lemma pfp_inv:
   "pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
 unfolding pfp_def by (metis (lifting) while_option_rule)