src/HOL/NatBin.thy
changeset 28969 4ed63cdda799
parent 28968 a4f3db5d1393
child 28984 060832a1f087
equal deleted inserted replaced
28968:a4f3db5d1393 28969:4ed63cdda799
   244 by (auto elim!: nonneg_eq_int)
   244 by (auto elim!: nonneg_eq_int)
   245 
   245 
   246 (*"neg" is used in rewrite rules for binary comparisons*)
   246 (*"neg" is used in rewrite rules for binary comparisons*)
   247 lemma eq_nat_number_of [simp]:
   247 lemma eq_nat_number_of [simp]:
   248      "((number_of v :: nat) = number_of v') =  
   248      "((number_of v :: nat) = number_of v') =  
   249       (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
   249       (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
   250        else if neg (number_of v' :: int) then iszero (number_of v :: int)  
   250        else if neg (number_of v' :: int) then (number_of v :: int) = 0
   251        else iszero (number_of (v + uminus v') :: int))"
   251        else v = v')"
   252 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   252   unfolding nat_number_of_def number_of_is_id neg_def
   253                   eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
   253   by auto
   254             split add: split_if cong add: imp_cong)
       
   255 apply (simp only: nat_eq_iff nat_eq_iff2)
       
   256 apply (simp add: not_neg_eq_ge_0 [symmetric])
       
   257 done
       
   258 
   254 
   259 
   255 
   260 subsubsection{*Less-than (<) *}
   256 subsubsection{*Less-than (<) *}
   261 
   257 
   262 (*"neg" is used in rewrite rules for binary comparisons*)
   258 (*"neg" is used in rewrite rules for binary comparisons*)
   452      "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
   448      "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
   453 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
   449 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
   454 
   450 
   455 
   451 
   456 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   452 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   457 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
   453 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   458 
   454 
   459 
   455 
   460 
   456 
   461 subsection{*Comparisons involving  @{term Suc} *}
   457 subsection{*Comparisons involving  @{term Suc} *}
   462 
   458 
   639   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   635   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   640   done
   636   done
   641 
   637 
   642 lemma nat_number_of_Bit0:
   638 lemma nat_number_of_Bit0:
   643     "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   639     "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   644   apply (simp only: nat_number_of_def Let_def)
   640   unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
   645   apply (cases "neg (number_of w :: int)")
   641   by auto
   646    apply (simp add: neg_nat neg_number_of_Bit0)
       
   647   apply (rule int_int_eq [THEN iffD1])
       
   648   apply (simp only: not_neg_nat neg_number_of_Bit0 int_Suc zadd_int [symmetric] simp_thms)
       
   649   apply (simp only: number_of_Bit0 zadd_assoc)
       
   650   apply simp
       
   651   done
       
   652 
   642 
   653 lemma nat_number_of_Bit1:
   643 lemma nat_number_of_Bit1:
   654   "number_of (Int.Bit1 w) =
   644   "number_of (Int.Bit1 w) =
   655     (if neg (number_of w :: int) then 0
   645     (if neg (number_of w :: int) then 0
   656      else let n = number_of w in Suc (n + n))"
   646      else let n = number_of w in Suc (n + n))"
   657   unfolding nat_number_of_def number_of_Bit1
   647   unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
   658   unfolding number_of_is_id neg_def Let_def
       
   659   by auto
   648   by auto
   660 
   649 
   661 lemmas nat_number =
   650 lemmas nat_number =
   662   nat_number_of_Pls nat_number_of_Min
   651   nat_number_of_Pls nat_number_of_Min
   663   nat_number_of_Bit0 nat_number_of_Bit1
   652   nat_number_of_Bit0 nat_number_of_Bit1