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.4 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
1.5
1.6
1.7 -(** Successor **)
1.8 +subsubsection{*Successor *}
1.9
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.14
1.15
1.16 -(** Addition **)
1.17 +subsubsection{*Addition *}
1.18
1.19 (*"neg" is used in rewrite rules for binary comparisons*)
1.20 lemma add_nat_number_of [simp]:
1.21 @@ -121,7 +121,7 @@
1.22 simp add: nat_number_of_def nat_add_distrib [symmetric])
1.23
1.24
1.25 -(** Subtraction **)
1.26 +subsubsection{*Subtraction *}
1.27
1.28 lemma diff_nat_eq_if:
1.29 "nat z - nat z' =
1.30 @@ -141,7 +141,7 @@
1.31
1.32
1.33
1.34 -(** Multiplication **)
1.35 +subsubsection{*Multiplication *}
1.36
1.37 lemma mult_nat_number_of [simp]:
1.38 "(number_of v :: nat) * number_of v' =
1.39 @@ -152,7 +152,7 @@
1.40
1.41
1.42
1.43 -(** Quotient **)
1.44 +subsubsection{*Quotient *}
1.45
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.50
1.51
1.52 -(** Remainder **)
1.53 +subsubsection{*Remainder *}
1.54
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.59
1.60
1.61 -(*** Comparisons ***)
1.62 +subsection{*Comparisons*}
1.63
1.64 -(** Equals (=) **)
1.65 +subsubsection{*Equals (=) *}
1.66
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.70
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.80
1.81 -declare eq_nat_number_of [simp]
1.82
1.83 -(** Less-than (<) **)
1.84 +subsubsection{*Less-than (<) *}
1.85
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.98
1.99 -declare less_nat_number_of [simp]
1.100 +
1.101
1.102
1.103 (*Maps #n to n for n = 0, 1, 2*)
1.104 @@ -335,7 +333,7 @@
1.105 done
1.106
1.107
1.108 -(** Nat **)
1.109 +subsubsection{*Nat *}
1.110
1.111 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
1.112 by (simp add: numerals)
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.116
1.117 -(** Arith **)
1.118 +subsubsection{*Arith *}
1.119
1.120 lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
1.121 by (simp add: numerals)
1.122 @@ -372,33 +370,31 @@
1.123 declare diff_less' [of "number_of v", standard, simp]
1.124
1.125
1.126 -(*** Comparisons involving (0::nat) ***)
1.127 +subsection{*Comparisons involving (0::nat) *}
1.128
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.131 +
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.138
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.146
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.151
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.154
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.157
1.158
1.159
1.160 -(*** Comparisons involving Suc ***)
1.161 +subsection{*Comparisons involving Suc *}
1.162
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.172
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.182
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.190
1.191
1.192 (* Push int(.) inwards: *)
1.193 @@ -500,7 +493,7 @@
1.194
1.195
1.196
1.197 -(*** Literal arithmetic involving powers, type nat ***)
1.198 +subsection{*Literal arithmetic involving powers*}
1.199
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.203
1.204
1.205
1.206 -(*** Literal arithmetic involving powers, type int ***)
1.207 +text{*For the integers*}
1.208
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.212 by (simp add: Let_def)
1.213
1.214
1.215 +subsection{*Literal arithmetic and @{term of_nat}*}
1.216 +
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.219 +by (simp only: mult_2 nat_add_distrib of_nat_add)
1.220 +
1.221 +lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
1.222 +by (simp only: nat_number_of_def, simp)
1.223 +
1.224 +lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
1.225 +by arith
1.226 +
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.239 +apply (simp add: nat_add_distrib of_nat_double int_double_iff)
1.240 +done
1.241 +
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.247 +
1.248 +
1.249 subsection {*Lemmas for the Combination and Cancellation Simprocs*}
1.250
1.251 lemma nat_number_of_add_left:
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.259
1.260
1.261 -(** For combine_numerals **)
1.262 +subsubsection{*For @{text combine_numerals}*}
1.263
1.264 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
1.265 by (simp add: add_mult_distrib)
1.266
1.267
1.268 -(** For cancel_numerals **)
1.269 +subsubsection{*For @{text cancel_numerals}*}
1.270
1.271 lemma nat_diff_add_eq1:
1.272 "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
1.273 @@ -664,7 +690,7 @@
1.274 by (auto split add: nat_diff_split simp add: add_mult_distrib)
1.275
1.276
1.277 -(** For cancel_numeral_factors **)
1.278 +subsubsection{*For @{text cancel_numeral_factors} *}
1.279
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.284
1.285
1.286 -(** For cancel_factor **)
1.287 +subsubsection{*For @{text cancel_factor} *}
1.288
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";