--- a/src/HOL/Hyperreal/Transcendental.thy Mon May 21 19:14:12 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Mon May 21 19:43:33 2007 +0200
@@ -1946,7 +1946,7 @@
have pos_c: "0 < ?c"
by (rule cos_gt_zero, simp, simp)
have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
- by (simp only: add_divide_distrib [symmetric], simp)
+ by simp
also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
by (simp only: cos_add sin_add)
also have "\<dots> = ?c * (?c\<twosuperior> - 3 * ?s\<twosuperior>)"
@@ -1983,8 +1983,7 @@
lemma sin_30: "sin (pi / 6) = 1 / 2"
proof -
have "sin (pi / 6) = cos (pi / 2 - pi / 6)" by (rule sin_cos_eq)
- also have "pi / 2 - pi / 6 = pi / 3"
- by (simp add: diff_divide_distrib [symmetric])
+ also have "pi / 2 - pi / 6 = pi / 3" by simp
also have "cos (pi / 3) = 1 / 2" by (rule cos_60)
finally show ?thesis .
qed
@@ -2030,18 +2029,16 @@
by (simp add: cos_double mult_assoc power_add [symmetric] numeral_2_eq_2)
lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
-apply (subgoal_tac "3/2 = (1+1 / 2::real)")
-apply (simp only: left_distrib)
-apply (auto simp add: cos_add mult_ac)
+apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
+apply (subst cos_add, simp)
done
lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
by (auto simp add: mult_assoc)
lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
-apply (subgoal_tac "3/2 = (1+1 / 2::real)")
-apply (simp only: left_distrib)
-apply (auto simp add: sin_add mult_ac)
+apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
+apply (subst sin_add, simp)
done
(*NEEDED??*)
--- a/src/HOL/Integ/int_arith1.ML Mon May 21 19:14:12 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML Mon May 21 19:43:33 2007 +0200
@@ -258,11 +258,41 @@
end
handle TERM _ => find_first_coeff (t::past) u terms;
+(*Fractions as pairs of ints. Can't use Rat.rat because the representation
+ needs to preserve negative values in the denominator.*)
+fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
+
+(*Don't reduce fractions; sums must be proved by rule add_frac_eq.
+ Fractions are reduced later by the cancel_numeral_factor simproc.*)
+fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
+
+val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
+
+(*Build term (p / q) * t*)
+fun mk_fcoeff ((p, q), t) =
+ let val T = Term.fastype_of t
+ in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
+
+(*Express t as a product of a fraction with other sorted terms*)
+fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
+ | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
+ let val (p, t') = dest_coeff sign t
+ val (q, u') = dest_coeff 1 u
+ in (mk_frac (p, q), mk_divide (t', u')) end
+ | dest_fcoeff sign t =
+ let val (p, t') = dest_coeff sign t
+ val T = Term.fastype_of t
+ in (mk_frac (p, 1), mk_divide (t', mk_number T 1)) end;
+
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
val add_0s = thms "add_0s";
val mult_1s = thms "mult_1s";
+(*Simplify inverse Numeral1, a/Numeral1*)
+val inverse_1s = [@{thm inverse_numeral_1}];
+val divide_1s = [@{thm divide_numeral_1}];
+
(*To perform binary arithmetic. The "left" rewriting handles patterns
created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
val simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
@@ -282,6 +312,9 @@
(*To let us treat subtraction as addition*)
val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
+(*To let us treat division as multiplication*)
+val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
+
(*push the unary minus down: - x * y = x * - y *)
val minus_mult_eq_1_to_2 =
[@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
@@ -410,16 +443,54 @@
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+(*Version for fields, where coefficients can be fractions*)
+structure FieldCombineNumeralsData =
+ struct
+ type coeff = IntInf.int * IntInf.int
+ val iszero = (fn (p, q) => p = 0)
+ val add = add_frac
+ val mk_sum = long_mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_fcoeff
+ val dest_coeff = dest_fcoeff 1
+ val left_distrib = combine_common_factor RS trans
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+ val trans_tac = fn _ => trans_tac
+
+ val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+ inverse_1s @ divide_simps @ diff_simps @ minus_simps @ add_ac
+ val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
+ val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+ fun norm_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+ THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+ THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
+ fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
+ val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
+ end;
+
+structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
+
val combine_numerals =
Int_Numeral_Base_Simprocs.prep_simproc
("int_combine_numerals",
["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"],
K CombineNumerals.proc);
+val field_combine_numerals =
+ Int_Numeral_Base_Simprocs.prep_simproc
+ ("field_combine_numerals",
+ ["(i::'a::{number_ring,field,division_by_zero}) + j",
+ "(i::'a::{number_ring,field,division_by_zero}) - j"],
+ K FieldCombineNumerals.proc);
+
end;
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
+Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
(*examples:
print_depth 22;