# HG changeset patch # User paulson # Date 1447417633 0 # Node ID 268d88ec9087d1b90773bf7a5316d840626ad2e1 # Parent b1c24adc15814973c1c05ef16a629bc088b7fe5f Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes. diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Archimedean_Field.thy Fri Nov 13 12:27:13 2015 +0000 @@ -152,7 +152,7 @@ shows "\x\ = a \ of_int a \ x \ x < of_int a + 1" using floor_correct floor_unique by auto -lemma of_int_floor_le: "of_int (floor x) \ x" +lemma of_int_floor_le [simp]: "of_int (floor x) \ x" using floor_correct .. lemma le_floor_iff: "z \ floor x \ of_int z \ x" @@ -381,12 +381,12 @@ ceiling ("\_\") lemma ceiling_correct: "of_int (ceiling x) - 1 < x \ x \ of_int (ceiling x)" - unfolding ceiling_def using floor_correct [of "- x"] by simp + unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) lemma ceiling_unique: "\of_int z - 1 < x; x \ of_int z\ \ ceiling x = z" unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp -lemma le_of_int_ceiling: "x \ of_int (ceiling x)" +lemma le_of_int_ceiling [simp]: "x \ of_int (ceiling x)" using ceiling_correct .. lemma ceiling_le_iff: "ceiling x \ z \ x \ of_int z" @@ -494,7 +494,7 @@ text \Addition and subtraction of integers\ lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z" - using ceiling_correct [of x] by (simp add: ceiling_unique) + using ceiling_correct [of x] by (simp add: ceiling_def) lemma ceiling_add_numeral [simp]: "ceiling (x + numeral v) = ceiling x + numeral v" diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Binomial.thy Fri Nov 13 12:27:13 2015 +0000 @@ -67,11 +67,11 @@ proof (induct n) case (Suc n) then have *: "fact n \ (of_nat (Suc n ^ n) ::'a)" - by (rule order_trans) (simp add: power_mono) + by (rule order_trans) (simp add: power_mono del: of_nat_power) have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)" by (simp add: algebra_simps) also have "... \ (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)" - by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono) + by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power) also have "... \ (of_nat (Suc n ^ Suc n) ::'a)" by (metis of_nat_mult order_refl power_Suc) finally show ?case . diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Complex.thy Fri Nov 13 12:27:13 2015 +0000 @@ -842,7 +842,7 @@ by (simp add: cis_divide [symmetric] cis_2pi_int) moreover have "- pi < c \ c \ pi" using ceiling_correct [of "(b - pi) / (2*pi)"] - by (simp add: c_def less_divide_eq divide_le_eq algebra_simps) + by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling) ultimately show "\a. sgn z = cis a \ -pi < a \ a \ pi" by fast qed diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Nov 13 12:27:13 2015 +0000 @@ -808,7 +808,7 @@ also note float_round_up finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \ arctan x" using \0 \ arctan x\ arctan_inverse[OF \1 / x \ 0\] - unfolding real_sgn_pos[OF \0 < 1 / real_of_float x\] le_diff_eq by auto + unfolding sgn_pos[OF \0 < 1 / real_of_float x\] le_diff_eq by auto moreover have "lb_pi prec * Float 1 (- 1) \ pi / 2" unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp @@ -935,7 +935,7 @@ unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl) finally have "arctan x \ pi / 2 - (?lb_horner ?invx)" using \0 \ arctan x\ arctan_inverse[OF \1 / x \ 0\] - unfolding real_sgn_pos[OF \0 < 1 / x\] le_diff_eq by auto + unfolding sgn_pos[OF \0 < 1 / x\] le_diff_eq by auto moreover have "pi / 2 \ ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_right diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Fri Nov 13 12:27:13 2015 +0000 @@ -35,12 +35,12 @@ hence th: "\ k. x=real_of_int (i*k)" by (simp add: rdvd_def) hence th': "real_of_int (floor x) = x" by (auto simp del: of_int_mult) with th have "\ k. real_of_int (floor x) = real_of_int (i*k)" by simp - hence "\ k. floor x = i*k" by blast + hence "\ k. floor x = i*k" by presburger thus ?r using th' by (simp add: dvd_def) next assume "?r" hence "(i::int) dvd \x::real\" .. hence "\ k. real_of_int (floor x) = real_of_int (i*k)" - using dvd_def by blast + by (metis (no_types) dvd_def) thus ?l using \?r\ by (simp add: rdvd_def) qed @@ -123,7 +123,7 @@ let ?fe = "floor ?e" assume be: "isint e bs" hence efe:"real_of_int ?fe = ?e" by (simp add: isint_iff) have "real_of_int ((floor (Inum bs (Mul c e)))) = real_of_int (floor (real_of_int (c * ?fe)))" using efe by simp - also have "\ = real_of_int (c* ?fe)" using floor_of_int by blast + also have "\ = real_of_int (c* ?fe)" by (metis floor_of_int) also have "\ = real_of_int c * ?e" using efe by simp finally show ?thesis using isint_iff by simp qed @@ -1053,9 +1053,10 @@ "iff p q \ (if (p = q) then T else if (p = not q \ not p = q) then F else if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else Iff p q)" + lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" - by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) -(cases "not p= q", auto simp add:not) + by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) (cases "not p= q", auto simp add:not) + lemma iff_qf[simp]: "\qfree p ; qfree q\ \ qfree (iff p q)" by (unfold iff_def,cases "p=q", auto) @@ -2623,7 +2624,7 @@ hence "x + floor ?e +1 \ 1 \ x + floor ?e + 1 \ d" by simp hence "\ (j::int) \ {1 .. d}. j = x + floor ?e + 1" by simp hence "\ (j::int) \ {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps) - hence "\ (j::int) \ {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by blast + hence "\ (j::int) \ {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by presburger hence "\ (j::int) \ {1 .. d}. real_of_int x= - ?e - 1 + real_of_int j" by (simp add: ie[simplified isint_iff]) with nob have ?case by simp } diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Divides.thy Fri Nov 13 12:27:13 2015 +0000 @@ -1696,17 +1696,14 @@ lemma divmod_int_rel: "divmod_int_rel k l (k div l, k mod l)" + unfolding divmod_int_rel_def divide_int_def mod_int_def apply (cases k rule: int_cases3) - apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric]) + apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps) apply (cases l rule: int_cases3) - apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric]) - apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric]) - apply (simp add: of_nat_add [symmetric]) - apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric]) - apply (simp add: of_nat_add [symmetric]) + apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps) + apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric]) apply (cases l rule: int_cases3) - apply (simp_all add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric]) - apply (simp_all add: of_nat_add [symmetric]) + apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric]) done instantiation int :: ring_div diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/GCD.thy Fri Nov 13 12:27:13 2015 +0000 @@ -1133,10 +1133,7 @@ apply (erule subst) apply (rule iffI) apply force - apply (drule_tac x = "abs e" for e in exI) - apply (case_tac "e >= 0" for e :: int) - apply force - apply force + using abs_dvd_iff abs_ge_zero apply blast done lemma gcd_coprime_nat: diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Inequalities.thy --- a/src/HOL/Inequalities.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Inequalities.thy Fri Nov 13 12:27:13 2015 +0000 @@ -34,7 +34,7 @@ by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum split: zdiff_int_split) thus ?thesis - by blast + using int_int_eq by blast qed lemma Setsum_Ico_nat: assumes "(m::nat) \ n" diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Int.thy --- a/src/HOL/Int.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Int.thy Fri Nov 13 12:27:13 2015 +0000 @@ -319,25 +319,25 @@ text \Comparisons involving @{term of_int}.\ lemma of_int_eq_numeral_iff [iff]: - "of_int z = (numeral n :: 'a::ring_char_0) + "of_int z = (numeral n :: 'a::ring_char_0) \ z = numeral n" using of_int_eq_iff by fastforce -lemma of_int_le_numeral_iff [simp]: - "of_int z \ (numeral n :: 'a::linordered_idom) +lemma of_int_le_numeral_iff [simp]: + "of_int z \ (numeral n :: 'a::linordered_idom) \ z \ numeral n" using of_int_le_iff [of z "numeral n"] by simp -lemma of_int_numeral_le_iff [simp]: +lemma of_int_numeral_le_iff [simp]: "(numeral n :: 'a::linordered_idom) \ of_int z \ numeral n \ z" using of_int_le_iff [of "numeral n"] by simp -lemma of_int_less_numeral_iff [simp]: - "of_int z < (numeral n :: 'a::linordered_idom) +lemma of_int_less_numeral_iff [simp]: + "of_int z < (numeral n :: 'a::linordered_idom) \ z < numeral n" using of_int_less_iff [of z "numeral n"] by simp -lemma of_int_numeral_less_iff [simp]: +lemma of_int_numeral_less_iff [simp]: "(numeral n :: 'a::linordered_idom) < of_int z \ numeral n < z" using of_int_less_iff [of "numeral n" z] by simp @@ -815,22 +815,22 @@ subsection \@{term setsum} and @{term setprod}\ -lemma of_nat_setsum: "of_nat (setsum f A) = (\x\A. of_nat(f x))" +lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\x\A. of_nat(f x))" apply (cases "finite A") apply (erule finite_induct, auto) done -lemma of_int_setsum: "of_int (setsum f A) = (\x\A. of_int(f x))" +lemma of_int_setsum [simp]: "of_int (setsum f A) = (\x\A. of_int(f x))" apply (cases "finite A") apply (erule finite_induct, auto) done -lemma of_nat_setprod: "of_nat (setprod f A) = (\x\A. of_nat(f x))" +lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\x\A. of_nat(f x))" apply (cases "finite A") apply (erule finite_induct, auto simp add: of_nat_mult) done -lemma of_int_setprod: "of_int (setprod f A) = (\x\A. of_int(f x))" +lemma of_int_setprod [simp]: "of_int (setprod f A) = (\x\A. of_int(f x))" apply (cases "finite A") apply (erule finite_induct, auto) done @@ -1401,7 +1401,7 @@ then show "x dvd y" proof (cases k) case (nonneg n) - with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) + with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric]) then show ?thesis .. next case (neg n) @@ -1695,16 +1695,6 @@ lemmas zpower_numeral_even = power_numeral_even [where 'a=int] lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int] -lemma zpower_zpower: - "(x ^ y) ^ z = (x ^ (y * z)::int)" - by (rule power_mult [symmetric]) - -lemma int_power: - "int (m ^ n) = int m ^ n" - by (fact of_nat_power) - -lemmas zpower_int = int_power [symmetric] - text \De-register @{text "int"} as a quotient type:\ lifting_update int.lifting diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Library/Float.thy Fri Nov 13 12:27:13 2015 +0000 @@ -375,7 +375,7 @@ also have "\ = m2 * 2^nat (e2 - e1)" by (simp add: powr_realpow) finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)" - by blast + by linarith with m1 have "m1 = m2" by (cases "nat (e2 - e1)") (auto simp add: dvd_def) then show ?thesis @@ -526,8 +526,10 @@ ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)" by (simp add: powr_realpow[symmetric]) with \e \ exponent f\ - show "m = mantissa f * 2 ^ nat (exponent f - e)" "e = exponent f - nat (exponent f - e)" - by force+ + show "m = mantissa f * 2 ^ nat (exponent f - e)" + by linarith + show "e = exponent f - nat (exponent f - e)" + using `e \ exponent f` by auto qed context @@ -1258,7 +1260,7 @@ case True def x' \ "x * 2 ^ nat l" have "int x * 2 ^ nat l = x'" - by (simp add: x'_def int_mult int_power) + by (simp add: x'_def int_mult of_nat_power) moreover have "real x * 2 powr l = real x'" by (simp add: powr_realpow[symmetric] \0 \ l\ x'_def) ultimately show ?thesis @@ -1271,7 +1273,7 @@ case False def y' \ "y * 2 ^ nat (- l)" from \y \ 0\ have "y' \ 0" by (simp add: y'_def) - have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power) + have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult of_nat_power) moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'" using \\ 0 \ l\ by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps) @@ -1554,7 +1556,7 @@ using bitlen_bounds[of "\m2\"] by (auto simp: powr_add bitlen_nonneg) then show ?thesis - by (metis bitlen_nonneg powr_int real_of_int_abs real_of_int_less_numeral_power_cancel_iff zero_less_numeral) + by (metis bitlen_nonneg powr_int of_int_abs real_of_int_less_numeral_power_cancel_iff zero_less_numeral) qed lemma floor_sum_times_2_powr_sgn_eq: @@ -1984,7 +1986,7 @@ by simp also have "\ \ 2 powr (bitlen \mantissa x\)" using bitlen_bounds[of "\mantissa x\"] bitlen_nonneg \mantissa x \ 0\ - by (auto simp del: real_of_int_abs simp add: powr_int) + by (auto simp del: of_int_abs simp add: powr_int) finally show ?thesis by (simp add: powr_add) qed diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Nov 13 12:27:13 2015 +0000 @@ -3787,10 +3787,8 @@ lemma binomial_Vandermonde: "setsum (\k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n] - apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] - of_nat_setsum[symmetric] of_nat_add[symmetric]) - apply blast - done + by (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] + of_nat_setsum[symmetric] of_nat_add[symmetric] of_nat_eq_iff) lemma binomial_Vandermonde_same: "setsum (\k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n" using binomial_Vandermonde[of n n n, symmetric] diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Fri Nov 13 12:27:13 2015 +0000 @@ -376,7 +376,6 @@ lemma Abs_bit0'_code [code abstract]: "Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))" by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse) - (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int) lemma inj_on_Abs_bit0: "inj_on (Abs_bit0 :: int \ 'a bit0) {0..<2 * int CARD('a :: finite)}" @@ -389,8 +388,7 @@ lemma Abs_bit1'_code [code abstract]: "Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))" -by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse) - (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc) + by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse) lemma inj_on_Abs_bit1: "inj_on (Abs_bit1 :: int \ 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}" @@ -414,7 +412,7 @@ instance proof(intro_classes) show "distinct (enum_class.enum :: 'a bit0 list)" - by(auto intro!: inj_onI simp add: Abs_bit0'_def Abs_bit0_inject zmod_int[symmetric] enum_bit0_def distinct_map) + by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial) show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum" unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric] diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Limits.thy Fri Nov 13 12:27:13 2015 +0000 @@ -89,7 +89,7 @@ lemma BfunE: assumes "Bfun f F" obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) F" -using assms unfolding Bfun_def by fast +using assms unfolding Bfun_def by blast lemma Cauchy_Bseq: "Cauchy X \ Bseq X" unfolding Cauchy_def Bfun_metric_def eventually_sequentially @@ -175,7 +175,10 @@ ultimately have "\m. norm (X m) \ real (Suc n)" by (blast intro: order_trans) then show "\N. \n. norm (X n) \ real (Suc N)" .. -qed (force simp add: of_nat_Suc) +next + show "\N. \n. norm (X n) \ real (Suc N) \ \K>0. \n. norm (X n) \ K" + using of_nat_0_less_iff by blast +qed text\alternative definition for Bseq\ lemma Bseq_iff: "Bseq X = (\N. \n. norm (X n) \ real(Suc N))" @@ -367,7 +370,7 @@ fix r::real assume "0 < r" hence "0 < r / K" using K by simp then have "eventually (\x. norm (f x) < r / K) F" - using ZfunD [OF f] by fast + using ZfunD [OF f] by blast with g show "eventually (\x. norm (g x) < r) F" proof eventually_elim case (elim x) @@ -433,7 +436,7 @@ shows "Zfun (\x. f (g x)) F" proof - obtain K where "\x. norm (f x) \ norm x * K" - using bounded by fast + using bounded by blast then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) F" by simp with g show ?thesis @@ -448,7 +451,7 @@ fix r::real assume r: "0 < r" obtain K where K: "0 < K" and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" - using pos_bounded by fast + using pos_bounded by blast from K have K': "0 < inverse K" by (rule positive_imp_inverse_positive) have "eventually (\x. norm (f x) < r) F" @@ -787,7 +790,7 @@ proof - obtain K where K: "0 \ K" and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" - using nonneg_bounded by fast + using nonneg_bounded by blast obtain B where B: "0 < B" and norm_g: "eventually (\x. norm (g x) \ B) F" using g by (rule BfunE) @@ -816,7 +819,7 @@ apply (rule scaleR_left) apply (subst mult.commute) using bounded - apply fast + apply blast done lemma (in bounded_bilinear) Bfun_prod_Zfun: @@ -840,9 +843,9 @@ proof - from a have "0 < norm a" by simp hence "\r>0. r < norm a" by (rule dense) - then obtain r where r1: "0 < r" and r2: "r < norm a" by fast + then obtain r where r1: "0 < r" and r2: "r < norm a" by blast have "eventually (\x. dist (f x) a < r) F" - using tendstoD [OF f r1] by fast + using tendstoD [OF f r1] by blast hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) F" proof eventually_elim case (elim x) @@ -911,7 +914,7 @@ fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" assumes "continuous_on s f" and "\x\s. f x \ 0" shows "continuous_on s (\x. inverse (f x))" - using assms unfolding continuous_on_def by (fast intro: tendsto_inverse) + using assms unfolding continuous_on_def by (blast intro: tendsto_inverse) lemma tendsto_divide [tendsto_intros]: fixes a b :: "'a::real_normed_field" @@ -941,7 +944,7 @@ fixes f :: "'a::topological_space \ 'b::real_normed_field" assumes "continuous_on s f" "continuous_on s g" and "\x\s. g x \ 0" shows "continuous_on s (\x. (f x) / (g x))" - using assms unfolding continuous_on_def by (fast intro: tendsto_divide) + using assms unfolding continuous_on_def by (blast intro: tendsto_divide) lemma tendsto_sgn [tendsto_intros]: fixes l :: "'a::real_normed_vector" @@ -970,7 +973,7 @@ fixes f :: "'a::topological_space \ 'b::real_normed_vector" assumes "continuous_on s f" and "\x\s. f x \ 0" shows "continuous_on s (\x. sgn (f x))" - using assms unfolding continuous_on_def by (fast intro: tendsto_sgn) + using assms unfolding continuous_on_def by (blast intro: tendsto_sgn) lemma filterlim_at_infinity: fixes f :: "_ \ 'a::real_normed_vector" @@ -1685,7 +1688,7 @@ assumes "convergent (\n. X n)" assumes "convergent (\n. Y n)" shows "convergent (\n. X n + Y n)" - using assms unfolding convergent_def by (fast intro: tendsto_add) + using assms unfolding convergent_def by (blast intro: tendsto_add) lemma convergent_setsum: fixes X :: "'a \ nat \ 'b::real_normed_vector" @@ -1699,12 +1702,12 @@ lemma (in bounded_linear) convergent: assumes "convergent (\n. X n)" shows "convergent (\n. f (X n))" - using assms unfolding convergent_def by (fast intro: tendsto) + using assms unfolding convergent_def by (blast intro: tendsto) lemma (in bounded_bilinear) convergent: assumes "convergent (\n. X n)" and "convergent (\n. Y n)" shows "convergent (\n. X n ** Y n)" - using assms unfolding convergent_def by (fast intro: tendsto) + using assms unfolding convergent_def by (blast intro: tendsto) lemma convergent_minus_iff: fixes X :: "nat \ 'a::real_normed_vector" @@ -1719,7 +1722,7 @@ assumes "convergent (\n. X n)" assumes "convergent (\n. Y n)" shows "convergent (\n. X n - Y n)" - using assms unfolding convergent_def by (fast intro: tendsto_diff) + using assms unfolding convergent_def by (blast intro: tendsto_diff) lemma convergent_norm: assumes "convergent f" @@ -1757,7 +1760,7 @@ assumes "convergent (\n. X n)" assumes "convergent (\n. Y n)" shows "convergent (\n. X n * Y n)" - using assms unfolding convergent_def by (fast intro: tendsto_mult) + using assms unfolding convergent_def by (blast intro: tendsto_mult) lemma convergent_mult_const_iff: assumes "c \ 0" @@ -2122,7 +2125,7 @@ proof (intro allI impI) fix r::real assume r: "0 < r" obtain K where K: "0 < K" and norm_le: "\x. norm (f x) \ norm x * K" - using pos_bounded by fast + using pos_bounded by blast show "\s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r" proof (rule exI, safe) from r K show "0 < r / K" by simp diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Fri Nov 13 12:27:13 2015 +0000 @@ -2399,15 +2399,15 @@ by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma) lemma Re_Arccos_bound: "abs(Re(Arccos z)) \ pi" - using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast + by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff) lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \ pi" unfolding Re_Arcsin by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma) lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \ pi" - using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast - + by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff) + subsection\Interrelations between Arcsin and Arccos\ diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 13 12:27:13 2015 +0000 @@ -2139,7 +2139,7 @@ have *: "\n. \f f'. \x\s. (f has_derivative (f' x)) (at x within s) \ (\h. norm(f' x h - g' x h) \ inverse (real (Suc n)) * norm h)" - by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero) + by (simp add: assms(2)) obtain f where *: "\x. \f'. \xa\s. (f x has_derivative f' xa) (at xa within s) \ (\h. norm (f' xa h - g' xa h) \ inverse (real (Suc x)) * norm h)" @@ -2221,7 +2221,7 @@ have "norm ((\iii e" by simp - hence "norm ((\i e * norm h" + hence "norm ((\i e * norm h" by (intro mult_right_mono) simp_all finally have "norm ((\i e * norm h" . } @@ -2245,9 +2245,9 @@ "\x. x \ s \ (\n. f n x) sums g x" "\x. x \ s \ (g has_field_derivative g' x) (at x within s)" by blast from g(1)[OF \x \ s\] show "summable (\n. f n x)" by (simp add: sums_iff) - from g(2)[OF \x \ s\] \x \ interior s\ have "(g has_field_derivative g' x) (at x)" + from g(2)[OF \x \ s\] \x \ interior s\ have "(g has_field_derivative g' x) (at x)" by (simp add: at_within_interior[of x s]) - also have "(g has_field_derivative g' x) (at x) \ + also have "(g has_field_derivative g' x) (at x) \ ((\x. \n. f n x) has_field_derivative g' x) (at x)" using eventually_nhds_in_nhd[OF \x \ interior s\] interior_subset[of s] g(1) by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff) @@ -2311,7 +2311,7 @@ qed qed (insert f' f'', auto simp: has_vector_derivative_def) then show ?thesis - unfolding fun_eq_iff by auto + unfolding fun_eq_iff by (metis scaleR_one) qed lemma vector_derivative_unique_at: @@ -2350,7 +2350,7 @@ intro: someI frechet_derivative_at [symmetric]) lemma has_real_derivative: - fixes f :: "real \ real" + fixes f :: "real \ real" assumes "(f has_derivative f') F" obtains c where "(f has_real_derivative c) F" proof - @@ -2361,7 +2361,7 @@ qed lemma has_real_derivative_iff: - fixes f :: "real \ real" + fixes f :: "real \ real" shows "(\c. (f has_real_derivative c) F) = (\D. (f has_derivative D) F)" by (metis has_field_derivative_def has_real_derivative) @@ -2390,7 +2390,7 @@ assumes "open s" and t: "t = closure s" "x \ t" shows "x islimpt t" proof cases - assume "x \ s" + assume "x \ s" { fix T assume "x \ T" "open T" then have "open (s \ T)" using \open s\ by auto @@ -2579,7 +2579,7 @@ by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto hence "f y - f c \ (f x - f c) * ((c - y) / (c - x))" by simp also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps) - finally show "(f y - f c) / (y - c) \ (f x - f c) / (x - c)" using y xc + finally show "(f y - f c) / (y - c) \ (f x - f c) / (x - c)" using y xc by (simp add: divide_simps) qed hence "eventually (\y. (f y - f c) / (y - c) \ (f x - f c) / (x - c)) (at c within ?A')" diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 13 12:27:13 2015 +0000 @@ -14,7 +14,8 @@ lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *) fixes S :: "real set" shows "S \ {} \ (\x. x\S \ \x\ \ a) \ \Sup S\ \ a" - by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI) + apply (auto simp add: abs_le_iff intro: cSup_least) + by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans) lemma cInf_abs_ge: fixes S :: "real set" diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/NSA/NSA.thy Fri Nov 13 12:27:13 2015 +0000 @@ -1243,7 +1243,9 @@ apply (frule lemma_st_part1a) apply (frule_tac [4] lemma_st_part2a, auto) apply (drule order_le_imp_less_or_eq)+ -apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff) +apply auto +using lemma_st_part_not_eq2 apply fastforce +using lemma_st_part_not_eq1 apply fastforce done lemma lemma_st_part_major2: @@ -1252,6 +1254,7 @@ by (blast dest!: lemma_st_part_major) + text{*Existence of real and Standard Part Theorem*} lemma lemma_st_part_Ex: "(x::hypreal) \ HFinite @@ -1778,7 +1781,7 @@ done lemma st_SReal_eq: "x \ \ ==> st x = x" - by (metis approx_refl st_unique) + by (metis approx_refl st_unique) lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x" by (rule SReal_hypreal_of_real [THEN st_SReal_eq]) @@ -2022,7 +2025,7 @@ lemma lemma_Infinitesimal: "(\r. 0 < r --> x < r) = (\n. x < inverse(real (Suc n)))" -apply (auto simp add: real_of_nat_Suc_gt_zero simp del: of_nat_Suc) +apply (auto simp del: of_nat_Suc) apply (blast dest!: reals_Archimedean intro: order_less_trans) done @@ -2031,10 +2034,8 @@ (\n. x < inverse(hypreal_of_nat (Suc n)))" apply safe apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec) - apply (simp (no_asm_use)) - apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE]) - prefer 2 apply assumption - apply simp + apply simp_all + using less_imp_of_nat_less apply fastforce apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc) apply (drule star_of_less [THEN iffD2]) apply simp @@ -2077,7 +2078,7 @@ by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real) lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \ u}" -apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real) +apply (simp (no_asm) add: finite_real_of_nat_le_real) done lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: @@ -2133,7 +2134,7 @@ apply (simp add: inverse_eq_divide) apply (subst pos_less_divide_eq, assumption) apply (subst pos_less_divide_eq) - apply (simp add: real_of_nat_Suc_gt_zero) + apply simp apply (simp add: mult.commute) done @@ -2153,7 +2154,7 @@ lemma finite_inverse_real_of_posnat_ge_real: "0 < u ==> finite {n. u \ inverse(real(Suc n))}" -by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real +by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real simp del: of_nat_Suc) lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: @@ -2181,8 +2182,8 @@ lemma SEQ_Infinitesimal: "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" -by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff - real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc) +by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff + FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc) text{* Example where we get a hyperreal from a real sequence for which a particular property holds. The theorem is @@ -2198,7 +2199,7 @@ "\n. norm(X n - x) < inverse(real(Suc n)) ==> star_n X - star_of x \ Infinitesimal" unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse -by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat +by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat intro: order_less_trans elim!: eventually_elim1) lemma real_seq_to_hypreal_approx: diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Nat.thy Fri Nov 13 12:27:13 2015 +0000 @@ -1469,7 +1469,7 @@ lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" by (induct m) (simp_all add: ac_simps) -lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n" +lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n" by (induct m) (simp_all add: ac_simps distrib_right) lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x" diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Nat_Transfer.thy --- a/src/HOL/Nat_Transfer.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Nat_Transfer.thy Fri Nov 13 12:27:13 2015 +0000 @@ -203,11 +203,9 @@ lemma transfer_nat_int_sum_prod2: "setsum f A = nat(setsum (%x. int (f x)) A)" "setprod f A = nat(setprod (%x. int (f x)) A)" - apply (subst int_setsum [symmetric]) - apply auto - apply (subst int_setprod [symmetric]) - apply auto -done + apply (simp only: int_setsum [symmetric] nat_int) + apply (simp only: int_setprod [symmetric] nat_int) + done lemma transfer_nat_int_sum_prod_closure: "nat_set A \ (!!x. x >= 0 \ f x >= (0::int)) \ setsum f A >= 0" @@ -288,7 +286,7 @@ "(int x) * (int y) = int (x * y)" "tsub (int x) (int y) = int (x - y)" "(int x)^n = int (x^n)" - by (auto simp add: int_mult tsub_def int_power) + by (auto simp add: int_mult tsub_def of_nat_power) lemma transfer_int_nat_function_closures: "is_nat x \ is_nat y \ is_nat (x + y)" @@ -411,9 +409,7 @@ "(!!x. x:A \ is_nat (f x)) \ setprod f A = int(setprod (%x. nat (f x)) A)" unfolding is_nat_def - apply (subst int_setsum, auto) - apply (subst int_setprod, auto simp add: cong: setprod.cong) -done + by (subst int_setsum) auto declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2 diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/NthRoot.thy Fri Nov 13 12:27:13 2015 +0000 @@ -257,7 +257,7 @@ have "continuous_on ({0..} \ {.. 0}) (\x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)" using n by (intro continuous_on_If continuous_intros) auto then have "continuous_on UNIV ?f" - by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n) + by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less sgn_neg le_less n) then have [simp]: "\x. isCont ?f x" by (simp add: continuous_on_eq_continuous_at) @@ -697,7 +697,7 @@ (simp_all add: at_infinity_eq_at_top_bot) { fix n :: nat assume "1 < n" have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" - using \1 < n\ unfolding gbinomial_def binomial_gbinomial by simp + using \1 < n\ unfolding gbinomial_def binomial_gbinomial by simp also have "\ \ (\k\{0, 1}. of_nat (n choose k) * x n^k)" by (simp add: x_def) also have "\ \ (\k=0..n. of_nat (n choose k) * x n^k)" @@ -741,8 +741,4 @@ lemmas real_sqrt_mult_distrib2 = real_sqrt_mult lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff -(* needed for CauchysMeanTheorem.het_base from AFP *) -lemma real_root_pos: "0 < x \ root (Suc n) (x ^ (Suc n)) = x" -by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le]) - end diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Number_Theory/Fib.thy --- a/src/HOL/Number_Theory/Fib.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Number_Theory/Fib.thy Fri Nov 13 12:27:13 2015 +0000 @@ -51,7 +51,7 @@ lemma fib_Cassini_nat: "fib (Suc (Suc n)) * fib n = (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)" - using fib_Cassini_int [of n] by auto + using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power) subsection \Law 6.111 of Concrete Mathematics\ diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Old_Number_Theory/Euler.thy --- a/src/HOL/Old_Number_Theory/Euler.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Old_Number_Theory/Euler.thy Fri Nov 13 12:27:13 2015 +0000 @@ -284,7 +284,7 @@ apply (metis zprime_zOdd_eq_grt_2) apply (frule aux__1, auto) apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower) - apply (auto simp add: zpower_zpower) + apply (auto simp add: power_mult [symmetric]) apply (rule zcong_trans) apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]) apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2) diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Old_Number_Theory/EvenOdd.thy --- a/src/HOL/Old_Number_Theory/EvenOdd.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Fri Nov 13 12:27:13 2015 +0000 @@ -176,7 +176,7 @@ finally have "(-1::int)^nat x = (-1)^(2 * nat a)" by simp also have "... = (-1::int)\<^sup>2 ^ nat a" - by (simp add: zpower_zpower [symmetric]) + by (simp add: power_mult) also have "(-1::int)\<^sup>2 = 1" by simp finally show ?thesis diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Old_Number_Theory/WilsonRuss.thy --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri Nov 13 12:27:13 2015 +0000 @@ -133,7 +133,7 @@ 5 \ p \ 0 < a \ a < p ==> inv p (inv p a) = a" apply (unfold inv_def) apply (subst power_mod) - apply (subst zpower_zpower) + apply (subst power_mult [symmetric]) apply (rule zcong_zless_imp_eq) prefer 5 apply (subst zcong_zmod) diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Power.thy --- a/src/HOL/Power.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Power.thy Fri Nov 13 12:27:13 2015 +0000 @@ -175,7 +175,7 @@ context semiring_1 begin -lemma of_nat_power: +lemma of_nat_power [simp]: "of_nat (m ^ n) = of_nat m ^ n" by (induct n) (simp_all add: of_nat_mult) @@ -310,7 +310,7 @@ lemma power_minus1_odd: "(- 1) ^ Suc (2*n) = -1" by simp - + lemma power_minus_even [simp]: "(-a) ^ (2*n) = a ^ (2*n)" by (simp add: power_minus [of a]) @@ -320,7 +320,7 @@ context ring_1_no_zero_divisors begin -subclass semiring_1_no_zero_divisors .. +subclass semiring_1_no_zero_divisors .. lemma power2_eq_1_iff: "a\<^sup>2 = 1 \ a = 1 \ a = - 1" @@ -377,7 +377,7 @@ "(1 / a) ^ n = 1 / a ^ n" using power_inverse [of a] by (simp add: divide_inverse) -end +end context field begin @@ -463,6 +463,10 @@ qed qed +lemma of_nat_zero_less_power_iff [simp]: + "of_nat x ^ n > 0 \ x > 0 \ n = 0" + by (induct n) auto + text\Surely we can strengthen this? It holds for @{text "0 lemma power_inject_exp [simp]: "1 < a \ a ^ m = a ^ n \ m = n" @@ -491,7 +495,7 @@ proof (induct N) case 0 then show ?case by simp next - case (Suc N) then show ?case + case (Suc N) then show ?case apply (auto simp add: power_Suc_less less_Suc_eq) apply (subgoal_tac "a * a^N < 1 * a^n") apply simp @@ -505,7 +509,7 @@ proof (induct N) case 0 then show ?case by simp next - case (Suc N) then show ?case + case (Suc N) then show ?case apply (auto simp add: le_Suc_eq) apply (subgoal_tac "a * a^N \ 1 * a^n", simp) apply (rule mult_mono) apply auto @@ -522,7 +526,7 @@ proof (induct N) case 0 then show ?case by simp next - case (Suc N) then show ?case + case (Suc N) then show ?case apply (auto simp add: le_Suc_eq) apply (subgoal_tac "1 * a^n \ a * a^N", simp) apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one]) @@ -539,7 +543,7 @@ proof (induct N) case 0 then show ?case by simp next - case (Suc N) then show ?case + case (Suc N) then show ?case apply (auto simp add: power_less_power_Suc less_Suc_eq) apply (subgoal_tac "1 * a^n < a * a^N", simp) apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) @@ -552,7 +556,7 @@ lemma power_strict_increasing_iff [simp]: "1 < b \ b ^ x < b ^ y \ x < y" -by (blast intro: power_less_imp_less_exp power_strict_increasing) +by (blast intro: power_less_imp_less_exp power_strict_increasing) lemma power_le_imp_le_base: assumes le: "a ^ Suc n \ b ^ Suc n" @@ -680,7 +684,7 @@ lemma odd_0_le_power_imp_0_le: "0 \ a ^ Suc (2*n) \ 0 \ a" using odd_power_less_zero [of a n] - by (force simp add: linorder_not_less [symmetric]) + by (force simp add: linorder_not_less [symmetric]) lemma zero_le_even_power'[simp]: "0 \ a ^ (2*n)" @@ -689,7 +693,7 @@ show ?case by simp next case (Suc n) - have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" + have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" by (simp add: ac_simps power_add power2_eq_square) thus ?case by (simp add: Suc zero_le_mult_iff) @@ -733,7 +737,7 @@ lemma abs_square_eq_1: "x\<^sup>2 = 1 \ abs(x) = 1" by (auto simp add: abs_if power2_eq_1_iff) - + lemma abs_square_less_1: "x\<^sup>2 < 1 \ abs(x) < 1" using abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less) @@ -768,10 +772,10 @@ lemmas zero_compare_simps = add_strict_increasing add_strict_increasing2 add_increasing - zero_le_mult_iff zero_le_divide_iff - zero_less_mult_iff zero_less_divide_iff - mult_le_0_iff divide_le_0_iff - mult_less_0_iff divide_less_0_iff + zero_le_mult_iff zero_le_divide_iff + zero_less_mult_iff zero_less_divide_iff + mult_le_0_iff divide_le_0_iff + mult_less_0_iff divide_less_0_iff zero_le_power2 power2_less_0 @@ -785,7 +789,7 @@ "x ^ n > 0 \ x > (0::nat) \ n = 0" by (induct n) auto -lemma nat_power_eq_Suc_0_iff [simp]: +lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \ m = 0 \ x = Suc 0" by (induct m) auto @@ -842,13 +846,13 @@ lemma card_Pow: "finite A \ card (Pow A) = 2 ^ card A" proof (induct rule: finite_induct) - case empty + case empty show ?case by auto next case (insert x A) - then have "inj_on (insert x) (Pow A)" + then have "inj_on (insert x) (Pow A)" unfolding inj_on_def by (blast elim!: equalityE) - then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" + then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" by (simp add: mult_2 card_image Pow_insert insert.hyps) then show ?case using insert apply (simp add: Pow_insert) @@ -882,11 +886,11 @@ lemma setprod_power_distrib: fixes f :: "'a \ 'b::comm_semiring_1" shows "setprod f A ^ n = setprod (\x. (f x) ^ n) A" -proof (cases "finite A") - case True then show ?thesis +proof (cases "finite A") + case True then show ?thesis by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) next - case False then show ?thesis + case False then show ?thesis by simp qed @@ -902,13 +906,13 @@ {assume a: "a \ S" hence "\ k\ S. ?f k = c" by simp hence ?thesis using a setprod_constant[OF fS, of c] by simp } - moreover + moreover {assume a: "a \ S" let ?A = "S - {a}" let ?B = "{a}" - have eq: "S = ?A \ ?B" using a by blast + have eq: "S = ?A \ ?B" using a by blast have dj: "?A \ ?B = {}" by simp - from fS have fAB: "finite ?A" "finite ?B" by auto + from fS have fAB: "finite ?A" "finite ?B" by auto have fA0:"setprod ?f ?A = setprod (\i. c) ?A" apply (rule setprod.cong) by auto have cA: "card ?A = card S - 1" using fS a by auto diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Nov 13 12:27:13 2015 +0000 @@ -471,7 +471,7 @@ using entropy_le_card[of "t\OB", OF simple_distributedI[OF simple_function_finite refl]] by simp also have "\ \ log b (real (n + 1)^card observations)" using card_T_bound not_empty - by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: of_nat_power of_nat_Suc) + by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc) also have "\ = real (card observations) * log b (real n + 1)" by (simp add: log_nat_power add.commute) finally show ?thesis . diff -r b1c24adc1581 -r 268d88ec9087 src/HOL/Real.thy --- a/src/HOL/Real.thy Thu Nov 12 11:22:26 2015 +0100 +++ b/src/HOL/Real.thy Fri Nov 13 12:27:13 2015 +0000 @@ -114,7 +114,7 @@ proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a where a: "0 < a" "\n. \X n\ < a" - using X by fast + using X by blast obtain b where b: "0 < b" "r = a * b" proof show "0 < r / a" using r a by simp @@ -217,9 +217,9 @@ then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v" by (rule obtain_pos_sum) obtain a where a: "0 < a" "\