src/HOL/NatBin.thy
changeset 28968 a4f3db5d1393
parent 28961 9f33ab8e15db
child 28969 4ed63cdda799
equal deleted inserted replaced
28967:3bdb1eae352c 28968:a4f3db5d1393
   439 subsection{*Comparisons involving (0::nat) *}
   439 subsection{*Comparisons involving (0::nat) *}
   440 
   440 
   441 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   441 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   442 
   442 
   443 lemma eq_number_of_0 [simp]:
   443 lemma eq_number_of_0 [simp]:
   444      "(number_of v = (0::nat)) =  
   444   "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"  
   445       (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   445   unfolding nat_number_of_def number_of_is_id by auto
   446 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
       
   447 
   446 
   448 lemma eq_0_number_of [simp]:
   447 lemma eq_0_number_of [simp]:
   449      "((0::nat) = number_of v) =  
   448   "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"  
   450       (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
       
   451 by (rule trans [OF eq_sym_conv eq_number_of_0])
   449 by (rule trans [OF eq_sym_conv eq_number_of_0])
   452 
   450 
   453 lemma less_0_number_of [simp]:
   451 lemma less_0_number_of [simp]:
   454      "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
   452      "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
   455 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
   453 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
   654 
   652 
   655 lemma nat_number_of_Bit1:
   653 lemma nat_number_of_Bit1:
   656   "number_of (Int.Bit1 w) =
   654   "number_of (Int.Bit1 w) =
   657     (if neg (number_of w :: int) then 0
   655     (if neg (number_of w :: int) then 0
   658      else let n = number_of w in Suc (n + n))"
   656      else let n = number_of w in Suc (n + n))"
   659   apply (simp only: nat_number_of_def Let_def split: split_if)
   657   unfolding nat_number_of_def number_of_Bit1
   660   apply (intro conjI impI)
   658   unfolding number_of_is_id neg_def Let_def
   661    apply (simp add: neg_nat neg_number_of_Bit1)
   659   by auto
   662   apply (rule int_int_eq [THEN iffD1])
       
   663   apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms)
       
   664   apply (simp only: number_of_Bit1 zadd_assoc)
       
   665   done
       
   666 
   660 
   667 lemmas nat_number =
   661 lemmas nat_number =
   668   nat_number_of_Pls nat_number_of_Min
   662   nat_number_of_Pls nat_number_of_Min
   669   nat_number_of_Bit0 nat_number_of_Bit1
   663   nat_number_of_Bit0 nat_number_of_Bit1
   670 
   664 
   706 lemma nat_number_of_add_left:
   700 lemma nat_number_of_add_left:
   707      "number_of v + (number_of v' + (k::nat)) =  
   701      "number_of v + (number_of v' + (k::nat)) =  
   708          (if neg (number_of v :: int) then number_of v' + k  
   702          (if neg (number_of v :: int) then number_of v' + k  
   709           else if neg (number_of v' :: int) then number_of v + k  
   703           else if neg (number_of v' :: int) then number_of v + k  
   710           else number_of (v + v') + k)"
   704           else number_of (v + v') + k)"
   711 by simp
   705   unfolding nat_number_of_def number_of_is_id neg_def
       
   706   by auto
   712 
   707 
   713 lemma nat_number_of_mult_left:
   708 lemma nat_number_of_mult_left:
   714      "number_of v * (number_of v' * (k::nat)) =  
   709      "number_of v * (number_of v' * (k::nat)) =  
   715          (if neg (number_of v :: int) then 0
   710          (if neg (number_of v :: int) then 0
   716           else number_of (v * v') * k)"
   711           else number_of (v * v') * k)"