src/HOL/Library/Continuity.thy
changeset 44928 7ef6505bde7f
parent 32960 69916a850301
child 46508 ec9630fe9ca7
     1.1 --- a/src/HOL/Library/Continuity.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -21,12 +21,12 @@
     1.4  lemma SUP_nat_conv:
     1.5    "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
     1.6  apply(rule order_antisym)
     1.7 - apply(rule SUP_leI)
     1.8 + apply(rule SUP_least)
     1.9   apply(case_tac n)
    1.10    apply simp
    1.11 - apply (fast intro:le_SUPI le_supI2)
    1.12 + apply (fast intro:SUP_upper le_supI2)
    1.13  apply(simp)
    1.14 -apply (blast intro:SUP_leI le_SUPI)
    1.15 +apply (blast intro:SUP_least SUP_upper)
    1.16  done
    1.17  
    1.18  lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.19 @@ -61,7 +61,7 @@
    1.20        also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    1.21        finally show ?case .
    1.22      qed }
    1.23 -  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    1.24 +  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least)
    1.25    moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
    1.26    proof (rule lfp_lowerbound)
    1.27      have "chain(%i. (F ^^ i) bot)"
    1.28 @@ -75,7 +75,7 @@
    1.29        thus ?thesis by(auto simp add:chain_def)
    1.30      qed
    1.31      hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    1.32 -    also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
    1.33 +    also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper)
    1.34      finally show "F ?U \<le> ?U" .
    1.35    qed
    1.36    ultimately show ?thesis by (blast intro:order_antisym)