random tidying of proofs
authorpaulson
Tue Oct 23 13:10:19 2007 +0200 (2007-10-23)
changeset 251578b80535cd017
parent 25156 59c300e94293
child 25158 271e499f2d03
random tidying of proofs
src/HOL/Hyperreal/Poly.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/NumberTheory/Factorization.thy
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 12:47:21 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 13:10:19 2007 +0200
     1.3 @@ -792,9 +792,8 @@
     1.4  apply (case_tac "poly p = poly []", auto)
     1.5  apply (simp add: poly_linear_divides del: pmult_Cons, safe)
     1.6  apply (drule_tac [!] a = a in order2)
     1.7 -apply (rule ccontr)
     1.8  apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
     1.9 -apply (blast intro: lemma_order_root)
    1.10 +apply (metis gr0_conv lemma_order_root)
    1.11  done
    1.12  
    1.13  lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
    1.14 @@ -885,7 +884,7 @@
    1.15  apply (case_tac "poly p = poly []")
    1.16  apply (auto dest: pderiv_zero)
    1.17  apply (drule_tac a = a and p = p in order_decomp)
    1.18 -apply (blast intro: lemma_order_pderiv)
    1.19 +apply (metis lemma_order_pderiv length_0_conv length_greater_0_conv)
    1.20  done
    1.21  
    1.22  text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
    1.23 @@ -934,8 +933,7 @@
    1.24  
    1.25  lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
    1.26        ==> (order a (pderiv p) = n) = (order a p = Suc n)"
    1.27 -apply (auto dest: order_pderiv)
    1.28 -done
    1.29 +by (metis Suc_Suc_eq order_pderiv)
    1.30  
    1.31  lemma rsquarefree_roots:
    1.32    "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
    1.33 @@ -950,7 +948,7 @@
    1.34  apply (cut_tac p = "[h]" and a = a in order_root)
    1.35  apply (simp add: fun_eq)
    1.36  apply (blast intro: order_poly)
    1.37 -apply (auto simp add: order_root order_pderiv2)
    1.38 +apply (metis One_nat_def order_pderiv2 order_root rsquarefree_def)
    1.39  done
    1.40  
    1.41  lemma pmult_one: "[1] *** p = p"
     2.1 --- a/src/HOL/List.thy	Tue Oct 23 12:47:21 2007 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Oct 23 13:10:19 2007 +0200
     2.3 @@ -961,9 +961,7 @@
     2.4    next
     2.5      assume "\<not> p x"
     2.6      hence eq: "?S' = Suc ` ?S"
     2.7 -      apply(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
     2.8 -      apply (rule_tac x="xa - 1" in exI, auto)
     2.9 -      done
    2.10 +      by(auto simp add: image_def neq0_conv split:nat.split elim:lessE)
    2.11      have "length (filter p (x # xs)) = card ?S"
    2.12        using Cons `\<not> p x` by simp
    2.13      also have "\<dots> = card(Suc ` ?S)" using fin
     3.1 --- a/src/HOL/Nat.thy	Tue Oct 23 12:47:21 2007 +0200
     3.2 +++ b/src/HOL/Nat.thy	Tue Oct 23 13:10:19 2007 +0200
     3.3 @@ -1104,8 +1104,8 @@
     3.4    apply (drule sym)
     3.5    apply (rule disjCI)
     3.6    apply (rule nat_less_cases, erule_tac [2] _)
     3.7 -  apply (fastsimp elim!: less_SucE)
     3.8 -  apply (auto simp add: neq0_conv dest: mult_less_mono2)
     3.9 +   apply (drule_tac [2] mult_less_mono2)
    3.10 +    apply (auto simp add: neq0_conv)
    3.11    done
    3.12  
    3.13  
     4.1 --- a/src/HOL/NumberTheory/Factorization.thy	Tue Oct 23 12:47:21 2007 +0200
     4.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Tue Oct 23 13:10:19 2007 +0200
     4.3 @@ -291,8 +291,7 @@
     4.4  lemma primel_prod_less:
     4.5    "primel (x # xs) ==>
     4.6      primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
     4.7 -  apply (auto intro: prod_mn_less_k prime_g_one primel_prod_gz simp add: primel_hd_tl)
     4.8 -  done
     4.9 +  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))
    4.10  
    4.11  lemma prod_one_empty:
    4.12      "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
    4.13 @@ -323,15 +322,7 @@
    4.14     apply (simp add: perm_sing_eq primel_hd_tl)
    4.15     apply (rule_tac p = a in prod_one_empty)
    4.16       apply simp_all
    4.17 -  apply (erule uniq_ex_aux)
    4.18 -     apply (auto intro: primel_tl perm_primel simp add: primel_hd_tl)
    4.19 -   apply (rule_tac k = a and n = "prod list" and m = "prod x" in mult_left_cancel)
    4.20 -    apply (rule_tac [3] x = a in primel_prod_less)
    4.21 -      apply (rule_tac [2] prod_xy_prod)
    4.22 -      apply (rule_tac [2] s = "prod ys" in HOL.trans)
    4.23 -       apply (erule_tac [3] perm_prod)
    4.24 -      apply (erule_tac [5] perm_prod [symmetric])
    4.25 -     apply (auto intro: perm_primel prime_g_zero)
    4.26 +  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))
    4.27    done
    4.28  
    4.29  lemma perm_nondec_unique:
     5.1 --- a/src/HOL/ex/Primrec.thy	Tue Oct 23 12:47:21 2007 +0200
     5.2 +++ b/src/HOL/ex/Primrec.thy	Tue Oct 23 13:10:19 2007 +0200
     5.3 @@ -140,7 +140,7 @@
     5.4  lemma ack2_le_ack1 [iff]: "ack (i, Suc j) \<le> ack (Suc i, j)"
     5.5    apply (induct j)
     5.6     apply simp_all
     5.7 -  apply (blast intro: ack_le_mono2 less_ack2 [THEN Suc_leI] le_trans)
     5.8 +  apply (metis Suc_leI Suc_lessI ack_le_mono2 le_def less_ack2)
     5.9    done
    5.10  
    5.11