# HG changeset patch # User haftmann # Date 1256800479 -3600 # Node ID dfda7461950926ff3e0155c15df7fafabd65688a # Parent ce8faf41b0d4600b3472e50cc4faef6a51ee8c0b# Parent d76d968a4ec3d79d1e136d2e41c4f3fc4f9ab7e0 merged diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Code_Numeral.thy Thu Oct 29 08:14:39 2009 +0100 @@ -3,7 +3,7 @@ header {* Type of target language numerals *} theory Code_Numeral -imports Nat_Numeral +imports Nat_Numeral Divides begin text {* diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Divides.thy Thu Oct 29 08:14:39 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\nat) mod 2 \ m mod 2 = 1" +proof - + { fix n :: nat have "(n::nat) < 2 \ n = 0 \ n = 1" by (induct n) simp_all } + moreover have "m mod 2 < 2" by simp + ultimately have "m mod 2 = 0 \ 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 (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 \ (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 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 diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Thu Oct 29 08:14:39 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" diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Int.thy Thu Oct 29 08:14:39 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 \ (0::int)"; + "1 + z + z \ (0::int)" proof (cases z rule: int_cases) case (nonneg n) have le: "0 \ 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 \ 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 \ 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: "\ 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 (\i\int. 2 * i)" + by (rule injI) simp + ultimately have "surj (\i\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 diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/IntDiv.thy Thu Oct 29 08:14:39 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 *} diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/IsaMakefile Thu Oct 29 08:14:39 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 \ diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Nat_Numeral.thy Thu Oct 29 08:14:39 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)\ = x\ + y\ + 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)\ = x\ + y\ - 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 \ 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 \ 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 \ (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 (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 \ (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 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 diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Plain.thy --- a/src/HOL/Plain.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Plain.thy Thu Oct 29 08:14:39 2009 +0100 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype FunDef Record Extraction Divides +imports Datatype FunDef Record Extraction begin text {* diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/Tools/int_arith.ML Thu Oct 29 08:14:39 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} diff -r ce8faf41b0d4 -r dfda74619509 src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Wed Oct 28 23:21:45 2009 +0100 +++ b/src/HOL/ex/Numeral.thy Thu Oct 29 08:14:39 2009 +0100 @@ -5,7 +5,7 @@ header {* An experimental alternative numeral representation. *} theory Numeral -imports Int Inductive +imports Plain Divides begin subsection {* The @{text num} type *}