src/HOL/Integ/NatBin.thy
 changeset 14390 55fe71faadda parent 14387 e96d5c42c4b0 child 14417 34ffa53db76c
1.1 --- a/src/HOL/Integ/NatBin.thy	Mon Feb 16 15:24:03 2004 +0100
1.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Feb 17 10:41:59 2004 +0100
1.3 @@ -86,7 +86,7 @@
1.7 -(** Successor **)
1.8 +subsubsection{*Successor *}
1.10  lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
1.11  apply (rule sym)
1.12 @@ -108,7 +108,7 @@
1.13  done
1.19  (*"neg" is used in rewrite rules for binary comparisons*)
1.21 @@ -121,7 +121,7 @@
1.25 -(** Subtraction **)
1.26 +subsubsection{*Subtraction *}
1.28  lemma diff_nat_eq_if:
1.29       "nat z - nat z' =
1.30 @@ -141,7 +141,7 @@
1.34 -(** Multiplication **)
1.35 +subsubsection{*Multiplication *}
1.37  lemma mult_nat_number_of [simp]:
1.38       "(number_of v :: nat) * number_of v' =
1.39 @@ -152,7 +152,7 @@
1.43 -(** Quotient **)
1.44 +subsubsection{*Quotient *}
1.46  lemma div_nat_number_of [simp]:
1.47       "(number_of v :: nat)  div  number_of v' =
1.48 @@ -167,7 +167,7 @@
1.49  by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
1.52 -(** Remainder **)
1.53 +subsubsection{*Remainder *}
1.55  lemma mod_nat_number_of [simp]:
1.56       "(number_of v :: nat)  mod  number_of v' =
1.57 @@ -210,16 +210,16 @@
1.58  *}
1.61 -(*** Comparisons ***)
1.62 +subsection{*Comparisons*}
1.64 -(** Equals (=) **)
1.65 +subsubsection{*Equals (=) *}
1.67  lemma eq_nat_nat_iff:
1.68       "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
1.69  by (auto elim!: nonneg_eq_int)
1.71  (*"neg" is used in rewrite rules for binary comparisons*)
1.72 -lemma eq_nat_number_of:
1.73 +lemma eq_nat_number_of [simp]:
1.74       "((number_of v :: nat) = number_of v') =
1.75        (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))
1.76         else if neg (number_of v' :: int) then iszero (number_of v :: int)
1.77 @@ -231,21 +231,19 @@
1.78  apply (simp add: not_neg_eq_ge_0 [symmetric])
1.79  done
1.81 -declare eq_nat_number_of [simp]
1.83 -(** Less-than (<) **)
1.84 +subsubsection{*Less-than (<) *}
1.86  (*"neg" is used in rewrite rules for binary comparisons*)
1.87 -lemma less_nat_number_of:
1.88 +lemma less_nat_number_of [simp]:
1.89       "((number_of v :: nat) < number_of v') =
1.90           (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)
1.91            else neg (number_of (bin_add v (bin_minus v')) :: int))"
1.92 -apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
1.93 +by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
1.94                  nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
1.95 -            cong add: imp_cong, simp)
1.96 -done
1.97 +         cong add: imp_cong, simp)
1.99 -declare less_nat_number_of [simp]
1.103  (*Maps #n to n for n = 0, 1, 2*)
1.104 @@ -335,7 +333,7 @@
1.105  done
1.108 -(** Nat **)
1.109 +subsubsection{*Nat *}
1.111  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
1.113 @@ -344,7 +342,7 @@
1.114    NOT suitable for rewriting because n recurs in the condition.*)
1.115  lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
1.117 -(** Arith **)
1.118 +subsubsection{*Arith *}
1.120  lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
1.122 @@ -372,33 +370,31 @@
1.123  declare diff_less' [of "number_of v", standard, simp]
1.126 -(*** Comparisons involving (0::nat) ***)
1.127 +subsection{*Comparisons involving (0::nat) *}
1.129 -lemma eq_number_of_0:
1.130 +text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
1.132 +lemma eq_number_of_0 [simp]:
1.133       "(number_of v = (0::nat)) =
1.134        (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
1.135 -apply (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
1.136 -done
1.137 +by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
1.139 -lemma eq_0_number_of:
1.140 +lemma eq_0_number_of [simp]:
1.141       "((0::nat) = number_of v) =
1.142        (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
1.143 -apply (rule trans [OF eq_sym_conv eq_number_of_0])
1.144 -done
1.145 +by (rule trans [OF eq_sym_conv eq_number_of_0])
1.147 -lemma less_0_number_of:
1.148 +lemma less_0_number_of [simp]:
1.149       "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
1.150  by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
1.152 -(*Simplification already handles n<0, n<=0 and 0<=n.*)
1.153 -declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
1.155  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
1.156  by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
1.160 -(*** Comparisons involving Suc ***)
1.161 +subsection{*Comparisons involving Suc *}
1.163  lemma eq_number_of_Suc [simp]:
1.164       "(number_of v = Suc n) =
1.165 @@ -415,8 +411,7 @@
1.166       "(Suc n = number_of v) =
1.167          (let pv = number_of (bin_pred v) in
1.168           if neg pv then False else nat pv = n)"
1.169 -apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
1.170 -done
1.171 +by (rule trans [OF eq_sym_conv eq_number_of_Suc])
1.173  lemma less_number_of_Suc [simp]:
1.174       "(number_of v < Suc n) =
1.175 @@ -444,15 +439,13 @@
1.176       "(number_of v <= Suc n) =
1.177          (let pv = number_of (bin_pred v) in
1.178           if neg pv then True else nat pv <= n)"
1.179 -apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
1.180 -done
1.181 +by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
1.183  lemma le_Suc_number_of [simp]:
1.184       "(Suc n <= number_of v) =
1.185          (let pv = number_of (bin_pred v) in
1.186           if neg pv then False else n <= nat pv)"
1.187 -apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
1.188 -done
1.189 +by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
1.192  (* Push int(.) inwards: *)
1.193 @@ -500,7 +493,7 @@
1.197 -(*** Literal arithmetic involving powers, type nat ***)
1.198 +subsection{*Literal arithmetic involving powers*}
1.200  lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
1.201  apply (induct_tac "n")
1.202 @@ -518,7 +511,7 @@
1.206 -(*** Literal arithmetic involving powers, type int ***)
1.207 +text{*For the integers*}
1.209  lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
1.210  by (simp add: zpower_zpower mult_commute)
1.211 @@ -612,6 +605,40 @@
1.215 +subsection{*Literal arithmetic and @{term of_nat}*}
1.217 +lemma of_nat_double:
1.218 +     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
1.221 +lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
1.222 +by (simp only:  nat_number_of_def, simp)
1.224 +lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
1.225 +by arith
1.227 +lemma of_nat_number_of_lemma:
1.228 +     "of_nat (number_of v :: nat) =
1.229 +         (if 0 \<le> (number_of v :: int)
1.230 +          then (number_of v :: 'a :: number_ring)
1.231 +          else 0)"
1.232 +apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
1.233 +apply (simp only: number_of nat_number_of_def)
1.234 +txt{*Generalize in order to eliminate the function @{term number_of} and
1.235 +its annoying simprules*}
1.236 +apply (erule rev_mp)
1.237 +apply (rule_tac x="number_of bin :: int" in spec)
1.238 +apply (rule_tac x="number_of bin :: 'a" in spec)
1.240 +done
1.242 +lemma of_nat_number_of_eq [simp]:
1.243 +     "of_nat (number_of v :: nat) =
1.244 +         (if neg (number_of v :: int) then 0
1.245 +          else (number_of v :: 'a :: number_ring))"
1.246 +by (simp only: of_nat_number_of_lemma neg_def, simp)
1.249  subsection {*Lemmas for the Combination and Cancellation Simprocs*}
1.252 @@ -619,17 +646,16 @@
1.253           (if neg (number_of v :: int) then number_of v' + k
1.254            else if neg (number_of v' :: int) then number_of v + k
1.255            else number_of (bin_add v v') + k)"
1.256 -apply simp
1.257 -done
1.258 +by simp
1.261 -(** For combine_numerals **)
1.262 +subsubsection{*For @{text combine_numerals}*}
1.264  lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
1.268 -(** For cancel_numerals **)
1.269 +subsubsection{*For @{text cancel_numerals}*}
1.272       "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
1.273 @@ -664,7 +690,7 @@
1.277 -(** For cancel_numeral_factors **)
1.278 +subsubsection{*For @{text cancel_numeral_factors} *}
1.280  lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
1.281  by auto
1.282 @@ -679,7 +705,7 @@
1.283  by auto
1.286 -(** For cancel_factor **)
1.287 +subsubsection{*For @{text cancel_factor} *}
1.289  lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
1.290  by auto
1.291 @@ -734,6 +760,7 @@
1.292  val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
1.293  val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
1.294  val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
1.295 +val of_nat_number_of_eq = thm"of_nat_number_of_eq";
1.296  val nat_power_eq = thm"nat_power_eq";
1.297  val power_nat_number_of = thm"power_nat_number_of";
1.298  val zpower_even = thm"zpower_even";