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
authorhoelzl
Mon Mar 10 20:04:40 2014 +0100 (2014-03-10)
changeset 56020f92479477c52
parent 56019 682bba24e474
child 56021 e0c9d76c2a6d
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
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Library.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon Mar 10 17:14:57 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon Mar 10 20:04:40 2014 +0100
     1.3 @@ -22,8 +22,8 @@
     1.4    (? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
     1.5  by (unfold BufAC_Asm_F_def, auto)
     1.6  
     1.7 -lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F"
     1.8 -by (auto simp add: down_cont_def BufAC_Asm_F_def3)
     1.9 +lemma cont_BufAC_Asm_F: "down_continuous BufAC_Asm_F"
    1.10 +by (auto simp add: down_continuous_def BufAC_Asm_F_def3)
    1.11  
    1.12  lemma BufAC_Cmt_F_def3:
    1.13   "((s,t):BufAC_Cmt_F C) = (!d x.
    1.14 @@ -37,8 +37,8 @@
    1.15  apply (auto intro: surjectiv_scons [symmetric])
    1.16  done
    1.17  
    1.18 -lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F"
    1.19 -by (auto simp add: down_cont_def BufAC_Cmt_F_def3)
    1.20 +lemma cont_BufAC_Cmt_F: "down_continuous BufAC_Cmt_F"
    1.21 +by (auto simp add: down_continuous_def BufAC_Cmt_F_def3)
    1.22  
    1.23  
    1.24  (**** adm_BufAC_Asm ***********************************************************)
    1.25 @@ -117,8 +117,8 @@
    1.26  
    1.27  (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
    1.28  lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x --> 
    1.29 -                     (x,f\<cdot>x):down_iterate BufAC_Cmt_F i --> 
    1.30 -                     (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
    1.31 +                     (x,f\<cdot>x):(BufAC_Cmt_F ^^ i) top --> 
    1.32 +                     (s,f\<cdot>s):(BufAC_Cmt_F ^^ i) top"
    1.33  apply (rule_tac x="%i. 2*i" in exI)
    1.34  apply (rule allI)
    1.35  apply (induct_tac "i")
    1.36 @@ -182,9 +182,9 @@
    1.37  apply assumption
    1.38  done
    1.39  
    1.40 -lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)"
    1.41 +lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>(BufAC_Cmt_F ^^ n) top)"
    1.42  apply (unfold BufAC_Cmt_def)
    1.43 -apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp])
    1.44 +apply (subst cont_BufAC_Cmt_F [THEN down_continuous_gfp])
    1.45  apply (fast)
    1.46  done
    1.47  
     2.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon Mar 10 17:14:57 2014 +0100
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Mon Mar 10 20:04:40 2014 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Admissibility for streams *}
     2.5  
     2.6  theory Stream_adm
     2.7 -imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity"
     2.8 +imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
     2.9  begin
    2.10  
    2.11  definition
    2.12 @@ -93,7 +93,7 @@
    2.13  
    2.14  lemma stream_monoP2I:
    2.15  "!!X. stream_monoP F ==> !i. ? l. !x y. 
    2.16 -  enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
    2.17 +  enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top"
    2.18  apply (unfold stream_monoP_def)
    2.19  apply (safe)
    2.20  apply (rule_tac x="i*ia" in exI)
    2.21 @@ -120,9 +120,9 @@
    2.22  done
    2.23  
    2.24  lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
    2.25 - enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
    2.26 -    down_cont F |] ==> adm (%x. x:gfp F)"
    2.27 -apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
    2.28 + enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top;
    2.29 +    down_continuous F |] ==> adm (%x. x:gfp F)"
    2.30 +apply (erule down_continuous_gfp[of F, THEN ssubst])
    2.31  apply (simp (no_asm))
    2.32  apply (rule adm_lemmas)
    2.33  apply (rule flatstream_admI)
    2.34 @@ -144,7 +144,7 @@
    2.35  
    2.36  lemma stream_antiP2I:
    2.37  "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]
    2.38 -  ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i"
    2.39 +  ==> !i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top"
    2.40  apply (unfold stream_antiP_def)
    2.41  apply (rule allI)
    2.42  apply (induct_tac "i")
    2.43 @@ -170,10 +170,10 @@
    2.44  done
    2.45  
    2.46  lemma stream_antiP2_non_gfp_admI:
    2.47 -"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] 
    2.48 +"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |] 
    2.49    ==> adm (%u. ~ u:gfp F)"
    2.50  apply (unfold adm_def)
    2.51 -apply (simp add: INTER_down_iterate_is_gfp)
    2.52 +apply (simp add: down_continuous_gfp)
    2.53  apply (fast dest!: is_ub_thelub)
    2.54  done
    2.55  
     3.1 --- a/src/HOL/Library/Continuity.thy	Mon Mar 10 17:14:57 2014 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,297 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Continuity.thy
     3.5 -    Author:     David von Oheimb, TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -header {* Continuity and iterations (of set transformers) *}
     3.9 -
    3.10 -theory Continuity
    3.11 -imports Main
    3.12 -begin
    3.13 -
    3.14 -subsection {* Continuity for complete lattices *}
    3.15 -
    3.16 -definition
    3.17 -  chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    3.18 -  "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
    3.19 -
    3.20 -definition
    3.21 -  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    3.22 -  "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    3.23 -
    3.24 -lemma SUP_nat_conv:
    3.25 -  fixes M :: "nat \<Rightarrow> 'a::complete_lattice"
    3.26 -  shows "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
    3.27 -apply(rule order_antisym)
    3.28 - apply(rule SUP_least)
    3.29 - apply(case_tac n)
    3.30 -  apply simp
    3.31 - apply (fast intro:SUP_upper le_supI2)
    3.32 -apply(simp)
    3.33 -apply (blast intro:SUP_least SUP_upper)
    3.34 -done
    3.35 -
    3.36 -lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    3.37 -  assumes "continuous F" shows "mono F"
    3.38 -proof
    3.39 -  fix A B :: "'a" assume "A <= B"
    3.40 -  let ?C = "%i::nat. if i=0 then A else B"
    3.41 -  have "chain ?C" using `A <= B` by(simp add:chain_def)
    3.42 -  have "F B = sup (F A) (F B)"
    3.43 -  proof -
    3.44 -    have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
    3.45 -    hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp
    3.46 -    also have "\<dots> = (SUP i. F(?C i))"
    3.47 -      using `chain ?C` `continuous F` by(simp add:continuous_def)
    3.48 -    also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp
    3.49 -    finally show ?thesis .
    3.50 -  qed
    3.51 -  thus "F A \<le> F B" by(subst le_iff_sup, simp)
    3.52 -qed
    3.53 -
    3.54 -lemma continuous_lfp:
    3.55 - assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)"
    3.56 -proof -
    3.57 -  note mono = continuous_mono[OF `continuous F`]
    3.58 -  { fix i have "(F ^^ i) bot \<le> lfp F"
    3.59 -    proof (induct i)
    3.60 -      show "(F ^^ 0) bot \<le> lfp F" by simp
    3.61 -    next
    3.62 -      case (Suc i)
    3.63 -      have "(F ^^ Suc i) bot = F((F ^^ i) bot)" by simp
    3.64 -      also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
    3.65 -      also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    3.66 -      finally show ?case .
    3.67 -    qed }
    3.68 -  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least)
    3.69 -  moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
    3.70 -  proof (rule lfp_lowerbound)
    3.71 -    have "chain(%i. (F ^^ i) bot)"
    3.72 -    proof -
    3.73 -      { fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
    3.74 -        proof (induct i)
    3.75 -          case 0 show ?case by simp
    3.76 -        next
    3.77 -          case Suc thus ?case using monoD[OF mono Suc] by auto
    3.78 -        qed }
    3.79 -      thus ?thesis by(auto simp add:chain_def)
    3.80 -    qed
    3.81 -    hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    3.82 -    also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper)
    3.83 -    finally show "F ?U \<le> ?U" .
    3.84 -  qed
    3.85 -  ultimately show ?thesis by (blast intro:order_antisym)
    3.86 -qed
    3.87 -
    3.88 -text{* The following development is just for sets but presents an up
    3.89 -and a down version of chains and continuity and covers @{const gfp}. *}
    3.90 -
    3.91 -
    3.92 -subsection "Chains"
    3.93 -
    3.94 -definition
    3.95 -  up_chain :: "(nat => 'a set) => bool" where
    3.96 -  "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
    3.97 -
    3.98 -lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
    3.99 -  by (simp add: up_chain_def)
   3.100 -
   3.101 -lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
   3.102 -  by (simp add: up_chain_def)
   3.103 -
   3.104 -lemma up_chain_less_mono:
   3.105 -    "up_chain F ==> x < y ==> F x \<subseteq> F y"
   3.106 -  apply (induct y)
   3.107 -   apply (blast dest: up_chainD elim: less_SucE)+
   3.108 -  done
   3.109 -
   3.110 -lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
   3.111 -  apply (drule le_imp_less_or_eq)
   3.112 -  apply (blast dest: up_chain_less_mono)
   3.113 -  done
   3.114 -
   3.115 -
   3.116 -definition
   3.117 -  down_chain :: "(nat => 'a set) => bool" where
   3.118 -  "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
   3.119 -
   3.120 -lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
   3.121 -  by (simp add: down_chain_def)
   3.122 -
   3.123 -lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
   3.124 -  by (simp add: down_chain_def)
   3.125 -
   3.126 -lemma down_chain_less_mono:
   3.127 -    "down_chain F ==> x < y ==> F y \<subseteq> F x"
   3.128 -  apply (induct y)
   3.129 -   apply (blast dest: down_chainD elim: less_SucE)+
   3.130 -  done
   3.131 -
   3.132 -lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
   3.133 -  apply (drule le_imp_less_or_eq)
   3.134 -  apply (blast dest: down_chain_less_mono)
   3.135 -  done
   3.136 -
   3.137 -
   3.138 -subsection "Continuity"
   3.139 -
   3.140 -definition
   3.141 -  up_cont :: "('a set => 'a set) => bool" where
   3.142 -  "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
   3.143 -
   3.144 -lemma up_contI:
   3.145 -  "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
   3.146 -apply (unfold up_cont_def)
   3.147 -apply blast
   3.148 -done
   3.149 -
   3.150 -lemma up_contD:
   3.151 -  "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
   3.152 -apply (unfold up_cont_def)
   3.153 -apply auto
   3.154 -done
   3.155 -
   3.156 -
   3.157 -lemma up_cont_mono: "up_cont f ==> mono f"
   3.158 -apply (rule monoI)
   3.159 -apply (drule_tac F = "\<lambda>i. if i = 0 then x else y" in up_contD)
   3.160 - apply (rule up_chainI)
   3.161 - apply simp
   3.162 -apply (drule Un_absorb1)
   3.163 -apply (auto split:split_if_asm)
   3.164 -done
   3.165 -
   3.166 -
   3.167 -definition
   3.168 -  down_cont :: "('a set => 'a set) => bool" where
   3.169 -  "down_cont f =
   3.170 -    (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
   3.171 -
   3.172 -lemma down_contI:
   3.173 -  "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
   3.174 -    down_cont f"
   3.175 -  apply (unfold down_cont_def)
   3.176 -  apply blast
   3.177 -  done
   3.178 -
   3.179 -lemma down_contD: "down_cont f ==> down_chain F ==>
   3.180 -    f (Inter (range F)) = Inter (f ` range F)"
   3.181 -  apply (unfold down_cont_def)
   3.182 -  apply auto
   3.183 -  done
   3.184 -
   3.185 -lemma down_cont_mono: "down_cont f ==> mono f"
   3.186 -apply (rule monoI)
   3.187 -apply (drule_tac F = "\<lambda>i. if i = 0 then y else x" in down_contD)
   3.188 - apply (rule down_chainI)
   3.189 - apply simp
   3.190 -apply (drule Int_absorb1)
   3.191 -apply (auto split:split_if_asm)
   3.192 -done
   3.193 -
   3.194 -
   3.195 -subsection "Iteration"
   3.196 -
   3.197 -definition
   3.198 -  up_iterate :: "('a set => 'a set) => nat => 'a set" where
   3.199 -  "up_iterate f n = (f ^^ n) {}"
   3.200 -
   3.201 -lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   3.202 -  by (simp add: up_iterate_def)
   3.203 -
   3.204 -lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
   3.205 -  by (simp add: up_iterate_def)
   3.206 -
   3.207 -lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
   3.208 -  apply (rule up_chainI)
   3.209 -  apply (induct_tac i)
   3.210 -   apply simp+
   3.211 -  apply (erule (1) monoD)
   3.212 -  done
   3.213 -
   3.214 -lemma UNION_up_iterate_is_fp:
   3.215 -  "up_cont F ==>
   3.216 -    F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   3.217 -  apply (frule up_cont_mono [THEN up_iterate_chain])
   3.218 -  apply (drule (1) up_contD)
   3.219 -  apply simp
   3.220 -  apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   3.221 -  apply (case_tac xa)
   3.222 -   apply auto
   3.223 -  done
   3.224 -
   3.225 -lemma UNION_up_iterate_lowerbound:
   3.226 -    "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
   3.227 -  apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
   3.228 -   apply fast
   3.229 -  apply (induct_tac i)
   3.230 -  prefer 2 apply (drule (1) monoD)
   3.231 -   apply auto
   3.232 -  done
   3.233 -
   3.234 -lemma UNION_up_iterate_is_lfp:
   3.235 -    "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   3.236 -  apply (rule set_eq_subset [THEN iffD2])
   3.237 -  apply (rule conjI)
   3.238 -   prefer 2
   3.239 -   apply (drule up_cont_mono)
   3.240 -   apply (rule UNION_up_iterate_lowerbound)
   3.241 -    apply assumption
   3.242 -   apply (erule lfp_unfold [symmetric])
   3.243 -  apply (rule lfp_lowerbound)
   3.244 -  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   3.245 -  apply (erule UNION_up_iterate_is_fp [symmetric])
   3.246 -  done
   3.247 -
   3.248 -
   3.249 -definition
   3.250 -  down_iterate :: "('a set => 'a set) => nat => 'a set" where
   3.251 -  "down_iterate f n = (f ^^ n) UNIV"
   3.252 -
   3.253 -lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   3.254 -  by (simp add: down_iterate_def)
   3.255 -
   3.256 -lemma down_iterate_Suc [simp]:
   3.257 -    "down_iterate f (Suc i) = f (down_iterate f i)"
   3.258 -  by (simp add: down_iterate_def)
   3.259 -
   3.260 -lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
   3.261 -  apply (rule down_chainI)
   3.262 -  apply (induct_tac i)
   3.263 -   apply simp+
   3.264 -  apply (erule (1) monoD)
   3.265 -  done
   3.266 -
   3.267 -lemma INTER_down_iterate_is_fp:
   3.268 -  "down_cont F ==>
   3.269 -    F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   3.270 -  apply (frule down_cont_mono [THEN down_iterate_chain])
   3.271 -  apply (drule (1) down_contD)
   3.272 -  apply simp
   3.273 -  apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   3.274 -  apply (case_tac xa)
   3.275 -   apply auto
   3.276 -  done
   3.277 -
   3.278 -lemma INTER_down_iterate_upperbound:
   3.279 -    "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
   3.280 -  apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
   3.281 -   apply fast
   3.282 -  apply (induct_tac i)
   3.283 -  prefer 2 apply (drule (1) monoD)
   3.284 -   apply auto
   3.285 -  done
   3.286 -
   3.287 -lemma INTER_down_iterate_is_gfp:
   3.288 -    "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   3.289 -  apply (rule set_eq_subset [THEN iffD2])
   3.290 -  apply (rule conjI)
   3.291 -   apply (drule down_cont_mono)
   3.292 -   apply (rule INTER_down_iterate_upperbound)
   3.293 -    apply assumption
   3.294 -   apply (erule gfp_unfold [symmetric])
   3.295 -  apply (rule gfp_upperbound)
   3.296 -  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   3.297 -  apply (erule INTER_down_iterate_is_fp)
   3.298 -  done
   3.299 -
   3.300 -end
     4.1 --- a/src/HOL/Library/Library.thy	Mon Mar 10 17:14:57 2014 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Mon Mar 10 20:04:40 2014 +0100
     4.3 @@ -7,7 +7,6 @@
     4.4    BNF_Decl
     4.5    Boolean_Algebra
     4.6    Char_ord
     4.7 -  Continuity
     4.8    ContNotDenum
     4.9    Convex
    4.10    Countable
    4.11 @@ -41,6 +40,7 @@
    4.12    Numeral_Type
    4.13    OptionalSugar
    4.14    Option_ord
    4.15 +  Order_Continuity
    4.16    Parallel
    4.17    Permutation
    4.18    Permutations
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Order_Continuity.thy	Mon Mar 10 20:04:40 2014 +0100
     5.3 @@ -0,0 +1,141 @@
     5.4 +(*  Title:      HOL/Library/Order_Continuity.thy
     5.5 +    Author:     David von Oheimb, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* Continuity and iterations (of set transformers) *}
     5.9 +
    5.10 +theory Order_Continuity
    5.11 +imports Main
    5.12 +begin
    5.13 +
    5.14 +(* TODO: Generalize theory to chain-complete partial orders *)
    5.15 +
    5.16 +lemma SUP_nat_binary:
    5.17 +  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
    5.18 +  apply (auto intro!: antisym SUP_least)
    5.19 +  apply (rule SUP_upper2[where i=0])
    5.20 +  apply simp_all
    5.21 +  apply (rule SUP_upper2[where i=1])
    5.22 +  apply simp_all
    5.23 +  done
    5.24 +
    5.25 +lemma INF_nat_binary:
    5.26 +  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
    5.27 +  apply (auto intro!: antisym INF_greatest)
    5.28 +  apply (rule INF_lower2[where i=0])
    5.29 +  apply simp_all
    5.30 +  apply (rule INF_lower2[where i=1])
    5.31 +  apply simp_all
    5.32 +  done
    5.33 +
    5.34 +subsection {* Continuity for complete lattices *}
    5.35 +
    5.36 +definition
    5.37 +  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    5.38 +  "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    5.39 +
    5.40 +lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    5.41 +  by (auto simp: continuous_def)
    5.42 +
    5.43 +lemma continuous_mono:
    5.44 +  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    5.45 +  assumes [simp]: "continuous F" shows "mono F"
    5.46 +proof
    5.47 +  fix A B :: "'a" assume [simp]: "A \<le> B"
    5.48 +  have "F B = F (SUP n::nat. if n = 0 then A else B)"
    5.49 +    by (simp add: sup_absorb2 SUP_nat_binary)
    5.50 +  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    5.51 +    by (auto simp: continuousD mono_def intro!: SUP_cong)
    5.52 +  finally show "F A \<le> F B"
    5.53 +    by (simp add: SUP_nat_binary le_iff_sup)
    5.54 +qed
    5.55 +
    5.56 +lemma continuous_lfp:
    5.57 +  assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    5.58 +proof (rule antisym)
    5.59 +  note mono = continuous_mono[OF `continuous F`]
    5.60 +  show "?U \<le> lfp F"
    5.61 +  proof (rule SUP_least)
    5.62 +    fix i show "(F ^^ i) bot \<le> lfp F"
    5.63 +    proof (induct i)
    5.64 +      case (Suc i)
    5.65 +      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
    5.66 +      also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
    5.67 +      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
    5.68 +      finally show ?case .
    5.69 +    qed simp
    5.70 +  qed
    5.71 +  show "lfp F \<le> ?U"
    5.72 +  proof (rule lfp_lowerbound)
    5.73 +    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
    5.74 +    proof -
    5.75 +      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
    5.76 +        proof (induct i)
    5.77 +          case 0 show ?case by simp
    5.78 +        next
    5.79 +          case Suc thus ?case using monoD[OF mono Suc] by auto
    5.80 +        qed }
    5.81 +      thus ?thesis by (auto simp add: mono_iff_le_Suc)
    5.82 +    qed
    5.83 +    hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
    5.84 +    also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
    5.85 +    finally show "F ?U \<le> ?U" .
    5.86 +  qed
    5.87 +qed
    5.88 +
    5.89 +definition
    5.90 +  down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    5.91 +  "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    5.92 +
    5.93 +lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    5.94 +  by (auto simp: down_continuous_def)
    5.95 +
    5.96 +lemma down_continuous_mono:
    5.97 +  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    5.98 +  assumes [simp]: "down_continuous F" shows "mono F"
    5.99 +proof
   5.100 +  fix A B :: "'a" assume [simp]: "A \<le> B"
   5.101 +  have "F A = F (INF n::nat. if n = 0 then B else A)"
   5.102 +    by (simp add: inf_absorb2 INF_nat_binary)
   5.103 +  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
   5.104 +    by (auto simp: down_continuousD antimono_def intro!: INF_cong)
   5.105 +  finally show "F A \<le> F B"
   5.106 +    by (simp add: INF_nat_binary le_iff_inf inf_commute)
   5.107 +qed
   5.108 +
   5.109 +lemma down_continuous_gfp:
   5.110 +  assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
   5.111 +proof (rule antisym)
   5.112 +  note mono = down_continuous_mono[OF `down_continuous F`]
   5.113 +  show "gfp F \<le> ?U"
   5.114 +  proof (rule INF_greatest)
   5.115 +    fix i show "gfp F \<le> (F ^^ i) top"
   5.116 +    proof (induct i)
   5.117 +      case (Suc i)
   5.118 +      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
   5.119 +      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
   5.120 +      also have "\<dots> = (F ^^ Suc i) top" by simp
   5.121 +      finally show ?case .
   5.122 +    qed simp
   5.123 +  qed
   5.124 +  show "?U \<le> gfp F"
   5.125 +  proof (rule gfp_upperbound)
   5.126 +    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
   5.127 +    proof -
   5.128 +      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
   5.129 +        proof (induct i)
   5.130 +          case 0 show ?case by simp
   5.131 +        next
   5.132 +          case Suc thus ?case using monoD[OF mono Suc] by auto
   5.133 +        qed }
   5.134 +      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
   5.135 +    qed
   5.136 +    have "?U \<le> (INF i. (F ^^ Suc i) top)"
   5.137 +      by (fast intro: INF_greatest INF_lower)
   5.138 +    also have "\<dots> \<le> F ?U"
   5.139 +      by (simp add: down_continuousD `down_continuous F` *)
   5.140 +    finally show "?U \<le> F ?U" .
   5.141 +  qed
   5.142 +qed
   5.143 +
   5.144 +end
     6.1 --- a/src/HOL/Nat.thy	Mon Mar 10 17:14:57 2014 +0100
     6.2 +++ b/src/HOL/Nat.thy	Mon Mar 10 20:04:40 2014 +0100
     6.3 @@ -1618,6 +1618,15 @@
     6.4      by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
     6.5  qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
     6.6  
     6.7 +lemma lift_Suc_antimono_le:
     6.8 +  assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
     6.9 +  shows "f n \<ge> f n'"
    6.10 +proof (cases "n < n'")
    6.11 +  case True
    6.12 +  then show ?thesis
    6.13 +    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    6.14 +qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
    6.15 +
    6.16  lemma lift_Suc_mono_less:
    6.17    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
    6.18    shows "f n < f n'"
    6.19 @@ -1635,6 +1644,10 @@
    6.20    "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
    6.21    unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
    6.22  
    6.23 +lemma antimono_iff_le_Suc:
    6.24 +  "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
    6.25 +  unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
    6.26 +
    6.27  lemma mono_nat_linear_lb:
    6.28    fixes f :: "nat \<Rightarrow> nat"
    6.29    assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
     7.1 --- a/src/HOL/Orderings.thy	Mon Mar 10 17:14:57 2014 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Mon Mar 10 20:04:40 2014 +0100
     7.3 @@ -1010,6 +1010,28 @@
     7.4    from assms show "f x \<le> f y" by (simp add: mono_def)
     7.5  qed
     7.6  
     7.7 +definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
     7.8 +  "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
     7.9 +
    7.10 +lemma antimonoI [intro?]:
    7.11 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    7.12 +  shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
    7.13 +  unfolding antimono_def by iprover
    7.14 +
    7.15 +lemma antimonoD [dest?]:
    7.16 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    7.17 +  shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
    7.18 +  unfolding antimono_def by iprover
    7.19 +
    7.20 +lemma antimonoE:
    7.21 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    7.22 +  assumes "antimono f"
    7.23 +  assumes "x \<le> y"
    7.24 +  obtains "f x \<ge> f y"
    7.25 +proof
    7.26 +  from assms show "f x \<ge> f y" by (simp add: antimono_def)
    7.27 +qed
    7.28 +
    7.29  definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    7.30    "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
    7.31  
     8.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 10 17:14:57 2014 +0100
     8.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 10 20:04:40 2014 +0100
     8.3 @@ -678,7 +678,7 @@
     8.4        by (auto simp: incseq_Suc_iff le_fun_def image_iff u' intro!: real_of_ereal_positive_mono)
     8.5      show "\<And>x. (\<lambda>k. u' k x) ----> f' x"
     8.6        using SUP_eq u(2)
     8.7 -      by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_mono incseq_Suc_iff le_fun_def)
     8.8 +      by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_Suc_iff le_fun_def)
     8.9      show "bounded {integral UNIV (u' k)|k. True}"
    8.10      proof (safe intro!: bounded_realI)
    8.11        fix k
     9.1 --- a/src/HOL/Topological_Spaces.thy	Mon Mar 10 17:14:57 2014 +0100
     9.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Mar 10 20:04:40 2014 +0100
     9.3 @@ -1193,26 +1193,25 @@
     9.4          The use of disjunction here complicates proofs considerably.
     9.5          One alternative is to add a Boolean argument to indicate the direction.
     9.6          Another is to develop the notions of increasing and decreasing first.*}
     9.7 -  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
     9.8 -
     9.9 -definition
    9.10 -  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    9.11 -    --{*Increasing sequence*}
    9.12 -  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
    9.13 -
    9.14 -definition
    9.15 -  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    9.16 -    --{*Decreasing sequence*}
    9.17 -  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
    9.18 +  "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))"
    9.19 +
    9.20 +abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    9.21 +  "incseq X \<equiv> mono X"
    9.22 +
    9.23 +lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)"
    9.24 +  unfolding mono_def ..
    9.25 +
    9.26 +abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    9.27 +  "decseq X \<equiv> antimono X"
    9.28 +
    9.29 +lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
    9.30 +  unfolding antimono_def ..
    9.31  
    9.32  definition
    9.33    subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
    9.34      --{*Definition of subsequence*}
    9.35    "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
    9.36  
    9.37 -lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
    9.38 -  unfolding mono_def incseq_def by auto
    9.39 -
    9.40  lemma incseq_SucI:
    9.41    "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
    9.42    using lift_Suc_mono_le[of X]