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 -
```