# HG changeset patch # User haftmann # Date 1383592206 -3600 # Node ID ce00f2fef556ca4412eae619d6ed1b772e1e2b3a # Parent c7af3d651658b87fdff1b22e520b4e9eecf1e4ba streamlined setup of linear arithmetic diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Int.thy Mon Nov 04 20:10:06 2013 +0100 @@ -424,6 +424,11 @@ end +lemma diff_nat_numeral [simp]: + "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" + by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) + + text {* For termination proofs: *} lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. @@ -747,14 +752,11 @@ subsection {* Setting up simplification procedures *} +lemmas of_int_simps = + of_int_0 of_int_1 of_int_add of_int_mult + lemmas int_arith_rules = - neg_le_iff_le numeral_One - minus_zero left_minus right_minus - mult_zero_left mult_zero_right mult_1_left mult_1_right - mult_minus_left mult_minus_right - minus_add_distrib minus_minus mult_assoc - of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult - of_int_0 of_int_1 of_int_add of_int_mult + numeral_One more_arith_simps of_nat_simps of_int_simps ML_file "Tools/int_arith.ML" declaration {* K Int_Arith.setup *} @@ -875,16 +877,10 @@ if d < 0 then 0 else nat d)" by (simp add: Let_def nat_diff_distrib [symmetric]) -lemma diff_nat_numeral [simp]: - "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" - by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) - lemma nat_numeral_diff_1 [simp]: "numeral v - (1::nat) = nat (numeral v - 1)" using diff_nat_numeral [of v Num.One] by simp -lemmas nat_arith = diff_nat_numeral - subsection "Induction principles for int" diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Num.thy --- a/src/HOL/Num.thy Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Num.thy Mon Nov 04 20:10:06 2013 +0100 @@ -1072,6 +1072,16 @@ BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps abs_zero abs_one arith_extra_simps +lemmas more_arith_simps = + neg_le_iff_le + minus_zero left_minus right_minus + mult_1_left mult_1_right + mult_minus_left mult_minus_right + minus_add_distrib minus_minus mult_assoc + +lemmas of_nat_simps = + of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult + text {* Simplification of relational operations *} lemmas eq_numeral_extra = @@ -1083,6 +1093,38 @@ less_numeral_simps less_neg_numeral_simps less_numeral_extra eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra +lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)" + -- {* Unfold all @{text let}s involving constants *} + unfolding Let_def .. + +lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)" + -- {* Unfold all @{text let}s involving constants *} + unfolding Let_def .. + +declaration {* +let + fun number_of thy T n = + if not (Sign.of_sort thy (T, @{sort numeral})) + then raise CTERM ("number_of", []) + else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; +in + K ( + Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps} + @ @{thms rel_simps} + @ @{thms pred_numeral_simps} + @ @{thms arith_special numeral_One} + @ @{thms of_nat_simps}) + #> Lin_Arith.add_simps [@{thm Suc_numeral}, + @{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1}, + @{thm le_Suc_numeral}, @{thm le_numeral_Suc}, + @{thm less_Suc_numeral}, @{thm less_numeral_Suc}, + @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc}, + @{thm mult_Suc}, @{thm mult_Suc_right}, + @{thm of_nat_numeral}] + #> Lin_Arith.set_number_of number_of) +end +*} + subsubsection {* Simplification of arithmetic when nested to the right. *} @@ -1113,4 +1155,3 @@ end - diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Mon Nov 04 20:10:06 2013 +0100 @@ -13,7 +13,7 @@ ML_file "~~/src/Provers/Arith/extract_common_term.ML" lemmas semiring_norm = - Let_def arith_simps nat_arith rel_simps + Let_def arith_simps diff_nat_numeral rel_simps if_False if_True add_0 add_Suc add_numeral_left add_neg_numeral_left mult_numeral_left @@ -278,27 +278,8 @@ ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *} -(* FIXME: duplicate rule warnings for: - ring_distribs - numeral_plus_numeral numeral_times_numeral - numeral_eq_iff numeral_less_iff numeral_le_iff - numeral_neq_zero zero_neq_numeral zero_less_numeral - if_True if_False *) declaration {* - K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}]) - #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1}, - @{thm nat_0}, @{thm nat_1}, - @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral}, - @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff}, - @{thm le_Suc_numeral}, @{thm le_numeral_Suc}, - @{thm less_Suc_numeral}, @{thm less_numeral_Suc}, - @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc}, - @{thm mult_Suc}, @{thm mult_Suc_right}, - @{thm add_Suc}, @{thm add_Suc_right}, - @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral}, - @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral}, - @{thm if_True}, @{thm if_False}]) - #> Lin_Arith.add_simprocs + K (Lin_Arith.add_simprocs [@{simproc semiring_assoc_fold}, @{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}, diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Power.thy Mon Nov 04 20:10:06 2013 +0100 @@ -730,8 +730,18 @@ fixes m n :: nat assumes "m\<^sup>2 \ n" shows "m \ n" - using assms by (cases m) (simp_all add: power2_eq_square) - +proof (cases m) + case 0 then show ?thesis by simp +next + case (Suc k) + show ?thesis + proof (rule ccontr) + assume "\ m \ n" + then have "n < m" by simp + with assms Suc show False + by (auto simp add: algebra_simps) (simp add: power2_eq_square) + qed +qed subsection {* Code generator tweak *} diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Tools/int_arith.ML Mon Nov 04 20:10:06 2013 +0100 @@ -87,9 +87,9 @@ val setup = Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle} - #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps} - @ @{thms pred_numeral_simps} - @ @{thms arith_special} @ @{thms int_arith_rules}) + #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps} + #> Lin_Arith.add_simps + [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}] #> Lin_Arith.add_simprocs [zero_one_idom_simproc] #> Lin_Arith.set_number_of number_of #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Nov 04 20:10:06 2013 +0100 @@ -791,37 +791,16 @@ Most of the work is done by the cancel tactics. *) val init_arith_data = - Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} => - {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @ - @{thms add_mono_thms_linordered_field} @ add_mono_thms, - mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: - @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms, + Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, number_of, ...} => + {add_mono_thms = @{thms add_mono_thms_linordered_semiring} + @ @{thms add_mono_thms_linordered_field} @ add_mono_thms, + mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} + :: @{lemma "a = b ==> c * a = c * b" by (rule arg_cong)} :: mult_mono_thms, inj_thms = inj_thms, - lessD = lessD @ [@{thm "Suc_leI"}], - neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_linordered_idom}], - simpset = - put_simpset HOL_basic_ss @{context} - addsimps @{thms ring_distribs} - addsimps [@{thm if_True}, @{thm if_False}] - addsimps - [@{thm add_0_left}, @{thm add_0_right}, - @{thm add_Suc}, @{thm add_Suc_right}, - @{thm nat.inject}, @{thm Suc_le_mono}, @{thm Suc_less_eq}, - @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, - @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, - @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, - @{thm "not_one_less_zero"}] - addsimprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff}, - @{simproc group_cancel_eq}, @{simproc group_cancel_le}, - @{simproc group_cancel_less}] - (*abel_cancel helps it work in abstract algebraic domains*) - addsimprocs [@{simproc nateq_cancel_sums}, - @{simproc natless_cancel_sums}, - @{simproc natle_cancel_sums}] - |> Simplifier.add_cong @{thm if_weak_cong} - |> simpset_of, - number_of = number_of}) #> - add_discrete_type @{type_name nat}; + lessD = lessD, + neqE = @{thm linorder_neqE_nat} :: @{thm linorder_neqE_linordered_idom} :: neqE, + simpset = put_simpset HOL_basic_ss @{context} |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of, + number_of = number_of}); (* FIXME !?? *) fun add_arith_facts ctxt = @@ -909,9 +888,6 @@ (* context setup *) -val setup = - init_arith_data; - val global_setup = map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #> @@ -924,4 +900,22 @@ THEN' tac ctxt)))) "linear arithmetic" #> Arith_Data.add_tactic "linear arithmetic" gen_tac; +val setup = + init_arith_data + #> add_discrete_type @{type_name nat} + #> add_lessD @{thm Suc_leI} + #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False}, + @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl}, + @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one}, + @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}]) + #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject}, + @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc}, + @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}] + #> add_simprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff}, + @{simproc group_cancel_eq}, @{simproc group_cancel_le}, + @{simproc group_cancel_less}] + (*abel_cancel helps it work in abstract algebraic domains*) + #> add_simprocs [@{simproc nateq_cancel_sums},@{simproc natless_cancel_sums}, + @{simproc natle_cancel_sums}]; + end; diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Mon Nov 04 18:08:47 2013 +0100 +++ b/src/HOL/Tools/semiring_normalizer.ML Mon Nov 04 20:10:06 2013 +0100 @@ -848,7 +848,7 @@ val nat_exp_ss = simpset_of (put_simpset HOL_basic_ss @{context} - addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) + addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps}) addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]); fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;