--- 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"
--- 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
--- 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
--- 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:
--- 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