Simprocs for type "nat" no longer introduce numerals unless they are already
authorpaulson
Mon Jun 25 15:35:59 2001 +0200 (2001-06-25)
changeset 113770f16ad464c62
parent 11376 bf98ad1c22c6
child 11378 5c84a5ca3a21
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).
src/HOL/Hyperreal/HSeries.ML
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/NumberTheory/Fib.thy
src/HOL/ex/NatSum.thy
     1.1 --- a/src/HOL/Hyperreal/HSeries.ML	Sat Jun 16 20:06:42 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Mon Jun 25 15:35:59 2001 +0200
     1.3 @@ -202,7 +202,8 @@
     1.4       "sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = #0";
     1.5  by (simp_tac (HOL_ss addsimps
     1.6               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
     1.7 -by (simp_tac (simpset() addsimps [sumhr,hypnat_add] delsimps [realpow_Suc]) 1);
     1.8 +by (simp_tac (simpset() addsimps [sumhr,hypnat_add,double_lemma] 
     1.9 +                        delsimps [realpow_Suc]) 1);
    1.10  qed "sumhr_minus_one_realpow_zero";
    1.11  Addsimps [sumhr_minus_one_realpow_zero];
    1.12  
     2.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Sat Jun 16 20:06:42 2001 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Mon Jun 25 15:35:59 2001 +0200
     2.3 @@ -149,14 +149,19 @@
     2.4  qed "two_hrealpow_gt";
     2.5  Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
     2.6  
     2.7 -Goal "#-1 ^ (2*n) = (#1::hypreal)";
     2.8 +Goal "#-1 ^ (#2*n) = (#1::hypreal)";
     2.9  by (induct_tac "n" 1);
    2.10  by (Auto_tac);
    2.11  qed "hrealpow_minus_one";
    2.12  
    2.13 +Goal "n+n = (#2*n::nat)";
    2.14 +by Auto_tac; 
    2.15 +qed "double_lemma";
    2.16 +
    2.17 +(*ugh: need to get rid fo the n+n*)
    2.18  Goal "#-1 ^ (n + n) = (#1::hypreal)";
    2.19 -by (induct_tac "n" 1);
    2.20 -by (Auto_tac);
    2.21 +by (auto_tac (claset(), 
    2.22 +              simpset() addsimps [double_lemma, hrealpow_minus_one]));
    2.23  qed "hrealpow_minus_one2";
    2.24  Addsimps [hrealpow_minus_one2];
    2.25  
    2.26 @@ -398,7 +403,8 @@
    2.27  by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
    2.28  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    2.29  by (auto_tac (claset(),
    2.30 -              simpset() addsimps [hyperpow, hypnat_add,hypreal_minus]));
    2.31 +              simpset() addsimps [double_lemma, hyperpow, hypnat_add,
    2.32 +                                  hypreal_minus]));
    2.33  qed "hyperpow_minus_one2";
    2.34  Addsimps [hyperpow_minus_one2];
    2.35  
     3.1 --- a/src/HOL/Integ/nat_simprocs.ML	Sat Jun 16 20:06:42 2001 +0200
     3.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Mon Jun 25 15:35:59 2001 +0200
     3.3 @@ -148,6 +148,9 @@
     3.4  
     3.5  fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
     3.6  
     3.7 +
     3.8 +(** Other simproc items **)
     3.9 +
    3.10  val trans_tac = Int_Numeral_Simprocs.trans_tac;
    3.11  
    3.12  val prove_conv = Int_Numeral_Simprocs.prove_conv;
    3.13 @@ -159,7 +162,8 @@
    3.14                  bin_arith_simps @ bin_rel_simps;
    3.15  
    3.16  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    3.17 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
    3.18 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
    3.19 +                                (s, HOLogic.termT);
    3.20  val prep_pats = map prep_pat;
    3.21  
    3.22  
    3.23 @@ -211,6 +215,23 @@
    3.24           mult_0, mult_0_right, mult_1, mult_1_right];
    3.25  
    3.26  
    3.27 +(** Restricted version of dest_Sucs_sum for nat_combine_numerals:
    3.28 +    Simprocs never apply unless the original expression contains at least one
    3.29 +    numeral in a coefficient position.
    3.30 +**)
    3.31 +
    3.32 +fun is_numeral (Const("Numeral.number_of", _) $ w) = true
    3.33 +  | is_numeral _ = false;
    3.34 +
    3.35 +fun prod_has_numeral t = exists is_numeral (dest_prod t);
    3.36 +
    3.37 +fun restricted_dest_Sucs_sum t = 
    3.38 +  let val ts = dest_Sucs_sum t
    3.39 +  in  if exists prod_has_numeral ts then ts
    3.40 +      else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", ts)
    3.41 +  end;
    3.42 +
    3.43 +
    3.44  (*** Applying CancelNumeralsFun ***)
    3.45  
    3.46  structure CancelNumeralsCommon =
    3.47 @@ -299,7 +320,7 @@
    3.48    struct
    3.49    val add		= op + : int*int -> int 
    3.50    val mk_sum            = long_mk_sum    (*to work for e.g. #2*x + #3*x *)
    3.51 -  val dest_sum          = dest_Sucs_sum
    3.52 +  val dest_sum          = restricted_dest_Sucs_sum
    3.53    val mk_coeff          = mk_coeff
    3.54    val dest_coeff        = dest_coeff
    3.55    val left_distrib      = left_add_mult_distrib RS trans
     4.1 --- a/src/HOL/NumberTheory/Fib.thy	Sat Jun 16 20:06:42 2001 +0200
     4.2 +++ b/src/HOL/NumberTheory/Fib.thy	Mon Jun 25 15:35:59 2001 +0200
     4.3 @@ -74,6 +74,8 @@
     4.4     apply (simp add: fib.Suc_Suc mod_Suc)
     4.5    apply (simp add: fib.Suc_Suc
     4.6      add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
     4.7 +  apply (subgoal_tac "x mod #2 < #2", arith)
     4.8 +  apply simp
     4.9    done
    4.10  
    4.11  
     5.1 --- a/src/HOL/ex/NatSum.thy	Sat Jun 16 20:06:42 2001 +0200
     5.2 +++ b/src/HOL/ex/NatSum.thy	Mon Jun 25 15:35:59 2001 +0200
     5.3 @@ -116,7 +116,7 @@
     5.4  
     5.5  lemma sum_of_2_powers: "setsum (\<lambda>i. #2^i) (lessThan n) = #2^n - 1"
     5.6    apply (induct n)
     5.7 -   apply auto
     5.8 +   apply (auto split: nat_diff_split) 
     5.9    done
    5.10  
    5.11  lemma sum_of_3_powers: "#2 * setsum (\<lambda>i. #3^i) (lessThan n) = #3^n - 1"