src/HOL/Library/Continuity.thy
changeset 22367 6860f09242bf
parent 21404 eb85850d3eb7
child 22422 ee19cdb07528
     1.1 --- a/src/HOL/Library/Continuity.thy	Tue Feb 27 00:32:52 2007 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Tue Feb 27 00:33:49 2007 +0100
     1.3 @@ -9,20 +9,22 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -subsection{*Continuity for complete lattices*}
     1.8 +subsection {* Continuity for complete lattices *}
     1.9  
    1.10 -constdefs
    1.11 - chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
    1.12 -"chain M == !i. M i \<le> M(Suc i)"
    1.13 - continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
    1.14 -"continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
    1.15 +definition
    1.16 +  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    1.17 +  "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
    1.18 +
    1.19 +definition
    1.20 +  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    1.21 +  "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.22  
    1.23  abbreviation
    1.24    bot :: "'a::order" where
    1.25 -  "bot == Sup {}"
    1.26 +  "bot \<equiv> Sup {}"
    1.27  
    1.28  lemma SUP_nat_conv:
    1.29 - "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
    1.30 +  "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
    1.31  apply(rule order_antisym)
    1.32   apply(rule SUP_leI)
    1.33   apply(case_tac n)