src/HOL/Integ/NatBin.thy
changeset 14390 55fe71faadda
parent 14387 e96d5c42c4b0
child 14417 34ffa53db76c
--- a/src/HOL/Integ/NatBin.thy	Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy	Tue Feb 17 10:41:59 2004 +0100
@@ -86,7 +86,7 @@
 	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
 
 
-(** Successor **)
+subsubsection{*Successor *}
 
 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
 apply (rule sym)
@@ -108,7 +108,7 @@
 done
 
 
-(** Addition **)
+subsubsection{*Addition *}
 
 (*"neg" is used in rewrite rules for binary comparisons*)
 lemma add_nat_number_of [simp]:
@@ -121,7 +121,7 @@
           simp add: nat_number_of_def nat_add_distrib [symmetric]) 
 
 
-(** Subtraction **)
+subsubsection{*Subtraction *}
 
 lemma diff_nat_eq_if:
      "nat z - nat z' =  
@@ -141,7 +141,7 @@
 
 
 
-(** Multiplication **)
+subsubsection{*Multiplication *}
 
 lemma mult_nat_number_of [simp]:
      "(number_of v :: nat) * number_of v' =  
@@ -152,7 +152,7 @@
 
 
 
-(** Quotient **)
+subsubsection{*Quotient *}
 
 lemma div_nat_number_of [simp]:
      "(number_of v :: nat)  div  number_of v' =  
@@ -167,7 +167,7 @@
 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
 
 
-(** Remainder **)
+subsubsection{*Remainder *}
 
 lemma mod_nat_number_of [simp]:
      "(number_of v :: nat)  mod  number_of v' =  
@@ -210,16 +210,16 @@
 *}
 
 
-(*** Comparisons ***)
+subsection{*Comparisons*}
 
-(** Equals (=) **)
+subsubsection{*Equals (=) *}
 
 lemma eq_nat_nat_iff:
      "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
 by (auto elim!: nonneg_eq_int)
 
 (*"neg" is used in rewrite rules for binary comparisons*)
