# HG changeset patch
# User huffman
# Date 1228623931 28800
# Node ID 62a6ddcbb53b3abef6c98294a043713696b53a14
# Parent  9140227dc8c5277fedfbb3a0e4157f25353161fe
fix proofs

diff -r 9140227dc8c5 -r 62a6ddcbb53b src/HOL/Tools/ComputeNumeral.thy
--- a/src/HOL/Tools/ComputeNumeral.thy	Sat Dec 06 19:39:53 2008 -0800
+++ b/src/HOL/Tools/ComputeNumeral.thy	Sat Dec 06 20:25:31 2008 -0800
@@ -129,7 +129,8 @@
 
 (* Addition for nat *)
 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))))"
-  by (auto simp add: number_of_is_id)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by auto
 
 (* Subtraction for nat *)
 lemma natsub: "(number_of x) - ((number_of y)::nat) = 
@@ -140,18 +141,14 @@
 (* Multiplication for nat *)
 lemma natmul: "(number_of x) * ((number_of y)::nat) = 
   (if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
-  apply (auto simp add: number_of_is_id neg_def iszero_def)
-  apply (case_tac "x > 0")
-  apply auto
-  apply (rule order_less_imp_le)
-  apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified])
-  done
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mult_distrib)
 
 lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
   by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
 
 lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
-  by (auto simp add: number_of_is_id neg_def lezero_def)
+  by (simp add: lezero_def numeral_simps not_le)
 
 lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
   by (auto simp add: number_of_is_id lezero_def nat_number_of_def)