src/HOL/Nat_Numeral.thy
changeset 31104 ac8a12b0ed3c
parent 31096 e546e15089ef
parent 31100 6a2e67fe4488
child 31182 7ac0a57a57ed
     1.1 --- a/src/HOL/Nat_Numeral.thy	Tue May 05 17:09:18 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Mon May 11 19:51:21 2009 +0200
     1.3 @@ -874,33 +874,21 @@
     1.4  
     1.5  use "Tools/nat_numeral_simprocs.ML"
     1.6  
     1.7 -declaration {*
     1.8 -let
     1.9 -
    1.10 -val less_eq_rules = @{thms ring_distribs} @
    1.11 -  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
    1.12 -   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    1.13 -   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    1.14 -   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    1.15 -   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    1.16 -   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    1.17 -   @{thm mult_Suc}, @{thm mult_Suc_right},
    1.18 -   @{thm add_Suc}, @{thm add_Suc_right},
    1.19 -   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    1.20 -   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
    1.21 -
    1.22 -val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
    1.23 -
    1.24 -in
    1.25 -
    1.26 -K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.27 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    1.28 -    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    1.29 -    simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    1.30 -      addsimps less_eq_rules
    1.31 -      addsimprocs simprocs}))
    1.32 -
    1.33 -end
    1.34 +declaration {* 
    1.35 +  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    1.36 +  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
    1.37 +     @{thm nat_0}, @{thm nat_1},
    1.38 +     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    1.39 +     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    1.40 +     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    1.41 +     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    1.42 +     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    1.43 +     @{thm mult_Suc}, @{thm mult_Suc_right},
    1.44 +     @{thm add_Suc}, @{thm add_Suc_right},
    1.45 +     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    1.46 +     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
    1.47 +     @{thm if_True}, @{thm if_False}])
    1.48 +  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
    1.49  *}
    1.50  
    1.51