# HG changeset patch
# User nipkow
# Date 1348116517 -7200
# Node ID 4e4bdd12280f76b524ed61da0181c9e05a626ed8
# Parent  83ac281bcdc27552dac73ffadb6e96979027c3c2
removed lpfp and proved least pfp thm

diff -r 83ac281bcdc2 -r 4e4bdd12280f src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Sep 20 06:48:37 2012 +0200
@@ -201,41 +201,28 @@
 
 subsubsection "Post-fixed point iteration"
 
-definition
-  pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+definition pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
 "pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
 
 lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
 using while_option_stop[OF assms[simplified pfp_def]] by simp
 
-lemma pfp_least:
-assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p"
-proof-
-  { fix x assume "x \<sqsubseteq> p"
-    hence  "f x \<sqsubseteq> f p" by(rule mono)
-    from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans)
-  }
-  thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"]
-    unfolding pfp_def by blast
-qed
+lemma while_least:
+assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
+and "\<forall>x \<in> L. b \<sqsubseteq> x" and "b \<in> L" and "f q \<sqsubseteq> q" and "q \<in> L"
+and "while_option P f b = Some p"
+shows "p \<sqsubseteq> q"
+using while_option_rule[OF _  assms(7)[unfolded pfp_def],
+                        where P = "%x. x \<in> L \<and> x \<sqsubseteq> q"]
+by (metis assms(1-6) le_trans)
 
-definition
- lpfp :: "('a::preord option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
-where "lpfp f c = pfp f (bot c)"
-
-lemma lpfpc_pfp: "lpfp f c = Some p \<Longrightarrow> f p \<sqsubseteq> p"
-by(simp add: pfp_pfp lpfp_def)
+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)
 
 lemma strip_pfp:
 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
-using assms while_option_rule[where P = "%x. g x = g x0" and c = f]
-unfolding pfp_def by metis
-
-lemma strip_lpfp: assumes "\<And>C. strip(f C) = strip C" and "lpfp f c = Some C"
-shows "strip C = c"
-using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp_def]]
-by(metis strip_bot)
+using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp
 
 
 subsection "Abstract Interpretation"
@@ -281,7 +268,7 @@
   {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI = lpfp (step' \<top>)"
+"AI c = pfp (step' \<top>) (bot c)"
 
 
 lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -361,10 +348,10 @@
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "lpfp (step' \<top>) c = Some C"
-  have 2: "step' \<top> C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
+  assume 1: "pfp (step' \<top>) (bot c) = Some C"
+  have 2: "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c"
-    by(simp add: strip_lpfp[OF _ 1])
+    by(simp add: strip_pfp[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> C)) \<le> \<gamma>\<^isub>c (step' \<top> C)"
diff -r 83ac281bcdc2 -r 4e4bdd12280f src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Sep 20 06:48:37 2012 +0200
@@ -34,12 +34,6 @@
 lemma post_in_L[simp]: "C \<in> L X \<Longrightarrow> post C \<in> L X"
 by(simp add: L_acom_def post_in_annos)
 
-lemma lpfp_inv:
-assumes "lpfp f x0 = Some x" and "\<And>x. P x \<Longrightarrow> P(f x)" and "P(bot x0)"
-shows "P x"
-using assms unfolding lpfp_def pfp_def
-by (metis (lifting) while_option_rule)
-
 
 subsection "Computable Abstract Interpretation"
 
@@ -77,7 +71,7 @@
    {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = lpfp (step' (top c)) c"
+"AI c = pfp (step' (top c)) (bot c)"
 
 
 lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -139,13 +133,13 @@
 
 theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "lpfp (step' (top c)) c = Some C"
+  assume 1: "pfp (step' (top c)) (bot c) = Some C"
   have "C \<in> L(vars c)"
-    by(rule lpfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
+    by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
       (erule step'_in_L[OF _ top_in_L])
-  have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
+  have 2: "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
-    by(simp add: strip_lpfp[OF _ 1])
+    by(simp add: strip_pfp[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
@@ -187,6 +181,21 @@
   C \<sqsubseteq> C' \<Longrightarrow> step' (top c) C \<sqsubseteq> step' (top c) C'"
 by (metis top_in_L mono_step' preord_class.le_refl)
 
+lemma pfp_bot_least:
+assumes "\<forall>x\<in>L(vars c)\<inter>{C. strip C = c}.\<forall>y\<in>L(vars c)\<inter>{C. strip C = c}.
+  x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
+and "\<forall>C. C \<in> L(vars c)\<inter>{C. strip C = c} \<longrightarrow> f C \<in> L(vars c)\<inter>{C. strip C = c}"
+and "f C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
+shows "C \<sqsubseteq> C'"
+apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
+by (simp_all add: assms(4,5) bot_least)
+
+lemma AI_least_pfp: assumes "AI c = Some C"
+and "step' (top c) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
+shows "C \<sqsubseteq> C'"
+apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
+by (simp_all add: mono_step'_top)
+
 end
 
 
@@ -200,7 +209,7 @@
 assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
 and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
 and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"
-shows "EX x. pfp f x0 = Some x"
+shows "\<exists>x. pfp f x0 = Some x"
 proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<sqsubseteq> f x"])
   show "wf {(y,x). ((I x \<and> x \<sqsubseteq> f x) \<and> \<not> f x \<sqsubseteq> x) \<and> y = f x}"
     by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
@@ -211,18 +220,6 @@
     by (blast intro: I mono)
 qed
 
-lemma lpfp_termination:
-fixes f :: "'a::preord option acom \<Rightarrow> 'a option acom"
-and m :: "'a option acom \<Rightarrow> nat" and I :: "'a option acom \<Rightarrow> bool"
-assumes "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
-and "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and "\<And>x y. I x \<Longrightarrow> I(f x)" and "I(bot c)"
-and "\<And>C. strip (f C) = strip C"
-shows "\<exists>c'. lpfp f c = Some c'"
-unfolding lpfp_def
-by(fastforce intro: pfp_termination[where I=I and m=m] assms bot_least
-   simp: assms(5))
-
 
 locale Abs_Int_measure =
   Abs_Int_mono where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set" +
@@ -329,9 +326,9 @@
 
 lemma AI_Some_measure: "\<exists>C. AI c = Some C"
 unfolding AI_def
-apply(rule lpfp_termination[where I = "%C. strip C = c \<and> C \<in> L(vars c)"
+apply(rule pfp_termination[where I = "%C. strip C = c \<and> C \<in> L(vars c)"
   and m="m_c"])
-apply(simp_all add: m_c2 mono_step'_top)
+apply(simp_all add: m_c2 mono_step'_top bot_least)
 done
 
 end
diff -r 83ac281bcdc2 -r 4e4bdd12280f src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Sep 20 06:48:37 2012 +0200
@@ -167,7 +167,7 @@
    {bfilter b False I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = lpfp (step' \<top>\<^bsub>c\<^esub>) c"
+"AI c = pfp (step' \<top>\<^bsub>c\<^esub>) (bot c)"
 
 lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(induct c arbitrary: S) (simp_all add: Let_def)
@@ -231,13 +231,13 @@
 
 theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "lpfp (step' (top c)) c = Some C"
+  assume 1: "pfp (step' (top c)) (bot c) = Some C"
   have "C \<in> L(vars c)"
-    by(rule lpfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
+    by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
       (erule step'_in_L[OF _ top_in_L])
-  have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
+  have 2: "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
-    by(simp add: strip_lpfp[OF _ 1])
+    by(simp add: strip_pfp[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"