# HG changeset patch
# User paulson
# Date 1193137819 -7200
# Node ID 8b80535cd017a3c3c6c48acb952f09ee10685910
# Parent  59c300e94293854b026a32cd85d227378fec46ac
random tidying of proofs

diff -r 59c300e94293 -r 8b80535cd017 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 12:47:21 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 13:10:19 2007 +0200
@@ -792,9 +792,8 @@
 apply (case_tac "poly p = poly []", auto)
 apply (simp add: poly_linear_divides del: pmult_Cons, safe)
 apply (drule_tac [!] a = a in order2)
-apply (rule ccontr)
 apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
-apply (blast intro: lemma_order_root)
+apply (metis gr0_conv lemma_order_root)
 done
 
 lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
@@ -885,7 +884,7 @@
 apply (case_tac "poly p = poly []")
 apply (auto dest: pderiv_zero)
 apply (drule_tac a = a and p = p in order_decomp)
-apply (blast intro: lemma_order_pderiv)
+apply (metis lemma_order_pderiv length_0_conv length_greater_0_conv)
 done
 
 text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
@@ -934,8 +933,7 @@
 
 lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
       ==> (order a (pderiv p) = n) = (order a p = Suc n)"
-apply (auto dest: order_pderiv)
-done
+by (metis Suc_Suc_eq order_pderiv)
 
 lemma rsquarefree_roots:
   "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
@@ -950,7 +948,7 @@
 apply (cut_tac p = "[h]" and a = a in order_root)
 apply (simp add: fun_eq)
 apply (blast intro: order_poly)
-apply (auto simp add: order_root order_pderiv2)
+apply (metis One_nat_def order_pderiv2 order_root rsquarefree_def)
 done
 
 lemma pmult_one: "[1] *** p = p"
diff -r 59c300e94293 -r 8b80535cd017 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 23 12:47:21 2007 +0200
+++ b/src/HOL/List.thy	Tue Oct 23 13:10:19 2007 +0200
@@ -961,9 +961,7 @@
   next
     assume "\<not> p x"
     hence eq: "?S' = Suc ` ?S"
-      apply(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
-      apply (rule_tac x="xa - 1" in exI, auto)
-      done
+      by(auto simp add: image_def neq0_conv split:nat.split elim:lessE)
     have "length (filter p (x # xs)) = card ?S"
       using Cons `\<not> p x` by simp
     also have "\<dots> = card(Suc ` ?S)" using fin
diff -r 59c300e94293 -r 8b80535cd017 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Oct 23 12:47:21 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Oct 23 13:10:19 2007 +0200
@@ -1104,8 +1104,8 @@
   apply (drule sym)
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)
-  apply (fastsimp elim!: less_SucE)
-  apply (auto simp add: neq0_conv dest: mult_less_mono2)
+   apply (drule_tac [2] mult_less_mono2)
+    apply (auto simp add: neq0_conv)
   done
 
 
diff -r 59c300e94293 -r 8b80535cd017 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Tue Oct 23 12:47:21 2007 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy	Tue Oct 23 13:10:19 2007 +0200
@@ -291,8 +291,7 @@
 lemma primel_prod_less:
   "primel (x # xs) ==>
     primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
-  apply (auto intro: prod_mn_less_k prime_g_one primel_prod_gz simp add: primel_hd_tl)
-  done
+  by (metis Nat.less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
 
 lemma prod_one_empty:
     "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
@@ -323,15 +322,7 @@
    apply (simp add: perm_sing_eq primel_hd_tl)
    apply (rule_tac p = a in prod_one_empty)
      apply simp_all
-  apply (erule uniq_ex_aux)
-     apply (auto intro: primel_tl perm_primel simp add: primel_hd_tl)
-   apply (rule_tac k = a and n = "prod list" and m = "prod x" in mult_left_cancel)
-    apply (rule_tac [3] x = a in primel_prod_less)
-      apply (rule_tac [2] prod_xy_prod)
-      apply (rule_tac [2] s = "prod ys" in HOL.trans)
-       apply (erule_tac [3] perm_prod)
-      apply (erule_tac [5] perm_prod [symmetric])
-     apply (auto intro: perm_primel prime_g_zero)
+  apply (metis nat_0_less_mult_iff nat_mult_eq_cancel1 perm_primel perm_prod primel_prod_gz primel_prod_less primel_tl prod.simps(2))
   done
 
 lemma perm_nondec_unique:
diff -r 59c300e94293 -r 8b80535cd017 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Tue Oct 23 12:47:21 2007 +0200
+++ b/src/HOL/ex/Primrec.thy	Tue Oct 23 13:10:19 2007 +0200
@@ -140,7 +140,7 @@
 lemma ack2_le_ack1 [iff]: "ack (i, Suc j) \<le> ack (Suc i, j)"
   apply (induct j)
    apply simp_all
-  apply (blast intro: ack_le_mono2 less_ack2 [THEN Suc_leI] le_trans)
+  apply (metis Suc_leI Suc_lessI ack_le_mono2 le_def less_ack2)
   done