-lemma eq_nat_number_of:
+lemma eq_nat_number_of [simp]:
      "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
        else if neg (number_of v' :: int) then iszero (number_of v :: int)  
@@ -231,21 +231,19 @@
 apply (simp add: not_neg_eq_ge_0 [symmetric])
 done
 
-declare eq_nat_number_of [simp]
 
-(** Less-than (<) **)
+subsubsection{*Less-than (<) *}
 
 (*"neg" is used in rewrite rules for binary comparisons*)
-lemma less_nat_number_of:
+lemma less_nat_number_of [simp]:
      "((number_of v :: nat) < number_of v') =  
          (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)  
           else neg (number_of (bin_add v (bin_minus v')) :: int))"
-apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
+by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
                 nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
-            cong add: imp_cong, simp) 
-done
+         cong add: imp_cong, simp) 
 
-declare less_nat_number_of [simp]
+
 
 
 (*Maps #n to n for n = 0, 1, 2*)
@@ -335,7 +333,7 @@
 done
 
 
-(** Nat **)
+subsubsection{*Nat *}
 
 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
 by (simp add: numerals)
@@ -344,7 +342,7 @@
   NOT suitable for rewriting because n recurs in the condition.*)
 lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
 
-(** Arith **)
+subsubsection{*Arith *}
 
 lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
 by (simp add: numerals)
@@ -372,33 +370,31 @@
 declare diff_less' [of "number_of v", standard, simp]
 
 
-(*** Comparisons involving (0::nat) ***)
+subsection{*Comparisons involving (0::nat) *}
 
-lemma eq_number_of_0:
+text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
+
+lemma eq_number_of_0 [simp]:
      "(number_of v = (0::nat)) =  
       (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
-apply (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
-done
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
 
-lemma eq_0_number_of:
+lemma eq_0_number_of [simp]:
      "((0::nat) = number_of v) =  
       (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
-apply (rule trans [OF eq_sym_conv eq_number_of_0])
-done
+by (rule trans [OF eq_sym_conv eq_number_of_0])
 
-lemma less_0_number_of:
+lemma less_0_number_of [simp]:
      "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
 
-(*Simplification already handles n<0, n<=0 and 0<=n.*)
-declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
 
 
 
-(*** Comparisons involving Suc ***)
+subsection{*Comparisons involving Suc *}
 
 lemma eq_number_of_Suc [simp]:
      "(number_of v = Suc n) =  
@@ -415,8 +411,7 @@
      "(Suc n = number_of v) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then False else nat pv = n)"
-apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
-done
+by (rule trans [OF eq_sym_conv eq_number_of_Suc])
 
 lemma less_number_of_Suc [simp]:
      "(number_of v < Suc n) =  
@@ -444,15 +439,13 @@
      "(number_of v <= Suc n) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then True else nat pv <= n)"
-apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
-done
+by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
 
 lemma le_Suc_number_of [simp]:
      "(Suc n <= number_of v) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then False else n <= nat pv)"
-apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
-done
+by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
 
 
 (* Push int(.) inwards: *)
@@ -500,7 +493,7 @@
 
 
 
-(*** Literal arithmetic involving powers, type nat ***)
+subsection{*Literal arithmetic involving powers*}
 
 lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
 apply (induct_tac "n")
@@ -518,7 +511,7 @@
 
 
 
-(*** Literal arithmetic involving powers, type int ***)
+text{*For the integers*}
 
 lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
 by (simp add: zpower_zpower mult_commute)
@@ -612,6 +605,40 @@
   by (simp add: Let_def)
 
 
+subsection{*Literal arithmetic and @{term of_nat}*}
+
+lemma of_nat_double:
+     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
+by (simp only: mult_2 nat_add_distrib of_nat_add) 
+
+lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
+by (simp only:  nat_number_of_def, simp)
+
+lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
+by arith
+
+lemma of_nat_number_of_lemma:
+     "of_nat (number_of v :: nat) =  
+         (if 0 \<le> (number_of v :: int) 
+          then (number_of v :: 'a :: number_ring)
+          else 0)"
+apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
+apply (simp only: number_of nat_number_of_def)
+txt{*Generalize in order to eliminate the function @{term number_of} and
+its annoying simprules*}
+apply (erule rev_mp)
+apply (rule_tac x="number_of bin :: int" in spec) 
+apply (rule_tac x="number_of bin :: 'a" in spec) 
+apply (simp add: nat_add_distrib of_nat_double int_double_iff)
+done
+
+lemma of_nat_number_of_eq [simp]:
+     "of_nat (number_of v :: nat) =  
+         (if neg (number_of v :: int) then 0  
+          else (number_of v :: 'a :: number_ring))"
+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:
@@ -619,17 +646,16 @@
          (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 (bin_add v v') + k)"
-apply simp
-done
+by simp
 
 
-(** For combine_numerals **)
+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)
 
 
-(** For cancel_numerals **)
+subsubsection{*For @{text cancel_numerals}*}
 
 lemma nat_diff_add_eq1:
      "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
@@ -664,7 +690,7 @@
 by (auto split add: nat_diff_split simp add: add_mult_distrib)
 
 
-(** For cancel_numeral_factors **)
+subsubsection{*For @{text cancel_numeral_factors} *}
 
 lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
 by auto
@@ -679,7 +705,7 @@
 by auto
 
 
-(** For cancel_factor **)
+subsubsection{*For @{text cancel_factor} *}
 
 lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
 by auto
@@ -734,6 +760,7 @@
 val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
 val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
 val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
+val of_nat_number_of_eq = thm"of_nat_number_of_eq";
 val nat_power_eq = thm"nat_power_eq";
 val power_nat_number_of = thm"power_nat_number_of";
 val zpower_even = thm"zpower_even";