src/HOL/Integ/NatBin.thy
changeset 20485 3078fd2eec7b
parent 20355 50aaae6ae4db
child 20500 11da1ce8dbd8
--- a/src/HOL/Integ/NatBin.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -17,8 +17,7 @@
 instance nat :: number ..
 
 defs (overloaded)
-  nat_number_of_def:
-  "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+  nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))"
 
 abbreviation (xsymbols)
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
@@ -113,14 +112,14 @@
 
 lemma Suc_nat_number_of_add:
      "Suc (number_of v + n) =  
-        (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)" 
+        (if neg (number_of v :: int) then 1+n else number_of (succ v) + n)" 
 by (simp del: nat_number_of 
          add: nat_number_of_def neg_nat
               Suc_nat_eq_nat_zadd1 number_of_succ) 
 
 lemma Suc_nat_number_of [simp]:
      "Suc (number_of v) =  
-        (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
+        (if neg (number_of v :: int) then 1 else number_of (succ v))"
 apply (cut_tac n = 0 in Suc_nat_number_of_add)
 apply (simp cong del: if_weak_cong)
 done
@@ -133,7 +132,7 @@
      "(number_of v :: nat) + number_of v' =  
          (if neg (number_of v :: int) then number_of v'  
           else if neg (number_of v' :: int) then number_of v  
-          else number_of (bin_add v v'))"
+          else number_of (v + v'))"
 by (force dest!: neg_nat
           simp del: nat_number_of
           simp add: nat_number_of_def nat_add_distrib [symmetric]) 
@@ -152,7 +151,7 @@
 lemma diff_nat_number_of [simp]: 
      "(number_of v :: nat) - number_of v' =  
         (if neg (number_of v' :: int) then number_of v  
-         else let d = number_of (bin_add v (bin_minus v')) in     
+         else let d = number_of (v + uminus v') in     
               if neg d then 0 else nat d)"
 by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
 
@@ -162,7 +161,7 @@
 
 lemma mult_nat_number_of [simp]:
      "(number_of v :: nat) * number_of v' =  
-       (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
+       (if neg (number_of v :: int) then 0 else number_of (v * v'))"
 by (force dest!: neg_nat
           simp del: nat_number_of
           simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
@@ -246,7 +245,7 @@
      "((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)  
-       else iszero (number_of (bin_add v (bin_minus v')) :: int))"
+       else iszero (number_of (v + uminus v') :: int))"
 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
                   eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
             split add: split_if cong add: imp_cong)
@@ -260,13 +259,11 @@
 (*"neg" is used in rewrite rules for binary comparisons*)
 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))"
+         (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
+          else neg (number_of (v + uminus v') :: int))"
 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) 
-
-
+         cong add: imp_cong, simp add: Pls_def)
 
 
 (*Maps #n to n for n = 0, 1, 2*)
@@ -437,8 +434,8 @@
 by (rule trans [OF eq_sym_conv eq_number_of_0])
 
 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])
+     "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
 
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
@@ -450,7 +447,7 @@
 
 lemma eq_number_of_Suc [simp]:
      "(number_of v = Suc n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else nat pv = n)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def 
@@ -461,13 +458,13 @@
 
 lemma Suc_eq_number_of [simp]:
      "(Suc n = number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else nat pv = n)"
 by (rule trans [OF eq_sym_conv eq_number_of_Suc])
 
 lemma less_number_of_Suc [simp]:
      "(number_of v < Suc n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then True else nat pv < n)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def  
@@ -478,7 +475,7 @@
 
 lemma less_Suc_number_of [simp]:
      "(Suc n < number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else n < nat pv)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def
@@ -489,13 +486,13 @@
 
 lemma le_number_of_Suc [simp]:
      "(number_of v <= Suc n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then True else nat pv <= n)"
 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  
+        (let pv = number_of (pred v) in  
          if neg pv then False else n <= nat pv)"
 by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
 
@@ -568,23 +565,20 @@
 text{*For the integers*}
 
 lemma zpower_number_of_even:
-     "(z::int) ^ number_of (w BIT bit.B0) =  
-      (let w = z ^ (number_of w) in  w*w)"
-apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
-apply (simp only: number_of_add) 
+  "(z::int) ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
+unfolding Let_def nat_number_of_def number_of_BIT bit.cases
 apply (rule_tac x = "number_of w" in spec, clarify)
 apply (case_tac " (0::int) <= x")
 apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
 done
 
 lemma zpower_number_of_odd:
-     "(z::int) ^ number_of (w BIT bit.B1) =  
-          (if (0::int) <= number_of w                    
-           then (let w = z ^ (number_of w) in  z*w*w)    
-           else 1)"
-apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
-apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
-apply (rule_tac x = "number_of w" in spec, clarify)
+  "(z::int) ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w                    
+     then (let w = z ^ (number_of w) in z * w * w) else 1)"
+unfolding Let_def nat_number_of_def number_of_BIT bit.cases
+apply (rule_tac x = "number_of w" in spec, auto)
+apply (simp only: nat_add_distrib nat_mult_distrib)
+apply simp
 apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
 done
 
@@ -695,13 +689,13 @@
      "number_of v + (number_of v' + (k::nat)) =  
          (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)"
+          else number_of (v + v') + k)"
 by simp
 
 lemma nat_number_of_mult_left:
      "number_of v * (number_of v' * (k::nat)) =  
          (if neg (number_of v :: int) then 0
-          else number_of (bin_mult v v') * k)"
+          else number_of (v * v') * k)"
 by simp
 
 
@@ -780,7 +774,7 @@
 subsection {* code generator setup *}
 
 lemma number_of_is_nat_rep_bin [code inline]:
-  "(number_of b :: nat) = nat (Rep_Bin b)"
+  "(number_of b :: nat) = nat (number_of b)"
   unfolding nat_number_of_def int_number_of_def by simp