moved theory Divides after theory Nat_Numeral; tuned some proof texts
authorhaftmann
Wed Oct 28 19:09:47 2009 +0100 (2009-10-28)
changeset 33296a3924d1069e5
parent 33275 b497b2574bf6
child 33297 d76d968a4ec3
moved theory Divides after theory Nat_Numeral; tuned some proof texts
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/IsaMakefile
src/HOL/Nat_Numeral.thy
src/HOL/Plain.thy
src/HOL/Tools/int_arith.ML
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Oct 28 17:44:03 2009 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Oct 28 19:09:47 2009 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Type of target language numerals *}
     1.5  
     1.6  theory Code_Numeral
     1.7 -imports Nat_Numeral
     1.8 +imports Nat_Numeral Divides
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Divides.thy	Wed Oct 28 17:44:03 2009 +0100
     2.2 +++ b/src/HOL/Divides.thy	Wed Oct 28 19:09:47 2009 +0100
     2.3 @@ -6,8 +6,16 @@
     2.4  header {* The division operators div and mod *}
     2.5  
     2.6  theory Divides
     2.7 -imports Nat Power Product_Type
     2.8 -uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     2.9 +imports Nat_Numeral
    2.10 +uses
    2.11 +  "~~/src/Provers/Arith/assoc_fold.ML"
    2.12 +  "~~/src/Provers/Arith/cancel_numerals.ML"
    2.13 +  "~~/src/Provers/Arith/combine_numerals.ML"
    2.14 +  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    2.15 +  "~~/src/Provers/Arith/extract_common_term.ML"
    2.16 +  ("Tools/numeral_simprocs.ML")
    2.17 +  ("Tools/nat_numeral_simprocs.ML")
    2.18 +  "~~/src/Provers/Arith/cancel_div_mod.ML"
    2.19  begin
    2.20  
    2.21  subsection {* Syntactic division operations *}
    2.22 @@ -1092,4 +1100,158 @@
    2.23    with j show ?thesis by blast
    2.24  qed
    2.25  
    2.26 +lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
    2.27 +by (auto simp add: numeral_2_eq_2 le_div_geq)
    2.28 +
    2.29 +lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
    2.30 +by (simp add: nat_mult_2 [symmetric])
    2.31 +
    2.32 +lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
    2.33 +apply (subgoal_tac "m mod 2 < 2")
    2.34 +apply (erule less_2_cases [THEN disjE])
    2.35 +apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
    2.36 +done
    2.37 +
    2.38 +lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
    2.39 +proof -
    2.40 +  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all }
    2.41 +  moreover have "m mod 2 < 2" by simp
    2.42 +  ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
    2.43 +  then show ?thesis by auto
    2.44 +qed
    2.45 +
    2.46 +text{*These lemmas collapse some needless occurrences of Suc:
    2.47 +    at least three Sucs, since two and fewer are rewritten back to Suc again!
    2.48 +    We already have some rules to simplify operands smaller than 3.*}
    2.49 +
    2.50 +lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
    2.51 +by (simp add: Suc3_eq_add_3)
    2.52 +
    2.53 +lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
    2.54 +by (simp add: Suc3_eq_add_3)
    2.55 +
    2.56 +lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
    2.57 +by (simp add: Suc3_eq_add_3)
    2.58 +
    2.59 +lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
    2.60 +by (simp add: Suc3_eq_add_3)
    2.61 +
    2.62 +lemmas Suc_div_eq_add3_div_number_of =
    2.63 +    Suc_div_eq_add3_div [of _ "number_of v", standard]
    2.64 +declare Suc_div_eq_add3_div_number_of [simp]
    2.65 +
    2.66 +lemmas Suc_mod_eq_add3_mod_number_of =
    2.67 +    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
    2.68 +declare Suc_mod_eq_add3_mod_number_of [simp]
    2.69 +
    2.70 +
    2.71 +subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}
    2.72 +
    2.73 +declare split_div[of _ _ "number_of k", standard, arith_split]
    2.74 +declare split_mod[of _ _ "number_of k", standard, arith_split]
    2.75 +
    2.76 +
    2.77 +subsubsection{*For @{text combine_numerals}*}
    2.78 +
    2.79 +lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
    2.80 +by (simp add: add_mult_distrib)
    2.81 +
    2.82 +
    2.83 +subsubsection{*For @{text cancel_numerals}*}
    2.84 +
    2.85 +lemma nat_diff_add_eq1:
    2.86 +     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
    2.87 +by (simp split add: nat_diff_split add: add_mult_distrib)
    2.88 +
    2.89 +lemma nat_diff_add_eq2:
    2.90 +     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
    2.91 +by (simp split add: nat_diff_split add: add_mult_distrib)
    2.92 +
    2.93 +lemma nat_eq_add_iff1:
    2.94 +     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
    2.95 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
    2.96 +
    2.97 +lemma nat_eq_add_iff2:
    2.98 +     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
    2.99 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   2.100 +
   2.101 +lemma nat_less_add_iff1:
   2.102 +     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   2.103 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   2.104 +
   2.105 +lemma nat_less_add_iff2:
   2.106 +     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   2.107 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   2.108 +
   2.109 +lemma nat_le_add_iff1:
   2.110 +     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   2.111 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   2.112 +
   2.113 +lemma nat_le_add_iff2:
   2.114 +     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   2.115 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   2.116 +
   2.117 +
   2.118 +subsubsection{*For @{text cancel_numeral_factors} *}
   2.119 +
   2.120 +lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   2.121 +by auto
   2.122 +
   2.123 +lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   2.124 +by auto
   2.125 +
   2.126 +lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   2.127 +by auto
   2.128 +
   2.129 +lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   2.130 +by auto
   2.131 +
   2.132 +lemma nat_mult_dvd_cancel_disj[simp]:
   2.133 +  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
   2.134 +by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
   2.135 +
   2.136 +lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
   2.137 +by(auto)
   2.138 +
   2.139 +
   2.140 +subsubsection{*For @{text cancel_factor} *}
   2.141 +
   2.142 +lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   2.143 +by auto
   2.144 +
   2.145 +lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   2.146 +by auto
   2.147 +
   2.148 +lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   2.149 +by auto
   2.150 +
   2.151 +lemma nat_mult_div_cancel_disj[simp]:
   2.152 +     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   2.153 +by (simp add: nat_mult_div_cancel1)
   2.154 +
   2.155 +
   2.156 +use "Tools/numeral_simprocs.ML"
   2.157 +
   2.158 +use "Tools/nat_numeral_simprocs.ML"
   2.159 +
   2.160 +declaration {* 
   2.161 +  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   2.162 +  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
   2.163 +     @{thm nat_0}, @{thm nat_1},
   2.164 +     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   2.165 +     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   2.166 +     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   2.167 +     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   2.168 +     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   2.169 +     @{thm mult_Suc}, @{thm mult_Suc_right},
   2.170 +     @{thm add_Suc}, @{thm add_Suc_right},
   2.171 +     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   2.172 +     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   2.173 +     @{thm if_True}, @{thm if_False}])
   2.174 +  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
   2.175 +      :: Numeral_Simprocs.combine_numerals
   2.176 +      :: Numeral_Simprocs.cancel_numerals)
   2.177 +  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
   2.178 +*}
   2.179 +
   2.180  end
     3.1 --- a/src/HOL/Groebner_Basis.thy	Wed Oct 28 17:44:03 2009 +0100
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Oct 28 19:09:47 2009 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Semiring normalization and Groebner Bases *}
     3.5  
     3.6  theory Groebner_Basis
     3.7 -imports Nat_Numeral
     3.8 +imports IntDiv
     3.9  uses
    3.10    "Tools/Groebner_Basis/misc.ML"
    3.11    "Tools/Groebner_Basis/normalizer_data.ML"
     4.1 --- a/src/HOL/Int.thy	Wed Oct 28 17:44:03 2009 +0100
     4.2 +++ b/src/HOL/Int.thy	Wed Oct 28 19:09:47 2009 +0100
     4.3 @@ -13,12 +13,6 @@
     4.4    ("Tools/numeral.ML")
     4.5    ("Tools/numeral_syntax.ML")
     4.6    ("Tools/int_arith.ML")
     4.7 -  "~~/src/Provers/Arith/assoc_fold.ML"
     4.8 -  "~~/src/Provers/Arith/cancel_numerals.ML"
     4.9 -  "~~/src/Provers/Arith/combine_numerals.ML"
    4.10 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    4.11 -  "~~/src/Provers/Arith/extract_common_term.ML"
    4.12 -  ("Tools/numeral_simprocs.ML")
    4.13  begin
    4.14  
    4.15  subsection {* The equivalence relation underlying the integers *}
    4.16 @@ -1093,7 +1087,7 @@
    4.17  lemmas double_eq_0_iff = double_zero
    4.18  
    4.19  lemma odd_nonzero:
    4.20 -  "1 + z + z \<noteq> (0::int)";
    4.21 +  "1 + z + z \<noteq> (0::int)"
    4.22  proof (cases z rule: int_cases)
    4.23    case (nonneg n)
    4.24    have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
    4.25 @@ -1163,7 +1157,7 @@
    4.26  qed
    4.27  
    4.28  lemma odd_less_0:
    4.29 -  "(1 + z + z < 0) = (z < (0::int))";
    4.30 +  "(1 + z + z < 0) = (z < (0::int))"
    4.31  proof (cases z rule: int_cases)
    4.32    case (nonneg n)
    4.33    thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
    4.34 @@ -1368,7 +1362,7 @@
    4.35  
    4.36  lemma Ints_odd_less_0: 
    4.37    assumes in_Ints: "a \<in> Ints"
    4.38 -  shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
    4.39 +  shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))"
    4.40  proof -
    4.41    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
    4.42    then obtain z where a: "a = of_int z" ..
    4.43 @@ -1503,8 +1497,6 @@
    4.44    of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    4.45    of_int_0 of_int_1 of_int_add of_int_mult
    4.46  
    4.47 -use "Tools/numeral_simprocs.ML"
    4.48 -
    4.49  use "Tools/int_arith.ML"
    4.50  setup {* Int_Arith.global_setup *}
    4.51  declaration {* K Int_Arith.setup *}
    4.52 @@ -1540,11 +1532,7 @@
    4.53  
    4.54  text{*Lemmas for specialist use, NOT as default simprules*}
    4.55  lemma mult_2: "2 * z = (z+z::'a::number_ring)"
    4.56 -proof -
    4.57 -  have "2*z = (1 + 1)*z" by simp
    4.58 -  also have "... = z+z" by (simp add: left_distrib)
    4.59 -  finally show ?thesis .
    4.60 -qed
    4.61 +unfolding one_add_one_is_two [symmetric] left_distrib by simp
    4.62  
    4.63  lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
    4.64  by (subst mult_commute, rule mult_2)
    4.65 @@ -1830,14 +1818,15 @@
    4.66   apply (frule pos_zmult_eq_1_iff_lemma, auto) 
    4.67  done
    4.68  
    4.69 -(* Could be simplified but Presburger only becomes available too late *)
    4.70 -lemma infinite_UNIV_int: "~finite(UNIV::int set)"
    4.71 +lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
    4.72  proof
    4.73 -  assume "finite(UNIV::int set)"
    4.74 -  moreover have "~(EX i::int. 2*i = 1)"
    4.75 -    by (auto simp: pos_zmult_eq_1_iff)
    4.76 -  ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
    4.77 -    by (simp add:inj_on_def surj_def) (blast intro:sym)
    4.78 +  assume "finite (UNIV::int set)"
    4.79 +  moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
    4.80 +    by (rule injI) simp
    4.81 +  ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
    4.82 +    by (rule finite_UNIV_inj_surj)
    4.83 +  then obtain i :: int where "1 = 2 * i" by (rule surjE)
    4.84 +  then show False by (simp add: pos_zmult_eq_1_iff)
    4.85  qed
    4.86  
    4.87  
     5.1 --- a/src/HOL/IntDiv.thy	Wed Oct 28 17:44:03 2009 +0100
     5.2 +++ b/src/HOL/IntDiv.thy	Wed Oct 28 19:09:47 2009 +0100
     5.3 @@ -1318,6 +1318,36 @@
     5.4    thus  ?lhs by simp
     5.5  qed
     5.6  
     5.7 +lemma div_nat_number_of [simp]:
     5.8 +     "(number_of v :: nat)  div  number_of v' =  
     5.9 +          (if neg (number_of v :: int) then 0  
    5.10 +           else nat (number_of v div number_of v'))"
    5.11 +  unfolding nat_number_of_def number_of_is_id neg_def
    5.12 +  by (simp add: nat_div_distrib)
    5.13 +
    5.14 +lemma one_div_nat_number_of [simp]:
    5.15 +     "Suc 0 div number_of v' = nat (1 div number_of v')" 
    5.16 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    5.17 +
    5.18 +lemma mod_nat_number_of [simp]:
    5.19 +     "(number_of v :: nat)  mod  number_of v' =  
    5.20 +        (if neg (number_of v :: int) then 0  
    5.21 +         else if neg (number_of v' :: int) then number_of v  
    5.22 +         else nat (number_of v mod number_of v'))"
    5.23 +  unfolding nat_number_of_def number_of_is_id neg_def
    5.24 +  by (simp add: nat_mod_distrib)
    5.25 +
    5.26 +lemma one_mod_nat_number_of [simp]:
    5.27 +     "Suc 0 mod number_of v' =  
    5.28 +        (if neg (number_of v' :: int) then Suc 0
    5.29 +         else nat (1 mod number_of v'))"
    5.30 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    5.31 +
    5.32 +lemmas dvd_eq_mod_eq_0_number_of =
    5.33 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
    5.34 +
    5.35 +declare dvd_eq_mod_eq_0_number_of [simp]
    5.36 +
    5.37  
    5.38  subsection {* Code generation *}
    5.39  
     6.1 --- a/src/HOL/IsaMakefile	Wed Oct 28 17:44:03 2009 +0100
     6.2 +++ b/src/HOL/IsaMakefile	Wed Oct 28 19:09:47 2009 +0100
     6.3 @@ -138,7 +138,6 @@
     6.4  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
     6.5    Complete_Lattice.thy \
     6.6    Datatype.thy \
     6.7 -  Divides.thy \
     6.8    Extraction.thy \
     6.9    Finite_Set.thy \
    6.10    Fun.thy \
    6.11 @@ -246,6 +245,7 @@
    6.12    ATP_Linkup.thy \
    6.13    Code_Evaluation.thy \
    6.14    Code_Numeral.thy \
    6.15 +  Divides.thy \
    6.16    Equiv_Relations.thy \
    6.17    Groebner_Basis.thy \
    6.18    Hilbert_Choice.thy \
     7.1 --- a/src/HOL/Nat_Numeral.thy	Wed Oct 28 17:44:03 2009 +0100
     7.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Oct 28 19:09:47 2009 +0100
     7.3 @@ -6,8 +6,7 @@
     7.4  header {* Binary numerals for the natural numbers *}
     7.5  
     7.6  theory Nat_Numeral
     7.7 -imports IntDiv
     7.8 -uses ("Tools/nat_numeral_simprocs.ML")
     7.9 +imports Int
    7.10  begin
    7.11  
    7.12  subsection {* Numerals for natural numbers *}
    7.13 @@ -246,12 +245,12 @@
    7.14  lemma power2_sum:
    7.15    fixes x y :: "'a::number_ring"
    7.16    shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
    7.17 -  by (simp add: ring_distribs power2_eq_square)
    7.18 +  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
    7.19  
    7.20  lemma power2_diff:
    7.21    fixes x y :: "'a::number_ring"
    7.22    shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
    7.23 -  by (simp add: ring_distribs power2_eq_square)
    7.24 +  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
    7.25  
    7.26  
    7.27  subsection {* Predicate for negative binary numbers *}
    7.28 @@ -417,45 +416,6 @@
    7.29    by (simp add: nat_mult_distrib)
    7.30  
    7.31  
    7.32 -subsubsection{*Quotient *}
    7.33 -
    7.34 -lemma div_nat_number_of [simp]:
    7.35 -     "(number_of v :: nat)  div  number_of v' =  
    7.36 -          (if neg (number_of v :: int) then 0  
    7.37 -           else nat (number_of v div number_of v'))"
    7.38 -  unfolding nat_number_of_def number_of_is_id neg_def
    7.39 -  by (simp add: nat_div_distrib)
    7.40 -
    7.41 -lemma one_div_nat_number_of [simp]:
    7.42 -     "Suc 0 div number_of v' = nat (1 div number_of v')" 
    7.43 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    7.44 -
    7.45 -
    7.46 -subsubsection{*Remainder *}
    7.47 -
    7.48 -lemma mod_nat_number_of [simp]:
    7.49 -     "(number_of v :: nat)  mod  number_of v' =  
    7.50 -        (if neg (number_of v :: int) then 0  
    7.51 -         else if neg (number_of v' :: int) then number_of v  
    7.52 -         else nat (number_of v mod number_of v'))"
    7.53 -  unfolding nat_number_of_def number_of_is_id neg_def
    7.54 -  by (simp add: nat_mod_distrib)
    7.55 -
    7.56 -lemma one_mod_nat_number_of [simp]:
    7.57 -     "Suc 0 mod number_of v' =  
    7.58 -        (if neg (number_of v' :: int) then Suc 0
    7.59 -         else nat (1 mod number_of v'))"
    7.60 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    7.61 -
    7.62 -
    7.63 -subsubsection{* Divisibility *}
    7.64 -
    7.65 -lemmas dvd_eq_mod_eq_0_number_of =
    7.66 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
    7.67 -
    7.68 -declare dvd_eq_mod_eq_0_number_of [simp]
    7.69 -
    7.70 -
    7.71  subsection{*Comparisons*}
    7.72  
    7.73  subsubsection{*Equals (=) *}
    7.74 @@ -687,21 +647,16 @@
    7.75  lemma power_number_of_even:
    7.76    fixes z :: "'a::number_ring"
    7.77    shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
    7.78 -unfolding Let_def nat_number_of_def number_of_Bit0
    7.79 -apply (rule_tac x = "number_of w" in spec, clarify)
    7.80 -apply (case_tac " (0::int) <= x")
    7.81 -apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
    7.82 -done
    7.83 +by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
    7.84 +  nat_add_distrib power_add simp del: nat_number_of)
    7.85  
    7.86  lemma power_number_of_odd:
    7.87    fixes z :: "'a::number_ring"
    7.88    shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
    7.89       then (let w = z ^ (number_of w) in z * w * w) else 1)"
    7.90 -unfolding Let_def nat_number_of_def number_of_Bit1
    7.91 -apply (rule_tac x = "number_of w" in spec, auto)
    7.92 -apply (simp only: nat_add_distrib nat_mult_distrib)
    7.93 -apply simp
    7.94 -apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
    7.95 +apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id
    7.96 +  mult_assoc nat_add_distrib power_add not_le simp del: nat_number_of)
    7.97 +apply (simp add: not_le mult_2 [symmetric] add_assoc)
    7.98  done
    7.99  
   7.100  lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
   7.101 @@ -713,11 +668,6 @@
   7.102  lemmas power_number_of_odd_number_of [simp] =
   7.103      power_number_of_odd [of "number_of v", standard]
   7.104  
   7.105 -
   7.106 -(* Enable arith to deal with div/mod k where k is a numeral: *)
   7.107 -declare split_div[of _ _ "number_of k", standard, arith_split]
   7.108 -declare split_mod[of _ _ "number_of k", standard, arith_split]
   7.109 -
   7.110  lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   7.111    by (simp add: number_of_Pls nat_number_of_def)
   7.112  
   7.113 @@ -727,22 +677,24 @@
   7.114  
   7.115  lemma nat_number_of_Bit0:
   7.116      "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   7.117 -  unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
   7.118 -  by auto
   7.119 +by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   7.120 +  nat_add_distrib simp del: nat_number_of)
   7.121  
   7.122  lemma nat_number_of_Bit1:
   7.123    "number_of (Int.Bit1 w) =
   7.124      (if neg (number_of w :: int) then 0
   7.125       else let n = number_of w in Suc (n + n))"
   7.126 -  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
   7.127 -  by auto
   7.128 +apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
   7.129 +  nat_add_distrib simp del: nat_number_of)
   7.130 +apply (simp add: mult_2 [symmetric] add_assoc)
   7.131 +done
   7.132  
   7.133  lemmas nat_number =
   7.134    nat_number_of_Pls nat_number_of_Min
   7.135    nat_number_of_Bit0 nat_number_of_Bit1
   7.136  
   7.137  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   7.138 -  by (simp add: Let_def)
   7.139 +  by (fact Let_def)
   7.140  
   7.141  lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
   7.142    by (simp only: number_of_Min power_minus1_even)
   7.143 @@ -750,6 +702,20 @@
   7.144  lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
   7.145    by (simp only: number_of_Min power_minus1_odd)
   7.146  
   7.147 +lemma nat_number_of_add_left:
   7.148 +     "number_of v + (number_of v' + (k::nat)) =  
   7.149 +         (if neg (number_of v :: int) then number_of v' + k  
   7.150 +          else if neg (number_of v' :: int) then number_of v + k  
   7.151 +          else number_of (v + v') + k)"
   7.152 +by (auto simp add: neg_def)
   7.153 +
   7.154 +lemma nat_number_of_mult_left:
   7.155 +     "number_of v * (number_of v' * (k::nat)) =  
   7.156 +         (if v < Int.Pls then 0
   7.157 +          else number_of (v * v') * k)"
   7.158 +by (auto simp add: not_less Pls_def nat_number_of_def number_of_is_id
   7.159 +  nat_mult_distrib simp del: nat_number_of)
   7.160 +
   7.161  
   7.162  subsection{*Literal arithmetic and @{term of_nat}*}
   7.163  
   7.164 @@ -765,7 +731,7 @@
   7.165           (if 0 \<le> (number_of v :: int) 
   7.166            then (number_of v :: 'a :: number_ring)
   7.167            else 0)"
   7.168 -by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
   7.169 +by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat)
   7.170  
   7.171  lemma of_nat_number_of_eq [simp]:
   7.172       "of_nat (number_of v :: nat) =  
   7.173 @@ -774,124 +740,6 @@
   7.174  by (simp only: of_nat_number_of_lemma neg_def, simp) 
   7.175  
   7.176  
   7.177 -subsection {*Lemmas for the Combination and Cancellation Simprocs*}
   7.178 -
   7.179 -lemma nat_number_of_add_left:
   7.180 -     "number_of v + (number_of v' + (k::nat)) =  
   7.181 -         (if neg (number_of v :: int) then number_of v' + k  
   7.182 -          else if neg (number_of v' :: int) then number_of v + k  
   7.183 -          else number_of (v + v') + k)"
   7.184 -  unfolding nat_number_of_def number_of_is_id neg_def
   7.185 -  by auto
   7.186 -
   7.187 -lemma nat_number_of_mult_left:
   7.188 -     "number_of v * (number_of v' * (k::nat)) =  
   7.189 -         (if v < Int.Pls then 0
   7.190 -          else number_of (v * v') * k)"
   7.191 -by simp
   7.192 -
   7.193 -
   7.194 -subsubsection{*For @{text combine_numerals}*}
   7.195 -
   7.196 -lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   7.197 -by (simp add: add_mult_distrib)
   7.198 -
   7.199 -
   7.200 -subsubsection{*For @{text cancel_numerals}*}
   7.201 -
   7.202 -lemma nat_diff_add_eq1:
   7.203 -     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   7.204 -by (simp split add: nat_diff_split add: add_mult_distrib)
   7.205 -
   7.206 -lemma nat_diff_add_eq2:
   7.207 -     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   7.208 -by (simp split add: nat_diff_split add: add_mult_distrib)
   7.209 -
   7.210 -lemma nat_eq_add_iff1:
   7.211 -     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   7.212 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.213 -
   7.214 -lemma nat_eq_add_iff2:
   7.215 -     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   7.216 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.217 -
   7.218 -lemma nat_less_add_iff1:
   7.219 -     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   7.220 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.221 -
   7.222 -lemma nat_less_add_iff2:
   7.223 -     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   7.224 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.225 -
   7.226 -lemma nat_le_add_iff1:
   7.227 -     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   7.228 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.229 -
   7.230 -lemma nat_le_add_iff2:
   7.231 -     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   7.232 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.233 -
   7.234 -
   7.235 -subsubsection{*For @{text cancel_numeral_factors} *}
   7.236 -
   7.237 -lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   7.238 -by auto
   7.239 -
   7.240 -lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   7.241 -by auto
   7.242 -
   7.243 -lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   7.244 -by auto
   7.245 -
   7.246 -lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   7.247 -by auto
   7.248 -
   7.249 -lemma nat_mult_dvd_cancel_disj[simp]:
   7.250 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
   7.251 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
   7.252 -
   7.253 -lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
   7.254 -by(auto)
   7.255 -
   7.256 -
   7.257 -subsubsection{*For @{text cancel_factor} *}
   7.258 -
   7.259 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   7.260 -by auto
   7.261 -
   7.262 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   7.263 -by auto
   7.264 -
   7.265 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   7.266 -by auto
   7.267 -
   7.268 -lemma nat_mult_div_cancel_disj[simp]:
   7.269 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   7.270 -by (simp add: nat_mult_div_cancel1)
   7.271 -
   7.272 -
   7.273 -subsection {* Simprocs for the Naturals *}
   7.274 -
   7.275 -use "Tools/nat_numeral_simprocs.ML"
   7.276 -
   7.277 -declaration {* 
   7.278 -  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   7.279 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
   7.280 -     @{thm nat_0}, @{thm nat_1},
   7.281 -     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   7.282 -     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   7.283 -     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   7.284 -     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   7.285 -     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   7.286 -     @{thm mult_Suc}, @{thm mult_Suc_right},
   7.287 -     @{thm add_Suc}, @{thm add_Suc_right},
   7.288 -     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   7.289 -     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   7.290 -     @{thm if_True}, @{thm if_False}])
   7.291 -  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
   7.292 -*}
   7.293 -
   7.294 -
   7.295  subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   7.296  
   7.297  text{*Where K above is a literal*}
   7.298 @@ -977,35 +825,14 @@
   7.299  
   7.300  text{*Lemmas for specialist use, NOT as default simprules*}
   7.301  lemma nat_mult_2: "2 * z = (z+z::nat)"
   7.302 -proof -
   7.303 -  have "2*z = (1 + 1)*z" by simp
   7.304 -  also have "... = z+z" by (simp add: left_distrib)
   7.305 -  finally show ?thesis .
   7.306 -qed
   7.307 +unfolding nat_1_add_1 [symmetric] left_distrib by simp
   7.308  
   7.309  lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   7.310  by (subst mult_commute, rule nat_mult_2)
   7.311  
   7.312  text{*Case analysis on @{term "n<2"}*}
   7.313  lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   7.314 -by arith
   7.315 -
   7.316 -lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
   7.317 -by arith
   7.318 -
   7.319 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   7.320 -by (simp add: nat_mult_2 [symmetric])
   7.321 -
   7.322 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
   7.323 -apply (subgoal_tac "m mod 2 < 2")
   7.324 -apply (erule less_2_cases [THEN disjE])
   7.325 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
   7.326 -done
   7.327 -
   7.328 -lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
   7.329 -apply (subgoal_tac "m mod 2 < 2")
   7.330 -apply (force simp del: mod_less_divisor, simp)
   7.331 -done
   7.332 +by (auto simp add: nat_1_add_1 [symmetric])
   7.333  
   7.334  text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   7.335  
   7.336 @@ -1019,29 +846,4 @@
   7.337  lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   7.338  by simp
   7.339  
   7.340 -
   7.341 -text{*These lemmas collapse some needless occurrences of Suc:
   7.342 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
   7.343 -    We already have some rules to simplify operands smaller than 3.*}
   7.344 -
   7.345 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   7.346 -by (simp add: Suc3_eq_add_3)
   7.347 -
   7.348 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   7.349 -by (simp add: Suc3_eq_add_3)
   7.350 -
   7.351 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   7.352 -by (simp add: Suc3_eq_add_3)
   7.353 -
   7.354 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   7.355 -by (simp add: Suc3_eq_add_3)
   7.356 -
   7.357 -lemmas Suc_div_eq_add3_div_number_of =
   7.358 -    Suc_div_eq_add3_div [of _ "number_of v", standard]
   7.359 -declare Suc_div_eq_add3_div_number_of [simp]
   7.360 -
   7.361 -lemmas Suc_mod_eq_add3_mod_number_of =
   7.362 -    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
   7.363 -declare Suc_mod_eq_add3_mod_number_of [simp]
   7.364 -
   7.365  end
     8.1 --- a/src/HOL/Plain.thy	Wed Oct 28 17:44:03 2009 +0100
     8.2 +++ b/src/HOL/Plain.thy	Wed Oct 28 19:09:47 2009 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  header {* Plain HOL *}
     8.5  
     8.6  theory Plain
     8.7 -imports Datatype FunDef Record Extraction Divides
     8.8 +imports Datatype FunDef Record Extraction
     8.9  begin
    8.10  
    8.11  text {*
     9.1 --- a/src/HOL/Tools/int_arith.ML	Wed Oct 28 17:44:03 2009 +0100
     9.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Oct 28 19:09:47 2009 +0100
     9.3 @@ -98,9 +98,7 @@
     9.4    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
     9.5    #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
     9.6        @ @{thms arith_special} @ @{thms int_arith_rules})
     9.7 -  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
     9.8 -      :: Numeral_Simprocs.combine_numerals
     9.9 -      :: Numeral_Simprocs.cancel_numerals)
    9.10 +  #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    9.11    #> Lin_Arith.set_number_of number_of
    9.12    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
    9.13    #> Lin_Arith.add_discrete_type @{type_name Int.int}