src/HOL/NatBin.thy
changeset 28961 9f33ab8e15db
parent 28562 4e74209f113e
child 28968 a4f3db5d1393
equal deleted inserted replaced
28960:011a6c86ab31 28961:9f33ab8e15db
   262 (*"neg" is used in rewrite rules for binary comparisons*)
   262 (*"neg" is used in rewrite rules for binary comparisons*)
   263 lemma less_nat_number_of [simp]:
   263 lemma less_nat_number_of [simp]:
   264      "((number_of v :: nat) < number_of v') =  
   264      "((number_of v :: nat) < number_of v') =  
   265          (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
   265          (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
   266           else neg (number_of (v + uminus v') :: int))"
   266           else neg (number_of (v + uminus v') :: int))"
   267 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   267   unfolding neg_def nat_number_of_def number_of_is_id
   268                 nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
   268   by auto
   269          cong add: imp_cong, simp add: Pls_def)
       
   270 
   269 
   271 
   270 
   272 (*Maps #n to n for n = 0, 1, 2*)
   271 (*Maps #n to n for n = 0, 1, 2*)
   273 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   272 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   274 
   273