author haftmann Mon Nov 04 20:10:06 2013 +0100 (2013-11-04) changeset 54249 ce00f2fef556 parent 54248 c7af3d651658 child 54250 7d2544dd3988
streamlined setup of linear arithmetic
 src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Num.thy file | annotate | diff | revisions src/HOL/Numeral_Simprocs.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Tools/int_arith.ML file | annotate | diff | revisions src/HOL/Tools/lin_arith.ML file | annotate | diff | revisions src/HOL/Tools/semiring_normalizer.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Int.thy	Mon Nov 04 18:08:47 2013 +0100
1.2 +++ b/src/HOL/Int.thy	Mon Nov 04 20:10:06 2013 +0100
1.3 @@ -424,6 +424,11 @@
1.4
1.5  end
1.6
1.7 +lemma diff_nat_numeral [simp]:
1.8 +  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
1.9 +  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
1.10 +
1.11 +
1.12  text {* For termination proofs: *}
1.13  lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
1.14
1.15 @@ -747,14 +752,11 @@
1.16
1.17  subsection {* Setting up simplification procedures *}
1.18
1.19 +lemmas of_int_simps =
1.20 +  of_int_0 of_int_1 of_int_add of_int_mult
1.21 +
1.22  lemmas int_arith_rules =
1.23 -  neg_le_iff_le numeral_One
1.24 -  minus_zero left_minus right_minus
1.25 -  mult_zero_left mult_zero_right mult_1_left mult_1_right
1.26 -  mult_minus_left mult_minus_right
1.28 -  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
1.29 -  of_int_0 of_int_1 of_int_add of_int_mult
1.30 +  numeral_One more_arith_simps of_nat_simps of_int_simps
1.31
1.32  ML_file "Tools/int_arith.ML"
1.33  declaration {* K Int_Arith.setup *}
1.34 @@ -875,16 +877,10 @@
1.35                if d < 0 then 0 else nat d)"
1.36  by (simp add: Let_def nat_diff_distrib [symmetric])
1.37
1.38 -lemma diff_nat_numeral [simp]:
1.39 -  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
1.40 -  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
1.41 -
1.42  lemma nat_numeral_diff_1 [simp]:
1.43    "numeral v - (1::nat) = nat (numeral v - 1)"
1.44    using diff_nat_numeral [of v Num.One] by simp
1.45
1.46 -lemmas nat_arith = diff_nat_numeral
1.47 -
1.48
1.49  subsection "Induction principles for int"
1.50
```
```     2.1 --- a/src/HOL/Num.thy	Mon Nov 04 18:08:47 2013 +0100
2.2 +++ b/src/HOL/Num.thy	Mon Nov 04 20:10:06 2013 +0100
2.3 @@ -1072,6 +1072,16 @@
2.4    BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
2.5    abs_zero abs_one arith_extra_simps
2.6
2.7 +lemmas more_arith_simps =
2.8 +  neg_le_iff_le
2.9 +  minus_zero left_minus right_minus
2.10 +  mult_1_left mult_1_right
2.11 +  mult_minus_left mult_minus_right
2.13 +
2.14 +lemmas of_nat_simps =
2.15 +  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
2.16 +
2.17  text {* Simplification of relational operations *}
2.18
2.19  lemmas eq_numeral_extra =
2.20 @@ -1083,6 +1093,38 @@
2.21    less_numeral_simps less_neg_numeral_simps less_numeral_extra
2.22    eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
2.23
2.24 +lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
2.25 +  -- {* Unfold all @{text let}s involving constants *}
2.26 +  unfolding Let_def ..
2.27 +
2.28 +lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
2.29 +  -- {* Unfold all @{text let}s involving constants *}
2.30 +  unfolding Let_def ..
2.31 +
2.32 +declaration {*
2.33 +let
2.34 +  fun number_of thy T n =
2.35 +    if not (Sign.of_sort thy (T, @{sort numeral}))
2.36 +    then raise CTERM ("number_of", [])
2.37 +    else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
2.38 +in
2.39 +  K (
2.40 +    Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}
2.41 +      @ @{thms rel_simps}
2.42 +      @ @{thms pred_numeral_simps}
2.43 +      @ @{thms arith_special numeral_One}
2.44 +      @ @{thms of_nat_simps})
2.45 +    #> Lin_Arith.add_simps [@{thm Suc_numeral},
2.46 +      @{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
2.47 +      @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
2.48 +      @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
2.49 +      @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
2.50 +      @{thm mult_Suc}, @{thm mult_Suc_right},
2.51 +      @{thm of_nat_numeral}]
2.52 +    #> Lin_Arith.set_number_of number_of)
2.53 +end
2.54 +*}
2.55 +
2.56
2.57  subsubsection {* Simplification of arithmetic when nested to the right. *}
2.58
2.59 @@ -1113,4 +1155,3 @@
2.60
2.61  end
2.62
2.63 -
```
```     3.1 --- a/src/HOL/Numeral_Simprocs.thy	Mon Nov 04 18:08:47 2013 +0100
3.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Nov 04 20:10:06 2013 +0100
3.3 @@ -13,7 +13,7 @@
3.4  ML_file "~~/src/Provers/Arith/extract_common_term.ML"
3.5
3.6  lemmas semiring_norm =
3.7 -  Let_def arith_simps nat_arith rel_simps
3.8 +  Let_def arith_simps diff_nat_numeral rel_simps
3.9    if_False if_True
3.12 @@ -278,27 +278,8 @@
3.13    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
3.14    {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
3.15
3.16 -(* FIXME: duplicate rule warnings for:
3.17 -  ring_distribs
3.18 -  numeral_plus_numeral numeral_times_numeral
3.19 -  numeral_eq_iff numeral_less_iff numeral_le_iff
3.20 -  numeral_neq_zero zero_neq_numeral zero_less_numeral
3.21 -  if_True if_False *)
3.22  declaration {*
3.23 -  K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}])
3.24 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
3.25 -     @{thm nat_0}, @{thm nat_1},
3.26 -     @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral},
3.27 -     @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff},
3.28 -     @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
3.29 -     @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
3.30 -     @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
3.31 -     @{thm mult_Suc}, @{thm mult_Suc_right},
3.33 -     @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral},
3.34 -     @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral},
3.35 -     @{thm if_True}, @{thm if_False}])
3.38        [@{simproc semiring_assoc_fold},
3.39         @{simproc int_combine_numerals},
3.40         @{simproc inteq_cancel_numerals},
```
```     4.1 --- a/src/HOL/Power.thy	Mon Nov 04 18:08:47 2013 +0100
4.2 +++ b/src/HOL/Power.thy	Mon Nov 04 20:10:06 2013 +0100
4.3 @@ -730,8 +730,18 @@
4.4    fixes m n :: nat
4.5    assumes "m\<^sup>2 \<le> n"
4.6    shows "m \<le> n"
4.7 -  using assms by (cases m) (simp_all add: power2_eq_square)
4.8 -
4.9 +proof (cases m)
4.10 +  case 0 then show ?thesis by simp
4.11 +next
4.12 +  case (Suc k)
4.13 +  show ?thesis
4.14 +  proof (rule ccontr)
4.15 +    assume "\<not> m \<le> n"
4.16 +    then have "n < m" by simp
4.17 +    with assms Suc show False
4.19 +  qed
4.20 +qed
4.21
4.22
4.23  subsection {* Code generator tweak *}
```
```     5.1 --- a/src/HOL/Tools/int_arith.ML	Mon Nov 04 18:08:47 2013 +0100
5.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Nov 04 20:10:06 2013 +0100
5.3 @@ -87,9 +87,9 @@
5.4  val setup =
5.5    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
5.7 -  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
5.8 -      @ @{thms pred_numeral_simps}
5.9 -      @ @{thms arith_special} @ @{thms int_arith_rules})
5.10 +  #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
5.12 +      [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}]
5.14    #> Lin_Arith.set_number_of number_of
5.15    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
```
```     6.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Nov 04 18:08:47 2013 +0100
6.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Nov 04 20:10:06 2013 +0100
6.3 @@ -791,37 +791,16 @@
6.4     Most of the work is done by the cancel tactics. *)
6.5
6.6  val init_arith_data =
6.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
6.10 -    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
6.11 -      @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
6.12 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, number_of, ...} =>
6.15 +    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono}
6.16 +      :: @{lemma "a = b ==> c * a = c * b" by (rule arg_cong)} :: mult_mono_thms,
6.17      inj_thms = inj_thms,
6.18 -    lessD = lessD @ [@{thm "Suc_leI"}],
6.19 -    neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_linordered_idom}],
6.20 -    simpset =
6.21 -      put_simpset HOL_basic_ss @{context}
6.23 -      addsimps [@{thm if_True}, @{thm if_False}]
6.27 -        @{thm nat.inject}, @{thm Suc_le_mono}, @{thm Suc_less_eq},
6.28 -        @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
6.29 -        @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
6.30 -        @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
6.31 -        @{thm "not_one_less_zero"}]
6.33 -                   @{simproc group_cancel_eq}, @{simproc group_cancel_le},
6.34 -                   @{simproc group_cancel_less}]
6.35 -       (*abel_cancel helps it work in abstract algebraic domains*)
6.37 -                   @{simproc natless_cancel_sums},
6.38 -                   @{simproc natle_cancel_sums}]
6.39 -      |> Simplifier.add_cong @{thm if_weak_cong}
6.40 -      |> simpset_of,
6.41 -    number_of = number_of}) #>
6.43 +    lessD = lessD,
6.44 +    neqE = @{thm linorder_neqE_nat} :: @{thm linorder_neqE_linordered_idom} :: neqE,
6.45 +    simpset = put_simpset HOL_basic_ss @{context} |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of,
6.46 +    number_of = number_of});
6.47
6.48  (* FIXME !?? *)
6.50 @@ -909,9 +888,6 @@
6.51
6.52  (* context setup *)
6.53
6.54 -val setup =
6.55 -  init_arith_data;
6.56 -
6.57  val global_setup =
6.58    map_theory_simpset (fn ctxt => ctxt
6.60 @@ -924,4 +900,22 @@
6.61            THEN' tac ctxt)))) "linear arithmetic" #>
6.63
6.64 +val setup =
6.65 +  init_arith_data
6.66 +  #> add_discrete_type @{type_name nat}
6.67 +  #> add_lessD @{thm Suc_leI}
6.68 +  #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
6.70 +      @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
6.71 +      @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
6.73 +      @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
6.74 +      @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}]
6.76 +      @{simproc group_cancel_eq}, @{simproc group_cancel_le},
6.77 +      @{simproc group_cancel_less}]
6.78 +     (*abel_cancel helps it work in abstract algebraic domains*)
6.79 +  #> add_simprocs [@{simproc nateq_cancel_sums},@{simproc natless_cancel_sums},
6.80 +      @{simproc natle_cancel_sums}];
6.81 +
6.82  end;
```
```     7.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Nov 04 18:08:47 2013 +0100
7.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Nov 04 20:10:06 2013 +0100
7.3 @@ -848,7 +848,7 @@
7.4  val nat_exp_ss =
7.5    simpset_of
7.6     (put_simpset HOL_basic_ss @{context}
7.7 -    addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
7.8 +    addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})