# HG changeset patch
# User paulson
# Date 993476159 -7200
# Node ID 0f16ad464c62b8b9cb7a6b6934d8809b1c5fab68
# Parent  bf98ad1c22c6415ed2718fe991abae368214dd81
Simprocs for type "nat" no longer introduce numerals unless they are already
present in the expression, and in a coefficient position (i.e. as a factor
of a monomial).

diff -r bf98ad1c22c6 -r 0f16ad464c62 src/HOL/Hyperreal/HSeries.ML
--- a/src/HOL/Hyperreal/HSeries.ML	Sat Jun 16 20:06:42 2001 +0200
+++ b/src/HOL/Hyperreal/HSeries.ML	Mon Jun 25 15:35:59 2001 +0200
@@ -202,7 +202,8 @@
      "sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = #0";
 by (simp_tac (HOL_ss addsimps
              [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
-by (simp_tac (simpset() addsimps [sumhr,hypnat_add] delsimps [realpow_Suc]) 1);
+by (simp_tac (simpset() addsimps [sumhr,hypnat_add,double_lemma] 
+                        delsimps [realpow_Suc]) 1);
 qed "sumhr_minus_one_realpow_zero";
 Addsimps [sumhr_minus_one_realpow_zero];
 
diff -r bf98ad1c22c6 -r 0f16ad464c62 src/HOL/Hyperreal/HyperPow.ML
--- a/src/HOL/Hyperreal/HyperPow.ML	Sat Jun 16 20:06:42 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.ML	Mon Jun 25 15:35:59 2001 +0200
@@ -149,14 +149,19 @@
 qed "two_hrealpow_gt";
 Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
 
-Goal "#-1 ^ (2*n) = (#1::hypreal)";
+Goal "#-1 ^ (#2*n) = (#1::hypreal)";
 by (induct_tac "n" 1);
 by (Auto_tac);
 qed "hrealpow_minus_one";
 
+Goal "n+n = (#2*n::nat)";
+by Auto_tac; 
+qed "double_lemma";
+
+(*ugh: need to get rid fo the n+n*)
 Goal "#-1 ^ (n + n) = (#1::hypreal)";
-by (induct_tac "n" 1);
-by (Auto_tac);
+by (auto_tac (claset(), 
+              simpset() addsimps [double_lemma, hrealpow_minus_one]));
 qed "hrealpow_minus_one2";
 Addsimps [hrealpow_minus_one2];
 
@@ -398,7 +403,8 @@
 by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (auto_tac (claset(),
-              simpset() addsimps [hyperpow, hypnat_add,hypreal_minus]));
+              simpset() addsimps [double_lemma, hyperpow, hypnat_add,
+                                  hypreal_minus]));
 qed "hyperpow_minus_one2";
 Addsimps [hyperpow_minus_one2];
 
diff -r bf98ad1c22c6 -r 0f16ad464c62 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Sat Jun 16 20:06:42 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon Jun 25 15:35:59 2001 +0200
@@ -148,6 +148,9 @@
 
 fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
 
+
+(** Other simproc items **)
+
 val trans_tac = Int_Numeral_Simprocs.trans_tac;
 
 val prove_conv = Int_Numeral_Simprocs.prove_conv;
@@ -159,7 +162,8 @@
                 bin_arith_simps @ bin_rel_simps;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
+                                (s, HOLogic.termT);
 val prep_pats = map prep_pat;
 
 
@@ -211,6 +215,23 @@
          mult_0, mult_0_right, mult_1, mult_1_right];
 
 
+(** Restricted version of dest_Sucs_sum for nat_combine_numerals:
+    Simprocs never apply unless the original expression contains at least one
+    numeral in a coefficient position.
+**)
+
+fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+  | is_numeral _ = false;
+
+fun prod_has_numeral t = exists is_numeral (dest_prod t);
+
+fun restricted_dest_Sucs_sum t = 
+  let val ts = dest_Sucs_sum t
+  in  if exists prod_has_numeral ts then ts
+      else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", ts)
+  end;
+
+
 (*** Applying CancelNumeralsFun ***)
 
 structure CancelNumeralsCommon =
@@ -299,7 +320,7 @@
   struct
   val add		= op + : int*int -> int 
   val mk_sum            = long_mk_sum    (*to work for e.g. #2*x + #3*x *)
-  val dest_sum          = dest_Sucs_sum
+  val dest_sum          = restricted_dest_Sucs_sum
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val left_distrib      = left_add_mult_distrib RS trans
diff -r bf98ad1c22c6 -r 0f16ad464c62 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Sat Jun 16 20:06:42 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Mon Jun 25 15:35:59 2001 +0200
@@ -74,6 +74,8 @@
    apply (simp add: fib.Suc_Suc mod_Suc)
   apply (simp add: fib.Suc_Suc
     add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
+  apply (subgoal_tac "x mod #2 < #2", arith)
+  apply simp
   done
 
 
diff -r bf98ad1c22c6 -r 0f16ad464c62 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Sat Jun 16 20:06:42 2001 +0200
+++ b/src/HOL/ex/NatSum.thy	Mon Jun 25 15:35:59 2001 +0200
@@ -116,7 +116,7 @@
 
 lemma sum_of_2_powers: "setsum (\<lambda>i. #2^i) (lessThan n) = #2^n - 1"
   apply (induct n)
-   apply auto
+   apply (auto split: nat_diff_split) 
   done
 
 lemma sum_of_3_powers: "#2 * setsum (\<lambda>i. #3^i) (lessThan n) = #3^n - 1"