--- a/src/HOL/Complex/CLim.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Complex/CLim.thy Thu Oct 07 15:42:30 2004 +0200
@@ -1014,16 +1014,11 @@
\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
-(* FIXME tidy! How about a NS proof? *)
lemma CARAT_CDERIVD:
"(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
==> NSCDERIV f x :> l"
-apply (simp only: NSCDERIV_iff2)
-apply (tactic {*(auto_tac (claset(),
- simpset() delsimprocs field_cancel_factor
- addsimps [thm"NSCDERIV_iff2"])) *})
-apply (simp add: isNSContc_def)
-done
+by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq);
+
ML
{*
--- a/src/HOL/Complex/CStar.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Complex/CStar.thy Thu Oct 07 15:42:30 2004 +0200
@@ -218,6 +218,13 @@
apply (auto iff add: hcomplexrel_iff, ultra)
done
+lemma cstarfun_if_eq:
+ "w \<noteq> hcomplex_of_complex x
+ ==> ( *fc* (\<lambda>z. if z = x then a else g z)) w = ( *fc* g) w"
+apply (cases w)
+apply (simp add: hcomplex_of_complex_def starfunC, ultra)
+done
+
lemma starfunRC:
"( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) =
Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"
--- a/src/HOL/Complex/Complex.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Complex/Complex.thy Thu Oct 07 15:42:30 2004 +0200
@@ -212,10 +212,10 @@
lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
apply (induct z)
apply (rename_tac x y)
-apply (auto simp add: complex_mult complex_inverse complex_one_def
- complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
-apply (drule_tac y = y in real_sum_squares_not_zero)
-apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
+apply (auto simp add: times_divide_eq complex_mult complex_inverse
+ complex_one_def complex_zero_def add_divide_distrib [symmetric]
+ power2_eq_square mult_ac)
+apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2)
done
--- a/src/HOL/Finite_Set.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Finite_Set.thy Thu Oct 07 15:42:30 2004 +0200
@@ -1297,7 +1297,7 @@
apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
apply (erule ssubst)
apply (subst times_divide_eq_right [THEN sym])
- apply (auto simp add: mult_ac divide_self)
+ apply (auto simp add: mult_ac times_divide_eq_right divide_self)
done
lemma setprod_inversef: "finite A ==>
--- a/src/HOL/Hyperreal/HTranscendental.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Thu Oct 07 15:42:30 2004 +0200
@@ -386,14 +386,12 @@
lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
apply (cases x)
apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
-apply (auto dest: ln_not_eq_zero)
done
lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
apply (rule HFinite_bounded)
-apply (rule_tac [2] order_less_imp_le)
-apply (rule_tac [2] starfun_ln_less_self)
-apply (rule_tac [2] order_less_le_trans, auto)
+apply assumption
+apply (simp_all add: starfun_ln_less_self order_less_imp_le)
done
lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
@@ -453,7 +451,6 @@
lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
apply (cases x)
apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
-apply (auto intro: ln_less_zero)
done
lemma starfun_ln_Infinitesimal_less_zero:
--- a/src/HOL/Hyperreal/HyperDef.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Thu Oct 07 15:42:30 2004 +0200
@@ -506,9 +506,7 @@
qed
lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
-apply auto
-apply (rule OrderedGroup.add_right_cancel [of _ "-y", THEN iffD1], auto)
-done
+by auto
lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
by auto
--- a/src/HOL/Hyperreal/Integration.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Thu Oct 07 15:42:30 2004 +0200
@@ -432,7 +432,7 @@
apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
prefer 2 apply simp
apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
-apply (drule_tac x = v in spec, simp)
+apply (drule_tac x = v in spec, simp add: times_divide_eq)
apply (drule_tac x = u in spec, auto, arith)
apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
apply (rule order_trans)
--- a/src/HOL/Hyperreal/Lim.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Thu Oct 07 15:42:30 2004 +0200
@@ -277,7 +277,7 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
+apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
apply (auto simp add: starfun hypreal_minus hypreal_of_real_def hypreal_add)
apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def hypreal_minus hypreal_add, blast)
@@ -603,10 +603,12 @@
\<bar>z + -y\<bar> < inverse(real(Suc n)) &
r \<le> \<bar>f z + -f y\<bar>"
apply clarify
-apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
+apply (cut_tac n1 = n
+ in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
done
-lemma lemma_skolemize_LIM2u: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
+lemma lemma_skolemize_LIM2u:
+ "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
==> \<exists>X Y. \<forall>n::nat.
abs(X n + -(Y n)) < inverse(real(Suc n)) &
r \<le> abs(f (X n) + -f (Y n))"
@@ -627,8 +629,8 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2u, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
-apply (drule_tac x = "Abs_hypreal (hyprel``{Y}) " in spec)
+apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
+apply (drule_tac x = "Abs_hypreal (hyprel``{Y})" in spec)
apply (simp add: starfun hypreal_minus hypreal_add, auto)
apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
@@ -778,7 +780,7 @@
apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
-apply (auto simp add: diff_minus
+apply (auto simp add: times_divide_eq_left diff_minus
approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
Infinitesimal_subset_HFinite [THEN subsetD])
done
@@ -794,7 +796,7 @@
apply (drule_tac x = h in bspec)
apply (drule_tac [2] c = h in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
- simp add: diff_minus)
+ simp add: times_divide_eq_left diff_minus)
done
lemma NSDERIVD3:
@@ -806,7 +808,7 @@
apply (rule ccontr, drule_tac x = h in bspec)
apply (drule_tac [2] c = h in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
- simp add: mult_assoc diff_minus)
+ simp add: mult_assoc times_divide_eq_left diff_minus)
done
text{*Now equivalence between NSDERIV and DERIV*}
@@ -821,14 +823,14 @@
apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
apply (drule_tac x = "-hypreal_of_real x + xa" in bspec)
prefer 2 apply (simp add: add_assoc [symmetric])
-apply (auto simp add: mem_infmal_iff [symmetric] hypreal_add_commute)
+apply (auto simp add: mem_infmal_iff [symmetric] add_commute)
apply (drule_tac c = "xa + -hypreal_of_real x" in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
simp add: mult_assoc)
apply (drule_tac x3=D in
HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
THEN mem_infmal_iff [THEN iffD1]])
-apply (auto simp add: mult_commute
+apply (auto simp add: times_divide_eq_right mult_commute
intro: approx_trans approx_minus_iff [THEN iffD2])
done
@@ -877,9 +879,9 @@
z \<in> Infinitesimal; yb \<in> Infinitesimal |]
==> x + y \<approx> 0"
apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
-apply (erule_tac V = " (x + y) / z = hypreal_of_real D + yb" in thin_rl)
+apply (erule_tac V = "(x + y) / z = hypreal_of_real D + yb" in thin_rl)
apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
- simp add: hypreal_mult_assoc mem_infmal_iff [symmetric])
+ simp add: times_divide_eq_left mult_assoc mem_infmal_iff [symmetric])
apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
done
@@ -891,7 +893,8 @@
simp add: starfun_lambda_cancel lemma_nsderiv1)
apply (simp (no_asm) add: add_divide_distrib)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
-apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
+apply (auto simp add: times_divide_eq_right [symmetric]
+ simp del: times_divide_eq)
apply (drule_tac D = Db in lemma_nsderiv2)
apply (drule_tac [4]
approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
@@ -989,7 +992,7 @@
in hypreal_mult_right_cancel [THEN iffD2])
apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) + - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
apply assumption
-apply (simp add: times_divide_eq_right [symmetric] del: times_divide_eq_right)
+apply (simp add: times_divide_eq_left times_divide_eq_right [symmetric])
apply (auto simp add: left_distrib)
done
@@ -1116,7 +1119,7 @@
apply (auto simp add: real_of_nat_Suc left_distrib)
apply (case_tac "0 < n")
apply (drule_tac x = x in realpow_minus_mult)
-apply (auto simp add: real_mult_assoc real_add_commute)
+apply (auto simp add: mult_assoc add_commute)
done
(* NS version *)
@@ -1140,7 +1143,7 @@
minus_mult_left [symmetric] minus_mult_right [symmetric])
apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
del: minus_mult_left [symmetric] minus_mult_right [symmetric])
-apply (rule_tac y = " inverse (- hypreal_of_real x * hypreal_of_real x) " in approx_trans)
+apply (rule_tac y = "inverse (- hypreal_of_real x * hypreal_of_real x)" in approx_trans)
apply (rule inverse_add_Infinitesimal_approx2)
apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
@@ -1194,7 +1197,7 @@
show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
proof (intro exI conjI)
let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
- show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
+ show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp add: times_divide_eq)
show "isCont ?g x" using der
by (simp add: isCont_iff DERIV_iff diff_minus
cong: LIM_equal [rule_format])
@@ -1231,10 +1234,8 @@
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
qed
-(*--------------------------------------------------------------------------*)
-(* Lemmas about nested intervals and proof by bisection (cf.Harrison) *)
-(* All considerably tidied by lcp *)
-(*--------------------------------------------------------------------------*)
+text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
+ All considerably tidied by lcp.*}
lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) --> f m \<le> f(m + no)"
apply (induct_tac "no")
@@ -1248,7 +1249,7 @@
apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
apply (induct_tac "n")
apply (auto intro: order_trans)
-apply (rule_tac y = "g (Suc na) " in order_trans)
+apply (rule_tac y = "g (Suc na)" in order_trans)
apply (induct_tac [2] "na")
apply (auto intro: order_trans)
done
@@ -1258,7 +1259,7 @@
\<forall>n. f(n) \<le> g(n) |]
==> Bseq g"
apply (subst Bseq_minus_iff [symmetric])
-apply (rule_tac g = "%x. - (f x) " in f_inc_g_dec_Beq_f)
+apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
apply auto
done
@@ -1282,7 +1283,7 @@
lemma g_dec_imp_lim_le: "[| \<forall>n. g(Suc n) \<le> g(n); convergent g |] ==> lim g \<le> g n"
apply (subgoal_tac "- (g n) \<le> - (lim g) ")
-apply (cut_tac [2] f = "%x. - (g x) " in f_inc_imp_le_lim)
+apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
done
@@ -1335,13 +1336,13 @@
\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
apply (rule allI)
apply (induct_tac "n")
-apply (auto simp add: Bolzano_bisect_le Let_def split_def)
+apply (auto simp add: Bolzano_bisect_le Let_def split_def times_divide_eq)
done
-lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
-apply auto
+lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
+apply (auto simp add: times_divide_eq)
apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
-apply auto
+apply (simp add: times_divide_eq)
done
lemma Bolzano_bisect_diff:
@@ -1403,7 +1404,7 @@
apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
apply safe
apply (simp_all (no_asm_simp))
-apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l) " in order_le_less_trans)
+apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l)" in order_le_less_trans)
apply (simp (no_asm_simp) add: abs_if)
apply (rule real_sum_of_halves [THEN subst])
apply (rule add_strict_mono)
@@ -1438,7 +1439,7 @@
apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
apply (drule_tac x = x in spec)+
apply simp
-apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar> " in spec)
+apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
apply safe
apply simp
apply (drule_tac x = s in spec, clarify)
@@ -1471,15 +1472,12 @@
apply (blast intro: IVT2)
done
-(*---------------------------------------------------------------------------*)
-(* By bisection, function continuous on closed interval is bounded above *)
-(*---------------------------------------------------------------------------*)
-
+subsection{*By bisection, function continuous on closed interval is bounded above*}
lemma isCont_bounded:
"[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
-apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M) " in lemma_BOLZANO2)
+apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
apply safe
apply simp_all
apply (rename_tac x xa ya M Ma)
@@ -1501,19 +1499,17 @@
apply (auto simp add: abs_ge_self, arith+)
done
-(*----------------------------------------------------------------------------*)
-(* Refine the above to existence of least upper bound *)
-(*----------------------------------------------------------------------------*)
+text{*Refine the above to existence of least upper bound*}
lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) -->
(\<exists>t. isLub UNIV S t)"
-apply (blast intro: reals_complete)
-done
+by (blast intro: reals_complete)
lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
(\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
-apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x) " in lemma_reals_complete)
+apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
+ in lemma_reals_complete)
apply auto
apply (drule isCont_bounded, assumption)
apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
@@ -1521,9 +1517,7 @@
apply (auto dest!: spec simp add: linorder_not_less)
done
-(*----------------------------------------------------------------------------*)
-(* Now show that it attains its upper bound *)
-(*----------------------------------------------------------------------------*)
+text{*Now show that it attains its upper bound*}
lemma isCont_eq_Ub:
assumes le: "a \<le> b"
@@ -1565,25 +1559,20 @@
qed
-
-(*----------------------------------------------------------------------------*)
-(* Same theorem for lower bound *)
-(*----------------------------------------------------------------------------*)
+text{*Same theorem for lower bound*}
lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
(\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
prefer 2 apply (blast intro: isCont_minus)
-apply (drule_tac f = " (%x. - (f x))" in isCont_eq_Ub)
+apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub)
apply safe
apply auto
done
-(* ------------------------------------------------------------------------- *)
-(* Another version. *)
-(* ------------------------------------------------------------------------- *)
+text{*Another version.*}
lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
@@ -1821,7 +1810,8 @@
hence ba: "b-a \<noteq> 0" by arith
show ?thesis
by (rule real_mult_left_cancel [OF ba, THEN iffD1],
- simp add: right_diff_distrib, simp add: left_diff_distrib)
+ simp add: times_divide_eq right_diff_distrib,
+ simp add: left_diff_distrib)
qed
theorem MVT:
@@ -1856,7 +1846,8 @@
proof (intro exI conjI)
show "a < z" .
show "z < b" .
- show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by simp
+ show "f b - f a = (b - a) * ((f b - f a)/(b-a))"
+ by (simp add: times_divide_eq)
show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp
qed
qed
@@ -1906,14 +1897,14 @@
lemma DERIV_const_ratio_const2:
"[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
-apply (auto dest!: DERIV_const_ratio_const simp add: real_mult_assoc)
+apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc times_divide_eq)
done
lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
-by auto
+by (simp add: times_divide_eq)
lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
-by auto
+by (simp add: times_divide_eq)
text{*Gallileo's "trick": average velocity = av. of end velocities*}
--- a/src/HOL/Hyperreal/MacLaurin.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Thu Oct 07 15:42:30 2004 +0200
@@ -38,10 +38,11 @@
"0 < h ==>
\<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
(B * ((h^n) / real(fact n)))"
-by (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
+apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
real(fact n) / (h^n)"
- in exI, auto)
-
+ in exI)
+apply (simp add: times_divide_eq)
+done
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
by arith
@@ -159,12 +160,12 @@
prefer 2 apply simp
apply (frule Maclaurin_lemma2, assumption+)
apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
-apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
-apply (erule impE)
-apply (simp (no_asm_simp))
-apply (erule exE)
-apply (rule_tac x = t in exI)
-apply (simp del: realpow_Suc fact_Suc)
+ apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
+ apply (erule impE)
+ apply (simp (no_asm_simp))
+ apply (erule exE)
+ apply (rule_tac x = t in exI)
+ apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
prefer 2
apply clarify
@@ -254,7 +255,7 @@
apply (cut_tac f = "%x. f (-x)"
and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
and h = "-h" and n = n in Maclaurin_objl)
-apply simp
+apply (simp add: times_divide_eq)
apply safe
apply (subst minus_mult_right)
apply (rule DERIV_cmult)
@@ -303,7 +304,7 @@
apply (case_tac "n = 0", force)
apply (case_tac "x = 0")
apply (rule_tac x = 0 in exI)
-apply (force simp add: Maclaurin_bi_le_lemma)
+apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
txt{*Case 1, where @{term "x < 0"}*}
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
@@ -414,27 +415,8 @@
"0 < n --> Suc (2 * n - 1) = 2*n"
by (induct_tac "n", auto)
-lemma Maclaurin_sin_expansion:
- "\<exists>t. sin x =
- (sumr 0 n (%m. (if even m then 0
- else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
- x ^ m))
- + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
-apply (cut_tac f = sin and n = n and x = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
-apply safe
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (case_tac "n", clarify, simp)
-apply (drule_tac x = 0 in spec, simp, simp)
-apply (rule ccontr, simp)
-apply (drule_tac x = x in spec, simp)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
-(*Could sin_zero_iff help?*)
-done
+
+text{*It is unclear why so many variant results are needed.*}
lemma Maclaurin_sin_expansion2:
"\<exists>t. abs t \<le> abs x &
@@ -447,17 +429,28 @@
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
apply (case_tac "n", clarify, simp, simp)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
done
+lemma Maclaurin_sin_expansion:
+ "\<exists>t. sin x =
+ (sumr 0 n (%m. (if even m then 0
+ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+ x ^ m))
+ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+apply (insert Maclaurin_sin_expansion2 [of x n])
+apply (blast intro: elim:);
+done
+
+
+
lemma Maclaurin_sin_expansion3:
"[| 0 < n; 0 < x |] ==>
\<exists>t. 0 < t & t < x &
@@ -469,12 +462,11 @@
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
done
lemma Maclaurin_sin_expansion4:
@@ -488,12 +480,11 @@
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
done
@@ -518,7 +509,7 @@
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
apply (case_tac "n", simp)
apply (simp del: sumr_Suc)
apply (rule ccontr, simp)
@@ -526,9 +517,7 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
done
lemma Maclaurin_cos_expansion2:
@@ -543,16 +532,15 @@
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
done
-lemma Maclaurin_minus_cos_expansion: "[| x < 0; 0 < n |] ==>
+lemma Maclaurin_minus_cos_expansion:
+ "[| x < 0; 0 < n |] ==>
\<exists>t. x < t & t < 0 &
cos x =
(sumr 0 n (%m. (if even m
@@ -563,13 +551,11 @@
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
done
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Hyperreal/NSA.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Thu Oct 07 15:42:30 2004 +0200
@@ -324,10 +324,8 @@
apply (frule hrabs_less_gt_zero)
apply (drule_tac x = "r/t" in bspec)
apply (blast intro: SReal_divide)
-apply (simp add: zero_less_divide_iff)
-apply (case_tac "x=0 | y=0")
-apply (cut_tac [2] a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
-apply (auto simp add: zero_less_divide_iff)
+apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
+apply (auto simp add: times_divide_eq_left zero_less_divide_iff)
done
lemma Infinitesimal_HFinite_mult2:
--- a/src/HOL/Hyperreal/Series.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy Thu Oct 07 15:42:30 2004 +0200
@@ -259,11 +259,12 @@
lemma sumr_pos_lt_pair:
- "[|summable f; \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]
+ "[|summable f;
+ \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]
==> sumr 0 n f < suminf f"
apply (drule summable_sums)
apply (auto simp add: sums_def LIMSEQ_def)
-apply (drule_tac x = "f (n) + f (n + 1) " in spec)
+apply (drule_tac x = "f (n) + f (n + 1)" in spec)
apply (auto iff: real_0_less_add_iff)
--{*legacy proof: not necessarily better!*}
apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
@@ -312,17 +313,18 @@
lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
apply (induct_tac "n", auto)
apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
-apply (auto simp add: real_mult_assoc left_distrib)
-apply (simp add: right_distrib real_diff_def real_mult_commute)
+apply (auto simp add: mult_assoc left_distrib times_divide_eq)
+apply (simp add: right_distrib diff_minus mult_commute)
done
lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
apply (case_tac "x = 1")
-apply (auto dest!: LIMSEQ_rabs_realpow_zero2 simp add: sumr_geometric sums_def real_diff_def add_divide_distrib)
+apply (auto dest!: LIMSEQ_rabs_realpow_zero2
+ simp add: sumr_geometric sums_def diff_minus add_divide_distrib)
apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ")
apply (erule ssubst)
apply (rule LIMSEQ_add, rule LIMSEQ_divide)
-apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
+apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
done
text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
@@ -433,18 +435,19 @@
"[| c < 1; \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]
==> summable f"
apply (frule ratio_test_lemma2, auto)
-apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" in summable_comparison_test)
+apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n"
+ in summable_comparison_test)
apply (rule_tac x = N in exI, safe)
apply (drule le_Suc_ex_iff [THEN iffD1])
apply (auto simp add: power_add realpow_not_zero)
-apply (induct_tac "na", auto)
+apply (induct_tac "na", auto simp add: times_divide_eq)
apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
apply (auto intro: mult_right_mono simp add: summable_def)
apply (simp add: mult_ac)
-apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N) " in exI)
-apply (rule sums_divide)
-apply (rule sums_mult)
-apply (auto intro!: sums_mult geometric_sums simp add: abs_if)
+apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
+apply (rule sums_divide)
+apply (rule sums_mult)
+apply (auto intro!: geometric_sums)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Thu Oct 07 15:42:30 2004 +0200
@@ -424,9 +424,8 @@
apply (subgoal_tac "x \<noteq> 0")
apply (subgoal_tac [3] "x \<noteq> 0")
apply (auto simp del: abs_inverse abs_mult simp add: abs_inverse [symmetric] realpow_not_zero abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
-apply (auto intro!: geometric_sums simp add: power_abs inverse_eq_divide)
-apply (rule_tac c="\<bar>x\<bar>" in mult_right_less_imp_less)
-apply (auto simp add: abs_mult [symmetric] mult_assoc)
+apply (auto intro!: geometric_sums
+ simp add: power_abs inverse_eq_divide times_divide_eq)
done
lemma powser_inside:
@@ -912,7 +911,7 @@
hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
by (auto simp add: exp_add exp_minus)
thus ?thesis
- by (simp add: divide_inverse [symmetric] pos_less_divide_eq
+ by (simp add: divide_inverse [symmetric] pos_less_divide_eq times_divide_eq
del: divide_self_if)
qed
@@ -1008,7 +1007,7 @@
apply (rule ln_less_cancel_iff [THEN iffD2], auto)
done
-lemma ln_ge_zero:
+lemma ln_ge_zero [simp]:
assumes x: "1 \<le> x" shows "0 \<le> ln x"
proof -
have "0 < x" using x by arith
@@ -1029,6 +1028,9 @@
lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
+lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
+by (insert ln_ge_zero_iff [of x], arith)
+
lemma ln_gt_zero:
assumes x: "1 < x" shows "0 < ln x"
proof -
@@ -1050,16 +1052,11 @@
lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
-lemma ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ln x \<noteq> 0"
-apply safe
-apply (drule exp_inj_iff [THEN iffD2])
-apply (drule exp_ln_iff [THEN iffD2], auto)
-done
+lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
+by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
-apply (rule exp_less_cancel_iff [THEN iffD1])
-apply (auto simp add: exp_ln_iff [symmetric] simp del: exp_ln_iff)
-done
+by simp
lemma exp_ln_eq: "exp u = x ==> ln x = u"
by auto
@@ -1364,9 +1361,10 @@
apply (erule sums_summable)
apply (case_tac "m=0")
apply (simp (no_asm_simp))
-apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
-apply (simp only: mult_less_cancel_left, simp)
-apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
+apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
+apply (simp only: mult_less_cancel_left, simp add: times_divide_eq)
+apply (simp (no_asm_simp) add: times_divide_eq
+ numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
apply (subgoal_tac "x*x < 2*3", simp)
apply (rule mult_strict_mono)
apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
@@ -1425,10 +1423,10 @@
apply (cut_tac x = 2 in cos_paired)
apply (drule sums_minus)
apply (rule neg_less_iff_less [THEN iffD1])
-apply (frule sums_unique, auto)
+apply (frule sums_unique, auto simp add: times_divide_eq)
apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n)))" in order_less_trans)
apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
-apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
+apply (simp (no_asm) add: mult_assoc times_divide_eq del: sumr_Suc)
apply (rule sumr_pos_lt_pair)
apply (erule sums_summable, safe)
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
@@ -1522,10 +1520,10 @@
done
lemma cos_pi [simp]: "cos pi = -1"
-by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp)
+by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp add: times_divide_eq)
lemma sin_pi [simp]: "sin pi = 0"
-by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
+by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp add: times_divide_eq)
lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
by (simp add: diff_minus cos_add)
@@ -1703,7 +1701,7 @@
apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
apply (force simp add: minus_equation_iff [of x])
apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
-apply (auto simp add: cos_add)
+apply (auto simp add: cos_add times_divide_eq)
done
(* ditto: but to a lesser extent *)
@@ -1716,7 +1714,7 @@
apply (drule sin_zero_lemma, assumption+)
apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
apply (force simp add: minus_equation_iff [of x])
-apply (auto simp add: even_mult_two_ex)
+apply (auto simp add: even_mult_two_ex times_divide_eq)
done
@@ -1746,7 +1744,7 @@
apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
apply (auto simp del: inverse_mult_distrib
simp add: mult_assoc left_diff_distrib cos_add)
-done
+done
lemma add_tan_eq:
"[| cos x \<noteq> 0; cos y \<noteq> 0 |]
@@ -1754,7 +1752,7 @@
apply (simp add: tan_def)
apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
apply (auto simp add: mult_assoc left_distrib)
-apply (simp (no_asm) add: sin_add)
+apply (simp add: sin_add times_divide_eq)
done
lemma tan_add:
@@ -2065,7 +2063,7 @@
by (rule DERIV_exp [THEN DERIV_isCont])
lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
-by (auto simp add: sin_zero_iff even_mult_two_ex)
+by (auto simp add: sin_zero_iff even_mult_two_ex times_divide_eq)
lemma exp_eq_one_iff [simp]: "(exp x = 1) = (x = 0)"
apply auto
@@ -2130,13 +2128,17 @@
"[| 0 \<le> x; 0 \<le> y |]
==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
apply (rule real_root_pos_unique)
-apply (auto intro!: real_root_pos_pos_le simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 simp del: realpow_Suc)
+apply (auto intro!: real_root_pos_pos_le
+ simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2
+ simp del: realpow_Suc)
done
lemma real_root_inverse:
"0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
apply (rule real_root_pos_unique)
-apply (auto intro: real_root_pos_pos_le simp add: power_inverse [symmetric] real_root_pow_pos2 simp del: realpow_Suc)
+apply (auto intro: real_root_pos_pos_le
+ simp add: power_inverse [symmetric] real_root_pow_pos2
+ simp del: realpow_Suc)
done
lemma real_root_divide:
@@ -2449,11 +2451,11 @@
apply (rule order_less_le_trans [of _ "7/5"], simp)
apply (rule_tac n = 1 in realpow_increasing)
prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
-apply (simp_all add: numeral_2_eq_2)
+apply (simp_all add: numeral_2_eq_2 times_divide_eq)
done
lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
-by (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
+by (simp add: divide_less_eq mult_compare_simps)
lemma four_x_squared:
fixes x::real
@@ -2690,7 +2692,6 @@
val ln_less_self = thm "ln_less_self";
val ln_ge_zero = thm "ln_ge_zero";
val ln_gt_zero = thm "ln_gt_zero";
-val ln_not_eq_zero = thm "ln_not_eq_zero";
val ln_less_zero = thm "ln_less_zero";
val exp_ln_eq = thm "exp_ln_eq";
val sin_zero = thm "sin_zero";
--- a/src/HOL/Integ/IntArith.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/IntArith.thy Thu Oct 07 15:42:30 2004 +0200
@@ -326,38 +326,36 @@
subsection{*Products and 1, by T. M. Rasmussen*}
-lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
-apply auto
-apply (subgoal_tac "m*1 = m*n")
-apply (drule mult_cancel_left [THEN iffD1], auto)
+lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
+by arith
+
+lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
+apply (case_tac "\<bar>n\<bar>=1")
+apply (simp add: abs_mult)
+apply (rule ccontr)
+apply (auto simp add: linorder_neq_iff abs_mult)
+apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
+ prefer 2 apply arith
+apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp)
+apply (rule mult_mono, auto)
done
-text{*FIXME: tidy*}
+lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
+by (insert abs_zmult_eq_1 [of m n], arith)
+
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
-apply auto
-apply (case_tac "m=1")
-apply (case_tac [2] "n=1")
-apply (case_tac [4] "m=1")
-apply (case_tac [5] "n=1", auto)
-apply (tactic"distinct_subgoals_tac")
-apply (subgoal_tac "1<m*n", simp)
-apply (rule less_1_mult, arith)
-apply (subgoal_tac "0<n", arith)
-apply (subgoal_tac "0<m*n")
-apply (drule zero_less_mult_iff [THEN iffD1], auto)
+apply (auto dest: pos_zmult_eq_1_iff_lemma)
+apply (simp add: mult_commute [of m])
+apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
-apply (case_tac "0<m")
-apply (simp add: pos_zmult_eq_1_iff)
-apply (case_tac "m=0")
-apply (simp del: number_of_reorient)
-apply (subgoal_tac "0 < -m")
-apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
+apply (rule iffI)
+ apply (frule pos_zmult_eq_1_iff_lemma)
+ apply (simp add: mult_commute [of m])
+ apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
-
-
ML
{*
val zle_diff1_eq = thm "zle_diff1_eq";
@@ -376,7 +374,6 @@
val nat_le_eq_zle = thm "nat_le_eq_zle";
val nat_intermed_int_val = thm "nat_intermed_int_val";
-val zmult_eq_self_iff = thm "zmult_eq_self_iff";
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
val zmult_eq_1_iff = thm "zmult_eq_1_iff";
val nat_add_distrib = thm "nat_add_distrib";
--- a/src/HOL/Integ/IntDiv.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy Thu Oct 07 15:42:30 2004 +0200
@@ -241,7 +241,7 @@
by(simp add: zmod_zdiv_equality[symmetric])
lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
-by(simp add: zmult_commute zmod_zdiv_equality[symmetric])
+by(simp add: mult_commute zmod_zdiv_equality[symmetric])
use "IntDiv_setup.ML"
@@ -606,7 +606,7 @@
apply (rule trans)
apply (rule_tac s = "b*a mod c" in trans)
apply (rule_tac [2] zmod_zmult1_eq)
-apply (simp_all add: zmult_commute)
+apply (simp_all add: mult_commute)
done
lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
@@ -618,13 +618,13 @@
by (simp add: zdiv_zmult1_eq)
lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst zmult_commute, erule zdiv_zmult_self1)
+by (subst mult_commute, erule zdiv_zmult_self1)
lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
by (simp add: zmod_zmult1_eq)
lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: zmult_commute zmod_zmult1_eq)
+by (simp add: mult_commute zmod_zmult1_eq)
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
proof
@@ -773,7 +773,7 @@
lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
apply (drule zdiv_zmult_zmult1)
-apply (auto simp add: zmult_commute)
+apply (auto simp add: mult_commute)
done
@@ -798,7 +798,7 @@
lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
apply (cut_tac c = c in zmod_zmult_zmult1)
-apply (auto simp add: zmult_commute)
+apply (auto simp add: mult_commute)
done
@@ -922,7 +922,7 @@
prefer 2 apply arith
apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
apply (rule_tac [2] mult_left_mono)
-apply (auto simp add: add_commute [of 1] zmult_commute add1_zle_eq
+apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
pos_mod_bound)
apply (subst zmod_zadd1_eq)
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
@@ -1009,7 +1009,7 @@
by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
-by (auto simp add: dvd_def intro: zmult_assoc)
+by (auto simp add: dvd_def intro: mult_assoc)
lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
apply (simp add: dvd_def, auto)
@@ -1024,7 +1024,7 @@
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
apply (simp add: dvd_def, auto)
- apply (simp add: zmult_assoc zmult_eq_self_iff zero_less_mult_iff zmult_eq_1_iff)
+ apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
done
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
@@ -1049,7 +1049,7 @@
done
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
- apply (subst zmult_commute)
+ apply (subst mult_commute)
apply (erule zdvd_zmult)
done
@@ -1065,12 +1065,12 @@
lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
apply (simp add: dvd_def)
- apply (simp add: zmult_assoc, blast)
+ apply (simp add: mult_assoc, blast)
done
lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
apply (rule zdvd_zmultD2)
- apply (subst zmult_commute, assumption)
+ apply (subst mult_commute, assumption)
done
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
--- a/src/HOL/Integ/NatBin.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy Thu Oct 07 15:42:30 2004 +0200
@@ -252,7 +252,7 @@
lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
-subsection{*General Theorems About Powers Involving Binary Numerals*}
+subsection{*Powers with Numeric Exponents*}
text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
We cannot prove general results about the numeral @{term "-1"}, so we have to
@@ -277,6 +277,11 @@
"(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
+lemma power2_less_0 [simp]:
+ fixes a :: "'a::{ordered_idom,recpower}"
+ shows "~ (a\<twosuperior> < 0)"
+by (force simp add: power2_eq_square mult_less_0_iff)
+
lemma zero_eq_power2 [simp]:
"(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
by (force simp add: power2_eq_square mult_eq_0_iff)
@@ -340,6 +345,14 @@
apply (force simp add: linorder_not_less [symmetric])
done
+text{*Simprules for comparisons where common factors can be cancelled.*}
+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_power2 power2_less_0
subsubsection{*Nat *}
--- a/src/HOL/Integ/NatSimprocs.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Thu Oct 07 15:42:30 2004 +0200
@@ -174,6 +174,23 @@
declare zero_le_divide_iff [of "number_of w", standard, simp]
declare divide_le_0_iff [of "number_of w", standard, simp]
+(****
+IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
+then these special-case declarations may be useful.
+
+text{*These simprules move numerals into numerators and denominators.*}
+lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
+by (simp add: times_divide_eq)
+
+lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
+by (simp add: times_divide_eq)
+
+declare times_divide_eq_right [of "number_of w", standard, simp]
+declare times_divide_eq_right [of _ _ "number_of w", standard, simp]
+declare times_divide_eq_left [of _ "number_of w", standard, simp]
+declare times_divide_eq_left [of _ _ "number_of w", standard, simp]
+****)
+
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
strange, but then other simprocs simplify the quotient.*}
--- a/src/HOL/OrderedGroup.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/OrderedGroup.thy Thu Oct 07 15:42:30 2004 +0200
@@ -314,9 +314,22 @@
"a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"
by simp
-lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add})"
+lemma add_increasing:
+ fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+ shows "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
by (insert add_mono [of 0 a b c], simp)
+lemma add_strict_increasing:
+ fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+ shows "[|0<a; b\<le>c|] ==> b < a + c"
+by (insert add_less_le_mono [of 0 a b c], simp)
+
+lemma add_strict_increasing2:
+ fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+ shows "[|0\<le>a; b<c|] ==> b < a + c"
+by (insert add_le_less_mono [of 0 a b c], simp)
+
+
subsection {* Ordering Rules for Unary Minus *}
lemma le_imp_neg_le:
--- a/src/HOL/Real/PReal.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Real/PReal.thy Thu Oct 07 15:42:30 2004 +0200
@@ -808,7 +808,7 @@
also with ypos have "... = (r/y) * (y + ?d)"
by (simp only: right_distrib divide_inverse mult_ac, simp)
also have "... = r*x" using ypos
- by simp
+ by (simp add: times_divide_eq_left)
finally show "r + ?d < r*x" .
qed
with r notin rdpos
--- a/src/HOL/Real/RComplete.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Real/RComplete.thy Thu Oct 07 15:42:30 2004 +0200
@@ -153,7 +153,7 @@
apply (rule lemma_real_complete2b)
apply (erule_tac [2] order_less_imp_le)
apply (blast intro!: isLubD2, blast)
-apply (simp (no_asm_use) add: real_add_assoc)
+apply (simp (no_asm_use) add: add_assoc)
apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono)
apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono, auto)
done
@@ -169,7 +169,7 @@
apply (drule_tac x = n in spec)
apply (drule_tac c = "real (Suc n)" in mult_right_mono)
apply (rule real_of_nat_ge_zero)
-apply (simp add: real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_commute)
+apply (simp add: times_divide_eq_right real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] mult_commute)
apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} 1")
apply (subgoal_tac "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}")
apply (drule reals_complete)
--- a/src/HOL/Ring_and_Field.thy Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy Thu Oct 07 15:42:30 2004 +0200
@@ -472,7 +472,10 @@
text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
also with the relations @{text "\<le>"} and equality.*}
-lemma mult_less_cancel_right:
+text{*These ``disjunction'' versions produce two cases when the comparison is
+ an assumption, but effectively four when the comparison is a goal.*}
+
+lemma mult_less_cancel_right_disj:
"(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
apply (case_tac "c = 0")
apply (auto simp add: linorder_neq_iff mult_strict_right_mono
@@ -485,7 +488,7 @@
mult_right_mono_neg)
done
-lemma mult_less_cancel_left:
+lemma mult_less_cancel_left_disj:
"(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
apply (case_tac "c = 0")
apply (auto simp add: linorder_neq_iff mult_strict_left_mono
@@ -498,13 +501,27 @@
mult_left_mono_neg)
done
+
+text{*The ``conjunction of implication'' lemmas produce two cases when the
+comparison is a goal, but give four when the comparison is an assumption.*}
+
+lemma mult_less_cancel_right:
+ fixes c :: "'a :: ordered_ring_strict"
+ shows "(a*c < b*c) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"
+by (insert mult_less_cancel_right_disj [of a c b], auto)
+
+lemma mult_less_cancel_left:
+ fixes c :: "'a :: ordered_ring_strict"
+ shows "(c*a < c*b) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"
+by (insert mult_less_cancel_left_disj [of c a b], auto)
+
lemma mult_le_cancel_right:
"(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
-by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
+by (simp add: linorder_not_less [symmetric] mult_less_cancel_right_disj)
lemma mult_le_cancel_left:
"(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
-by (simp add: linorder_not_less [symmetric] mult_less_cancel_left)
+by (simp add: linorder_not_less [symmetric] mult_less_cancel_left_disj)
lemma mult_less_imp_less_left:
assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
@@ -545,6 +562,85 @@
simp add: linorder_neq_iff)
done
+
+subsubsection{*Special Cancellation Simprules for Multiplication*}
+
+text{*These also produce two cases when the comparison is a goal.*}
+
+lemma mult_le_cancel_right1:
+ fixes c :: "'a :: ordered_idom"
+ shows "(c \<le> b*c) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
+by (insert mult_le_cancel_right [of 1 c b], simp)
+
+lemma mult_le_cancel_right2:
+ fixes c :: "'a :: ordered_idom"
+ shows "(a*c \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
+by (insert mult_le_cancel_right [of a c 1], simp)
+
+lemma mult_le_cancel_left1:
+ fixes c :: "'a :: ordered_idom"
+ shows "(c \<le> c*b) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
+by (insert mult_le_cancel_left [of c 1 b], simp)
+
+lemma mult_le_cancel_left2:
+ fixes c :: "'a :: ordered_idom"
+ shows "(c*a \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
+by (insert mult_le_cancel_left [of c a 1], simp)
+
+lemma mult_less_cancel_right1:
+ fixes c :: "'a :: ordered_idom"
+ shows "(c < b*c) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
+by (insert mult_less_cancel_right [of 1 c b], simp)
+
+lemma mult_less_cancel_right2:
+ fixes c :: "'a :: ordered_idom"
+ shows "(a*c < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
+by (insert mult_less_cancel_right [of a c 1], simp)
+
+lemma mult_less_cancel_left1:
+ fixes c :: "'a :: ordered_idom"
+ shows "(c < c*b) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
+by (insert mult_less_cancel_left [of c 1 b], simp)
+
+lemma mult_less_cancel_left2:
+ fixes c :: "'a :: ordered_idom"
+ shows "(c*a < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
+by (insert mult_less_cancel_left [of c a 1], simp)
+
+lemma mult_cancel_right1 [simp]:
+fixes c :: "'a :: ordered_idom"
+ shows "(c = b*c) = (c = 0 | b=1)"
+by (insert mult_cancel_right [of 1 c b], force)
+
+lemma mult_cancel_right2 [simp]:
+fixes c :: "'a :: ordered_idom"
+ shows "(a*c = c) = (c = 0 | a=1)"
+by (insert mult_cancel_right [of a c 1], simp)
+
+lemma mult_cancel_left1 [simp]:
+fixes c :: "'a :: ordered_idom"
+ shows "(c = c*b) = (c = 0 | b=1)"
+by (insert mult_cancel_left [of c 1 b], force)
+
+lemma mult_cancel_left2 [simp]:
+fixes c :: "'a :: ordered_idom"
+ shows "(c*a = c) = (c = 0 | a=1)"
+by (insert mult_cancel_left [of c a 1], simp)
+
+
+text{*Simprules for comparisons where common factors can be cancelled.*}
+lemmas mult_compare_simps =
+ mult_le_cancel_right mult_le_cancel_left
+ mult_le_cancel_right1 mult_le_cancel_right2
+ mult_le_cancel_left1 mult_le_cancel_left2
+ mult_less_cancel_right mult_less_cancel_left
+ mult_less_cancel_right1 mult_less_cancel_right2
+ mult_less_cancel_left1 mult_less_cancel_left2
+ mult_cancel_right mult_cancel_left
+ mult_cancel_right1 mult_cancel_right2
+ mult_cancel_left1 mult_cancel_left2
+
+
text{*This list of rewrites decides ring equalities by ordered rewriting.*}
lemmas ring_eq_simps =
(* mult_ac*)
@@ -824,7 +920,7 @@
lemma divide_1 [simp]: "a/1 = (a::'a::field)"
by (simp add: divide_inverse)
-lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
+lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
by (simp add: divide_inverse mult_assoc)
lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
@@ -839,6 +935,59 @@
by (simp add: divide_inverse mult_assoc)
+subsubsection{*Special Cancellation Simprules for Division*}
+
+lemma mult_divide_cancel_left_if [simp]:
+ fixes c :: "'a :: {field,division_by_zero}"
+ shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
+by (simp add: mult_divide_cancel_left)
+
+lemma mult_divide_cancel_right_if [simp]:
+ fixes c :: "'a :: {field,division_by_zero}"
+ shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
+by (simp add: mult_divide_cancel_right)
+
+lemma mult_divide_cancel_left_if1 [simp]:
+ fixes c :: "'a :: {field,division_by_zero}"
+ shows "c / (c*b) = (if c=0 then 0 else 1/b)"
+apply (insert mult_divide_cancel_left_if [of c 1 b])
+apply (simp del: mult_divide_cancel_left_if)
+done
+
+lemma mult_divide_cancel_left_if2 [simp]:
+ fixes c :: "'a :: {field,division_by_zero}"
+ shows "(c*a) / c = (if c=0 then 0 else a)"
+apply (insert mult_divide_cancel_left_if [of c a 1])
+apply (simp del: mult_divide_cancel_left_if)
+done
+
+lemma mult_divide_cancel_right_if1 [simp]:
+ fixes c :: "'a :: {field,division_by_zero}"
+ shows "c / (b*c) = (if c=0 then 0 else 1/b)"
+apply (insert mult_divide_cancel_right_if [of 1 c b])
+apply (simp del: mult_divide_cancel_right_if)
+done
+
+lemma mult_divide_cancel_right_if2 [simp]:
+ fixes c :: "'a :: {field,division_by_zero}"
+ shows "(a*c) / c = (if c=0 then 0 else a)"
+apply (insert mult_divide_cancel_right_if [of a c 1])
+apply (simp del: mult_divide_cancel_right_if)
+done
+
+text{*Two lemmas for cancelling the denominator*}
+
+lemma times_divide_self_right [simp]:
+ fixes a :: "'a :: {field,division_by_zero}"
+ shows "a * (b/a) = (if a=0 then 0 else b)"
+by (simp add: times_divide_eq_right)
+
+lemma times_divide_self_left [simp]:
+ fixes a :: "'a :: {field,division_by_zero}"
+ shows "(b/a) * a = (if a=0 then 0 else b)"
+by (simp add: times_divide_eq_left)
+
+
subsection {* Division and Unary Minus *}
lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
@@ -1167,7 +1316,7 @@
proof -
assume less: "0<c"
hence "(a < b/c) = (a*c < (b/c)*c)"
- by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
also have "... = (a*c < b)"
by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
finally show ?thesis .
@@ -1178,7 +1327,7 @@
proof -
assume less: "c<0"
hence "(a < b/c) = ((b/c)*c < a*c)"
- by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
also have "... = (b < a*c)"
by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
finally show ?thesis .
@@ -1198,7 +1347,7 @@
proof -
assume less: "0<c"
hence "(b/c < a) = ((b/c)*c < a*c)"
- by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
also have "... = (b < a*c)"
by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
finally show ?thesis .
@@ -1209,7 +1358,7 @@
proof -
assume less: "c<0"
hence "(b/c < a) = (a*c < (b/c)*c)"
- by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
also have "... = (a*c < b)"
by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
finally show ?thesis .
@@ -1252,6 +1401,7 @@
"(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
by (force simp add: nonzero_divide_eq_eq)
+
subsection{*Cancellation Laws for Division*}
lemma divide_cancel_right [simp]:
@@ -1366,6 +1516,17 @@
lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
by (blast intro!: less_half_sum gt_half_sum)
+
+lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
+
+text{*It's not obvious whether these should be simprules or not.
+ Their effect is to gather terms into one big fraction, like
+ a*b*c / x*y*z. The rationale for that is unclear, but many proofs
+ seem to need them.*}
+
+declare times_divide_eq [simp]
+
+
subsection {* Absolute Value *}
lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
@@ -1486,7 +1647,7 @@
"b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
-lemma abs_divide:
+lemma abs_divide [simp]:
"abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
apply (case_tac "b=0", simp)
apply (simp add: nonzero_abs_divide)
@@ -1513,9 +1674,6 @@
apply (simp add: le_minus_self_iff linorder_neq_iff)
done
-text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
-declare times_divide_eq_left [simp]
-
lemma linprog_dual_estimate:
assumes
"A * x \<le> (b::'a::lordered_ring)"
@@ -1670,6 +1828,8 @@
val mult_strict_mono' = thm "mult_strict_mono'";
val mult_mono = thm "mult_mono";
val less_1_mult = thm "less_1_mult";
+val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";
+val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";
val mult_less_cancel_right = thm "mult_less_cancel_right";
val mult_less_cancel_left = thm "mult_less_cancel_left";
val mult_le_cancel_right = thm "mult_le_cancel_right";
--- a/src/HOL/arith_data.ML Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/arith_data.ML Thu Oct 07 15:42:30 2004 +0200
@@ -424,7 +424,11 @@
mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD @ [Suc_leI],
- simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
+ simpset = HOL_basic_ss addsimps add_rules
+ addsimprocs [ab_group_add_cancel.sum_conv,
+ ab_group_add_cancel.rel_conv]
+ (*abel_cancel helps it work in abstract algebraic domains*)
+ addsimprocs nat_cancel_sums_add}),
ArithTheoryData.init, arith_discrete "nat"];
end;