author huffman Mon, 21 May 2007 19:43:33 +0200 changeset 23066 26a9157b620a parent 23065 ab28e8398670 child 23067 b4f38a12f74a
new field_combine_numerals simproc, which uses fractions as coefficients
 src/HOL/Hyperreal/Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Integ/int_arith1.ML file | annotate | diff | comparison | revisions
```--- 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"
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 @@

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 (subgoal_tac "cos (pi + pi/2) = 0", simp)
done

lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"

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 (subgoal_tac "sin (pi + pi/2) = - 1", 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 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 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
+  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))
+
+  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;