src/HOL/Library/Continuity.thy
changeset 11355 778c369559d9
parent 11351 c5c403d30c77
child 11461 ffeac9aa1967
     1.1 --- a/src/HOL/Library/Continuity.thy	Thu May 31 18:28:23 2001 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Thu May 31 20:52:51 2001 +0200
     1.3 @@ -1,219 +1,222 @@
     1.4  (*  Title:      HOL/Library/Continuity.thy
     1.5 -    ID:         $$
     1.6 -    Author: 	David von Oheimb, TU Muenchen
     1.7 +    ID:         $Id$
     1.8 +    Author:     David von Oheimb, TU Muenchen
     1.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10 -
    1.11  *)
    1.12  
    1.13  header {*
    1.14 -  \title{Continuity and interations (of set transformers)}
    1.15 +  \title{Continuity and iterations (of set transformers)}
    1.16    \author{David von Oheimb}
    1.17  *}
    1.18  
    1.19 -theory Continuity = Relation_Power:
    1.20 -
    1.21 +theory Continuity = Main:
    1.22  
    1.23  subsection "Chains"
    1.24  
    1.25  constdefs
    1.26 -  up_chain      :: "(nat => 'a set) => bool"
    1.27 - "up_chain F      == !i. F i <= F (Suc i)"
    1.28 +  up_chain :: "(nat => 'a set) => bool"
    1.29 +  "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
    1.30  
    1.31 -lemma up_chainI: "(!!i. F i <= F (Suc i)) ==> up_chain F"
    1.32 -by (simp add: up_chain_def);
    1.33 +lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
    1.34 +  by (simp add: up_chain_def)
    1.35  
    1.36 -lemma up_chainD: "up_chain F ==> F i <= F (Suc i)"
    1.37 -by (simp add: up_chain_def);
    1.38 +lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
    1.39 +  by (simp add: up_chain_def)
    1.40  
    1.41 -lemma up_chain_less_mono [rule_format]: "up_chain F ==> x < y --> F x <= F y"
    1.42 -apply (induct_tac y)
    1.43 -apply (blast dest: up_chainD elim: less_SucE)+
    1.44 -done
    1.45 +lemma up_chain_less_mono [rule_format]:
    1.46 +    "up_chain F ==> x < y --> F x \<subseteq> F y"
    1.47 +  apply (induct_tac y)
    1.48 +  apply (blast dest: up_chainD elim: less_SucE)+
    1.49 +  done
    1.50  
    1.51 -lemma up_chain_mono: "up_chain F ==> x <= y ==> F x <= F y"
    1.52 -apply (drule le_imp_less_or_eq)
    1.53 -apply (blast dest: up_chain_less_mono)
    1.54 -done
    1.55 +lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
    1.56 +  apply (drule le_imp_less_or_eq)
    1.57 +  apply (blast dest: up_chain_less_mono)
    1.58 +  done
    1.59  
    1.60  
    1.61  constdefs
    1.62 -  down_chain      :: "(nat => 'a set) => bool"
    1.63 - "down_chain F == !i. F (Suc i) <= F i"
    1.64 +  down_chain :: "(nat => 'a set) => bool"
    1.65 +  "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
    1.66  
    1.67 -lemma down_chainI: "(!!i. F (Suc i) <= F i) ==> down_chain F"
    1.68 -by (simp add: down_chain_def);
    1.69 +lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
    1.70 +  by (simp add: down_chain_def)
    1.71  
    1.72 -lemma down_chainD: "down_chain F ==> F (Suc i) <= F i"
    1.73 -by (simp add: down_chain_def);
    1.74 +lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
    1.75 +  by (simp add: down_chain_def)
    1.76  
    1.77 -lemma down_chain_less_mono[rule_format]: "down_chain F ==> x < y --> F y <= F x"
    1.78 -apply (induct_tac y)
    1.79 -apply (blast dest: down_chainD elim: less_SucE)+
    1.80 -done
    1.81 +lemma down_chain_less_mono [rule_format]:
    1.82 +    "down_chain F ==> x < y --> F y \<subseteq> F x"
    1.83 +  apply (induct_tac y)
    1.84 +  apply (blast dest: down_chainD elim: less_SucE)+
    1.85 +  done
    1.86  
    1.87 -lemma down_chain_mono: "down_chain F ==> x <= y ==> F y <= F x"
    1.88 -apply (drule le_imp_less_or_eq)
    1.89 -apply (blast dest: down_chain_less_mono)
    1.90 -done
    1.91 +lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
    1.92 +  apply (drule le_imp_less_or_eq)
    1.93 +  apply (blast dest: down_chain_less_mono)
    1.94 +  done
    1.95  
    1.96  
    1.97  subsection "Continuity"
    1.98  
    1.99  constdefs
   1.100    up_cont :: "('a set => 'a set) => bool"
   1.101 - "up_cont f == !F. up_chain F --> f (Union (range F)) = Union (f`(range F))"
   1.102 +  "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
   1.103  
   1.104 -lemma up_contI: 
   1.105 - "(!!F. up_chain F ==> f (Union (range F)) = Union (f`(range F))) ==> up_cont f"
   1.106 -apply (unfold up_cont_def)
   1.107 -by blast
   1.108 +lemma up_contI:
   1.109 +    "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
   1.110 +  apply (unfold up_cont_def)
   1.111 +  apply blast
   1.112 +  done
   1.113  
   1.114 -lemma up_contD: 
   1.115 -  "[| up_cont f; up_chain F |] ==> f (Union (range F)) = Union (f`(range F))"
   1.116 -apply (unfold up_cont_def)
   1.117 -by auto
   1.118 +lemma up_contD:
   1.119 +    "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
   1.120 +  apply (unfold up_cont_def)
   1.121 +  apply auto
   1.122 +  done
   1.123  
   1.124  
   1.125  lemma up_cont_mono: "up_cont f ==> mono f"
   1.126 -apply (rule monoI)
   1.127 -apply (drule_tac F = "%i. if i = 0 then A else B" in up_contD)
   1.128 -apply  (rule up_chainI)
   1.129 -apply  simp+
   1.130 -apply (drule Un_absorb1)
   1.131 -apply auto
   1.132 -done
   1.133 +  apply (rule monoI)
   1.134 +  apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
   1.135 +   apply (rule up_chainI)
   1.136 +   apply  simp+
   1.137 +  apply (drule Un_absorb1)
   1.138 +  apply auto
   1.139 +  done
   1.140  
   1.141  
   1.142  constdefs
   1.143    down_cont :: "('a set => 'a set) => bool"
   1.144 - "down_cont f == !F. down_chain F --> f (Inter (range F)) = Inter (f`(range F))"
   1.145 +  "down_cont f ==
   1.146 +    \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
   1.147  
   1.148 -lemma down_contI: 
   1.149 - "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f`(range F))) ==> 
   1.150 -  down_cont f"
   1.151 -apply (unfold down_cont_def)
   1.152 -by blast
   1.153 +lemma down_contI:
   1.154 +  "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
   1.155 +    down_cont f"
   1.156 +  apply (unfold down_cont_def)
   1.157 +  apply blast
   1.158 +  done
   1.159  
   1.160 -lemma down_contD: "[| down_cont f; down_chain F |] ==> 
   1.161 -  f (Inter (range F)) = Inter (f`(range F))"
   1.162 -apply (unfold down_cont_def)
   1.163 -by auto
   1.164 +lemma down_contD: "down_cont f ==> down_chain F ==>
   1.165 +    f (Inter (range F)) = Inter (f ` range F)"
   1.166 +  apply (unfold down_cont_def)
   1.167 +  apply auto
   1.168 +  done
   1.169  
   1.170  lemma down_cont_mono: "down_cont f ==> mono f"
   1.171 -apply (rule monoI)
   1.172 -apply (drule_tac F = "%i. if i = 0 then B else A" in down_contD)
   1.173 -apply  (rule down_chainI)
   1.174 -apply  simp+
   1.175 -apply (drule Int_absorb1)
   1.176 -apply auto
   1.177 -done
   1.178 +  apply (rule monoI)
   1.179 +  apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
   1.180 +   apply (rule down_chainI)
   1.181 +   apply simp+
   1.182 +  apply (drule Int_absorb1)
   1.183 +  apply auto
   1.184 +  done
   1.185  
   1.186  
   1.187  subsection "Iteration"
   1.188  
   1.189  constdefs
   1.190 -
   1.191    up_iterate :: "('a set => 'a set) => nat => 'a set"
   1.192 - "up_iterate f n == (f^n) {}"
   1.193 +  "up_iterate f n == (f^n) {}"
   1.194  
   1.195  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   1.196 -by (simp add: up_iterate_def)
   1.197 +  by (simp add: up_iterate_def)
   1.198  
   1.199 -lemma up_iterate_Suc [simp]: 
   1.200 -  "up_iterate f (Suc i) = f (up_iterate f i)"
   1.201 -by (simp add: up_iterate_def)
   1.202 +lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
   1.203 +  by (simp add: up_iterate_def)
   1.204  
   1.205  lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
   1.206 -apply (rule up_chainI)
   1.207 -apply (induct_tac i)
   1.208 -apply simp+
   1.209 -apply (erule (1) monoD)
   1.210 -done
   1.211 +  apply (rule up_chainI)
   1.212 +  apply (induct_tac i)
   1.213 +   apply simp+
   1.214 +  apply (erule (1) monoD)
   1.215 +  done
   1.216  
   1.217 -lemma UNION_up_iterate_is_fp: 
   1.218 -"up_cont F ==> F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   1.219 -apply (frule up_cont_mono [THEN up_iterate_chain])
   1.220 -apply (drule (1) up_contD)
   1.221 -apply simp
   1.222 -apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   1.223 -apply (case_tac "xa")
   1.224 -apply auto
   1.225 -done
   1.226 +lemma UNION_up_iterate_is_fp:
   1.227 +  "up_cont F ==>
   1.228 +    F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   1.229 +  apply (frule up_cont_mono [THEN up_iterate_chain])
   1.230 +  apply (drule (1) up_contD)
   1.231 +  apply simp
   1.232 +  apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   1.233 +  apply (case_tac xa)
   1.234 +   apply auto
   1.235 +  done
   1.236  
   1.237 -lemma UNION_up_iterate_lowerbound: 
   1.238 -"[| mono F; F P = P |] ==> UNION UNIV (up_iterate F) <= P"
   1.239 -apply (subgoal_tac "(!!i. up_iterate F i <= P)")
   1.240 -apply  fast
   1.241 -apply (induct_tac "i")
   1.242 -prefer 2 apply (drule (1) monoD)
   1.243 -apply auto
   1.244 -done
   1.245 +lemma UNION_up_iterate_lowerbound:
   1.246 +    "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
   1.247 +  apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
   1.248 +   apply fast
   1.249 +  apply (induct_tac i)
   1.250 +  prefer 2 apply (drule (1) monoD)
   1.251 +   apply auto
   1.252 +  done
   1.253  
   1.254 -lemma UNION_up_iterate_is_lfp: 
   1.255 -  "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   1.256 -apply (rule set_eq_subset [THEN iffD2])
   1.257 -apply (rule conjI)
   1.258 -prefer 2
   1.259 -apply  (drule up_cont_mono)
   1.260 -apply  (rule UNION_up_iterate_lowerbound)
   1.261 -apply   assumption
   1.262 -apply  (erule lfp_unfold [symmetric])
   1.263 -apply (rule lfp_lowerbound)
   1.264 -apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   1.265 -apply (erule UNION_up_iterate_is_fp [symmetric])
   1.266 -done
   1.267 +lemma UNION_up_iterate_is_lfp:
   1.268 +    "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   1.269 +  apply (rule set_eq_subset [THEN iffD2])
   1.270 +  apply (rule conjI)
   1.271 +   prefer 2
   1.272 +   apply (drule up_cont_mono)
   1.273 +   apply (rule UNION_up_iterate_lowerbound)
   1.274 +    apply assumption
   1.275 +   apply (erule lfp_unfold [symmetric])
   1.276 +  apply (rule lfp_lowerbound)
   1.277 +  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   1.278 +  apply (erule UNION_up_iterate_is_fp [symmetric])
   1.279 +  done
   1.280  
   1.281  
   1.282  constdefs
   1.283 -
   1.284    down_iterate :: "('a set => 'a set) => nat => 'a set"
   1.285 - "down_iterate f n == (f^n) UNIV"
   1.286 +  "down_iterate f n == (f^n) UNIV"
   1.287  
   1.288  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   1.289 -by (simp add: down_iterate_def)
   1.290 +  by (simp add: down_iterate_def)
   1.291  
   1.292 -lemma down_iterate_Suc [simp]: 
   1.293 -  "down_iterate f (Suc i) = f (down_iterate f i)"
   1.294 -by (simp add: down_iterate_def)
   1.295 +lemma down_iterate_Suc [simp]:
   1.296 +    "down_iterate f (Suc i) = f (down_iterate f i)"
   1.297 +  by (simp add: down_iterate_def)
   1.298  
   1.299  lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
   1.300 -apply (rule down_chainI)
   1.301 -apply (induct_tac i)
   1.302 -apply simp+
   1.303 -apply (erule (1) monoD)
   1.304 -done
   1.305 +  apply (rule down_chainI)
   1.306 +  apply (induct_tac i)
   1.307 +   apply simp+
   1.308 +  apply (erule (1) monoD)
   1.309 +  done
   1.310  
   1.311 -lemma INTER_down_iterate_is_fp: 
   1.312 -"down_cont F ==> 
   1.313 - F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   1.314 -apply (frule down_cont_mono [THEN down_iterate_chain])
   1.315 -apply (drule (1) down_contD)
   1.316 -apply simp
   1.317 -apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   1.318 -apply (case_tac "xa")
   1.319 -apply auto
   1.320 -done
   1.321 +lemma INTER_down_iterate_is_fp:
   1.322 +  "down_cont F ==>
   1.323 +    F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   1.324 +  apply (frule down_cont_mono [THEN down_iterate_chain])
   1.325 +  apply (drule (1) down_contD)
   1.326 +  apply simp
   1.327 +  apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   1.328 +  apply (case_tac xa)
   1.329 +   apply auto
   1.330 +  done
   1.331  
   1.332 -lemma INTER_down_iterate_upperbound: 
   1.333 -"[| mono F; F P = P |] ==> P <= INTER UNIV (down_iterate F)"
   1.334 -apply (subgoal_tac "(!!i. P <= down_iterate F i)")
   1.335 -apply  fast
   1.336 -apply (induct_tac "i")
   1.337 -prefer 2 apply (drule (1) monoD)
   1.338 -apply auto
   1.339 -done
   1.340 +lemma INTER_down_iterate_upperbound:
   1.341 +    "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
   1.342 +  apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
   1.343 +   apply fast
   1.344 +  apply (induct_tac i)
   1.345 +  prefer 2 apply (drule (1) monoD)
   1.346 +   apply auto
   1.347 +  done
   1.348  
   1.349 -lemma INTER_down_iterate_is_gfp: 
   1.350 -  "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   1.351 -apply (rule set_eq_subset [THEN iffD2])
   1.352 -apply (rule conjI)
   1.353 -apply  (drule down_cont_mono)
   1.354 -apply  (rule INTER_down_iterate_upperbound)
   1.355 -apply   assumption
   1.356 -apply  (erule gfp_unfold [symmetric])
   1.357 -apply (rule gfp_upperbound)
   1.358 -apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   1.359 -apply (erule INTER_down_iterate_is_fp)
   1.360 -done
   1.361 +lemma INTER_down_iterate_is_gfp:
   1.362 +    "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   1.363 +  apply (rule set_eq_subset [THEN iffD2])
   1.364 +  apply (rule conjI)
   1.365 +   apply (drule down_cont_mono)
   1.366 +   apply (rule INTER_down_iterate_upperbound)
   1.367 +    apply assumption
   1.368 +   apply (erule gfp_unfold [symmetric])
   1.369 +  apply (rule gfp_upperbound)
   1.370 +  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   1.371 +  apply (erule INTER_down_iterate_is_fp)
   1.372 +  done
   1.373  
   1.374  end