--- a/src/HOL/Arith_Tools.thy Sun Mar 22 21:48:14 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-(* Title: HOL/Arith_Tools.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Amine Chaieb, TU Muenchen
-*)
-
-header {* Setup of arithmetic tools *}
-
-theory Arith_Tools
-imports NatBin
-uses
- "~~/src/Provers/Arith/cancel_numeral_factor.ML"
- "~~/src/Provers/Arith/extract_common_term.ML"
- "Tools/int_factor_simprocs.ML"
- "Tools/nat_simprocs.ML"
- "Tools/Qelim/qelim.ML"
-begin
-
-subsection {* Simprocs for the Naturals *}
-
-declaration {* K nat_simprocs_setup *}
-
-subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
-
-text{*Where K above is a literal*}
-
-lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
-by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
-
-text {*Now just instantiating @{text n} to @{text "number_of v"} does
- the right simplification, but with some redundant inequality
- tests.*}
-lemma neg_number_of_pred_iff_0:
- "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
-apply (simp only: less_Suc_eq_le le_0_eq)
-apply (subst less_number_of_Suc, simp)
-done
-
-text{*No longer required as a simprule because of the @{text inverse_fold}
- simproc*}
-lemma Suc_diff_number_of:
- "Int.Pls < v ==>
- Suc m - (number_of v) = m - (number_of (Int.pred v))"
-apply (subst Suc_diff_eq_diff_pred)
-apply simp
-apply (simp del: nat_numeral_1_eq_1)
-apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
-by (simp add: numerals split add: nat_diff_split)
-
-
-subsubsection{*For @{term nat_case} and @{term nat_rec}*}
-
-lemma nat_case_number_of [simp]:
- "nat_case a f (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then a else f (nat pv))"
-by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
-
-lemma nat_case_add_eq_if [simp]:
- "nat_case a f ((number_of v) + n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then nat_case a f n else f (nat pv + n))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
- del: nat_numeral_1_eq_1
- add: nat_numeral_1_eq_1 [symmetric]
- numeral_1_eq_Suc_0 [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-lemma nat_rec_number_of [simp]:
- "nat_rec a f (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
-apply (case_tac " (number_of v) ::nat")
-apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
-apply (simp split add: split_if_asm)
-done
-
-lemma nat_rec_add_eq_if [simp]:
- "nat_rec a f (number_of v + n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then nat_rec a f n
- else f (nat pv + n) (nat_rec a f (nat pv + n)))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
- del: nat_numeral_1_eq_1
- add: nat_numeral_1_eq_1 [symmetric]
- numeral_1_eq_Suc_0 [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-
-subsubsection{*Various Other Lemmas*}
-
-text {*Evens and Odds, for Mutilated Chess Board*}
-
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma nat_mult_2: "2 * z = (z+z::nat)"
-proof -
- have "2*z = (1 + 1)*z" by simp
- also have "... = z+z" by (simp add: left_distrib)
- finally show ?thesis .
-qed
-
-lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (subst mult_commute, rule nat_mult_2)
-
-text{*Case analysis on @{term "n<2"}*}
-lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
-by arith
-
-lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
-by arith
-
-lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
-
-lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
-apply (subgoal_tac "m mod 2 < 2")
-apply (erule less_2_cases [THEN disjE])
-apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
-done
-
-lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
-apply (subgoal_tac "m mod 2 < 2")
-apply (force simp del: mod_less_divisor, simp)
-done
-
-text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
-
-lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
-by simp
-
-lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
-by simp
-
-text{*Can be used to eliminate long strings of Sucs, but not by default*}
-lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
-by simp
-
-
-text{*These lemmas collapse some needless occurrences of Suc:
- at least three Sucs, since two and fewer are rewritten back to Suc again!
- We already have some rules to simplify operands smaller than 3.*}
-
-lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
-by (simp add: Suc3_eq_add_3)
-
-lemmas Suc_div_eq_add3_div_number_of =
- Suc_div_eq_add3_div [of _ "number_of v", standard]
-declare Suc_div_eq_add3_div_number_of [simp]
-
-lemmas Suc_mod_eq_add3_mod_number_of =
- Suc_mod_eq_add3_mod [of _ "number_of v", standard]
-declare Suc_mod_eq_add3_mod_number_of [simp]
-
-
-subsubsection{*Special Simplification for Constants*}
-
-text{*These belong here, late in the development of HOL, to prevent their
-interfering with proofs of abstract properties of instances of the function
-@{term number_of}*}
-
-text{*These distributive laws move literals inside sums and differences.*}
-lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
-declare left_distrib_number_of [simp]
-
-lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
-declare right_distrib_number_of [simp]
-
-
-lemmas left_diff_distrib_number_of =
- left_diff_distrib [of _ _ "number_of v", standard]
-declare left_diff_distrib_number_of [simp]
-
-lemmas right_diff_distrib_number_of =
- right_diff_distrib [of "number_of v", standard]
-declare right_diff_distrib_number_of [simp]
-
-
-text{*These are actually for fields, like real: but where else to put them?*}
-lemmas zero_less_divide_iff_number_of =
- zero_less_divide_iff [of "number_of w", standard]
-declare zero_less_divide_iff_number_of [simp,noatp]
-
-lemmas divide_less_0_iff_number_of =
- divide_less_0_iff [of "number_of w", standard]
-declare divide_less_0_iff_number_of [simp,noatp]
-
-lemmas zero_le_divide_iff_number_of =
- zero_le_divide_iff [of "number_of w", standard]
-declare zero_le_divide_iff_number_of [simp,noatp]
-
-lemmas divide_le_0_iff_number_of =
- divide_le_0_iff [of "number_of w", standard]
-declare divide_le_0_iff_number_of [simp,noatp]
-
-
-(****
-IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
-then these special-case declarations may be useful.
-
-text{*These simprules move numerals into numerators and denominators.*}
-lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
-by (simp add: times_divide_eq)
-
-lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
-by (simp add: times_divide_eq)
-
-lemmas times_divide_eq_right_number_of =
- times_divide_eq_right [of "number_of w", standard]
-declare times_divide_eq_right_number_of [simp]
-
-lemmas times_divide_eq_right_number_of =
- times_divide_eq_right [of _ _ "number_of w", standard]
-declare times_divide_eq_right_number_of [simp]
-
-lemmas times_divide_eq_left_number_of =
- times_divide_eq_left [of _ "number_of w", standard]
-declare times_divide_eq_left_number_of [simp]
-
-lemmas times_divide_eq_left_number_of =
- times_divide_eq_left [of _ _ "number_of w", standard]
-declare times_divide_eq_left_number_of [simp]
-
-****)
-
-text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
- strange, but then other simprocs simplify the quotient.*}
-
-lemmas inverse_eq_divide_number_of =
- inverse_eq_divide [of "number_of w", standard]
-declare inverse_eq_divide_number_of [simp]
-
-
-text {*These laws simplify inequalities, moving unary minus from a term
-into the literal.*}
-lemmas less_minus_iff_number_of =
- less_minus_iff [of "number_of v", standard]
-declare less_minus_iff_number_of [simp,noatp]
-
-lemmas le_minus_iff_number_of =
- le_minus_iff [of "number_of v", standard]
-declare le_minus_iff_number_of [simp,noatp]
-
-lemmas equation_minus_iff_number_of =
- equation_minus_iff [of "number_of v", standard]
-declare equation_minus_iff_number_of [simp,noatp]
-
-
-lemmas minus_less_iff_number_of =
- minus_less_iff [of _ "number_of v", standard]
-declare minus_less_iff_number_of [simp,noatp]
-
-lemmas minus_le_iff_number_of =
- minus_le_iff [of _ "number_of v", standard]
-declare minus_le_iff_number_of [simp,noatp]
-
-lemmas minus_equation_iff_number_of =
- minus_equation_iff [of _ "number_of v", standard]
-declare minus_equation_iff_number_of [simp,noatp]
-
-
-text{*To Simplify Inequalities Where One Side is the Constant 1*}
-
-lemma less_minus_iff_1 [simp,noatp]:
- fixes b::"'b::{ordered_idom,number_ring}"
- shows "(1 < - b) = (b < -1)"
-by auto
-
-lemma le_minus_iff_1 [simp,noatp]:
- fixes b::"'b::{ordered_idom,number_ring}"
- shows "(1 \<le> - b) = (b \<le> -1)"
-by auto
-
-lemma equation_minus_iff_1 [simp,noatp]:
- fixes b::"'b::number_ring"
- shows "(1 = - b) = (b = -1)"
-by (subst equation_minus_iff, auto)
-
-lemma minus_less_iff_1 [simp,noatp]:
- fixes a::"'b::{ordered_idom,number_ring}"
- shows "(- a < 1) = (-1 < a)"
-by auto
-
-lemma minus_le_iff_1 [simp,noatp]:
- fixes a::"'b::{ordered_idom,number_ring}"
- shows "(- a \<le> 1) = (-1 \<le> a)"
-by auto
-
-lemma minus_equation_iff_1 [simp,noatp]:
- fixes a::"'b::number_ring"
- shows "(- a = 1) = (a = -1)"
-by (subst minus_equation_iff, auto)
-
-
-text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
-
-lemmas mult_less_cancel_left_number_of =
- mult_less_cancel_left [of "number_of v", standard]
-declare mult_less_cancel_left_number_of [simp,noatp]
-
-lemmas mult_less_cancel_right_number_of =
- mult_less_cancel_right [of _ "number_of v", standard]
-declare mult_less_cancel_right_number_of [simp,noatp]
-
-lemmas mult_le_cancel_left_number_of =
- mult_le_cancel_left [of "number_of v", standard]
-declare mult_le_cancel_left_number_of [simp,noatp]
-
-lemmas mult_le_cancel_right_number_of =
- mult_le_cancel_right [of _ "number_of v", standard]
-declare mult_le_cancel_right_number_of [simp,noatp]
-
-
-text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
-
-lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
-lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
-lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
-
-
-subsubsection{*Optional Simplification Rules Involving Constants*}
-
-text{*Simplify quotients that are compared with a literal constant.*}
-
-lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
-lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
-lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
-lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
-lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
-lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
-
-
-text{*Not good as automatic simprules because they cause case splits.*}
-lemmas divide_const_simps =
- le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
- divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
- le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
-
-text{*Division By @{text "-1"}*}
-
-lemma divide_minus1 [simp]:
- "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
-by simp
-
-lemma minus1_divide [simp]:
- "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
-by (simp add: divide_inverse inverse_minus_eq)
-
-lemma half_gt_zero_iff:
- "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
-by auto
-
-lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
-declare half_gt_zero [simp]
-
-(* The following lemma should appear in Divides.thy, but there the proof
- doesn't work. *)
-
-lemma nat_dvd_not_less:
- "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
- by (unfold dvd_def) auto
-
-ML {*
-val divide_minus1 = @{thm divide_minus1};
-val minus1_divide = @{thm minus1_divide};
-*}
-
-end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 23 07:41:07 2009 +0100
@@ -299,7 +299,7 @@
*} "Langford's algorithm for quantifier elimination in dense linear orders"
-section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
+section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *}
text {* Linear order without upper bounds *}
--- a/src/HOL/Divides.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Divides.thy Mon Mar 23 07:41:07 2009 +0100
@@ -1148,4 +1148,9 @@
with j show ?thesis by blast
qed
+lemma nat_dvd_not_less:
+ fixes m n :: nat
+ shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
end
--- a/src/HOL/Groebner_Basis.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Mon Mar 23 07:41:07 2009 +0100
@@ -5,7 +5,7 @@
header {* Semiring normalization and Groebner Bases *}
theory Groebner_Basis
-imports Arith_Tools
+imports NatBin
uses
"Tools/Groebner_Basis/misc.ML"
"Tools/Groebner_Basis/normalizer_data.ML"
--- a/src/HOL/Int.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Int.thy Mon Mar 23 07:41:07 2009 +0100
@@ -1256,14 +1256,14 @@
by (simp add: algebra_simps diff_number_of_eq [symmetric])
+
+
subsection {* The Set of Integers *}
context ring_1
begin
-definition
- Ints :: "'a set"
-where
+definition Ints :: "'a set" where
[code del]: "Ints = range of_int"
end
@@ -1854,7 +1854,7 @@
qed
-subsection{*Integer Powers*}
+subsection {* Integer Powers *}
instantiation int :: recpower
begin
@@ -1896,6 +1896,161 @@
lemmas zpower_int = int_power [symmetric]
+
+subsection {* Further theorems on numerals *}
+
+subsubsection{*Special Simplification for Constants*}
+
+text{*These distributive laws move literals inside sums and differences.*}
+
+lemmas left_distrib_number_of [simp] =
+ left_distrib [of _ _ "number_of v", standard]
+
+lemmas right_distrib_number_of [simp] =
+ right_distrib [of "number_of v", standard]
+
+lemmas left_diff_distrib_number_of [simp] =
+ left_diff_distrib [of _ _ "number_of v", standard]
+
+lemmas right_diff_distrib_number_of [simp] =
+ right_diff_distrib [of "number_of v", standard]
+
+text{*These are actually for fields, like real: but where else to put them?*}
+
+lemmas zero_less_divide_iff_number_of [simp, noatp] =
+ zero_less_divide_iff [of "number_of w", standard]
+
+lemmas divide_less_0_iff_number_of [simp, noatp] =
+ divide_less_0_iff [of "number_of w", standard]
+
+lemmas zero_le_divide_iff_number_of [simp, noatp] =
+ zero_le_divide_iff [of "number_of w", standard]
+
+lemmas divide_le_0_iff_number_of [simp, noatp] =
+ divide_le_0_iff [of "number_of w", standard]
+
+
+text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
+ strange, but then other simprocs simplify the quotient.*}
+
+lemmas inverse_eq_divide_number_of [simp] =
+ inverse_eq_divide [of "number_of w", standard]
+
+text {*These laws simplify inequalities, moving unary minus from a term
+into the literal.*}
+
+lemmas less_minus_iff_number_of [simp, noatp] =
+ less_minus_iff [of "number_of v", standard]
+
+lemmas le_minus_iff_number_of [simp, noatp] =
+ le_minus_iff [of "number_of v", standard]
+
+lemmas equation_minus_iff_number_of [simp, noatp] =
+ equation_minus_iff [of "number_of v", standard]
+
+lemmas minus_less_iff_number_of [simp, noatp] =
+ minus_less_iff [of _ "number_of v", standard]
+
+lemmas minus_le_iff_number_of [simp, noatp] =
+ minus_le_iff [of _ "number_of v", standard]
+
+lemmas minus_equation_iff_number_of [simp, noatp] =
+ minus_equation_iff [of _ "number_of v", standard]
+
+
+text{*To Simplify Inequalities Where One Side is the Constant 1*}
+
+lemma less_minus_iff_1 [simp,noatp]:
+ fixes b::"'b::{ordered_idom,number_ring}"
+ shows "(1 < - b) = (b < -1)"
+by auto
+
+lemma le_minus_iff_1 [simp,noatp]:
+ fixes b::"'b::{ordered_idom,number_ring}"
+ shows "(1 \<le> - b) = (b \<le> -1)"
+by auto
+
+lemma equation_minus_iff_1 [simp,noatp]:
+ fixes b::"'b::number_ring"
+ shows "(1 = - b) = (b = -1)"
+by (subst equation_minus_iff, auto)
+
+lemma minus_less_iff_1 [simp,noatp]:
+ fixes a::"'b::{ordered_idom,number_ring}"
+ shows "(- a < 1) = (-1 < a)"
+by auto
+
+lemma minus_le_iff_1 [simp,noatp]:
+ fixes a::"'b::{ordered_idom,number_ring}"
+ shows "(- a \<le> 1) = (-1 \<le> a)"
+by auto
+
+lemma minus_equation_iff_1 [simp,noatp]:
+ fixes a::"'b::number_ring"
+ shows "(- a = 1) = (a = -1)"
+by (subst minus_equation_iff, auto)
+
+
+text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
+
+lemmas mult_less_cancel_left_number_of [simp, noatp] =
+ mult_less_cancel_left [of "number_of v", standard]
+
+lemmas mult_less_cancel_right_number_of [simp, noatp] =
+ mult_less_cancel_right [of _ "number_of v", standard]
+
+lemmas mult_le_cancel_left_number_of [simp, noatp] =
+ mult_le_cancel_left [of "number_of v", standard]
+
+lemmas mult_le_cancel_right_number_of [simp, noatp] =
+ mult_le_cancel_right [of _ "number_of v", standard]
+
+
+text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
+
+lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
+lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
+lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
+
+
+subsubsection{*Optional Simplification Rules Involving Constants*}
+
+text{*Simplify quotients that are compared with a literal constant.*}
+
+lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
+lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
+lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
+lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
+lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
+lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
+
+
+text{*Not good as automatic simprules because they cause case splits.*}
+lemmas divide_const_simps =
+ le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
+ divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
+ le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
+
+text{*Division By @{text "-1"}*}
+
+lemma divide_minus1 [simp]:
+ "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
+by simp
+
+lemma minus1_divide [simp]:
+ "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
+by (simp add: divide_inverse inverse_minus_eq)
+
+lemma half_gt_zero_iff:
+ "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
+by auto
+
+lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
+
+
subsection {* Configuration of the code generator *}
code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
--- a/src/HOL/IntDiv.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/IntDiv.thy Mon Mar 23 07:41:07 2009 +0100
@@ -8,6 +8,10 @@
theory IntDiv
imports Int Divides FunDef
+uses
+ "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ "~~/src/Provers/Arith/extract_common_term.ML"
+ ("Tools/int_factor_simprocs.ML")
begin
definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -920,9 +924,10 @@
next
assume "a\<noteq>0" and le_a: "0\<le>a"
hence a_pos: "1 \<le> a" by arith
- hence one_less_a2: "1 < 2*a" by arith
+ hence one_less_a2: "1 < 2 * a" by arith
hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
- by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq)
+ unfolding mult_le_cancel_left
+ by (simp add: add1_zle_eq add_commute [of 1])
with a_pos have "0 \<le> b mod a" by simp
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
by (simp add: mod_pos_pos_trivial one_less_a2)
@@ -1357,6 +1362,11 @@
qed
+subsection {* Simproc setup *}
+
+use "Tools/int_factor_simprocs.ML"
+
+
subsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--- a/src/HOL/IsaMakefile Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/IsaMakefile Mon Mar 23 07:41:07 2009 +0100
@@ -204,7 +204,6 @@
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
- Arith_Tools.thy \
ATP_Linkup.thy \
Code_Eval.thy \
Code_Message.thy \
--- a/src/HOL/Library/Euclidean_Space.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Mar 23 07:41:07 2009 +0100
@@ -5,10 +5,10 @@
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
theory Euclidean_Space
- imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
+imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
Inner_Product
- uses ("normarith.ML")
+uses ("normarith.ML")
begin
text{* Some common special cases.*}
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 23 07:41:07 2009 +0100
@@ -6,10 +6,9 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
- imports SEQ Euclidean_Space
+imports SEQ Euclidean_Space
begin
-
declare fstcart_pastecart[simp] sndcart_pastecart[simp]
subsection{* General notion of a topology *}
@@ -474,7 +473,7 @@
have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym]
- by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1)
+ by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1)
then show ?thesis by blast
qed
@@ -662,7 +661,7 @@
have "?k/2 \<ge> 0" using kp by simp
then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist)
from iT[unfolded expand_set_eq mem_interior]
- have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+ have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: less_divide_eq_number_of1)
then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq)
have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp
using w e(1) d apply (auto simp only: dist_sym)
@@ -1323,7 +1322,7 @@
assume "e>0"
hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
"eventually (\<lambda>x. dist (g x) m < e/2) net" using as
- by (auto intro: tendstoD simp del: Arith_Tools.less_divide_eq_number_of1)
+ by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
proof(cases "trivial_limit net")
case True
@@ -3956,7 +3955,7 @@
hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
- have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1)
+ have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1)
hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar> \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto
hence "\<bar>f x * l\<bar> * 2 \<ge> \<bar>l\<bar>^2" unfolding real_mult_commute and power2_eq_square by auto
hence ***:"inverse \<bar>f x * l\<bar> \<le> inverse (l\<twosuperior> / 2)" using fxl0
@@ -4318,7 +4317,7 @@
have "a$i < b$i" using as[THEN spec[where x=i]] by auto
hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i"
unfolding vector_smult_component and vector_add_component
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1) }
+ by (auto simp add: less_divide_eq_number_of1) }
hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto }
ultimately show ?th1 by blast
@@ -4333,7 +4332,7 @@
have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
hence "a$i \<le> ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \<le> b$i"
unfolding vector_smult_component and vector_add_component
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1) }
+ by (auto simp add: less_divide_eq_number_of1) }
hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto }
ultimately show ?th2 by blast
qed
@@ -4397,13 +4396,13 @@
{ fix j
have "c $ j < ?x $ j \<and> ?x $ j < d $ j" unfolding Cart_lambda_beta
apply(cases "j=i") using as(2)[THEN spec[where x=j]]
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) }
+ by (auto simp add: less_divide_eq_number_of1 as2) }
hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
unfolding mem_interval apply auto apply(rule_tac x=i in exI)
using as(2)[THEN spec[where x=i]] and as2
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+ by (auto simp add: less_divide_eq_number_of1)
ultimately have False using as by auto }
hence "a$i \<le> c$i" by(rule ccontr)auto
moreover
@@ -4412,13 +4411,13 @@
{ fix j
have "d $ j > ?x $ j \<and> ?x $ j > c $ j" unfolding Cart_lambda_beta
apply(cases "j=i") using as(2)[THEN spec[where x=j]]
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) }
+ by (auto simp add: less_divide_eq_number_of1 as2) }
hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
unfolding mem_interval apply auto apply(rule_tac x=i in exI)
using as(2)[THEN spec[where x=i]] and as2
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+ by (auto simp add: less_divide_eq_number_of1)
ultimately have False using as by auto }
hence "b$i \<ge> d$i" by(rule ccontr)auto
ultimately
@@ -4449,7 +4448,7 @@
lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows
"{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
unfolding expand_set_eq and Int_iff and mem_interval
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI)
+ by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
(* Moved interval_open_subset_closed a bit upwards *)
@@ -4564,7 +4563,7 @@
have "a $ i < ((1 / 2) *s (a + b)) $ i \<and> ((1 / 2) *s (a + b)) $ i < b $ i"
using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
unfolding vector_smult_component and vector_add_component
- by(auto simp add: Arith_Tools.less_divide_eq_number_of1) }
+ by(auto simp add: less_divide_eq_number_of1) }
thus ?thesis unfolding mem_interval by auto
qed
@@ -5632,7 +5631,7 @@
{ assume as:"dist a b > dist (f n x) (f n y)"
then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
- using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: Arith_Tools.less_divide_eq_number_of1)
+ using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
apply(erule_tac x="Na+Nb+n" in allE)
apply(erule_tac x="Na+Nb+n" in allE) apply simp
--- a/src/HOL/NatBin.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/NatBin.thy Mon Mar 23 07:41:07 2009 +0100
@@ -7,6 +7,7 @@
theory NatBin
imports IntDiv
+uses ("Tools/nat_simprocs.ML")
begin
text {*
@@ -40,9 +41,7 @@
subsection {* Predicate for negative binary numbers *}
-definition
- neg :: "int \<Rightarrow> bool"
-where
+definition neg :: "int \<Rightarrow> bool" where
"neg Z \<longleftrightarrow> Z < 0"
lemma not_neg_int [simp]: "~ neg (of_nat n)"
@@ -818,4 +817,159 @@
"(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
by (simp add: nat_mult_div_cancel1)
+
+subsection {* Simprocs for the Naturals *}
+
+use "Tools/nat_simprocs.ML"
+declaration {* K nat_simprocs_setup *}
+
+subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
+
+text{*Where K above is a literal*}
+
+lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
+by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+
+text {*Now just instantiating @{text n} to @{text "number_of v"} does
+ the right simplification, but with some redundant inequality
+ tests.*}
+lemma neg_number_of_pred_iff_0:
+ "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
+apply (simp only: less_Suc_eq_le le_0_eq)
+apply (subst less_number_of_Suc, simp)
+done
+
+text{*No longer required as a simprule because of the @{text inverse_fold}
+ simproc*}
+lemma Suc_diff_number_of:
+ "Int.Pls < v ==>
+ Suc m - (number_of v) = m - (number_of (Int.pred v))"
+apply (subst Suc_diff_eq_diff_pred)
+apply simp
+apply (simp del: nat_numeral_1_eq_1)
+apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
+by (simp add: numerals split add: nat_diff_split)
+
+
+subsubsection{*For @{term nat_case} and @{term nat_rec}*}
+
+lemma nat_case_number_of [simp]:
+ "nat_case a f (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then a else f (nat pv))"
+by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
+
+lemma nat_case_add_eq_if [simp]:
+ "nat_case a f ((number_of v) + n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then nat_case a f n else f (nat pv + n))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ del: nat_numeral_1_eq_1
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+lemma nat_rec_number_of [simp]:
+ "nat_rec a f (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
+apply (case_tac " (number_of v) ::nat")
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
+apply (simp split add: split_if_asm)
+done
+
+lemma nat_rec_add_eq_if [simp]:
+ "nat_rec a f (number_of v + n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then nat_rec a f n
+ else f (nat pv + n) (nat_rec a f (nat pv + n)))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ del: nat_numeral_1_eq_1
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+
+subsubsection{*Various Other Lemmas*}
+
+text {*Evens and Odds, for Mutilated Chess Board*}
+
+text{*Lemmas for specialist use, NOT as default simprules*}
+lemma nat_mult_2: "2 * z = (z+z::nat)"
+proof -
+ have "2*z = (1 + 1)*z" by simp
+ also have "... = z+z" by (simp add: left_distrib)
+ finally show ?thesis .
+qed
+
+lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
+by (subst mult_commute, rule nat_mult_2)
+
+text{*Case analysis on @{term "n<2"}*}
+lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
+by arith
+
+lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
+by arith
+
+lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
+by (simp add: nat_mult_2 [symmetric])
+
+lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
+apply (subgoal_tac "m mod 2 < 2")
+apply (erule less_2_cases [THEN disjE])
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+done
+
+lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
+apply (subgoal_tac "m mod 2 < 2")
+apply (force simp del: mod_less_divisor, simp)
+done
+
+text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
+
+lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
+by simp
+
+lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
+by simp
+
+text{*Can be used to eliminate long strings of Sucs, but not by default*}
+lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
+by simp
+
+
+text{*These lemmas collapse some needless occurrences of Suc:
+ at least three Sucs, since two and fewer are rewritten back to Suc again!
+ We already have some rules to simplify operands smaller than 3.*}
+
+lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
+by (simp add: Suc3_eq_add_3)
+
+lemmas Suc_div_eq_add3_div_number_of =
+ Suc_div_eq_add3_div [of _ "number_of v", standard]
+declare Suc_div_eq_add3_div_number_of [simp]
+
+lemmas Suc_mod_eq_add3_mod_number_of =
+ Suc_mod_eq_add3_mod [of _ "number_of v", standard]
+declare Suc_mod_eq_add3_mod_number_of [simp]
+
end
--- a/src/HOL/Presburger.thy Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Presburger.thy Mon Mar 23 07:41:07 2009 +0100
@@ -7,6 +7,7 @@
theory Presburger
imports Groebner_Basis SetInterval
uses
+ "Tools/Qelim/qelim.ML"
"Tools/Qelim/cooper_data.ML"
"Tools/Qelim/generated_cooper.ML"
("Tools/Qelim/cooper.ML")
--- a/src/HOL/Tools/Qelim/qelim.ML Sun Mar 22 21:48:14 2009 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Mar 23 07:41:07 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/Qelim/qelim.ML
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
Generic quantifier elimination conversions for HOL formulae.
@@ -26,11 +25,12 @@
case (term_of p) of
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
- andalso s mem ["op &","op |","op -->","op ="]
+ andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
+ @{const_name "op -->"}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
- | Const("Not",_)$_ => arg_conv (conv env) p
- | Const("Ex",_)$Abs(s,_,_) =>
+ | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
+ | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
let
val (e,p0) = Thm.dest_comb p
val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
val (l,r) = Thm.dest_equals (cprop_of th')
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
- | Const("Ex",_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const("All",_)$_ =>
+ | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+ | Const(@{const_name "All"},_)$_ =>
let
val p = Thm.dest_arg p
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)