# HG changeset patch # User paulson # Date 1254760139 -3600 # Node ID f8d995b5dd60da54984944119e3f5217a82c5747 # Parent 0fbaf49367fff1c0edd57f77560dbb120f0a0e5b# Parent 6f09346c7c083918dce54553437678fc3cb1ff0a merged diff -r 0fbaf49367ff -r f8d995b5dd60 src/HOL/Real.thy --- 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 \ y + e)" + shows "x \ y" +proof (rule ccontr) + assume xy: "\ x \ y" + hence "(x-y)/2 > 0" + by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy) + hence "x \ 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 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 = {} \ 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 \ range"}. *} diff -r 0fbaf49367ff -r f8d995b5dd60 src/HOL/SEQ.thy --- 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) \ (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 \ real" + assumes inc: "!!n. f n \ f (Suc n)" + and bdd: "!!n. f n \ l" + and en: "!!e. 0 < e \ \n. l \ f n + e" + shows "f ----> l" +proof (auto simp add: LIMSEQ_def) + fix e :: real + assume e: "0 < e" + then obtain N where "l \ 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. \f n - l\ = l - f n" + by (simp add: bdd) + have "\f (N+k) - l\ < 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 \ n \ \f n - l\ < e" using 1 [of "n-N"] + by simp + } note [intro] = this + show " \no. \n\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 "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" diff -r 0fbaf49367ff -r f8d995b5dd60 src/HOL/Series.thy --- 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 @@ "\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..