src/HOL/Integ/NatBin.thy
changeset 14378 69c4d5997669
parent 14365 3d4df8c166ae
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Integ/NatBin.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  (*"neg" is used in rewrite rules for binary comparisons*)
     1.5  lemma int_nat_number_of:
     1.6       "int (number_of v :: nat) =  
     1.7 -         (if neg (number_of v) then 0  
     1.8 +         (if neg (number_of v :: int) then 0  
     1.9            else (number_of v :: int))"
    1.10  by (simp del: nat_number_of
    1.11  	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
    1.12 @@ -96,14 +96,14 @@
    1.13  
    1.14  lemma Suc_nat_number_of_add:
    1.15       "Suc (number_of v + n) =  
    1.16 -        (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)" 
    1.17 +        (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)" 
    1.18  by (simp del: nat_number_of 
    1.19           add: nat_number_of_def neg_nat
    1.20                Suc_nat_eq_nat_zadd1 number_of_succ) 
    1.21  
    1.22  lemma Suc_nat_number_of:
    1.23       "Suc (number_of v) =  
    1.24 -        (if neg (number_of v) then 1 else number_of (bin_succ v))"
    1.25 +        (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
    1.26  apply (cut_tac n = 0 in Suc_nat_number_of_add)
    1.27  apply (simp cong del: if_weak_cong)
    1.28  done
    1.29 @@ -115,8 +115,8 @@
    1.30  (*"neg" is used in rewrite rules for binary comparisons*)
    1.31  lemma add_nat_number_of:
    1.32       "(number_of v :: nat) + number_of v' =  
    1.33 -         (if neg (number_of v) then number_of v'  
    1.34 -          else if neg (number_of v') then number_of v  
    1.35 +         (if neg (number_of v :: int) then number_of v'  
    1.36 +          else if neg (number_of v' :: int) then number_of v  
    1.37            else number_of (bin_add v v'))"
    1.38  by (force dest!: neg_nat
    1.39            simp del: nat_number_of
    1.40 @@ -138,7 +138,7 @@
    1.41  
    1.42  lemma diff_nat_number_of: 
    1.43       "(number_of v :: nat) - number_of v' =  
    1.44 -        (if neg (number_of v') then number_of v  
    1.45 +        (if neg (number_of v' :: int) then number_of v  
    1.46           else let d = number_of (bin_add v (bin_minus v')) in     
    1.47                if neg d then 0 else nat d)"
    1.48  by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
    1.49 @@ -150,7 +150,7 @@
    1.50  
    1.51  lemma mult_nat_number_of:
    1.52       "(number_of v :: nat) * number_of v' =  
    1.53 -       (if neg (number_of v) then 0 else number_of (bin_mult v v'))"
    1.54 +       (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
    1.55  by (force dest!: neg_nat
    1.56            simp del: nat_number_of
    1.57            simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
    1.58 @@ -162,7 +162,7 @@
    1.59  
    1.60  lemma div_nat_number_of:
    1.61       "(number_of v :: nat)  div  number_of v' =  
    1.62 -          (if neg (number_of v) then 0  
    1.63 +          (if neg (number_of v :: int) then 0  
    1.64             else nat (number_of v div number_of v'))"
    1.65  by (force dest!: neg_nat
    1.66            simp del: nat_number_of
    1.67 @@ -175,8 +175,8 @@
    1.68  
    1.69  lemma mod_nat_number_of:
    1.70       "(number_of v :: nat)  mod  number_of v' =  
    1.71 -        (if neg (number_of v) then 0  
    1.72 -         else if neg (number_of v') then number_of v  
    1.73 +        (if neg (number_of v :: int) then 0  
    1.74 +         else if neg (number_of v' :: int) then number_of v  
    1.75           else nat (number_of v mod number_of v'))"
    1.76  by (force dest!: neg_nat
    1.77            simp del: nat_number_of
    1.78 @@ -242,9 +242,9 @@
    1.79  (*"neg" is used in rewrite rules for binary comparisons*)
    1.80  lemma eq_nat_number_of:
    1.81       "((number_of v :: nat) = number_of v') =  
    1.82 -      (if neg (number_of v) then (iszero (number_of v') | neg (number_of v'))  
    1.83 -       else if neg (number_of v') then iszero (number_of v)  
    1.84 -       else iszero (number_of (bin_add v (bin_minus v'))))"
    1.85 +      (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
    1.86 +       else if neg (number_of v' :: int) then iszero (number_of v :: int)  
    1.87 +       else iszero (number_of (bin_add v (bin_minus v')) :: int))"
    1.88  apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
    1.89                    eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
    1.90              split add: split_if cong add: imp_cong)
    1.91 @@ -259,8 +259,8 @@
    1.92  (*"neg" is used in rewrite rules for binary comparisons*)
    1.93  lemma less_nat_number_of:
    1.94       "((number_of v :: nat) < number_of v') =  
    1.95 -         (if neg (number_of v) then neg (number_of (bin_minus v'))  
    1.96 -          else neg (number_of (bin_add v (bin_minus v'))))"
    1.97 +         (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)  
    1.98 +          else neg (number_of (bin_add v (bin_minus v')) :: int))"
    1.99  apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   1.100                  nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
   1.101              cong add: imp_cong, simp) 
   1.102 @@ -397,24 +397,24 @@
   1.103  
   1.104  lemma eq_number_of_0:
   1.105       "(number_of v = (0::nat)) =  
   1.106 -      (if neg (number_of v) then True else iszero (number_of v))"
   1.107 +      (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   1.108  apply (simp add: numeral_0_eq_0 [symmetric] iszero_0)
   1.109  done
   1.110  
   1.111  lemma eq_0_number_of:
   1.112       "((0::nat) = number_of v) =  
   1.113 -      (if neg (number_of v) then True else iszero (number_of v))"
   1.114 +      (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   1.115  apply (rule trans [OF eq_sym_conv eq_number_of_0])
   1.116  done
   1.117  
   1.118  lemma less_0_number_of:
   1.119 -     "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
   1.120 +     "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
   1.121  by (simp add: numeral_0_eq_0 [symmetric])
   1.122  
   1.123  (*Simplification already handles n<0, n<=0 and 0<=n.*)
   1.124  declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
   1.125  
   1.126 -lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)"
   1.127 +lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   1.128  by (simp add: numeral_0_eq_0 [symmetric] iszero_0)
   1.129  
   1.130  
   1.131 @@ -530,7 +530,7 @@
   1.132  
   1.133  lemma power_nat_number_of:
   1.134       "(number_of v :: nat) ^ n =  
   1.135 -       (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"
   1.136 +       (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   1.137  by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   1.138           split add: split_if cong: imp_cong)
   1.139  
   1.140 @@ -605,7 +605,7 @@
   1.141  
   1.142  lemma nat_number_of_BIT_True:
   1.143    "number_of (w BIT True) =
   1.144 -    (if neg (number_of w) then 0
   1.145 +    (if neg (number_of w :: int) then 0
   1.146       else let n = number_of w in Suc (n + n))"
   1.147    apply (simp only: nat_number_of_def Let_def split: split_if)
   1.148    apply (intro conjI impI)
   1.149 @@ -618,7 +618,7 @@
   1.150  lemma nat_number_of_BIT_False:
   1.151      "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
   1.152    apply (simp only: nat_number_of_def Let_def)
   1.153 -  apply (cases "neg (number_of w)")
   1.154 +  apply (cases "neg (number_of w :: int)")
   1.155     apply (simp add: neg_nat neg_number_of_BIT)
   1.156    apply (rule int_int_eq [THEN iffD1])
   1.157    apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
   1.158 @@ -637,8 +637,8 @@
   1.159  
   1.160  lemma nat_number_of_add_left:
   1.161       "number_of v + (number_of v' + (k::nat)) =  
   1.162 -         (if neg (number_of v) then number_of v' + k  
   1.163 -          else if neg (number_of v') then number_of v + k  
   1.164 +         (if neg (number_of v :: int) then number_of v' + k  
   1.165 +          else if neg (number_of v' :: int) then number_of v + k  
   1.166            else number_of (bin_add v v') + k)"
   1.167  apply simp
   1.168  done
   1.169 @@ -831,6 +831,8 @@
   1.170    "uminus" :: "int => int"      ("`~")
   1.171    "op +" :: "int => int => int" ("(_ `+/ _)")
   1.172    "op *" :: "int => int => int" ("(_ `*/ _)")
   1.173 +  "op <" :: "int => int => bool" ("(_ </ _)")
   1.174 +  "op <=" :: "int => int => bool" ("(_ <=/ _)")
   1.175    "neg"                         ("(_ < 0)")
   1.176  
   1.177  end