--- 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"
--- 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
-
--- 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},
--- 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 \<le> n"
shows "m \<le> 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 "\<not> m \<le> 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 *}
--- 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)
--- 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;
--- 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;