--- a/src/HOL/Code_Numeral.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Oct 28 19:09:47 2009 +0100
@@ -3,7 +3,7 @@
header {* Type of target language numerals *}
theory Code_Numeral
-imports Nat_Numeral
+imports Nat_Numeral Divides
begin
text {*
--- a/src/HOL/Divides.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Divides.thy Wed Oct 28 19:09:47 2009 +0100
@@ -6,8 +6,16 @@
header {* The division operators div and mod *}
theory Divides
-imports Nat Power Product_Type
-uses "~~/src/Provers/Arith/cancel_div_mod.ML"
+imports Nat_Numeral
+uses
+ "~~/src/Provers/Arith/assoc_fold.ML"
+ "~~/src/Provers/Arith/cancel_numerals.ML"
+ "~~/src/Provers/Arith/combine_numerals.ML"
+ "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ "~~/src/Provers/Arith/extract_common_term.ML"
+ ("Tools/numeral_simprocs.ML")
+ ("Tools/nat_numeral_simprocs.ML")
+ "~~/src/Provers/Arith/cancel_div_mod.ML"
begin
subsection {* Syntactic division operations *}
@@ -1092,4 +1100,158 @@
with j show ?thesis by blast
qed
+lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
+by (auto simp add: numeral_2_eq_2 le_div_geq)
+
+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]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
+proof -
+ { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all }
+ moreover have "m mod 2 < 2" by simp
+ ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
+ then show ?thesis by auto
+qed
+
+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]
+
+
+subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}
+
+declare split_div[of _ _ "number_of k", standard, arith_split]
+declare split_mod[of _ _ "number_of k", standard, arith_split]
+
+
+subsubsection{*For @{text combine_numerals}*}
+
+lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
+by (simp add: add_mult_distrib)
+
+
+subsubsection{*For @{text cancel_numerals}*}
+
+lemma nat_diff_add_eq1:
+ "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_diff_add_eq2:
+ "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_eq_add_iff1:
+ "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_eq_add_iff2:
+ "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff1:
+ "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff2:
+ "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff1:
+ "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff2:
+ "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+
+subsubsection{*For @{text cancel_numeral_factors} *}
+
+lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
+by auto
+
+lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
+by auto
+
+lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
+by auto
+
+lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
+by auto
+
+lemma nat_mult_dvd_cancel_disj[simp]:
+ "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
+by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
+
+lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
+by(auto)
+
+
+subsubsection{*For @{text cancel_factor} *}
+
+lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
+by auto
+
+lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
+by auto
+
+lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
+by auto
+
+lemma nat_mult_div_cancel_disj[simp]:
+ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
+by (simp add: nat_mult_div_cancel1)
+
+
+use "Tools/numeral_simprocs.ML"
+
+use "Tools/nat_numeral_simprocs.ML"
+
+declaration {*
+ K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
+ #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
+ @{thm nat_0}, @{thm nat_1},
+ @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
+ @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
+ @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
+ @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
+ @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
+ @{thm mult_Suc}, @{thm mult_Suc_right},
+ @{thm add_Suc}, @{thm add_Suc_right},
+ @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
+ @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
+ @{thm if_True}, @{thm if_False}])
+ #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
+ :: Numeral_Simprocs.combine_numerals
+ :: Numeral_Simprocs.cancel_numerals)
+ #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
+*}
+
end
--- a/src/HOL/Groebner_Basis.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Wed Oct 28 19:09:47 2009 +0100
@@ -5,7 +5,7 @@
header {* Semiring normalization and Groebner Bases *}
theory Groebner_Basis
-imports Nat_Numeral
+imports IntDiv
uses
"Tools/Groebner_Basis/misc.ML"
"Tools/Groebner_Basis/normalizer_data.ML"
--- a/src/HOL/Int.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Int.thy Wed Oct 28 19:09:47 2009 +0100
@@ -13,12 +13,6 @@
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
("Tools/int_arith.ML")
- "~~/src/Provers/Arith/assoc_fold.ML"
- "~~/src/Provers/Arith/cancel_numerals.ML"
- "~~/src/Provers/Arith/combine_numerals.ML"
- "~~/src/Provers/Arith/cancel_numeral_factor.ML"
- "~~/src/Provers/Arith/extract_common_term.ML"
- ("Tools/numeral_simprocs.ML")
begin
subsection {* The equivalence relation underlying the integers *}
@@ -1093,7 +1087,7 @@
lemmas double_eq_0_iff = double_zero
lemma odd_nonzero:
- "1 + z + z \<noteq> (0::int)";
+ "1 + z + z \<noteq> (0::int)"
proof (cases z rule: int_cases)
case (nonneg n)
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
@@ -1163,7 +1157,7 @@
qed
lemma odd_less_0:
- "(1 + z + z < 0) = (z < (0::int))";
+ "(1 + z + z < 0) = (z < (0::int))"
proof (cases z rule: int_cases)
case (nonneg n)
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
@@ -1368,7 +1362,7 @@
lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
- shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
+ shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
then obtain z where a: "a = of_int z" ..
@@ -1503,8 +1497,6 @@
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
-use "Tools/numeral_simprocs.ML"
-
use "Tools/int_arith.ML"
setup {* Int_Arith.global_setup *}
declaration {* K Int_Arith.setup *}
@@ -1540,11 +1532,7 @@
text{*Lemmas for specialist use, NOT as default simprules*}
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
-proof -
- have "2*z = (1 + 1)*z" by simp
- also have "... = z+z" by (simp add: left_distrib)
- finally show ?thesis .
-qed
+unfolding one_add_one_is_two [symmetric] left_distrib by simp
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
by (subst mult_commute, rule mult_2)
@@ -1830,14 +1818,15 @@
apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
-(* Could be simplified but Presburger only becomes available too late *)
-lemma infinite_UNIV_int: "~finite(UNIV::int set)"
+lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
proof
- assume "finite(UNIV::int set)"
- moreover have "~(EX i::int. 2*i = 1)"
- by (auto simp: pos_zmult_eq_1_iff)
- ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
- by (simp add:inj_on_def surj_def) (blast intro:sym)
+ assume "finite (UNIV::int set)"
+ moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
+ by (rule injI) simp
+ ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
+ by (rule finite_UNIV_inj_surj)
+ then obtain i :: int where "1 = 2 * i" by (rule surjE)
+ then show False by (simp add: pos_zmult_eq_1_iff)
qed
--- a/src/HOL/IntDiv.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/IntDiv.thy Wed Oct 28 19:09:47 2009 +0100
@@ -1318,6 +1318,36 @@
thus ?lhs by simp
qed
+lemma div_nat_number_of [simp]:
+ "(number_of v :: nat) div number_of v' =
+ (if neg (number_of v :: int) then 0
+ else nat (number_of v div number_of v'))"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by (simp add: nat_div_distrib)
+
+lemma one_div_nat_number_of [simp]:
+ "Suc 0 div number_of v' = nat (1 div number_of v')"
+by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
+
+lemma mod_nat_number_of [simp]:
+ "(number_of v :: nat) mod number_of v' =
+ (if neg (number_of v :: int) then 0
+ else if neg (number_of v' :: int) then number_of v
+ else nat (number_of v mod number_of v'))"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by (simp add: nat_mod_distrib)
+
+lemma one_mod_nat_number_of [simp]:
+ "Suc 0 mod number_of v' =
+ (if neg (number_of v' :: int) then Suc 0
+ else nat (1 mod number_of v'))"
+by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
+
+lemmas dvd_eq_mod_eq_0_number_of =
+ dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare dvd_eq_mod_eq_0_number_of [simp]
+
subsection {* Code generation *}
--- a/src/HOL/IsaMakefile Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/IsaMakefile Wed Oct 28 19:09:47 2009 +0100
@@ -138,7 +138,6 @@
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
Complete_Lattice.thy \
Datatype.thy \
- Divides.thy \
Extraction.thy \
Finite_Set.thy \
Fun.thy \
@@ -246,6 +245,7 @@
ATP_Linkup.thy \
Code_Evaluation.thy \
Code_Numeral.thy \
+ Divides.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
--- a/src/HOL/Nat_Numeral.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Nat_Numeral.thy Wed Oct 28 19:09:47 2009 +0100
@@ -6,8 +6,7 @@
header {* Binary numerals for the natural numbers *}
theory Nat_Numeral
-imports IntDiv
-uses ("Tools/nat_numeral_simprocs.ML")
+imports Int
begin
subsection {* Numerals for natural numbers *}
@@ -246,12 +245,12 @@
lemma power2_sum:
fixes x y :: "'a::number_ring"
shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
- by (simp add: ring_distribs power2_eq_square)
+ by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
lemma power2_diff:
fixes x y :: "'a::number_ring"
shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
- by (simp add: ring_distribs power2_eq_square)
+ by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
subsection {* Predicate for negative binary numbers *}
@@ -417,45 +416,6 @@
by (simp add: nat_mult_distrib)
-subsubsection{*Quotient *}
-
-lemma div_nat_number_of [simp]:
- "(number_of v :: nat) div number_of v' =
- (if neg (number_of v :: int) then 0
- else nat (number_of v div number_of v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
- by (simp add: nat_div_distrib)
-
-lemma one_div_nat_number_of [simp]:
- "Suc 0 div number_of v' = nat (1 div number_of v')"
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
-
-
-subsubsection{*Remainder *}
-
-lemma mod_nat_number_of [simp]:
- "(number_of v :: nat) mod number_of v' =
- (if neg (number_of v :: int) then 0
- else if neg (number_of v' :: int) then number_of v
- else nat (number_of v mod number_of v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
- by (simp add: nat_mod_distrib)
-
-lemma one_mod_nat_number_of [simp]:
- "Suc 0 mod number_of v' =
- (if neg (number_of v' :: int) then Suc 0
- else nat (1 mod number_of v'))"
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
-
-
-subsubsection{* Divisibility *}
-
-lemmas dvd_eq_mod_eq_0_number_of =
- dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
-
-declare dvd_eq_mod_eq_0_number_of [simp]
-
-
subsection{*Comparisons*}
subsubsection{*Equals (=) *}
@@ -687,21 +647,16 @@
lemma power_number_of_even:
fixes z :: "'a::number_ring"
shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
-unfolding Let_def nat_number_of_def number_of_Bit0
-apply (rule_tac x = "number_of w" in spec, clarify)
-apply (case_tac " (0::int) <= x")
-apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
-done
+by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
+ nat_add_distrib power_add simp del: nat_number_of)
lemma power_number_of_odd:
fixes z :: "'a::number_ring"
shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
then (let w = z ^ (number_of w) in z * w * w) else 1)"
-unfolding Let_def nat_number_of_def number_of_Bit1
-apply (rule_tac x = "number_of w" in spec, auto)
-apply (simp only: nat_add_distrib nat_mult_distrib)
-apply simp
-apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
+apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id
+ mult_assoc nat_add_distrib power_add not_le simp del: nat_number_of)
+apply (simp add: not_le mult_2 [symmetric] add_assoc)
done
lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
@@ -713,11 +668,6 @@
lemmas power_number_of_odd_number_of [simp] =
power_number_of_odd [of "number_of v", standard]
-
-(* Enable arith to deal with div/mod k where k is a numeral: *)
-declare split_div[of _ _ "number_of k", standard, arith_split]
-declare split_mod[of _ _ "number_of k", standard, arith_split]
-
lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
by (simp add: number_of_Pls nat_number_of_def)
@@ -727,22 +677,24 @@
lemma nat_number_of_Bit0:
"number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
- unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
- by auto
+by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
+ nat_add_distrib simp del: nat_number_of)
lemma nat_number_of_Bit1:
"number_of (Int.Bit1 w) =
(if neg (number_of w :: int) then 0
else let n = number_of w in Suc (n + n))"
- unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
- by auto
+apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
+ nat_add_distrib simp del: nat_number_of)
+apply (simp add: mult_2 [symmetric] add_assoc)
+done
lemmas nat_number =
nat_number_of_Pls nat_number_of_Min
nat_number_of_Bit0 nat_number_of_Bit1
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
- by (simp add: Let_def)
+ by (fact Let_def)
lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
by (simp only: number_of_Min power_minus1_even)
@@ -750,6 +702,20 @@
lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
by (simp only: number_of_Min power_minus1_odd)
+lemma nat_number_of_add_left:
+ "number_of v + (number_of v' + (k::nat)) =
+ (if neg (number_of v :: int) then number_of v' + k
+ else if neg (number_of v' :: int) then number_of v + k
+ else number_of (v + v') + k)"
+by (auto simp add: neg_def)
+
+lemma nat_number_of_mult_left:
+ "number_of v * (number_of v' * (k::nat)) =
+ (if v < Int.Pls then 0
+ else number_of (v * v') * k)"
+by (auto simp add: not_less Pls_def nat_number_of_def number_of_is_id
+ nat_mult_distrib simp del: nat_number_of)
+
subsection{*Literal arithmetic and @{term of_nat}*}
@@ -765,7 +731,7 @@
(if 0 \<le> (number_of v :: int)
then (number_of v :: 'a :: number_ring)
else 0)"
-by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
+by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat)
lemma of_nat_number_of_eq [simp]:
"of_nat (number_of v :: nat) =
@@ -774,124 +740,6 @@
by (simp only: of_nat_number_of_lemma neg_def, simp)
-subsection {*Lemmas for the Combination and Cancellation Simprocs*}
-
-lemma nat_number_of_add_left:
- "number_of v + (number_of v' + (k::nat)) =
- (if neg (number_of v :: int) then number_of v' + k
- else if neg (number_of v' :: int) then number_of v + k
- else number_of (v + v') + k)"
- unfolding nat_number_of_def number_of_is_id neg_def
- by auto
-
-lemma nat_number_of_mult_left:
- "number_of v * (number_of v' * (k::nat)) =
- (if v < Int.Pls then 0
- else number_of (v * v') * k)"
-by simp
-
-
-subsubsection{*For @{text combine_numerals}*}
-
-lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
-by (simp add: add_mult_distrib)
-
-
-subsubsection{*For @{text cancel_numerals}*}
-
-lemma nat_diff_add_eq1:
- "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
-by (simp split add: nat_diff_split add: add_mult_distrib)
-
-lemma nat_diff_add_eq2:
- "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
-by (simp split add: nat_diff_split add: add_mult_distrib)
-
-lemma nat_eq_add_iff1:
- "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_eq_add_iff2:
- "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_less_add_iff1:
- "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_less_add_iff2:
- "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_le_add_iff1:
- "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_le_add_iff2:
- "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-
-subsubsection{*For @{text cancel_numeral_factors} *}
-
-lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
-by auto
-
-lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
-by auto
-
-lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
-by auto
-
-lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
-by auto
-
-lemma nat_mult_dvd_cancel_disj[simp]:
- "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
-by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
-
-lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
-by(auto)
-
-
-subsubsection{*For @{text cancel_factor} *}
-
-lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
-by auto
-
-lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
-by auto
-
-lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
-by auto
-
-lemma nat_mult_div_cancel_disj[simp]:
- "(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_numeral_simprocs.ML"
-
-declaration {*
- K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
- #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
- @{thm nat_0}, @{thm nat_1},
- @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
- @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
- @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
- @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
- @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
- @{thm mult_Suc}, @{thm mult_Suc_right},
- @{thm add_Suc}, @{thm add_Suc_right},
- @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
- @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
- @{thm if_True}, @{thm if_False}])
- #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
-*}
-
-
subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
text{*Where K above is a literal*}
@@ -977,35 +825,14 @@
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
+unfolding nat_1_add_1 [symmetric] left_distrib by simp
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
+by (auto simp add: nat_1_add_1 [symmetric])
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
@@ -1019,29 +846,4 @@
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/Plain.thy Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Plain.thy Wed Oct 28 19:09:47 2009 +0100
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction Divides
+imports Datatype FunDef Record Extraction
begin
text {*
--- a/src/HOL/Tools/int_arith.ML Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML Wed Oct 28 19:09:47 2009 +0100
@@ -98,9 +98,7 @@
#> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
#> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
@ @{thms arith_special} @ @{thms int_arith_rules})
- #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
- :: Numeral_Simprocs.combine_numerals
- :: Numeral_Simprocs.cancel_numerals)
+ #> 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)
#> Lin_Arith.add_discrete_type @{type_name Int.int}