src/HOL/Nat_Numeral.thy
changeset 31068 f591144b0f17
parent 31034 736f521ad036
child 31080 21ffc770ebc0
     1.1 --- a/src/HOL/Nat_Numeral.thy	Fri May 08 08:01:09 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Fri May 08 09:48:07 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory Nat_Numeral
     1.6  imports IntDiv
     1.7 -uses ("Tools/nat_simprocs.ML")
     1.8 +uses ("Tools/nat_numeral_simprocs.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Numerals for natural numbers *}
    1.12 @@ -455,29 +455,6 @@
    1.13  
    1.14  declare dvd_eq_mod_eq_0_number_of [simp]
    1.15  
    1.16 -ML
    1.17 -{*
    1.18 -val nat_number_of_def = thm"nat_number_of_def";
    1.19 -
    1.20 -val nat_number_of = thm"nat_number_of";
    1.21 -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
    1.22 -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
    1.23 -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
    1.24 -val numeral_2_eq_2 = thm"numeral_2_eq_2";
    1.25 -val nat_div_distrib = thm"nat_div_distrib";
    1.26 -val nat_mod_distrib = thm"nat_mod_distrib";
    1.27 -val int_nat_number_of = thm"int_nat_number_of";
    1.28 -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
    1.29 -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
    1.30 -val Suc_nat_number_of = thm"Suc_nat_number_of";
    1.31 -val add_nat_number_of = thm"add_nat_number_of";
    1.32 -val diff_nat_eq_if = thm"diff_nat_eq_if";
    1.33 -val diff_nat_number_of = thm"diff_nat_number_of";
    1.34 -val mult_nat_number_of = thm"mult_nat_number_of";
    1.35 -val div_nat_number_of = thm"div_nat_number_of";
    1.36 -val mod_nat_number_of = thm"mod_nat_number_of";
    1.37 -*}
    1.38 -
    1.39  
    1.40  subsection{*Comparisons*}
    1.41  
    1.42 @@ -737,23 +714,6 @@
    1.43      power_number_of_odd [of "number_of v", standard]
    1.44  
    1.45  
    1.46 -
    1.47 -ML
    1.48 -{*
    1.49 -val numeral_ss = @{simpset} addsimps @{thms numerals};
    1.50 -
    1.51 -val nat_bin_arith_setup =
    1.52 - Lin_Arith.map_data
    1.53 -   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.54 -     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    1.55 -      inj_thms = inj_thms,
    1.56 -      lessD = lessD, neqE = neqE,
    1.57 -      simpset = simpset addsimps @{thms neg_simps} @
    1.58 -        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
    1.59 -*}
    1.60 -
    1.61 -declaration {* K nat_bin_arith_setup *}
    1.62 -
    1.63  (* Enable arith to deal with div/mod k where k is a numeral: *)
    1.64  declare split_div[of _ _ "number_of k", standard, arith_split]
    1.65  declare split_mod[of _ _ "number_of k", standard, arith_split]
    1.66 @@ -912,8 +872,37 @@
    1.67  
    1.68  subsection {* Simprocs for the Naturals *}
    1.69  
    1.70 -use "Tools/nat_simprocs.ML"
    1.71 -declaration {* K nat_simprocs_setup *}
    1.72 +use "Tools/nat_numeral_simprocs.ML"
    1.73 +
    1.74 +declaration {*
    1.75 +let
    1.76 +
    1.77 +val less_eq_rules = @{thms ring_distribs} @
    1.78 +  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
    1.79 +   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    1.80 +   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    1.81 +   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    1.82 +   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    1.83 +   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    1.84 +   @{thm mult_Suc}, @{thm mult_Suc_right},
    1.85 +   @{thm add_Suc}, @{thm add_Suc_right},
    1.86 +   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    1.87 +   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
    1.88 +
    1.89 +val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
    1.90 +
    1.91 +in
    1.92 +
    1.93 +K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.94 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    1.95 +    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    1.96 +    simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    1.97 +      addsimps less_eq_rules
    1.98 +      addsimprocs simprocs}))
    1.99 +
   1.100 +end
   1.101 +*}
   1.102 +
   1.103  
   1.104  subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   1.105