src/HOL/Word/Misc_Numeric.thy
changeset 47108 2a1953f0d20d
parent 45604 29cf40fe8daf
child 47163 248376f8881d
     1.1 --- a/src/HOL/Word/Misc_Numeric.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Useful Numerical Lemmas *}
     1.5  
     1.6  theory Misc_Numeric
     1.7 -imports Main Parity
     1.8 +imports "~~/src/HOL/Main" "~~/src/HOL/Parity"
     1.9  begin
    1.10  
    1.11  lemma the_elemI: "y = {x} ==> the_elem y = x" 
    1.12 @@ -31,13 +31,6 @@
    1.13  
    1.14  lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith
    1.15  
    1.16 -lemma nobm1:
    1.17 -  "0 < (number_of w :: nat) ==> 
    1.18 -   number_of w - (1 :: nat) = number_of (Int.pred w)" 
    1.19 -  apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
    1.20 -  apply (simp add: number_of_eq nat_diff_distrib [symmetric])
    1.21 -  done
    1.22 -
    1.23  lemma zless2: "0 < (2 :: int)" by arith
    1.24  
    1.25  lemmas zless2p [simp] = zless2 [THEN zero_less_power]
    1.26 @@ -46,7 +39,6 @@
    1.27  lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
    1.28  lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
    1.29  
    1.30 --- "the inverse(s) of @{text number_of}"
    1.31  lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith
    1.32  
    1.33  lemma emep1:
    1.34 @@ -283,15 +275,6 @@
    1.35    
    1.36  lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
    1.37  
    1.38 -lemma nat_no_eq_iff: 
    1.39 -  "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==> 
    1.40 -   (number_of b = (number_of c :: nat)) = (b = c)" 
    1.41 -  apply (unfold nat_number_of_def) 
    1.42 -  apply safe
    1.43 -  apply (drule (2) eq_nat_nat_iff [THEN iffD1])
    1.44 -  apply (simp add: number_of_eq)
    1.45 -  done
    1.46 -
    1.47  lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]
    1.48  lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
    1.49  lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]