change lemmas to avoid using neg
authorhuffman
Sat Dec 06 19:39:53 2008 -0800 (2008-12-06)
changeset 290129140227dc8c5
parent 29011 a47003001699
child 29013 62a6ddcbb53b
change lemmas to avoid using neg
src/HOL/Arith_Tools.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/NatBin.thy
     1.1 --- a/src/HOL/Arith_Tools.thy	Fri Dec 05 17:35:22 2008 -0800
     1.2 +++ b/src/HOL/Arith_Tools.thy	Sat Dec 06 19:39:53 2008 -0800
     1.3 @@ -40,7 +40,7 @@
     1.4  text{*No longer required as a simprule because of the @{text inverse_fold}
     1.5     simproc*}
     1.6  lemma Suc_diff_number_of:
     1.7 -     "neg (number_of (uminus v)::int) ==>
     1.8 +     "Int.Pls < v ==>
     1.9        Suc m - (number_of v) = m - (number_of (Int.pred v))"
    1.10  apply (subst Suc_diff_eq_diff_pred)
    1.11  apply simp
     2.1 --- a/src/HOL/Library/Nat_Infinity.thy	Fri Dec 05 17:35:22 2008 -0800
     2.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 19:39:53 2008 -0800
     2.3 @@ -146,8 +146,8 @@
     2.4    by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
     2.5  
     2.6  lemma plus_inat_number [simp]:
     2.7 -  "(number_of k \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
     2.8 -    else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
     2.9 +  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
    2.10 +    else if l < Int.Pls then number_of k else number_of (k + l))"
    2.11    unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
    2.12  
    2.13  lemma iSuc_number [simp]:
     3.1 --- a/src/HOL/NatBin.thy	Fri Dec 05 17:35:22 2008 -0800
     3.2 +++ b/src/HOL/NatBin.thy	Sat Dec 06 19:39:53 2008 -0800
     3.3 @@ -141,10 +141,10 @@
     3.4  (*"neg" is used in rewrite rules for binary comparisons*)
     3.5  lemma add_nat_number_of [simp]:
     3.6       "(number_of v :: nat) + number_of v' =  
     3.7 -         (if neg (number_of v :: int) then number_of v'  
     3.8 -          else if neg (number_of v' :: int) then number_of v  
     3.9 +         (if v < Int.Pls then number_of v'  
    3.10 +          else if v' < Int.Pls then number_of v  
    3.11            else number_of (v + v'))"
    3.12 -  unfolding nat_number_of_def number_of_is_id neg_def
    3.13 +  unfolding nat_number_of_def number_of_is_id numeral_simps
    3.14    by (simp add: nat_add_distrib)
    3.15  
    3.16  
    3.17 @@ -160,19 +160,19 @@
    3.18  
    3.19  lemma diff_nat_number_of [simp]: 
    3.20       "(number_of v :: nat) - number_of v' =  
    3.21 -        (if neg (number_of v' :: int) then number_of v  
    3.22 +        (if v' < Int.Pls then number_of v  
    3.23           else let d = number_of (v + uminus v') in     
    3.24                if neg d then 0 else nat d)"
    3.25 -by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
    3.26 -
    3.27 +  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
    3.28 +  by auto
    3.29  
    3.30  
    3.31  subsubsection{*Multiplication *}
    3.32  
    3.33  lemma mult_nat_number_of [simp]:
    3.34       "(number_of v :: nat) * number_of v' =  
    3.35 -       (if neg (number_of v :: int) then 0 else number_of (v * v'))"
    3.36 -  unfolding nat_number_of_def number_of_is_id neg_def
    3.37 +       (if v < Int.Pls then 0 else number_of (v * v'))"
    3.38 +  unfolding nat_number_of_def number_of_is_id numeral_simps
    3.39    by (simp add: nat_mult_distrib)
    3.40  
    3.41  
    3.42 @@ -446,17 +446,18 @@
    3.43  text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
    3.44  
    3.45  lemma eq_number_of_0 [simp]:
    3.46 -  "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"  
    3.47 -  unfolding nat_number_of_def number_of_is_id by auto
    3.48 +  "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
    3.49 +  unfolding nat_number_of_def number_of_is_id numeral_simps
    3.50 +  by auto
    3.51  
    3.52  lemma eq_0_number_of [simp]:
    3.53 -  "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"  
    3.54 +  "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
    3.55  by (rule trans [OF eq_sym_conv eq_number_of_0])
    3.56  
    3.57  lemma less_0_number_of [simp]:
    3.58 -     "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
    3.59 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
    3.60 -
    3.61 +   "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
    3.62 +  unfolding nat_number_of_def number_of_is_id numeral_simps
    3.63 +  by simp
    3.64  
    3.65  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
    3.66  by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
    3.67 @@ -705,7 +706,7 @@
    3.68  
    3.69  lemma nat_number_of_mult_left:
    3.70       "number_of v * (number_of v' * (k::nat)) =  
    3.71 -         (if neg (number_of v :: int) then 0
    3.72 +         (if v < Int.Pls then 0
    3.73            else number_of (v * v') * k)"
    3.74  by simp
    3.75