# HG changeset patch
# User hoelzl
# Date 1394478280 -3600
# Node ID f92479477c52613cb6d8e68b3c9ceaf40f680913
# Parent  682bba24e474f474ac8b38574050721d4d5756c2
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices

diff -r 682bba24e474 -r f92479477c52 src/HOL/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -22,8 +22,8 @@
   (? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
 by (unfold BufAC_Asm_F_def, auto)
 
-lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F"
-by (auto simp add: down_cont_def BufAC_Asm_F_def3)
+lemma cont_BufAC_Asm_F: "down_continuous BufAC_Asm_F"
+by (auto simp add: down_continuous_def BufAC_Asm_F_def3)
 
 lemma BufAC_Cmt_F_def3:
  "((s,t):BufAC_Cmt_F C) = (!d x.
@@ -37,8 +37,8 @@
 apply (auto intro: surjectiv_scons [symmetric])
 done
 
-lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F"
-by (auto simp add: down_cont_def BufAC_Cmt_F_def3)
+lemma cont_BufAC_Cmt_F: "down_continuous BufAC_Cmt_F"
+by (auto simp add: down_continuous_def BufAC_Cmt_F_def3)
 
 
 (**** adm_BufAC_Asm ***********************************************************)
@@ -117,8 +117,8 @@
 
 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
 lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x --> 
-                     (x,f\<cdot>x):down_iterate BufAC_Cmt_F i --> 
-                     (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
+                     (x,f\<cdot>x):(BufAC_Cmt_F ^^ i) top --> 
+                     (s,f\<cdot>s):(BufAC_Cmt_F ^^ i) top"
 apply (rule_tac x="%i. 2*i" in exI)
 apply (rule allI)
 apply (induct_tac "i")
@@ -182,9 +182,9 @@
 apply assumption
 done
 
-lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)"
+lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>(BufAC_Cmt_F ^^ n) top)"
 apply (unfold BufAC_Cmt_def)
-apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp])
+apply (subst cont_BufAC_Cmt_F [THEN down_continuous_gfp])
 apply (fast)
 done
 
diff -r 682bba24e474 -r f92479477c52 src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -5,7 +5,7 @@
 header {* Admissibility for streams *}
 
 theory Stream_adm
-imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity"
+imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
 begin
 
 definition
@@ -93,7 +93,7 @@
 
 lemma stream_monoP2I:
 "!!X. stream_monoP F ==> !i. ? l. !x y. 
-  enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
+  enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top"
 apply (unfold stream_monoP_def)
 apply (safe)
 apply (rule_tac x="i*ia" in exI)
@@ -120,9 +120,9 @@
 done
 
 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
- enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
-    down_cont F |] ==> adm (%x. x:gfp F)"
-apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
+ enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top;
+    down_continuous F |] ==> adm (%x. x:gfp F)"
+apply (erule down_continuous_gfp[of F, THEN ssubst])
 apply (simp (no_asm))
 apply (rule adm_lemmas)
 apply (rule flatstream_admI)
@@ -144,7 +144,7 @@
 
 lemma stream_antiP2I:
 "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]
-  ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i"
+  ==> !i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top"
 apply (unfold stream_antiP_def)
 apply (rule allI)
 apply (induct_tac "i")
@@ -170,10 +170,10 @@
 done
 
 lemma stream_antiP2_non_gfp_admI:
-"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] 
+"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |] 
   ==> adm (%u. ~ u:gfp F)"
 apply (unfold adm_def)
-apply (simp add: INTER_down_iterate_is_gfp)
+apply (simp add: down_continuous_gfp)
 apply (fast dest!: is_ub_thelub)
 done
 
