# 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 \ 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) \ poly []; order a p \ 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 = (\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 "\ 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 `\ p x` by simp also have "\ = 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) \ 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