merged

--- a/src/HOL/Real.thy	Mon Oct 05 16:55:56 2009 +0200
+++ b/src/HOL/Real.thy	Mon Oct 05 17:28:59 2009 +0100
@@ -2,4 +2,28 @@
 imports RComplete RealVector
 begin
 
+lemma field_le_epsilon:
+  fixes x y :: "'a:: {number_ring,division_by_zero,ordered_field}"
+  assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
+  shows "x \<le> y"
+proof (rule ccontr)
+  assume xy: "\<not> x \<le> y"
+  hence "(x-y)/2 > 0"
+    by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
+  hence "x \<le> y + (x - y) / 2"
+    by (rule e [of "(x-y)/2"])
+  also have "... = (x - y + 2*y)/2"
+    by auto
+       (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
+           diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
+  also have "... = (x + y) / 2" 
+    by auto
+  also have "... < x" using xy 
+    by auto
+  finally have "x<x" .
+  thus False
+    by auto 
+qed
+
+
 end

--- a/src/HOL/Relation.thy	Mon Oct 05 16:55:56 2009 +0200
+++ b/src/HOL/Relation.thy	Mon Oct 05 17:28:59 2009 +0100
@@ -376,6 +376,9 @@
 lemma Domain_empty [simp]: "Domain {} = {}"
 by blast
 
+lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}"
+  by auto
+
 lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
 by blast
 
@@ -427,6 +430,9 @@
 lemma Range_empty [simp]: "Range {} = {}"
 by blast
 
+lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
+  by auto
+
 lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
 by blast
 
@@ -617,8 +623,11 @@
   apply simp
   done
 
-text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
-Ehmety) *}
+lemma finite_Domain: "finite r ==> finite (Domain r)"
+  by (induct set: finite) (auto simp add: Domain_insert)
+
+lemma finite_Range: "finite r ==> finite (Range r)"
+  by (induct set: finite) (auto simp add: Range_insert)
 
 lemma finite_Field: "finite r ==> finite (Field r)"
   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}

--- a/src/HOL/SEQ.thy	Mon Oct 05 16:55:56 2009 +0200
+++ b/src/HOL/SEQ.thy	Mon Oct 05 17:28:59 2009 +0100
@@ -193,6 +193,9 @@
 
 subsection {* Limits of Sequences *}
 
+lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
+  by simp
+
 lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
 unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
 
@@ -315,6 +318,39 @@
   shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
 by (rule mult.LIMSEQ)
 
+lemma increasing_LIMSEQ:
+  fixes f :: "nat \<Rightarrow> real"
+  assumes inc: "!!n. f n \<le> f (Suc n)"
+      and bdd: "!!n. f n \<le> l"
+      and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
+  shows "f ----> l"
+proof (auto simp add: LIMSEQ_def)
+  fix e :: real
+  assume e: "0 < e"
+  then obtain N where "l \<le> f N + e/2"
+    by (metis half_gt_zero e en that)
+  hence N: "l < f N + e" using e
+    by simp
+  { fix k
+    have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n"
+      by (simp add: bdd) 
+    have "\<bar>f (N+k) - l\<bar> < e"
+    proof (induct k)
+      case 0 show ?case using N
+	by simp   
+    next
+      case (Suc k) thus ?case using N inc [of "N+k"]
+	by simp
+    qed 
+  } note 1 = this
+  { fix n
+    have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"]
+      by simp 
+  } note [intro] = this
+  show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e"
+    by (auto simp add: dist_real_def) 
+  qed
+
 lemma Bseq_inverse_lemma:
   fixes x :: "'a::real_normed_div_algebra"
   shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"

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