fix proofs
authorhuffman
Sat Dec 06 20:25:31 2008 -0800 (2008-12-06)
changeset 2901362a6ddcbb53b
parent 29012 9140227dc8c5
child 29014 e515f42d1db7
fix proofs
src/HOL/Tools/ComputeNumeral.thy
     1.1 --- a/src/HOL/Tools/ComputeNumeral.thy	Sat Dec 06 19:39:53 2008 -0800
     1.2 +++ b/src/HOL/Tools/ComputeNumeral.thy	Sat Dec 06 20:25:31 2008 -0800
     1.3 @@ -129,7 +129,8 @@
     1.4  
     1.5  (* Addition for nat *)
     1.6  lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
     1.7 -  by (auto simp add: number_of_is_id)
     1.8 +  unfolding nat_number_of_def number_of_is_id neg_def
     1.9 +  by auto
    1.10  
    1.11  (* Subtraction for nat *)
    1.12  lemma natsub: "(number_of x) - ((number_of y)::nat) = 
    1.13 @@ -140,18 +141,14 @@
    1.14  (* Multiplication for nat *)
    1.15  lemma natmul: "(number_of x) * ((number_of y)::nat) = 
    1.16    (if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
    1.17 -  apply (auto simp add: number_of_is_id neg_def iszero_def)
    1.18 -  apply (case_tac "x > 0")
    1.19 -  apply auto
    1.20 -  apply (rule order_less_imp_le)
    1.21 -  apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified])
    1.22 -  done
    1.23 +  unfolding nat_number_of_def number_of_is_id neg_def
    1.24 +  by (simp add: nat_mult_distrib)
    1.25  
    1.26  lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
    1.27    by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
    1.28  
    1.29  lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
    1.30 -  by (auto simp add: number_of_is_id neg_def lezero_def)
    1.31 +  by (simp add: lezero_def numeral_simps not_le)
    1.32  
    1.33  lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
    1.34    by (auto simp add: number_of_is_id lezero_def nat_number_of_def)