tuned proofs;
authorwenzelm
Wed Aug 09 00:14:28 2006 +0200 (2006-08-09)
changeset 203697e03c3ed1a18
parent 20368 2461a0485623
child 20370 217aada4f795
tuned proofs;
src/HOL/Lambda/Type.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/NumberTheory/Finite2.thy
     1.1 --- a/src/HOL/Lambda/Type.thy	Wed Aug 09 00:12:40 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Type.thy	Wed Aug 09 00:14:28 2006 +0200
     1.3 @@ -365,7 +365,7 @@
     1.4    show ?case by (rule prems) simp_all
     1.5  next
     1.6    case Fun
     1.7 -  show ?case  by (rule prems) (insert Fun, simp_all)
     1.8 +  show ?case by (rule prems) (insert Fun, simp_all)
     1.9  qed
    1.10  
    1.11  end
     2.1 --- a/src/HOL/NumberTheory/Euler.thy	Wed Aug 09 00:12:40 2006 +0200
     2.2 +++ b/src/HOL/NumberTheory/Euler.thy	Wed Aug 09 00:14:28 2006 +0200
     2.3 @@ -25,14 +25,14 @@
     2.4    apply (drule StandardRes_SRStar_prop1a)+ defer 1
     2.5    apply (drule StandardRes_SRStar_prop1a)+
     2.6    apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
     2.7 -  apply (drule notE, rule MultInv_zcong_prop1, auto)
     2.8 -  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)
     2.9 -  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
    2.10 -  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
    2.11 -  apply (drule MultInv_zcong_prop1, auto)
    2.12 -  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
    2.13 -  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
    2.14 -  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
    2.15 +  apply (drule notE, rule MultInv_zcong_prop1, auto)[]
    2.16 +  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    2.17 +  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    2.18 +  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
    2.19 +  apply (drule MultInv_zcong_prop1, auto)[]
    2.20 +  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    2.21 +  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    2.22 +  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
    2.23    done
    2.24  
    2.25  lemma MultInvPair_prop1b:
    2.26 @@ -60,8 +60,7 @@
    2.27                                  ~([j = 0] (mod p)); 
    2.28                                  ~(QuadRes p a) |]  ==> 
    2.29                               ~([j = a * MultInv p j] (mod p))"
    2.30 -  apply auto
    2.31 -proof -
    2.32 +proof
    2.33    assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and 
    2.34      "~([j = 0] (mod p))" and "~(QuadRes p a)"
    2.35    assume "[j = a * MultInv p j] (mod p)"
    2.36 @@ -93,7 +92,8 @@
    2.37    apply auto
    2.38    apply (simp only: StandardRes_prop2)
    2.39    apply (drule MultInvPair_distinct)
    2.40 -by auto
    2.41 +  apply auto back
    2.42 +  done
    2.43  
    2.44  
    2.45  subsection {* Properties of SetS *}
    2.46 @@ -313,8 +313,8 @@
    2.47  theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
    2.48      a^(nat (((p) - 1) div 2))] (mod p)"
    2.49    apply (auto simp add: Legendre_def Euler_part2)
    2.50 -  apply (frule Euler_part3, auto simp add: zcong_sym)
    2.51 -  apply (frule Euler_part1, auto simp add: zcong_sym)
    2.52 +  apply (frule Euler_part3, auto simp add: zcong_sym)[]
    2.53 +  apply (frule Euler_part1, auto simp add: zcong_sym)[]
    2.54    done
    2.55  
    2.56  end
     3.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Wed Aug 09 00:12:40 2006 +0200
     3.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed Aug 09 00:14:28 2006 +0200
     3.3 @@ -165,12 +165,12 @@
     3.4  
     3.5  lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
     3.6  proof -
     3.7 -  assume 1: "x \<in> zEven" and 2: "0 \<le> x"
     3.8 -  from 1 obtain a where 3: "x = 2 * a" ..
     3.9 -  with 2 have "0 \<le> a" by simp
    3.10 -  from 2 3 have "nat x = nat (2 * a)"
    3.11 +  assume "x \<in> zEven" and "0 \<le> x"
    3.12 +  from `x \<in> zEven` obtain a where "x = 2 * a" ..
    3.13 +  with `0 \<le> x` have "0 \<le> a" by simp
    3.14 +  from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
    3.15      by simp
    3.16 -  also from 3 have "nat (2 * a) = 2 * nat a"
    3.17 +  also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
    3.18      by (simp add: nat_mult_distrib)
    3.19    finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
    3.20      by simp
    3.21 @@ -184,10 +184,10 @@
    3.22  
    3.23  lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
    3.24  proof -
    3.25 -  assume 1: "x \<in> zOdd" and 2: "0 \<le> x"
    3.26 -  from 1 obtain a where 3: "x = 2 * a + 1" ..
    3.27 -  with 2 have a: "0 \<le> a" by simp
    3.28 -  with 2 3 have "nat x = nat (2 * a + 1)"
    3.29 +  assume "x \<in> zOdd" and "0 \<le> x"
    3.30 +  from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
    3.31 +  with `0 \<le> x` have a: "0 \<le> a" by simp
    3.32 +  with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
    3.33      by simp
    3.34    also from a have "nat (2 * a + 1) = 2 * nat a + 1"
    3.35      by (auto simp add: nat_mult_distrib nat_add_distrib)
    3.36 @@ -202,7 +202,7 @@
    3.37  qed
    3.38  
    3.39  lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==>
    3.40 -  (-1::int)^(nat x) = (-1::int)^(nat y)"
    3.41 +    (-1::int)^(nat x) = (-1::int)^(nat y)"
    3.42    using even_odd_disj [of x] even_odd_disj [of y]
    3.43    by (auto simp add: neg_one_even_power neg_one_odd_power)
    3.44  
    3.45 @@ -212,9 +212,9 @@
    3.46  
    3.47  lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
    3.48  proof -
    3.49 -  assume 1: "y \<in> zEven" and 2: "x < y"
    3.50 -  from 1 obtain k where k: "y = 2 * k" ..
    3.51 -  with 2 have "x < 2 * k" by simp
    3.52 +  assume "y \<in> zEven" and "x < y"
    3.53 +  from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
    3.54 +  with `x < y` have "x < 2 * k" by simp
    3.55    then have "x div 2 < k" by (auto simp add: div_prop1)
    3.56    also have "k = (2 * k) div 2" by simp
    3.57    finally have "x div 2 < 2 * k div 2" by simp
     4.1 --- a/src/HOL/NumberTheory/Finite2.thy	Wed Aug 09 00:12:40 2006 +0200
     4.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Wed Aug 09 00:14:28 2006 +0200
     4.3 @@ -98,10 +98,10 @@
     4.4  
     4.5  lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
     4.6  proof (induct x)
     4.7 +  case 0
     4.8    show "card {y::nat . y < 0} = 0" by simp
     4.9  next
    4.10 -  fix n::nat
    4.11 -  assume "card {y. y < n} = n"
    4.12 +  case (Suc n)
    4.13    have "{y. y < Suc n} = insert n {y. y < n}"
    4.14      by auto
    4.15    then have "card {y. y < Suc n} = card (insert n {y. y < n})"
    4.16 @@ -109,7 +109,7 @@
    4.17    also have "... = Suc (card {y. y < n})"
    4.18      by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
    4.19    finally show "card {y. y < Suc n} = Suc n"
    4.20 -    by (simp add: prems)
    4.21 +    using `card {y. y < n} = n` by simp
    4.22  qed
    4.23  
    4.24  lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
    4.25 @@ -126,7 +126,7 @@
    4.26      by (auto simp add: inj_on_def)
    4.27    hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
    4.28      by (rule card_image)
    4.29 -  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
    4.30 +  also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
    4.31      apply (auto simp add: zless_nat_eq_int_zless image_def)
    4.32      apply (rule_tac x = "nat x" in exI)
    4.33      apply (auto simp add: nat_0_le)