src/HOL/Library/Continuity.thy
changeset 22431 28344ccffc35
parent 22422 ee19cdb07528
child 22452 8a86fd2a1bf0
     1.1 --- a/src/HOL/Library/Continuity.thy	Sat Mar 10 16:23:28 2007 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Sat Mar 10 16:24:52 2007 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
     1.5  
     1.6  definition
     1.7 -  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where
     1.8 +  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
     1.9    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.10  
    1.11  abbreviation
    1.12 @@ -24,12 +24,12 @@
    1.13    "bot \<equiv> Sup {}"
    1.14  
    1.15  lemma SUP_nat_conv:
    1.16 -  "(SUP n::nat. M n::'a::comp_lat) = sup (M 0) (SUP n. M(Suc n))"
    1.17 +  "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
    1.18  apply(rule order_antisym)
    1.19   apply(rule SUP_leI)
    1.20   apply(case_tac n)
    1.21    apply simp
    1.22 - apply (blast intro:le_SUPI le_supI2)
    1.23 + apply (fast intro:le_SUPI le_supI2)
    1.24  apply(simp)
    1.25  apply (blast intro:SUP_leI le_SUPI)
    1.26  done
    1.27 @@ -43,10 +43,10 @@
    1.28    have "F B = sup (F A) (F B)"
    1.29    proof -
    1.30      have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
    1.31 -    hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
    1.32 +    hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp
    1.33      also have "\<dots> = (SUP i. F(?C i))"
    1.34        using `chain ?C` `continuous F` by(simp add:continuous_def)
    1.35 -    also have "\<dots> = sup (F A) (F B)" by(simp add: SUP_nat_conv)
    1.36 +    also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp
    1.37      finally show ?thesis .
    1.38    qed
    1.39    thus "F A \<le> F B" by(subst le_iff_sup, simp)
    1.40 @@ -80,7 +80,7 @@
    1.41        thus ?thesis by(auto simp add:chain_def)
    1.42      qed
    1.43      hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    1.44 -    also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
    1.45 +    also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
    1.46      finally show "F ?U \<le> ?U" .
    1.47    qed
    1.48    ultimately show ?thesis by (blast intro:order_antisym)