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.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";