src/HOL/Library/Continuity.thy
changeset 22452 8a86fd2a1bf0
parent 22431 28344ccffc35
child 23752 15839159f8b6
     1.1 --- a/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:07 2007 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:08 2007 +0100
     1.3 @@ -12,15 +12,15 @@
     1.4  subsection {* Continuity for complete lattices *}
     1.5  
     1.6  definition
     1.7 -  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
     1.8 +  chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
     1.9    "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
    1.10  
    1.11  definition
    1.12 -  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
    1.13 +  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.14    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.15  
    1.16  abbreviation
    1.17 -  bot :: "'a::order" where
    1.18 +  bot :: "'a::complete_lattice" where
    1.19    "bot \<equiv> Sup {}"
    1.20  
    1.21  lemma SUP_nat_conv:
    1.22 @@ -34,7 +34,7 @@
    1.23  apply (blast intro:SUP_leI le_SUPI)
    1.24  done
    1.25  
    1.26 -lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
    1.27 +lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.28    assumes "continuous F" shows "mono F"
    1.29  proof
    1.30    fix A B :: "'a" assume "A <= B"