# HG changeset patch
# User wenzelm
# Date 1475334995 -7200
# Node ID 95c3ae4baba8d37bfbd48c88c14ffef77b15aa50
# Parent  ec0fb01c6d50d3699521ded75720946272f04a2a
clarified lfp/gfp statements and proofs;

diff -r ec0fb01c6d50 -r 95c3ae4baba8 NEWS
--- a/NEWS	Sat Oct 01 12:03:27 2016 +0200
+++ b/NEWS	Sat Oct 01 17:16:35 2016 +0200
@@ -336,6 +336,12 @@
 eliminates the need to qualify any of those names in the presence of
 infix "mod" syntax. INCOMPATIBILITY.
 
+* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
+have been clarified. The fixpoint properties are lfp_fixpoint, its
+symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
+for the proof (lfp_lemma2 etc.) are no longer exported, but can be
+easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
+
 * Constant "surj" is a mere input abbreviation, to avoid hiding an
 equation in term output. Minor INCOMPATIBILITY.
 
diff -r ec0fb01c6d50 -r 95c3ae4baba8 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Sat Oct 01 17:16:35 2016 +0200
@@ -365,15 +365,15 @@
   by standard (fast intro: Sup_upper Sup_least)+
 
 lemma lfp_eq_fixp:
-  assumes f: "mono f"
+  assumes mono: "mono f"
   shows "lfp f = fixp f"
 proof (rule antisym)
-  from f have f': "monotone (op \<le>) (op \<le>) f"
+  from mono have f': "monotone (op \<le>) (op \<le>) f"
     unfolding mono_def monotone_def .
   show "lfp f \<le> fixp f"
     by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
   show "fixp f \<le> lfp f"
-    by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl)
+    by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono])
 qed
 
 hide_const (open) iterates fixp
diff -r ec0fb01c6d50 -r 95c3ae4baba8 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Inductive.thy	Sat Oct 01 17:16:35 2016 +0200
@@ -14,22 +14,14 @@
     "primrec" :: thy_decl
 begin
 
-subsection \<open>Least and greatest fixed points\<close>
+subsection \<open>Least fixed points\<close>
 
 context complete_lattice
 begin
 
-definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
+definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
   where "lfp f = Inf {u. f u \<le> u}"
 
-definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
-  where "gfp f = Sup {u. u \<le> f u}"
-
-
-subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
-
-text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
-
 lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
   by (auto simp add: lfp_def intro: Inf_lower)
 
@@ -38,14 +30,31 @@
 
 end
 
-lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
-  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
-
-lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
-  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
+lemma lfp_fixpoint:
+  assumes "mono f"
+  shows "f (lfp f) = lfp f"
+  unfolding lfp_def
+proof (rule order_antisym)
+  let ?H = "{u. f u \<le> u}"
+  let ?a = "\<Sqinter>?H"
+  show "f ?a \<le> ?a"
+  proof (rule Inf_greatest)
+    fix x
+    assume "x \<in> ?H"
+    then have "?a \<le> x" by (rule Inf_lower)
+    with \<open>mono f\<close> have "f ?a \<le> f x" ..
+    also from \<open>x \<in> ?H\<close> have "f x \<le> x" ..
+    finally show "f ?a \<le> x" .
+  qed
+  show "?a \<le> f ?a"
+  proof (rule Inf_lower)
+    from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
+    then show "f ?a \<in> ?H" ..
+  qed
+qed
 
 lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
-  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
+  by (rule lfp_fixpoint [symmetric])
 
 lemma lfp_const: "lfp (\<lambda>x. t) = t"
   by (rule lfp_unfold) (simp add: mono_def)
@@ -132,9 +141,13 @@
   by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
 
 
-subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
+subsection \<open>Greatest fixed points\<close>
 
-text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
+context complete_lattice
+begin
+
+definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "gfp f = Sup {u. u \<le> f u}"
 
 lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
   by (auto simp add: gfp_def intro: Sup_upper)
@@ -142,14 +155,36 @@
 lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
   by (auto simp add: gfp_def intro: Sup_least)
 
-lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
-  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
+end
+
+lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
+  by (rule gfp_upperbound) (simp add: lfp_fixpoint)
 
-lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
-  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
+lemma gfp_fixpoint:
+  assumes "mono f"
+  shows "f (gfp f) = gfp f"
+  unfolding gfp_def
+proof (rule order_antisym)
+  let ?H = "{u. u \<le> f u}"
+  let ?a = "\<Squnion>?H"
+  show "?a \<le> f ?a"
+  proof (rule Sup_least)
+    fix x
+    assume "x \<in> ?H"
+    then have "x \<le> f x" ..
+    also from \<open>x \<in> ?H\<close> have "x \<le> ?a" by (rule Sup_upper)
+    with \<open>mono f\<close> have "f x \<le> f ?a" ..
+    finally show "x \<le> f ?a" .
+  qed
+  show "f ?a \<le> ?a"
+  proof (rule Sup_upper)
+    from \<open>mono f\<close> and \<open>?a \<le> f ?a\<close> have "f ?a \<le> f (f ?a)" ..
+    then show "f ?a \<in> ?H" ..
+  qed
+qed
 
 lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
-  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
+  by (rule gfp_fixpoint [symmetric])
 
 lemma gfp_const: "gfp (\<lambda>x. t) = t"
   by (rule gfp_unfold) (simp add: mono_def)
@@ -158,10 +193,6 @@
   by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
 
 
-lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
-  by (iprover intro: gfp_upperbound lfp_lemma3)
-
-
 subsection \<open>Coinduction rules for greatest fixed points\<close>
 
 text \<open>Weak version.\<close>
@@ -174,7 +205,7 @@
   done
 
 lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
-  apply (frule gfp_lemma2)
+  apply (frule gfp_unfold [THEN eq_refl])
   apply (drule mono_sup)
   apply (rule le_supI)
    apply assumption
@@ -190,7 +221,7 @@
   by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
 
 lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
-  by (blast dest: gfp_lemma2 mono_Un)
+  by (blast dest: gfp_fixpoint mono_Un)
 
 lemma gfp_ordinal_induct[case_names mono step union]:
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -248,7 +279,7 @@
   "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
     lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
   apply (rule subset_trans)
-   apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
+   apply (erule coinduct3_mono_lemma [THEN lfp_unfold [THEN eq_refl]])
   apply (rule Un_least [THEN Un_least])
     apply (rule subset_refl, assumption)
   apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
diff -r ec0fb01c6d50 -r 95c3ae4baba8 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Oct 01 17:16:35 2016 +0200
@@ -99,7 +99,7 @@
        (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
 
   show "lfp g \<le> \<alpha> (lfp f)"
-    by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_unfold[OF mf, symmetric])
+    by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
 qed
 
 lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"
diff -r ec0fb01c6d50 -r 95c3ae4baba8 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Library/Order_Continuity.thy	Sat Oct 01 17:16:35 2016 +0200
@@ -123,7 +123,7 @@
       case (Suc i)
       have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
       also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
-      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
+      also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono])
       finally show ?case .
     qed simp
   qed
@@ -287,7 +287,7 @@
     fix i show "gfp F \<le> (F ^^ i) top"
     proof (induct i)
       case (Suc i)
-      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
+      have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
       also have "\<dots> = (F ^^ Suc i) top" by simp
       finally show ?case .
diff -r ec0fb01c6d50 -r 95c3ae4baba8 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Nat.thy	Sat Oct 01 17:16:35 2016 +0200
@@ -1554,7 +1554,7 @@
       by (simp add: comp_def)
   qed
   have "(f ^^ n) (lfp f) = lfp f" for n
-    by (induct n) (auto intro: f lfp_unfold[symmetric])
+    by (induct n) (auto intro: f lfp_fixpoint)
   then show "lfp (f ^^ Suc n) \<le> lfp f"
     by (intro lfp_lowerbound) (simp del: funpow.simps)
 qed
@@ -1571,7 +1571,7 @@
       by (simp add: comp_def)
   qed
   have "(f ^^ n) (gfp f) = gfp f" for n
-    by (induct n) (auto intro: f gfp_unfold[symmetric])
+    by (induct n) (auto intro: f gfp_fixpoint)
   then show "gfp (f ^^ Suc n) \<ge> gfp f"
     by (intro gfp_upperbound) (simp del: funpow.simps)
 qed