diff -r 682bba24e474 -r f92479477c52 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Mon Mar 10 17:14:57 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,297 +0,0 @@
-(*  Title:      HOL/Library/Continuity.thy
-    Author:     David von Oheimb, TU Muenchen
-*)
-
-header {* Continuity and iterations (of set transformers) *}
-
-theory Continuity
-imports Main
-begin
-
-subsection {* Continuity for complete lattices *}
-
-definition
-  chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
-  "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
-
-definition
-  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
-  "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
-
-lemma SUP_nat_conv:
-  fixes M :: "nat \<Rightarrow> 'a::complete_lattice"
-  shows "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
-apply(rule order_antisym)
- apply(rule SUP_least)
- apply(case_tac n)
-  apply simp
- apply (fast intro:SUP_upper le_supI2)
-apply(simp)
-apply (blast intro:SUP_least SUP_upper)
-done
-
-lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
-  assumes "continuous F" shows "mono F"
-proof
-  fix A B :: "'a" assume "A <= B"
-  let ?C = "%i::nat. if i=0 then A else B"
-  have "chain ?C" using `A <= B` by(simp add:chain_def)
-  have "F B = sup (F A) (F B)"
-  proof -
-    have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
-    hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp
-    also have "\<dots> = (SUP i. F(?C i))"
-      using `chain ?C` `continuous F` by(simp add:continuous_def)
-    also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp
-    finally show ?thesis .
-  qed
-  thus "F A \<le> F B" by(subst le_iff_sup, simp)
-qed
-
-lemma continuous_lfp:
- assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)"
-proof -
-  note mono = continuous_mono[OF `continuous F`]
-  { fix i have "(F ^^ i) bot \<le> lfp F"
-    proof (induct i)
-      show "(F ^^ 0) bot \<le> lfp F" by simp
-    next
-      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])
-      finally show ?case .
-    qed }
-  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least)
-  moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
-  proof (rule lfp_lowerbound)
-    have "chain(%i. (F ^^ i) bot)"
-    proof -
-      { fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
-        proof (induct i)
-          case 0 show ?case by simp
-        next
-          case Suc thus ?case using monoD[OF mono Suc] by auto
-        qed }
-      thus ?thesis by(auto simp add:chain_def)
-    qed
-    hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
-    also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper)
-    finally show "F ?U \<le> ?U" .
-  qed
-  ultimately show ?thesis by (blast intro:order_antisym)
-qed
-
-text{* The following development is just for sets but presents an up
-and a down version of chains and continuity and covers @{const gfp}. *}
-
-
-subsection "Chains"
-
-definition
-  up_chain :: "(nat => 'a set) => bool" where
-  "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
-
-lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
-  by (simp add: up_chain_def)
-
-lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
-  by (simp add: up_chain_def)
-
-lemma up_chain_less_mono:
-    "up_chain F ==> x < y ==> F x \<subseteq> F y"
-  apply (induct y)
-   apply (blast dest: up_chainD elim: less_SucE)+
-  done
-
-lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
-  apply (drule le_imp_less_or_eq)
-  apply (blast dest: up_chain_less_mono)
-  done
-
-
-definition
-  down_chain :: "(nat => 'a set) => bool" where
-  "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
-
-lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
-  by (simp add: down_chain_def)
-
-lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
-  by (simp add: down_chain_def)
-
-lemma down_chain_less_mono:
-    "down_chain F ==> x < y ==> F y \<subseteq> F x"
-  apply (induct y)
-   apply (blast dest: down_chainD elim: less_SucE)+
-  done
-
-lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
-  apply (drule le_imp_less_or_eq)
-  apply (blast dest: down_chain_less_mono)
-  done
-
-
-subsection "Continuity"
-
-definition
-  up_cont :: "('a set => 'a set) => bool" where
-  "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
-
-lemma up_contI:
-  "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
-apply (unfold up_cont_def)
-apply blast
-done
-
-lemma up_contD:
-  "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
-apply (unfold up_cont_def)
-apply auto
-done
-
-
-lemma up_cont_mono: "up_cont f ==> mono f"
-apply (rule monoI)
-apply (drule_tac F = "\<lambda>i. if i = 0 then x else y" in up_contD)
- apply (rule up_chainI)
- apply simp
-apply (drule Un_absorb1)
-apply (auto split:split_if_asm)
-done
-
-
-definition
-  down_cont :: "('a set => 'a set) => bool" where
-  "down_cont f =
-    (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
-
-lemma down_contI:
-  "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
-    down_cont f"
-  apply (unfold down_cont_def)
-  apply blast
-  done
-
-lemma down_contD: "down_cont f ==> down_chain F ==>
-    f (Inter (range F)) = Inter (f ` range F)"
-  apply (unfold down_cont_def)
-  apply auto
-  done
-
-lemma down_cont_mono: "down_cont f ==> mono f"
-apply (rule monoI)
-apply (drule_tac F = "\<lambda>i. if i = 0 then y else x" in down_contD)
- apply (rule down_chainI)
- apply simp
-apply (drule Int_absorb1)
-apply (auto split:split_if_asm)
-done
-
-
-subsection "Iteration"
-
-definition
-  up_iterate :: "('a set => 'a set) => nat => 'a set" where
-  "up_iterate f n = (f ^^ n) {}"
-
-lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
-  by (simp add: up_iterate_def)
-
-lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
-  by (simp add: up_iterate_def)
-
-lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
-  apply (rule up_chainI)
-  apply (induct_tac i)
-   apply simp+
-  apply (erule (1) monoD)
-  done
-
-lemma UNION_up_iterate_is_fp:
-  "up_cont F ==>
-    F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
-  apply (frule up_cont_mono [THEN up_iterate_chain])
-  apply (drule (1) up_contD)
-  apply simp
-  apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
-  apply (case_tac xa)
-   apply auto
-  done
-
-lemma UNION_up_iterate_lowerbound:
-    "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
-  apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
-   apply fast
-  apply (induct_tac i)
-  prefer 2 apply (drule (1) monoD)
-   apply auto
-  done
-
-lemma UNION_up_iterate_is_lfp:
-    "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
-  apply (rule set_eq_subset [THEN iffD2])
-  apply (rule conjI)
-   prefer 2
-   apply (drule up_cont_mono)
-   apply (rule UNION_up_iterate_lowerbound)
-    apply assumption
-   apply (erule lfp_unfold [symmetric])
-  apply (rule lfp_lowerbound)
-  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
-  apply (erule UNION_up_iterate_is_fp [symmetric])
-  done
-
-
-definition
-  down_iterate :: "('a set => 'a set) => nat => 'a set" where
-  "down_iterate f n = (f ^^ n) UNIV"
-
-lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
-  by (simp add: down_iterate_def)
-
-lemma down_iterate_Suc [simp]:
-    "down_iterate f (Suc i) = f (down_iterate f i)"
-  by (simp add: down_iterate_def)
-
-lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
-  apply (rule down_chainI)
-  apply (induct_tac i)
-   apply simp+
-  apply (erule (1) monoD)
-  done
-
-lemma INTER_down_iterate_is_fp:
-  "down_cont F ==>
-    F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
-  apply (frule down_cont_mono [THEN down_iterate_chain])
-  apply (drule (1) down_contD)
-  apply simp
-  apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
-  apply (case_tac xa)
-   apply auto
-  done
-
-lemma INTER_down_iterate_upperbound:
-    "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
-  apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
-   apply fast
-  apply (induct_tac i)
-  prefer 2 apply (drule (1) monoD)
-   apply auto
-  done
-
-lemma INTER_down_iterate_is_gfp:
-    "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
-  apply (rule set_eq_subset [THEN iffD2])
-  apply (rule conjI)
-   apply (drule down_cont_mono)
-   apply (rule INTER_down_iterate_upperbound)
-    apply assumption
-   apply (erule gfp_unfold [symmetric])
-  apply (rule gfp_upperbound)
-  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
-  apply (erule INTER_down_iterate_is_fp)
-  done
-
-end
diff -r 682bba24e474 -r f92479477c52 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/Library/Library.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -7,7 +7,6 @@
   BNF_Decl
   Boolean_Algebra
   Char_ord
-  Continuity
   ContNotDenum
   Convex
   Countable
@@ -41,6 +40,7 @@
   Numeral_Type
   OptionalSugar
   Option_ord
+  Order_Continuity
   Parallel
   Permutation
   Permutations
diff -r 682bba24e474 -r f92479477c52 src/HOL/Library/Order_Continuity.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Order_Continuity.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -0,0 +1,141 @@
+(*  Title:      HOL/Library/Order_Continuity.thy
+    Author:     David von Oheimb, TU Muenchen
+*)
+
+header {* Continuity and iterations (of set transformers) *}
+
+theory Order_Continuity
+imports Main
+begin
+
+(* TODO: Generalize theory to chain-complete partial orders *)
+
+lemma SUP_nat_binary:
+  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
+  apply (auto intro!: antisym SUP_least)
+  apply (rule SUP_upper2[where i=0])
+  apply simp_all
+  apply (rule SUP_upper2[where i=1])
+  apply simp_all
+  done
+
+lemma INF_nat_binary:
+  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
+  apply (auto intro!: antisym INF_greatest)
+  apply (rule INF_lower2[where i=0])
+  apply simp_all
+  apply (rule INF_lower2[where i=1])
+  apply simp_all
+  done
+
+subsection {* Continuity for complete lattices *}
+
+definition
+  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+  "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
+
+lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
+  by (auto simp: continuous_def)
+
+lemma continuous_mono:
+  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
+  assumes [simp]: "continuous F" shows "mono F"
+proof
+  fix A B :: "'a" assume [simp]: "A \<le> B"
+  have "F B = F (SUP n::nat. if n = 0 then A else B)"
+    by (simp add: sup_absorb2 SUP_nat_binary)
+  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
+    by (auto simp: continuousD mono_def intro!: SUP_cong)
+  finally show "F A \<le> F B"
+    by (simp add: SUP_nat_binary le_iff_sup)
+qed
+
+lemma continuous_lfp:
+  assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
+proof (rule antisym)
+  note mono = continuous_mono[OF `continuous F`]
+  show "?U \<le> lfp F"
+  proof (rule SUP_least)
+    fix i show "(F ^^ i) bot \<le> lfp F"
+    proof (induct i)
+      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])
+      finally show ?case .
+    qed simp
+  qed
+  show "lfp F \<le> ?U"
+  proof (rule lfp_lowerbound)
+    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
+    proof -
+      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
+        proof (induct i)
+          case 0 show ?case by simp
+        next
+          case Suc thus ?case using monoD[OF mono Suc] by auto
+        qed }
+      thus ?thesis by (auto simp add: mono_iff_le_Suc)
+    qed
+    hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
+    also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
+    finally show "F ?U \<le> ?U" .
+  qed
+qed
+
+definition
+  down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+  "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
+
+lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
+  by (auto simp: down_continuous_def)
+
+lemma down_continuous_mono:
+  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
+  assumes [simp]: "down_continuous F" shows "mono F"
+proof
+  fix A B :: "'a" assume [simp]: "A \<le> B"
+  have "F A = F (INF n::nat. if n = 0 then B else A)"
+    by (simp add: inf_absorb2 INF_nat_binary)
+  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
+    by (auto simp: down_continuousD antimono_def intro!: INF_cong)
+  finally show "F A \<le> F B"
+    by (simp add: INF_nat_binary le_iff_inf inf_commute)
+qed
+
+lemma down_continuous_gfp:
+  assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
+proof (rule antisym)
+  note mono = down_continuous_mono[OF `down_continuous F`]
+  show "gfp F \<le> ?U"
+  proof (rule INF_greatest)
+    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])
+      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 .
+    qed simp
+  qed
+  show "?U \<le> gfp F"
+  proof (rule gfp_upperbound)
+    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
+    proof -
+      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
+        proof (induct i)
+          case 0 show ?case by simp
+        next
+          case Suc thus ?case using monoD[OF mono Suc] by auto
+        qed }
+      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
+    qed
+    have "?U \<le> (INF i. (F ^^ Suc i) top)"
+      by (fast intro: INF_greatest INF_lower)
+    also have "\<dots> \<le> F ?U"
+      by (simp add: down_continuousD `down_continuous F` *)
+    finally show "?U \<le> F ?U" .
+  qed
+qed
+
+end
diff -r 682bba24e474 -r f92479477c52 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -1618,6 +1618,15 @@
     by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
 qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
 
+lemma lift_Suc_antimono_le:
+  assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
+  shows "f n \<ge> f n'"
+proof (cases "n < n'")
+  case True
+  then show ?thesis
+    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
+qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
+
 lemma lift_Suc_mono_less:
   assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
   shows "f n < f n'"
@@ -1635,6 +1644,10 @@
   "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
   unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
 
+lemma antimono_iff_le_Suc:
+  "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
+  unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
+
 lemma mono_nat_linear_lb:
   fixes f :: "nat \<Rightarrow> nat"
   assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
diff -r 682bba24e474 -r f92479477c52 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/Orderings.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -1010,6 +1010,28 @@
   from assms show "f x \<le> f y" by (simp add: mono_def)
 qed
 
+definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
+  "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
+
+lemma antimonoI [intro?]:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+  shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
+  unfolding antimono_def by iprover
+
+lemma antimonoD [dest?]:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+  shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
+  unfolding antimono_def by iprover
+
+lemma antimonoE:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+  assumes "antimono f"
+  assumes "x \<le> y"
+  obtains "f x \<ge> f y"
+proof
+  from assms show "f x \<ge> f y" by (simp add: antimono_def)
+qed
+
 definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
   "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
 
diff -r 682bba24e474 -r f92479477c52 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -678,7 +678,7 @@
       by (auto simp: incseq_Suc_iff le_fun_def image_iff u' intro!: real_of_ereal_positive_mono)
     show "\<And>x. (\<lambda>k. u' k x) ----> f' x"
       using SUP_eq u(2)
-      by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_mono incseq_Suc_iff le_fun_def)
+      by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_Suc_iff le_fun_def)
     show "bounded {integral UNIV (u' k)|k. True}"
     proof (safe intro!: bounded_realI)
       fix k
diff -r 682bba24e474 -r f92479477c52 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -1193,26 +1193,25 @@
         The use of disjunction here complicates proofs considerably.
         One alternative is to add a Boolean argument to indicate the direction.
         Another is to develop the notions of increasing and decreasing first.*}
-  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
-
-definition
-  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
-    --{*Increasing sequence*}
-  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
-
-definition
-  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
-    --{*Decreasing sequence*}
-  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) \<or> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
+
+abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+  "incseq X \<equiv> mono X"
+
+lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)"
+  unfolding mono_def ..
+
+abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+  "decseq X \<equiv> antimono X"
+
+lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+  unfolding antimono_def ..
 
 definition
   subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
     --{*Definition of subsequence*}
   "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
 
-lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
-  unfolding mono_def incseq_def by auto
-
 lemma incseq_SucI:
   "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
   using lift_Suc_mono_le[of X]