rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity

--- a/src/HOL/Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
@@ -556,6 +556,14 @@
   shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
   using `mono f` by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
 
+lemma mono_INF:
+  "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
+  by (intro complete_lattice_class.INF_greatest monoD[OF `mono f`] INF_lower)
+
+lemma mono_SUP:
+  "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
+  by (intro complete_lattice_class.SUP_least monoD[OF `mono f`] SUP_upper)
+
 end
 
 end

--- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
@@ -452,6 +452,9 @@
 
 end
 
+instance complete_linorder < conditionally_complete_linorder
+  ..
+
 lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
   using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
 

--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon May 04 17:35:31 2015 +0200
@@ -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_continuous BufAC_Asm_F"
-by (auto simp add: down_continuous_def BufAC_Asm_F_def3)
+lemma cont_BufAC_Asm_F: "inf_continuous BufAC_Asm_F"
+by (auto simp add: inf_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_continuous BufAC_Cmt_F"
-by (auto simp add: down_continuous_def BufAC_Cmt_F_def3)
+lemma cont_BufAC_Cmt_F: "inf_continuous BufAC_Cmt_F"
+by (auto simp add: inf_continuous_def BufAC_Cmt_F_def3)
 
 
 (**** adm_BufAC_Asm ***********************************************************)
@@ -184,7 +184,7 @@
 
 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 down_continuous_gfp])
+apply (subst cont_BufAC_Cmt_F [THEN inf_continuous_gfp])
 apply (fast)
 done
 

--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon May 04 17:35:31 2015 +0200
@@ -121,8 +121,8 @@
 
 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
  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])
+    inf_continuous F |] ==> adm (%x. x:gfp F)"
+apply (erule inf_continuous_gfp[of F, THEN ssubst])
 apply (simp (no_asm))
 apply (rule adm_lemmas)
 apply (rule flatstream_admI)
@@ -170,10 +170,10 @@
 done
 
 lemma stream_antiP2_non_gfp_admI:
-"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |] 
+"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; inf_continuous F |] 
   ==> adm (%u. ~ u:gfp F)"
 apply (unfold adm_def)
-apply (simp add: down_continuous_gfp)
+apply (simp add: inf_continuous_gfp)
 apply (fast dest!: is_ub_thelub)
 done
 

--- a/src/HOL/Library/Extended_Real.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Mon May 04 17:35:31 2015 +0200
@@ -8,16 +8,90 @@
 section {* Extended real number line *}
 
 theory Extended_Real
-imports Complex_Main Extended_Nat Liminf_Limsup
+imports Complex_Main Extended_Nat Liminf_Limsup Order_Continuity
 begin
 
 text {*
 
-This should be part of @{theory Extended_Nat}, but then the AFP-entry @{text "Jinja_Thread"} fails, as it does
-overload certain named from @{theory Complex_Main}.
+This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
+AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}.
 
 *}
 
+lemma continuous_at_left_imp_sup_continuous:
+  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  assumes "mono f" "\<And>x. continuous (at_left x) f"
+  shows "sup_continuous f"
+  unfolding sup_continuous_def
+proof safe
+  fix M :: "nat \<Rightarrow> 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))"
+    using continuous_at_Sup_mono[OF assms, of "range M"] by simp
+qed
+
+lemma sup_continuous_at_left:
+  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  assumes f: "sup_continuous f"
+  shows "continuous (at_left x) f"
+proof cases
+  assume "x = bot" then show ?thesis
+    by (simp add: trivial_limit_at_left_bot)
+next
+  assume x: "x \<noteq> bot" 
+  show ?thesis
+    unfolding continuous_within
+  proof (intro tendsto_at_left_sequentially[of bot])
+    fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x"
+    from S_x have x_eq: "x = (SUP i. S i)"
+      by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S)
+    show "(\<lambda>n. f (S n)) ----> f x"
+      unfolding x_eq sup_continuousD[OF f S]
+      using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def)
+  qed (insert x, auto simp: bot_less)
+qed
+
+lemma sup_continuous_iff_at_left:
+  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
+  using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
+    sup_continuous_mono[of f] by auto
+  
+lemma continuous_at_right_imp_inf_continuous:
+  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  assumes "mono f" "\<And>x. continuous (at_right x) f"
+  shows "inf_continuous f"
+  unfolding inf_continuous_def
+proof safe
+  fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
+    using continuous_at_Inf_mono[OF assms, of "range M"] by simp
+qed
+
+lemma inf_continuous_at_right:
+  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  assumes f: "inf_continuous f"
+  shows "continuous (at_right x) f"
+proof cases
+  assume "x = top" then show ?thesis
+    by (simp add: trivial_limit_at_right_top)
+next
+  assume x: "x \<noteq> top" 
+  show ?thesis
+    unfolding continuous_within
+  proof (intro tendsto_at_right_sequentially[of _ top])
+    fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x"
+    from S_x have x_eq: "x = (INF i. S i)"
+      by (rule LIMSEQ_unique) (intro LIMSEQ_INF S)
+    show "(\<lambda>n. f (S n)) ----> f x"
+      unfolding x_eq inf_continuousD[OF f S]
+      using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def)
+  qed (insert x, auto simp: less_top)
+qed
+
+lemma inf_continuous_iff_at_right:
+  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  shows "inf_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_right x) f) \<and> mono f"
+  using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f]
+    inf_continuous_mono[of f] by auto
+
 instantiation enat :: linorder_topology
 begin
 

