src/HOL/Num.thy
changeset 54249 ce00f2fef556
parent 54230 b1d955791529
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Num.thy	Mon Nov 04 18:08:47 2013 +0100
     1.2 +++ b/src/HOL/Num.thy	Mon Nov 04 20:10:06 2013 +0100
     1.3 @@ -1072,6 +1072,16 @@
     1.4    BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
     1.5    abs_zero abs_one arith_extra_simps
     1.6  
     1.7 +lemmas more_arith_simps =
     1.8 +  neg_le_iff_le
     1.9 +  minus_zero left_minus right_minus
    1.10 +  mult_1_left mult_1_right
    1.11 +  mult_minus_left mult_minus_right
    1.12 +  minus_add_distrib minus_minus mult_assoc
    1.13 +
    1.14 +lemmas of_nat_simps =
    1.15 +  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.16 +
    1.17  text {* Simplification of relational operations *}
    1.18  
    1.19  lemmas eq_numeral_extra =
    1.20 @@ -1083,6 +1093,38 @@
    1.21    less_numeral_simps less_neg_numeral_simps less_numeral_extra
    1.22    eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
    1.23  
    1.24 +lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
    1.25 +  -- {* Unfold all @{text let}s involving constants *}
    1.26 +  unfolding Let_def ..
    1.27 +
    1.28 +lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
    1.29 +  -- {* Unfold all @{text let}s involving constants *}
    1.30 +  unfolding Let_def ..
    1.31 +
    1.32 +declaration {*
    1.33 +let 
    1.34 +  fun number_of thy T n =
    1.35 +    if not (Sign.of_sort thy (T, @{sort numeral}))
    1.36 +    then raise CTERM ("number_of", [])
    1.37 +    else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
    1.38 +in
    1.39 +  K (
    1.40 +    Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}
    1.41 +      @ @{thms rel_simps}
    1.42 +      @ @{thms pred_numeral_simps}
    1.43 +      @ @{thms arith_special numeral_One}
    1.44 +      @ @{thms of_nat_simps})
    1.45 +    #> Lin_Arith.add_simps [@{thm Suc_numeral},
    1.46 +      @{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
    1.47 +      @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
    1.48 +      @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
    1.49 +      @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
    1.50 +      @{thm mult_Suc}, @{thm mult_Suc_right},
    1.51 +      @{thm of_nat_numeral}]
    1.52 +    #> Lin_Arith.set_number_of number_of)
    1.53 +end
    1.54 +*}
    1.55 +
    1.56  
    1.57  subsubsection {* Simplification of arithmetic when nested to the right. *}
    1.58  
    1.59 @@ -1113,4 +1155,3 @@
    1.60  
    1.61  end
    1.62  
    1.63 -