rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
authorhoelzl
Mon May 04 17:35:31 2015 +0200 (2015-05-04)
changeset 60172423273355b55
parent 60171 b3be7677461e
child 60173 6a61bb577d5b
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
src/HOL/Complete_Lattices.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Stream_Space.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
     1.3 @@ -556,6 +556,14 @@
     1.4    shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
     1.5    using `mono f` by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
     1.6  
     1.7 +lemma mono_INF:
     1.8 +  "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
     1.9 +  by (intro complete_lattice_class.INF_greatest monoD[OF `mono f`] INF_lower)
    1.10 +
    1.11 +lemma mono_SUP:
    1.12 +  "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
    1.13 +  by (intro complete_lattice_class.SUP_least monoD[OF `mono f`] SUP_upper)
    1.14 +
    1.15  end
    1.16  
    1.17  end
     2.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
     2.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
     2.3 @@ -452,6 +452,9 @@
     2.4  
     2.5  end
     2.6  
     2.7 +instance complete_linorder < conditionally_complete_linorder
     2.8 +  ..
     2.9 +
    2.10  lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
    2.11    using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
    2.12  
     3.1 --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon May 04 16:01:36 2015 +0200
     3.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon May 04 17:35:31 2015 +0200
     3.3 @@ -22,8 +22,8 @@
     3.4    (? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
     3.5  by (unfold BufAC_Asm_F_def, auto)
     3.6  
     3.7 -lemma cont_BufAC_Asm_F: "down_continuous BufAC_Asm_F"
     3.8 -by (auto simp add: down_continuous_def BufAC_Asm_F_def3)
     3.9 +lemma cont_BufAC_Asm_F: "inf_continuous BufAC_Asm_F"
    3.10 +by (auto simp add: inf_continuous_def BufAC_Asm_F_def3)
    3.11  
    3.12  lemma BufAC_Cmt_F_def3:
    3.13   "((s,t):BufAC_Cmt_F C) = (!d x.
    3.14 @@ -37,8 +37,8 @@
    3.15  apply (auto intro: surjectiv_scons [symmetric])
    3.16  done
    3.17  
    3.18 -lemma cont_BufAC_Cmt_F: "down_continuous BufAC_Cmt_F"
    3.19 -by (auto simp add: down_continuous_def BufAC_Cmt_F_def3)
    3.20 +lemma cont_BufAC_Cmt_F: "inf_continuous BufAC_Cmt_F"
    3.21 +by (auto simp add: inf_continuous_def BufAC_Cmt_F_def3)
    3.22  
    3.23  
    3.24  (**** adm_BufAC_Asm ***********************************************************)
    3.25 @@ -184,7 +184,7 @@
    3.26  
    3.27  lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>(BufAC_Cmt_F ^^ n) top)"
    3.28  apply (unfold BufAC_Cmt_def)
    3.29 -apply (subst cont_BufAC_Cmt_F [THEN down_continuous_gfp])
    3.30 +apply (subst cont_BufAC_Cmt_F [THEN inf_continuous_gfp])
    3.31  apply (fast)
    3.32  done
    3.33  
     4.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon May 04 16:01:36 2015 +0200
     4.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon May 04 17:35:31 2015 +0200
     4.3 @@ -121,8 +121,8 @@
     4.4  
     4.5  lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
     4.6   enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top;
     4.7 -    down_continuous F |] ==> adm (%x. x:gfp F)"
     4.8 -apply (erule down_continuous_gfp[of F, THEN ssubst])
     4.9 +    inf_continuous F |] ==> adm (%x. x:gfp F)"
    4.10 +apply (erule inf_continuous_gfp[of F, THEN ssubst])
    4.11  apply (simp (no_asm))
    4.12  apply (rule adm_lemmas)
    4.13  apply (rule flatstream_admI)
    4.14 @@ -170,10 +170,10 @@
    4.15  done
    4.16  
    4.17  lemma stream_antiP2_non_gfp_admI:
    4.18 -"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |] 
    4.19 +"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; inf_continuous F |] 
    4.20    ==> adm (%u. ~ u:gfp F)"
    4.21  apply (unfold adm_def)
    4.22 -apply (simp add: down_continuous_gfp)
    4.23 +apply (simp add: inf_continuous_gfp)
    4.24  apply (fast dest!: is_ub_thelub)
    4.25  done
    4.26  
     5.1 --- a/src/HOL/Library/Extended_Real.thy	Mon May 04 16:01:36 2015 +0200
     5.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon May 04 17:35:31 2015 +0200
     5.3 @@ -8,16 +8,90 @@
     5.4  section {* Extended real number line *}
     5.5  
     5.6  theory Extended_Real
     5.7 -imports Complex_Main Extended_Nat Liminf_Limsup
     5.8 +imports Complex_Main Extended_Nat Liminf_Limsup Order_Continuity
     5.9  begin
    5.10  
    5.11  text {*
    5.12  
    5.13 -This should be part of @{theory Extended_Nat}, but then the AFP-entry @{text "Jinja_Thread"} fails, as it does
    5.14 -overload certain named from @{theory Complex_Main}.
    5.15 +This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
    5.16 +AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}.
    5.17  
    5.18  *}
    5.19  
    5.20 +lemma continuous_at_left_imp_sup_continuous:
    5.21 +  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    5.22 +  assumes "mono f" "\<And>x. continuous (at_left x) f"
    5.23 +  shows "sup_continuous f"
    5.24 +  unfolding sup_continuous_def
    5.25 +proof safe
    5.26 +  fix M :: "nat \<Rightarrow> 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))"
    5.27 +    using continuous_at_Sup_mono[OF assms, of "range M"] by simp
    5.28 +qed
    5.29 +
    5.30 +lemma sup_continuous_at_left:
    5.31 +  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    5.32 +  assumes f: "sup_continuous f"
    5.33 +  shows "continuous (at_left x) f"
    5.34 +proof cases
    5.35 +  assume "x = bot" then show ?thesis
    5.36 +    by (simp add: trivial_limit_at_left_bot)
    5.37 +next
    5.38 +  assume x: "x \<noteq> bot" 
    5.39 +  show ?thesis
    5.40 +    unfolding continuous_within
    5.41 +  proof (intro tendsto_at_left_sequentially[of bot])
    5.42 +    fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x"
    5.43 +    from S_x have x_eq: "x = (SUP i. S i)"
    5.44 +      by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S)
    5.45 +    show "(\<lambda>n. f (S n)) ----> f x"
    5.46 +      unfolding x_eq sup_continuousD[OF f S]
    5.47 +      using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def)
    5.48 +  qed (insert x, auto simp: bot_less)
    5.49 +qed
    5.50 +
    5.51 +lemma sup_continuous_iff_at_left:
    5.52 +  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    5.53 +  shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
    5.54 +  using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
    5.55 +    sup_continuous_mono[of f] by auto
    5.56 +  
    5.57 +lemma continuous_at_right_imp_inf_continuous:
    5.58 +  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    5.59 +  assumes "mono f" "\<And>x. continuous (at_right x) f"
    5.60 +  shows "inf_continuous f"
    5.61 +  unfolding inf_continuous_def
    5.62 +proof safe
    5.63 +  fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
    5.64 +    using continuous_at_Inf_mono[OF assms, of "range M"] by simp
    5.65 +qed
    5.66 +
    5.67 +lemma inf_continuous_at_right:
    5.68 +  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    5.69 +  assumes f: "inf_continuous f"
    5.70 +  shows "continuous (at_right x) f"
    5.71 +proof cases
    5.72 +  assume "x = top" then show ?thesis
    5.73 +    by (simp add: trivial_limit_at_right_top)
    5.74 +next
    5.75 +  assume x: "x \<noteq> top" 
    5.76 +  show ?thesis
    5.77 +    unfolding continuous_within
    5.78 +  proof (intro tendsto_at_right_sequentially[of _ top])
    5.79 +    fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x"
    5.80 +    from S_x have x_eq: "x = (INF i. S i)"
    5.81 +      by (rule LIMSEQ_unique) (intro LIMSEQ_INF S)
    5.82 +    show "(\<lambda>n. f (S n)) ----> f x"
    5.83 +      unfolding x_eq inf_continuousD[OF f S]
    5.84 +      using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def)
    5.85 +  qed (insert x, auto simp: less_top)
    5.86 +qed
    5.87 +
    5.88 +lemma inf_continuous_iff_at_right:
    5.89 +  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    5.90 +  shows "inf_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_right x) f) \<and> mono f"
    5.91 +  using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f]
    5.92 +    inf_continuous_mono[of f] by auto
    5.93 +
    5.94  instantiation enat :: linorder_topology
    5.95  begin
    5.96  
     6.1 --- a/src/HOL/Library/Order_Continuity.thy	Mon May 04 16:01:36 2015 +0200
     6.2 +++ b/src/HOL/Library/Order_Continuity.thy	Mon May 04 17:35:31 2015 +0200
     6.3 @@ -28,32 +28,38 @@
     6.4    apply simp_all
     6.5    done
     6.6  
     6.7 +text \<open>
     6.8 +  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
     6.9 +  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
    6.10 +  and have the advantage that these names are duals.
    6.11 +\<close>
    6.12 +
    6.13  subsection {* Continuity for complete lattices *}
    6.14  
    6.15  definition
    6.16 -  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    6.17 -  "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    6.18 +  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    6.19 +  "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    6.20  
    6.21 -lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    6.22 -  by (auto simp: continuous_def)
    6.23 +lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    6.24 +  by (auto simp: sup_continuous_def)
    6.25  
    6.26 -lemma continuous_mono:
    6.27 +lemma sup_continuous_mono:
    6.28    fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    6.29 -  assumes [simp]: "continuous F" shows "mono F"
    6.30 +  assumes [simp]: "sup_continuous F" shows "mono F"
    6.31  proof
    6.32    fix A B :: "'a" assume [simp]: "A \<le> B"
    6.33    have "F B = F (SUP n::nat. if n = 0 then A else B)"
    6.34      by (simp add: sup_absorb2 SUP_nat_binary)
    6.35    also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    6.36 -    by (auto simp: continuousD mono_def intro!: SUP_cong)
    6.37 +    by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
    6.38    finally show "F A \<le> F B"
    6.39      by (simp add: SUP_nat_binary le_iff_sup)
    6.40  qed
    6.41  
    6.42 -lemma continuous_lfp:
    6.43 -  assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    6.44 +lemma sup_continuous_lfp:
    6.45 +  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    6.46  proof (rule antisym)
    6.47 -  note mono = continuous_mono[OF `continuous F`]
    6.48 +  note mono = sup_continuous_mono[OF `sup_continuous F`]
    6.49    show "?U \<le> lfp F"
    6.50    proof (rule SUP_least)
    6.51      fix i show "(F ^^ i) bot \<le> lfp F"
    6.52 @@ -77,36 +83,38 @@
    6.53          qed }
    6.54        thus ?thesis by (auto simp add: mono_iff_le_Suc)
    6.55      qed
    6.56 -    hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
    6.57 -    also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
    6.58 +    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
    6.59 +      using `sup_continuous F` by (simp add: sup_continuous_def)
    6.60 +    also have "\<dots> \<le> ?U"
    6.61 +      by (fast intro: SUP_least SUP_upper)
    6.62      finally show "F ?U \<le> ?U" .
    6.63    qed
    6.64  qed
    6.65  
    6.66  definition
    6.67 -  down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    6.68 -  "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    6.69 +  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    6.70 +  "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    6.71  
    6.72 -lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    6.73 -  by (auto simp: down_continuous_def)
    6.74 +lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    6.75 +  by (auto simp: inf_continuous_def)
    6.76  
    6.77 -lemma down_continuous_mono:
    6.78 +lemma inf_continuous_mono:
    6.79    fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    6.80 -  assumes [simp]: "down_continuous F" shows "mono F"
    6.81 +  assumes [simp]: "inf_continuous F" shows "mono F"
    6.82  proof
    6.83    fix A B :: "'a" assume [simp]: "A \<le> B"
    6.84    have "F A = F (INF n::nat. if n = 0 then B else A)"
    6.85      by (simp add: inf_absorb2 INF_nat_binary)
    6.86    also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
    6.87 -    by (auto simp: down_continuousD antimono_def intro!: INF_cong)
    6.88 +    by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
    6.89    finally show "F A \<le> F B"
    6.90      by (simp add: INF_nat_binary le_iff_inf inf_commute)
    6.91  qed
    6.92  
    6.93 -lemma down_continuous_gfp:
    6.94 -  assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
    6.95 +lemma inf_continuous_gfp:
    6.96 +  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
    6.97  proof (rule antisym)
    6.98 -  note mono = down_continuous_mono[OF `down_continuous F`]
    6.99 +  note mono = inf_continuous_mono[OF `inf_continuous F`]
   6.100    show "gfp F \<le> ?U"
   6.101    proof (rule INF_greatest)
   6.102      fix i show "gfp F \<le> (F ^^ i) top"
   6.103 @@ -133,7 +141,7 @@
   6.104      have "?U \<le> (INF i. (F ^^ Suc i) top)"
   6.105        by (fast intro: INF_greatest INF_lower)
   6.106      also have "\<dots> \<le> F ?U"
   6.107 -      by (simp add: down_continuousD `down_continuous F` *)
   6.108 +      by (simp add: inf_continuousD `inf_continuous F` *)
   6.109      finally show "?U \<le> F ?U" .
   6.110    qed
   6.111  qed
     7.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon May 04 16:01:36 2015 +0200
     7.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon May 04 17:35:31 2015 +0200
     7.3 @@ -409,7 +409,7 @@
     7.4  
     7.5  lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
     7.6    fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
     7.7 -  assumes "Order_Continuity.continuous F"
     7.8 +  assumes "sup_continuous F"
     7.9    assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
    7.10    shows "lfp F \<in> borel_measurable M"
    7.11  proof -
    7.12 @@ -420,13 +420,13 @@
    7.13    also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
    7.14      by auto
    7.15    also have "(SUP i. (F ^^ i) bot) = lfp F"
    7.16 -    by (rule continuous_lfp[symmetric]) fact
    7.17 +    by (rule sup_continuous_lfp[symmetric]) fact
    7.18    finally show ?thesis .
    7.19  qed
    7.20  
    7.21  lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
    7.22    fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
    7.23 -  assumes "Order_Continuity.down_continuous F"
    7.24 +  assumes "inf_continuous F"
    7.25    assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
    7.26    shows "gfp F \<in> borel_measurable M"
    7.27  proof -
    7.28 @@ -437,7 +437,7 @@
    7.29    also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
    7.30      by auto
    7.31    also have "\<dots> = gfp F"
    7.32 -    by (rule down_continuous_gfp[symmetric]) fact
    7.33 +    by (rule inf_continuous_gfp[symmetric]) fact
    7.34    finally show ?thesis .
    7.35  qed
    7.36  
     8.1 --- a/src/HOL/Probability/Measurable.thy	Mon May 04 16:01:36 2015 +0200
     8.2 +++ b/src/HOL/Probability/Measurable.thy	Mon May 04 17:35:31 2015 +0200
     8.3 @@ -7,8 +7,6 @@
     8.4      "~~/src/HOL/Library/Order_Continuity"
     8.5  begin
     8.6  
     8.7 -hide_const (open) Order_Continuity.continuous
     8.8 -
     8.9  subsection {* Measurability prover *}
    8.10  
    8.11  lemma (in algebra) sets_Collect_finite_All:
    8.12 @@ -425,7 +423,7 @@
    8.13  lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
    8.14    fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    8.15    assumes "P M"
    8.16 -  assumes F: "Order_Continuity.continuous F"
    8.17 +  assumes F: "sup_continuous F"
    8.18    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)"
    8.19    shows "lfp F \<in> measurable M (count_space UNIV)"
    8.20  proof -
    8.21 @@ -434,13 +432,13 @@
    8.22    then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
    8.23      by measurable
    8.24    also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
    8.25 -    by (subst continuous_lfp) (auto intro: F)
    8.26 +    by (subst sup_continuous_lfp) (auto intro: F)
    8.27    finally show ?thesis .
    8.28  qed
    8.29  
    8.30  lemma measurable_lfp:
    8.31    fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    8.32 -  assumes F: "Order_Continuity.continuous F"
    8.33 +  assumes F: "sup_continuous F"
    8.34    assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
    8.35    shows "lfp F \<in> measurable M (count_space UNIV)"
    8.36    by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)
    8.37 @@ -448,7 +446,7 @@
    8.38  lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
    8.39    fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    8.40    assumes "P M"
    8.41 -  assumes F: "Order_Continuity.down_continuous F"
    8.42 +  assumes F: "inf_continuous F"
    8.43    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)"
    8.44    shows "gfp F \<in> measurable M (count_space UNIV)"
    8.45  proof -
    8.46 @@ -457,13 +455,13 @@
    8.47    then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
    8.48      by measurable
    8.49    also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
    8.50 -    by (subst down_continuous_gfp) (auto intro: F)
    8.51 +    by (subst inf_continuous_gfp) (auto intro: F)
    8.52    finally show ?thesis .
    8.53  qed
    8.54  
    8.55  lemma measurable_gfp:
    8.56    fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    8.57 -  assumes F: "Order_Continuity.down_continuous F"
    8.58 +  assumes F: "inf_continuous F"
    8.59    assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
    8.60    shows "gfp F \<in> measurable M (count_space UNIV)"
    8.61    by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)
    8.62 @@ -471,7 +469,7 @@
    8.63  lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
    8.64    fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
    8.65    assumes "P M s"
    8.66 -  assumes F: "Order_Continuity.continuous F"
    8.67 +  assumes F: "sup_continuous F"
    8.68    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)"
    8.69    shows "lfp F s \<in> measurable M (count_space UNIV)"
    8.70  proof -
    8.71 @@ -480,14 +478,14 @@
    8.72    then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
    8.73      by measurable
    8.74    also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
    8.75 -    by (subst continuous_lfp) (auto simp: F)
    8.76 +    by (subst sup_continuous_lfp) (auto simp: F)
    8.77    finally show ?thesis .
    8.78  qed
    8.79  
    8.80  lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
    8.81    fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
    8.82    assumes "P M s"
    8.83 -  assumes F: "Order_Continuity.down_continuous F"
    8.84 +  assumes F: "inf_continuous F"
    8.85    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)"
    8.86    shows "gfp F s \<in> measurable M (count_space UNIV)"
    8.87  proof -
    8.88 @@ -496,7 +494,7 @@
    8.89    then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
    8.90      by measurable
    8.91    also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
    8.92 -    by (subst down_continuous_gfp) (auto simp: F)
    8.93 +    by (subst inf_continuous_gfp) (auto simp: F)
    8.94    finally show ?thesis .
    8.95  qed
    8.96  
     9.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon May 04 16:01:36 2015 +0200
     9.2 +++ b/src/HOL/Probability/Measure_Space.thy	Mon May 04 17:35:31 2015 +0200
     9.3 @@ -550,12 +550,12 @@
     9.4  
     9.5  lemma emeasure_lfp[consumes 1, case_names cont measurable]:
     9.6    assumes "P M"
     9.7 -  assumes cont: "Order_Continuity.continuous F"
     9.8 +  assumes cont: "sup_continuous F"
     9.9    assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
    9.10    shows "emeasure M {x\<in>space M. lfp F x} = (SUP i. emeasure M {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
    9.11  proof -
    9.12    have "emeasure M {x\<in>space M. lfp F x} = emeasure M (\<Union>i. {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
    9.13 -    using continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure])
    9.14 +    using sup_continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure])
    9.15    moreover { fix i from `P M` have "{x\<in>space M. (F ^^ i) (\<lambda>x. False) x} \<in> sets M"
    9.16      by (induct i arbitrary: M) (auto simp add: pred_def[symmetric] intro: *) }
    9.17    moreover have "incseq (\<lambda>i. {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
    9.18 @@ -565,7 +565,7 @@
    9.19      proof (induct i)
    9.20        case 0 show ?case by (simp add: le_fun_def)
    9.21      next
    9.22 -      case Suc thus ?case using monoD[OF continuous_mono[OF cont] Suc] by auto
    9.23 +      case Suc thus ?case using monoD[OF sup_continuous_mono[OF cont] Suc] by auto
    9.24      qed
    9.25      then show "{x \<in> space M. (F ^^ i) (\<lambda>x. False) x} \<subseteq> {x \<in> space M. (F ^^ Suc i) (\<lambda>x. False) x}"
    9.26        by auto
    9.27 @@ -1227,7 +1227,7 @@
    9.28  
    9.29  lemma emeasure_lfp2[consumes 1, case_names cont f measurable]:
    9.30    assumes "P M"
    9.31 -  assumes cont: "Order_Continuity.continuous F"
    9.32 +  assumes cont: "sup_continuous F"
    9.33    assumes f: "\<And>M. P M \<Longrightarrow> f \<in> measurable M' M"
    9.34    assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
    9.35    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)})"
    10.1 --- a/src/HOL/Probability/Stream_Space.thy	Mon May 04 16:01:36 2015 +0200
    10.2 +++ b/src/HOL/Probability/Stream_Space.thy	Mon May 04 17:35:31 2015 +0200
    10.3 @@ -117,18 +117,18 @@
    10.4  lemma measurable_alw[measurable]:
    10.5    "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (alw P)"
    10.6    unfolding alw_def
    10.7 -  by (coinduction rule: measurable_gfp_coinduct) (auto simp: Order_Continuity.down_continuous_def)
    10.8 +  by (coinduction rule: measurable_gfp_coinduct) (auto simp: inf_continuous_def)
    10.9  
   10.10  lemma measurable_ev[measurable]:
   10.11    "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (ev P)"
   10.12    unfolding ev_def
   10.13 -  by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
   10.14 +  by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def)
   10.15  
   10.16  lemma measurable_until:
   10.17    assumes [measurable]: "Measurable.pred (stream_space M) \<phi>" "Measurable.pred (stream_space M) \<psi>"
   10.18    shows "Measurable.pred (stream_space M) (\<phi> until \<psi>)"
   10.19    unfolding UNTIL_def
   10.20 -  by (coinduction rule: measurable_gfp_coinduct) (simp_all add: down_continuous_def fun_eq_iff)
   10.21 +  by (coinduction rule: measurable_gfp_coinduct) (simp_all add: inf_continuous_def fun_eq_iff)
   10.22  
   10.23  lemma measurable_holds [measurable]: "Measurable.pred M P \<Longrightarrow> Measurable.pred (stream_space M) (holds P)"
   10.24    unfolding holds.simps[abs_def]
   10.25 @@ -144,7 +144,7 @@
   10.26  lemma measurable_suntil[measurable]:
   10.27    assumes [measurable]: "Measurable.pred (stream_space M) Q" "Measurable.pred (stream_space M) P"
   10.28    shows "Measurable.pred (stream_space M) (Q suntil P)"
   10.29 -  unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
   10.30 +  unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def)
   10.31  
   10.32  lemma measurable_szip:
   10.33    "(\<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))"
   10.34 @@ -263,7 +263,7 @@
   10.35    also have "\<dots> \<in> sets (stream_space M)"
   10.36      apply (intro predE)
   10.37      apply (coinduction rule: measurable_gfp_coinduct)
   10.38 -    apply (auto simp: down_continuous_def)
   10.39 +    apply (auto simp: inf_continuous_def)
   10.40      done
   10.41    finally show ?thesis .
   10.42  qed
    11.1 --- a/src/HOL/Topological_Spaces.thy	Mon May 04 16:01:36 2015 +0200
    11.2 +++ b/src/HOL/Topological_Spaces.thy	Mon May 04 17:35:31 2015 +0200
    11.3 @@ -1231,7 +1231,7 @@
    11.4    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
    11.5  
    11.6  lemma sequentially_imp_eventually_at_left:
    11.7 -  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
    11.8 +  fixes a :: "'a :: {linorder_topology, first_countable_topology}"
    11.9    assumes b[simp]: "b < a"
   11.10    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"
   11.11    shows "eventually P (at_left a)"
   11.12 @@ -1261,7 +1261,7 @@
   11.13  qed
   11.14  
   11.15  lemma tendsto_at_left_sequentially:
   11.16 -  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
   11.17 +  fixes a :: "_ :: {linorder_topology, first_countable_topology}"
   11.18    assumes "b < a"
   11.19    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"
   11.20    shows "(X ---> L) (at_left a)"
   11.21 @@ -1269,7 +1269,7 @@
   11.22    by (simp add: sequentially_imp_eventually_at_left)
   11.23  
   11.24  lemma sequentially_imp_eventually_at_right:
   11.25 -  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
   11.26 +  fixes a :: "'a :: {linorder_topology, first_countable_topology}"
   11.27    assumes b[simp]: "a < b"
   11.28    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"
   11.29    shows "eventually P (at_right a)"
   11.30 @@ -1299,7 +1299,7 @@
   11.31  qed
   11.32  
   11.33  lemma tendsto_at_right_sequentially:
   11.34 -  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
   11.35 +  fixes a :: "_ :: {linorder_topology, first_countable_topology}"
   11.36    assumes "a < b"
   11.37    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"
   11.38    shows "(X ---> L) (at_right a)"