--- a/src/HOL/Library/Order_Continuity.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Library/Order_Continuity.thy	Mon May 04 17:35:31 2015 +0200
@@ -28,32 +28,38 @@
   apply simp_all
   done
 
+text \<open>
+  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
+  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
+  and have the advantage that these names are duals.
+\<close>
+
 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)))"
+  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+  "sup_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 sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
+  by (auto simp: sup_continuous_def)
 
-lemma continuous_mono:
+lemma sup_continuous_mono:
   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
-  assumes [simp]: "continuous F" shows "mono F"
+  assumes [simp]: "sup_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)
+    by (auto simp: sup_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")
+lemma sup_continuous_lfp:
+  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
 proof (rule antisym)
-  note mono = continuous_mono[OF `continuous F`]
+  note mono = sup_continuous_mono[OF `sup_continuous F`]
   show "?U \<le> lfp F"
   proof (rule SUP_least)
     fix i show "(F ^^ i) bot \<le> lfp F"
@@ -77,36 +83,38 @@
         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)
+    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
+      using `sup_continuous F` by (simp add: sup_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)))"
+  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+  "inf_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 inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
+  by (auto simp: inf_continuous_def)
 
-lemma down_continuous_mono:
+lemma inf_continuous_mono:
   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
-  assumes [simp]: "down_continuous F" shows "mono F"
+  assumes [simp]: "inf_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)
+    by (auto simp: inf_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")
+lemma inf_continuous_gfp:
+  assumes "inf_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`]
+  note mono = inf_continuous_mono[OF `inf_continuous F`]
   show "gfp F \<le> ?U"
   proof (rule INF_greatest)
     fix i show "gfp F \<le> (F ^^ i) top"
@@ -133,7 +141,7 @@
     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` *)
+      by (simp add: inf_continuousD `inf_continuous F` *)
     finally show "?U \<le> F ?U" .
   qed
 qed

--- a/src/HOL/Probability/Borel_Space.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Mon May 04 17:35:31 2015 +0200
@@ -409,7 +409,7 @@
 
 lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
-  assumes "Order_Continuity.continuous F"
+  assumes "sup_continuous F"
   assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
   shows "lfp F \<in> borel_measurable M"
 proof -
@@ -420,13 +420,13 @@
   also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
     by auto
   also have "(SUP i. (F ^^ i) bot) = lfp F"
-    by (rule continuous_lfp[symmetric]) fact
+    by (rule sup_continuous_lfp[symmetric]) fact
   finally show ?thesis .
 qed
 
 lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
-  assumes "Order_Continuity.down_continuous F"
+  assumes "inf_continuous F"
   assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
   shows "gfp F \<in> borel_measurable M"
 proof -
@@ -437,7 +437,7 @@
   also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
     by auto
   also have "\<dots> = gfp F"
-    by (rule down_continuous_gfp[symmetric]) fact
+    by (rule inf_continuous_gfp[symmetric]) fact
   finally show ?thesis .
 qed
 

--- a/src/HOL/Probability/Measurable.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Probability/Measurable.thy	Mon May 04 17:35:31 2015 +0200
@@ -7,8 +7,6 @@
     "~~/src/HOL/Library/Order_Continuity"
 begin
 
-hide_const (open) Order_Continuity.continuous
-
 subsection {* Measurability prover *}
 
 lemma (in algebra) sets_Collect_finite_All:
@@ -425,7 +423,7 @@
 lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
   assumes "P M"
-  assumes F: "Order_Continuity.continuous F"
+  assumes F: "sup_continuous F"
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   shows "lfp F \<in> measurable M (count_space UNIV)"
 proof -
@@ -434,13 +432,13 @@
   then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
-    by (subst continuous_lfp) (auto intro: F)
+    by (subst sup_continuous_lfp) (auto intro: F)
   finally show ?thesis .
 qed
 
 lemma measurable_lfp:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
-  assumes F: "Order_Continuity.continuous F"
+  assumes F: "sup_continuous F"
   assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   shows "lfp F \<in> measurable M (count_space UNIV)"
   by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)
@@ -448,7 +446,7 @@
 lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
   assumes "P M"
-  assumes F: "Order_Continuity.down_continuous F"
+  assumes F: "inf_continuous F"
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   shows "gfp F \<in> measurable M (count_space UNIV)"
 proof -
@@ -457,13 +455,13 @@
   then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
-    by (subst down_continuous_gfp) (auto intro: F)
+    by (subst inf_continuous_gfp) (auto intro: F)
   finally show ?thesis .
 qed
 
 lemma measurable_gfp:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
-  assumes F: "Order_Continuity.down_continuous F"
+  assumes F: "inf_continuous F"
   assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   shows "gfp F \<in> measurable M (count_space UNIV)"
   by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)
@@ -471,7 +469,7 @@
 lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
   assumes "P M s"
-  assumes F: "Order_Continuity.continuous F"
+  assumes F: "sup_continuous F"
   assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
   shows "lfp F s \<in> measurable M (count_space UNIV)"
 proof -
@@ -480,14 +478,14 @@
   then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
-    by (subst continuous_lfp) (auto simp: F)
+    by (subst sup_continuous_lfp) (auto simp: F)
   finally show ?thesis .
 qed
 
 lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
   assumes "P M s"
-  assumes F: "Order_Continuity.down_continuous F"
+  assumes F: "inf_continuous F"
   assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
   shows "gfp F s \<in> measurable M (count_space UNIV)"
 proof -
@@ -496,7 +494,7 @@
   then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
-    by (subst down_continuous_gfp) (auto simp: F)
+    by (subst inf_continuous_gfp) (auto simp: F)
   finally show ?thesis .
 qed
 

--- a/src/HOL/Probability/Measure_Space.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Mon May 04 17:35:31 2015 +0200
@@ -550,12 +550,12 @@
 
 lemma emeasure_lfp[consumes 1, case_names cont measurable]:
   assumes "P M"
-  assumes cont: "Order_Continuity.continuous F"
+  assumes cont: "sup_continuous F"
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
   shows "emeasure M {x\<in>space M. lfp F x} = (SUP i. emeasure M {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
 proof -
   have "emeasure M {x\<in>space M. lfp F x} = emeasure M (\<Union>i. {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
-    using continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure])
+    using sup_continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure])
   moreover { fix i from `P M` have "{x\<in>space M. (F ^^ i) (\<lambda>x. False) x} \<in> sets M"
     by (induct i arbitrary: M) (auto simp add: pred_def[symmetric] intro: *) }
   moreover have "incseq (\<lambda>i. {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
@@ -565,7 +565,7 @@
     proof (induct i)
       case 0 show ?case by (simp add: le_fun_def)
     next
-      case Suc thus ?case using monoD[OF continuous_mono[OF cont] Suc] by auto
+      case Suc thus ?case using monoD[OF sup_continuous_mono[OF cont] Suc] by auto
     qed
     then show "{x \<in> space M. (F ^^ i) (\<lambda>x. False) x} \<subseteq> {x \<in> space M. (F ^^ Suc i) (\<lambda>x. False) x}"
       by auto
@@ -1227,7 +1227,7 @@
 
 lemma emeasure_lfp2[consumes 1, case_names cont f measurable]:
   assumes "P M"
-  assumes cont: "Order_Continuity.continuous F"
+  assumes cont: "sup_continuous F"
   assumes f: "\<And>M. P M \<Longrightarrow> f \<in> measurable M' M"
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
   shows "emeasure M' {x\<in>space M'. lfp F (f x)} = (SUP i. emeasure M' {x\<in>space M'. (F ^^ i) (\<lambda>x. False) (f x)})"

--- a/src/HOL/Probability/Stream_Space.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Mon May 04 17:35:31 2015 +0200
@@ -117,18 +117,18 @@
 lemma measurable_alw[measurable]:
   "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (alw P)"
   unfolding alw_def
-  by (coinduction rule: measurable_gfp_coinduct) (auto simp: Order_Continuity.down_continuous_def)
+  by (coinduction rule: measurable_gfp_coinduct) (auto simp: inf_continuous_def)
 
 lemma measurable_ev[measurable]:
   "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (ev P)"
   unfolding ev_def
-  by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
+  by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def)
 
 lemma measurable_until:
   assumes [measurable]: "Measurable.pred (stream_space M) \<phi>" "Measurable.pred (stream_space M) \<psi>"
   shows "Measurable.pred (stream_space M) (\<phi> until \<psi>)"
   unfolding UNTIL_def
-  by (coinduction rule: measurable_gfp_coinduct) (simp_all add: down_continuous_def fun_eq_iff)
+  by (coinduction rule: measurable_gfp_coinduct) (simp_all add: inf_continuous_def fun_eq_iff)
 
 lemma measurable_holds [measurable]: "Measurable.pred M P \<Longrightarrow> Measurable.pred (stream_space M) (holds P)"
   unfolding holds.simps[abs_def]
@@ -144,7 +144,7 @@
 lemma measurable_suntil[measurable]:
   assumes [measurable]: "Measurable.pred (stream_space M) Q" "Measurable.pred (stream_space M) P"
   shows "Measurable.pred (stream_space M) (Q suntil P)"
-  unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
+  unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def)
 
 lemma measurable_szip:
   "(\<lambda>(\<omega>1, \<omega>2). szip \<omega>1 \<omega>2) \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (stream_space (M \<Otimes>\<^sub>M N))"
@@ -263,7 +263,7 @@
   also have "\<dots> \<in> sets (stream_space M)"
     apply (intro predE)
     apply (coinduction rule: measurable_gfp_coinduct)
-    apply (auto simp: down_continuous_def)
+    apply (auto simp: inf_continuous_def)
     done
   finally show ?thesis .
 qed

--- a/src/HOL/Topological_Spaces.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon May 04 17:35:31 2015 +0200
@@ -1231,7 +1231,7 @@
   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
 
 lemma sequentially_imp_eventually_at_left:
-  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
+  fixes a :: "'a :: {linorder_topology, first_countable_topology}"
   assumes b[simp]: "b < a"
   assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
   shows "eventually P (at_left a)"
@@ -1261,7 +1261,7 @@
 qed
 
 lemma tendsto_at_left_sequentially:
-  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
+  fixes a :: "_ :: {linorder_topology, first_countable_topology}"
   assumes "b < a"
   assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
   shows "(X ---> L) (at_left a)"
@@ -1269,7 +1269,7 @@
   by (simp add: sequentially_imp_eventually_at_left)
 
 lemma sequentially_imp_eventually_at_right:
-  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
+  fixes a :: "'a :: {linorder_topology, first_countable_topology}"
   assumes b[simp]: "a < b"
   assumes *: "\<And>f. (\<And>n. a < f n) \<Longrightarrow> (\<And>n. f n < b) \<Longrightarrow> decseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
   shows "eventually P (at_right a)"
@@ -1299,7 +1299,7 @@
 qed
 
 lemma tendsto_at_right_sequentially:
-  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
+  fixes a :: "_ :: {linorder_topology, first_countable_topology}"
   assumes "a < b"
   assumes *: "\<And>S. (\<And>n. a < S n) \<Longrightarrow> (\<And>n. S n < b) \<Longrightarrow> decseq S \<Longrightarrow> S ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
   shows "(X ---> L) (at_right a)"