# HG changeset patch # User wenzelm # Date 1315161440 -7200 # Node ID 8c3d4063bf526a318c0885a98a7555be184d90a2 # Parent 1e490e891c88273d925c02917f4a45eba8a0276d# Parent fe319b45315c5e313727f9606038d6813d9d9014 merged diff -r fe319b45315c -r 8c3d4063bf52 NEWS --- a/NEWS Sun Sep 04 19:36:19 2011 +0200 +++ b/NEWS Sun Sep 04 20:37:20 2011 +0200 @@ -277,6 +277,8 @@ realpow_two_diff ~> square_diff_square_factored reals_complete2 ~> complete_real exp_ln_eq ~> ln_unique + expi_add ~> exp_add + expi_zero ~> exp_zero lemma_DERIV_subst ~> DERIV_cong LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff LIMSEQ_const ~> tendsto_const @@ -296,6 +298,9 @@ LIMSEQ_norm_zero ~> tendsto_norm_zero_iff LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff LIMSEQ_imp_rabs ~> tendsto_rabs + LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] + LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] + LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] LIM_ident ~> tendsto_ident_at LIM_const ~> tendsto_const LIM_add ~> tendsto_add diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/Complex.thy Sun Sep 04 20:37:20 2011 +0200 @@ -606,7 +606,7 @@ abbreviation expi :: "complex \ complex" where "expi \ exp" -lemma expi_imaginary: "expi (Complex 0 b) = cis b" +lemma cis_conv_exp: "cis b = exp (Complex 0 b)" proof (rule complex_eqI) { fix n have "Complex 0 b ^ n = real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)" @@ -614,23 +614,18 @@ apply (simp add: cos_coeff_def sin_coeff_def) apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc) done } note * = this - show "Re (exp (Complex 0 b)) = Re (cis b)" + show "Re (cis b) = Re (exp (Complex 0 b))" unfolding exp_def cis_def cos_def by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic], simp add: * mult_assoc [symmetric]) - show "Im (exp (Complex 0 b)) = Im (cis b)" + show "Im (cis b) = Im (exp (Complex 0 b))" unfolding exp_def cis_def sin_def by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic], simp add: * mult_assoc [symmetric]) qed lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)" -proof - - have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))" - by simp - thus ?thesis - unfolding exp_add exp_of_real expi_imaginary . -qed + unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp lemma complex_split_polar: "\r a. z = complex_of_real r * (Complex (cos a) (sin a))" @@ -736,12 +731,6 @@ lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" by (auto simp add: DeMoivre) -lemma expi_add: "expi(a + b) = expi(a) * expi(b)" - by (rule exp_add) (* FIXME: redundant *) - -lemma expi_zero: "expi (0::complex) = 1" - by (rule exp_zero) (* FIXME: redundant *) - lemma complex_expi_Ex: "\a r. z = complex_of_real r * expi a" apply (insert rcis_Ex [of z]) apply (auto simp add: expi_def rcis_def mult_assoc [symmetric]) diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/Int.thy Sun Sep 04 20:37:20 2011 +0200 @@ -162,7 +162,10 @@ by (simp add: Zero_int_def One_int_def) qed -lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" +abbreviation int :: "nat \ int" where + "int \ of_nat" + +lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})" by (induct m) (simp_all add: Zero_int_def One_int_def add) @@ -218,7 +221,7 @@ text{*strict, in 1st argument; proof is by induction on k>0*} lemma zmult_zless_mono2_lemma: - "(i::int) 0 of_nat k * i < of_nat k * j" + "(i::int) 0 int k * i < int k * j" apply (induct k) apply simp apply (simp add: left_distrib) @@ -226,13 +229,13 @@ apply (simp_all add: add_strict_mono) done -lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = of_nat n" +lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = int n" apply (cases k) apply (auto simp add: le add int_def Zero_int_def) apply (rule_tac x="x-y" in exI, simp) done -lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = of_nat n" +lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = int n" apply (cases k) apply (simp add: less int_def Zero_int_def) apply (rule_tac x="x-y" in exI, simp) @@ -261,7 +264,7 @@ done lemma zless_iff_Suc_zadd: - "(w \ int) < z \ (\n. z = w + of_nat (Suc n))" + "(w \ int) < z \ (\n. z = w + int (Suc n))" apply (cases z, cases w) apply (auto simp add: less add int_def) apply (rename_tac a b c d) @@ -314,7 +317,7 @@ done text{*Collapse nested embeddings*} -lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" +lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" by (induct n) auto lemma of_int_power: @@ -400,13 +403,13 @@ by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) qed -lemma nat_int [simp]: "nat (of_nat n) = n" +lemma nat_int [simp]: "nat (int n) = n" by (simp add: nat int_def) -lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \ z then z else 0)" +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" by (cases z) (simp add: nat le int_def Zero_int_def) -corollary nat_0_le: "0 \ z ==> of_nat (nat z) = z" +corollary nat_0_le: "0 \ z ==> int (nat z) = z" by simp lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" @@ -431,14 +434,14 @@ lemma nonneg_eq_int: fixes z :: int - assumes "0 \ z" and "\m. z = of_nat m \ P" + assumes "0 \ z" and "\m. z = int m \ P" shows P using assms by (blast dest: nat_0_le sym) -lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = of_nat m else m=0)" +lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = int m else m=0)" by (cases w) (simp add: nat le int_def Zero_int_def, arith) -corollary nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = of_nat m else m=0)" +corollary nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = int m else m=0)" by (simp only: eq_commute [of m] nat_eq_iff) lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < of_nat m)" @@ -446,6 +449,12 @@ apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith) done +lemma nat_le_iff: "nat x \ n \ x \ int n" + by (cases x, simp add: nat le int_def le_diff_conv) + +lemma nat_mono: "x \ y \ nat x \ nat y" + by (cases x, cases y, simp add: nat le) + lemma nat_0_iff[simp]: "nat(i::int) = 0 \ i\0" by(simp add: nat_eq_iff) arith @@ -464,10 +473,10 @@ by (cases z, cases z') (simp add: nat add minus diff_minus le Zero_int_def) -lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0" +lemma nat_zminus_int [simp]: "nat (- int n) = 0" by (simp add: int_def minus nat Zero_int_def) -lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)" +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" by (cases z) (simp add: nat less int_def, arith) context ring_1 @@ -485,31 +494,31 @@ subsection{*Lemmas about the Function @{term of_nat} and Orderings*} -lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \ int)" +lemma negative_zless_0: "- (int (Suc n)) < (0 \ int)" by (simp add: order_less_le del: of_nat_Suc) -lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \ int)" +lemma negative_zless [iff]: "- (int (Suc n)) < int m" by (rule negative_zless_0 [THEN order_less_le_trans], simp) -lemma negative_zle_0: "- of_nat n \ (0 \ int)" +lemma negative_zle_0: "- int n \ 0" by (simp add: minus_le_iff) -lemma negative_zle [iff]: "- of_nat n \ (of_nat m \ int)" +lemma negative_zle [iff]: "- int n \ int m" by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) -lemma not_zle_0_negative [simp]: "~ (0 \ - (of_nat (Suc n) \ int))" +lemma not_zle_0_negative [simp]: "~ (0 \ - (int (Suc n)))" by (subst le_minus_iff, simp del: of_nat_Suc) -lemma int_zle_neg: "((of_nat n \ int) \ - of_nat m) = (n = 0 & m = 0)" +lemma int_zle_neg: "(int n \ - int m) = (n = 0 & m = 0)" by (simp add: int_def le minus Zero_int_def) -lemma not_int_zless_negative [simp]: "~ ((of_nat n \ int) < - of_nat m)" +lemma not_int_zless_negative [simp]: "~ (int n < - int m)" by (simp add: linorder_not_less) -lemma negative_eq_positive [simp]: "((- of_nat n \ int) = of_nat m) = (n = 0 & m = 0)" +lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)" by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) -lemma zle_iff_zadd: "(w\int) \ z \ (\n. z = w + of_nat n)" +lemma zle_iff_zadd: "w \ z \ (\n. z = w + int n)" proof - have "(w \ z) = (0 \ z - w)" by (simp only: le_diff_eq add_0_left) @@ -520,10 +529,10 @@ finally show ?thesis . qed -lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\int)" +lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" by simp -lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\int)" +lemma int_Suc0_eq_1: "int (Suc 0) = 1" by simp text{*This version is proved for all ordered rings, not just integers! @@ -534,7 +543,7 @@ "P(abs(a::'a::linordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) -lemma negD: "(x \ int) < 0 \ \n. x = - (of_nat (Suc n))" +lemma negD: "x < 0 \ \n. x = - (int (Suc n))" apply (cases x) apply (auto simp add: le minus Zero_int_def int_def order_less_le) apply (rule_tac x="y - Suc x" in exI, arith) @@ -547,7 +556,7 @@ whether an integer is negative or not.*} theorem int_cases [case_names nonneg neg, cases type: int]: - "[|!! n. (z \ int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P" + "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P" apply (cases "z < 0") apply (blast dest!: negD) apply (simp add: linorder_not_less del: of_nat_Suc) @@ -556,12 +565,12 @@ done theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: - "[|!! n. P (of_nat n \ int); !!n. P (- (of_nat (Suc n))) |] ==> P z" + "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" by (cases z) auto text{*Contributed by Brian Huffman*} theorem int_diff_cases: - obtains (diff) m n where "(z\int) = of_nat m - of_nat n" + obtains (diff) m n where "z = int m - int n" apply (cases z rule: eq_Abs_Integ) apply (rule_tac m=x and n=y in diff) apply (simp add: int_def minus add diff_minus) @@ -938,11 +947,11 @@ assumes number_of_eq: "number_of k = of_int k" class number_semiring = number + comm_semiring_1 + - assumes number_of_int: "number_of (of_nat n) = of_nat n" + assumes number_of_int: "number_of (int n) = of_nat n" instance number_ring \ number_semiring proof - fix n show "number_of (of_nat n) = (of_nat n :: 'a)" + fix n show "number_of (int n) = (of_nat n :: 'a)" unfolding number_of_eq by (rule of_int_of_nat_eq) qed @@ -1118,7 +1127,7 @@ show ?thesis proof assume eq: "1 + z + z = 0" - have "(0::int) < 1 + (of_nat n + of_nat n)" + have "(0::int) < 1 + (int n + int n)" by (simp add: le_imp_0_less add_increasing) also have "... = - (1 + z + z)" by (simp add: neg add_assoc [symmetric]) @@ -1638,7 +1647,7 @@ lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard] lemma split_nat [arith_split]: - "P(nat(i::int)) = ((\n. i = of_nat n \ P n) & (i < 0 \ P 0))" + "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ P 0))" (is "?P = (?L & ?R)") proof (cases "i < 0") case True thus ?thesis by auto @@ -1731,11 +1740,6 @@ by (rule wf_subset [OF wf_measure]) qed -abbreviation - int :: "nat \ int" -where - "int \ of_nat" - (* `set:int': dummy construction *) theorem int_ge_induct [case_names base step, induct set: int]: fixes i :: int diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/NSA/NSComplex.thy --- a/src/HOL/NSA/NSComplex.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/NSA/NSComplex.thy Sun Sep 04 20:37:20 2011 +0200 @@ -613,7 +613,7 @@ by (simp add: NSDeMoivre_ext) lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" -by transfer (rule expi_add) +by transfer (rule exp_add) subsection{*@{term hcomplex_of_complex}: the Injection from diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/RComplete.thy --- a/src/HOL/RComplete.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/RComplete.thy Sun Sep 04 20:37:20 2011 +0200 @@ -336,9 +336,6 @@ lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" unfolding natfloor_def by simp -lemma nat_mono: "x \ y \ nat x \ nat y" - by simp (* TODO: move to Int.thy *) - lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" unfolding natfloor_def by (intro nat_mono floor_mono) @@ -474,19 +471,16 @@ lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" unfolding natceiling_def by (intro nat_mono ceiling_mono) -lemma nat_le_iff: "nat x \ n \ x \ int n" - by auto (* TODO: move to Int.thy *) - lemma natceiling_le: "x <= real a ==> natceiling x <= a" unfolding natceiling_def real_of_nat_def by (simp add: nat_le_iff ceiling_le_iff) -lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)" - unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *) +lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)" + unfolding natceiling_def real_of_nat_def by (simp add: nat_le_iff ceiling_le_iff) lemma natceiling_le_eq_number_of [simp]: - "~ neg((number_of n)::int) ==> 0 <= x ==> + "~ neg((number_of n)::int) ==> (natceiling x <= number_of n) = (x <= number_of n)" by (simp add: natceiling_le_eq) diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/SEQ.thy Sun Sep 04 20:37:20 2011 +0200 @@ -380,22 +380,6 @@ shows "\X ----> a; a \ 0\ \ Bseq (\n. inverse (X n))" unfolding Bseq_conv_Bfun by (rule Bfun_inverse) -lemma LIMSEQ_add_const: (* FIXME: delete *) - fixes a :: "'a::real_normed_vector" - shows "f ----> a ==> (%n.(f n + b)) ----> a + b" -by (intro tendsto_intros) - -(* FIXME: delete *) -lemma LIMSEQ_add_minus: - fixes a b :: "'a::real_normed_vector" - shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" -by (intro tendsto_intros) - -lemma LIMSEQ_diff_const: (* FIXME: delete *) - fixes a b :: "'a::real_normed_vector" - shows "f ----> a ==> (%n.(f n - b)) ----> a - b" -by (intro tendsto_intros) - lemma LIMSEQ_diff_approach_zero: fixes L :: "'a::real_normed_vector" shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L" @@ -438,7 +422,8 @@ lemma LIMSEQ_inverse_real_of_nat_add_minus: "(%n. r + -inverse(real(Suc n))) ----> r" - using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto + using tendsto_add [OF tendsto_const + tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/Series.thy --- a/src/HOL/Series.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/Series.thy Sun Sep 04 20:37:20 2011 +0200 @@ -122,7 +122,7 @@ shows "f sums s ==> (\n. f(n + k)) sums (s - (SUM i = 0..< k. f i))" apply (unfold sums_def) apply (simp add: sumr_offset) - apply (rule LIMSEQ_diff_const) + apply (rule tendsto_diff [OF _ tendsto_const]) apply (rule LIMSEQ_ignore_initial_segment) apply assumption done @@ -166,7 +166,7 @@ proof - from sumSuc[unfolded sums_def] have "(\i. \n = Suc 0.. l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def . - from LIMSEQ_add_const[OF this, where b="f 0"] + from tendsto_add[OF this tendsto_const, where b="f 0"] have "(\i. \n = 0.. l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] . thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc) qed @@ -625,7 +625,7 @@ apply (simp add:diff_Suc split:nat.splits) apply (blast intro: norm_ratiotest_lemma) apply (rule_tac x = "Suc N" in exI, clarify) -apply(simp cong:setsum_ivl_cong) +apply(simp cong del: setsum_cong cong: setsum_ivl_cong) done lemma ratio_test: diff -r fe319b45315c -r 8c3d4063bf52 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Sep 04 19:36:19 2011 +0200 +++ b/src/HOL/Transcendental.thy Sun Sep 04 20:37:20 2011 +0200 @@ -1999,7 +1999,7 @@ apply (drule tan_total_pos) apply (cut_tac [2] y="-y" in tan_total_pos, safe) apply (rule_tac [3] x = "-x" in exI) -apply (auto intro!: exI) +apply (auto del: exI intro!: exI) done lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y" @@ -2009,7 +2009,7 @@ apply (subgoal_tac "\z. xa < z & z < y & DERIV tan z :> 0") apply (rule_tac [4] Rolle) apply (rule_tac [2] Rolle) -apply (auto intro!: DERIV_tan DERIV_isCont exI +apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI simp add: differentiable_def) txt{*Now, simulate TRYALL*} apply (rule_tac [!] DERIV_tan asm_rl) @@ -2785,7 +2785,7 @@ have "norm (?diff 1 n - 0) < r" by auto } thus "\ N. \ n \ N. norm (?diff 1 n - 0) < r" by blast qed - from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus] + from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus] have "(?c 1) sums (arctan 1)" unfolding sums_def by auto hence "arctan 1 = (\ i. ?c 1 i)" by (rule sums_unique)