1.1 --- a/src/HOL/Real.thy	Mon Oct 05 16:55:56 2009 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Oct 05 17:28:59 2009 +0100
     1.3 @@ -2,4 +2,28 @@
     1.4  imports RComplete RealVector
     1.5  begin
     1.6  
     1.7 +lemma field_le_epsilon:
     1.8 +  fixes x y :: "'a:: {number_ring,division_by_zero,ordered_field}"
     1.9 +  assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
    1.10 +  shows "x \<le> y"
    1.11 +proof (rule ccontr)
    1.12 +  assume xy: "\<not> x \<le> y"
    1.13 +  hence "(x-y)/2 > 0"
    1.14 +    by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
    1.15 +  hence "x \<le> y + (x - y) / 2"
    1.16 +    by (rule e [of "(x-y)/2"])
    1.17 +  also have "... = (x - y + 2*y)/2"
    1.18 +    by auto
    1.19 +       (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
    1.20 +           diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
    1.21 +  also have "... = (x + y) / 2" 
    1.22 +    by auto
    1.23 +  also have "... < x" using xy 
    1.24 +    by auto
    1.25 +  finally have "x<x" .
    1.26 +  thus False
    1.27 +    by auto 
    1.28 +qed
    1.29 +
    1.30 +
    1.31  end

     2.1 --- a/src/HOL/Relation.thy	Mon Oct 05 16:55:56 2009 +0200
     2.2 +++ b/src/HOL/Relation.thy	Mon Oct 05 17:28:59 2009 +0100
     2.3 @@ -376,6 +376,9 @@
     2.4  lemma Domain_empty [simp]: "Domain {} = {}"
     2.5  by blast
     2.6  
     2.7 +lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}"
     2.8 +  by auto
     2.9 +
    2.10  lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
    2.11  by blast
    2.12  
    2.13 @@ -427,6 +430,9 @@
    2.14  lemma Range_empty [simp]: "Range {} = {}"
    2.15  by blast
    2.16  
    2.17 +lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
    2.18 +  by auto
    2.19 +
    2.20  lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
    2.21  by blast
    2.22  
    2.23 @@ -617,8 +623,11 @@
    2.24    apply simp
    2.25    done
    2.26  
    2.27 -text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
    2.28 -Ehmety) *}
    2.29 +lemma finite_Domain: "finite r ==> finite (Domain r)"
    2.30 +  by (induct set: finite) (auto simp add: Domain_insert)
    2.31 +
    2.32 +lemma finite_Range: "finite r ==> finite (Range r)"
    2.33 +  by (induct set: finite) (auto simp add: Range_insert)
    2.34  
    2.35  lemma finite_Field: "finite r ==> finite (Field r)"
    2.36    -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}

     3.1 --- a/src/HOL/SEQ.thy	Mon Oct 05 16:55:56 2009 +0200
     3.2 +++ b/src/HOL/SEQ.thy	Mon Oct 05 17:28:59 2009 +0100
     3.3 @@ -193,6 +193,9 @@
     3.4  
     3.5  subsection {* Limits of Sequences *}
     3.6  
     3.7 +lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
     3.8 +  by simp
     3.9 +
    3.10  lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
    3.11  unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
    3.12  
    3.13 @@ -315,6 +318,39 @@
    3.14    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
    3.15  by (rule mult.LIMSEQ)
    3.16  
    3.17 +lemma increasing_LIMSEQ:
    3.18 +  fixes f :: "nat \<Rightarrow> real"
    3.19 +  assumes inc: "!!n. f n \<le> f (Suc n)"
    3.20 +      and bdd: "!!n. f n \<le> l"
    3.21 +      and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
    3.22 +  shows "f ----> l"
    3.23 +proof (auto simp add: LIMSEQ_def)
    3.24 +  fix e :: real
    3.25 +  assume e: "0 < e"
    3.26 +  then obtain N where "l \<le> f N + e/2"
    3.27 +    by (metis half_gt_zero e en that)
    3.28 +  hence N: "l < f N + e" using e
    3.29 +    by simp
    3.30 +  { fix k
    3.31 +    have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n"
    3.32 +      by (simp add: bdd) 
    3.33 +    have "\<bar>f (N+k) - l\<bar> < e"
    3.34 +    proof (induct k)
    3.35 +      case 0 show ?case using N
    3.36 +	by simp   
    3.37 +    next
    3.38 +      case (Suc k) thus ?case using N inc [of "N+k"]
    3.39 +	by simp
    3.40 +    qed 
    3.41 +  } note 1 = this
    3.42 +  { fix n
    3.43 +    have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"]
    3.44 +      by simp 
    3.45 +  } note [intro] = this
    3.46 +  show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e"
    3.47 +    by (auto simp add: dist_real_def) 
    3.48 +  qed
    3.49 +
    3.50  lemma Bseq_inverse_lemma:
    3.51    fixes x :: "'a::real_normed_div_algebra"
    3.52    shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"

     4.1 --- a/src/HOL/Series.thy	Mon Oct 05 16:55:56 2009 +0200
     4.2 +++ b/src/HOL/Series.thy	Mon Oct 05 17:28:59 2009 +0100
     4.3 @@ -32,6 +32,9 @@
     4.4    "\<Sum>i. b" == "CONST suminf (%i. b)"
     4.5  
     4.6  
     4.7 +lemma [trans]: "f=g ==> g sums z ==> f sums z"
     4.8 +  by simp
     4.9 +
    4.10  lemma sumr_diff_mult_const:
    4.11   "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
    4.12  by (simp add: diff_minus setsum_addf real_of_nat_def)