change more lemmas to avoid using iszero
authorhuffman
Thu Dec 04 08:47:45 2008 -0800 (2008-12-04)
changeset 289694ed63cdda799
parent 28968 a4f3db5d1393
child 28970 1c743f58781a
change more lemmas to avoid using iszero
src/HOL/Library/Efficient_Nat.thy
src/HOL/NatBin.thy
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 03 22:16:20 2008 -0800
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Dec 04 08:47:45 2008 -0800
     1.3 @@ -349,7 +349,7 @@
     1.4  
     1.5  lemma nat_code' [code]:
     1.6    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
     1.7 -  by auto
     1.8 +  unfolding nat_number_of_def number_of_is_id neg_def by simp
     1.9  
    1.10  lemma of_nat_int [code unfold]:
    1.11    "of_nat = int" by (simp add: int_def)
     2.1 --- a/src/HOL/NatBin.thy	Wed Dec 03 22:16:20 2008 -0800
     2.2 +++ b/src/HOL/NatBin.thy	Thu Dec 04 08:47:45 2008 -0800
     2.3 @@ -246,15 +246,11 @@
     2.4  (*"neg" is used in rewrite rules for binary comparisons*)
     2.5  lemma eq_nat_number_of [simp]:
     2.6       "((number_of v :: nat) = number_of v') =  
     2.7 -      (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
     2.8 -       else if neg (number_of v' :: int) then iszero (number_of v :: int)  
     2.9 -       else iszero (number_of (v + uminus v') :: int))"
    2.10 -apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
    2.11 -                  eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
    2.12 -            split add: split_if cong add: imp_cong)
    2.13 -apply (simp only: nat_eq_iff nat_eq_iff2)
    2.14 -apply (simp add: not_neg_eq_ge_0 [symmetric])
    2.15 -done
    2.16 +      (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
    2.17 +       else if neg (number_of v' :: int) then (number_of v :: int) = 0
    2.18 +       else v = v')"
    2.19 +  unfolding nat_number_of_def number_of_is_id neg_def
    2.20 +  by auto
    2.21  
    2.22  
    2.23  subsubsection{*Less-than (<) *}
    2.24 @@ -454,7 +450,7 @@
    2.25  
    2.26  
    2.27  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
    2.28 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
    2.29 +by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
    2.30  
    2.31  
    2.32  
    2.33 @@ -641,21 +637,14 @@
    2.34  
    2.35  lemma nat_number_of_Bit0:
    2.36      "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
    2.37 -  apply (simp only: nat_number_of_def Let_def)
    2.38 -  apply (cases "neg (number_of w :: int)")
    2.39 -   apply (simp add: neg_nat neg_number_of_Bit0)
    2.40 -  apply (rule int_int_eq [THEN iffD1])
    2.41 -  apply (simp only: not_neg_nat neg_number_of_Bit0 int_Suc zadd_int [symmetric] simp_thms)
    2.42 -  apply (simp only: number_of_Bit0 zadd_assoc)
    2.43 -  apply simp
    2.44 -  done
    2.45 +  unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
    2.46 +  by auto
    2.47  
    2.48  lemma nat_number_of_Bit1:
    2.49    "number_of (Int.Bit1 w) =
    2.50      (if neg (number_of w :: int) then 0
    2.51       else let n = number_of w in Suc (n + n))"
    2.52 -  unfolding nat_number_of_def number_of_Bit1
    2.53 -  unfolding number_of_is_id neg_def Let_def
    2.54 +  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
    2.55    by auto
    2.56  
    2.57  lemmas nat_number =