# HG changeset patch
# User wenzelm
# Date 1155075268 -7200
# Node ID 7e03c3ed1a185522bbd647f3ab9bb7980d6d123a
# Parent  2461a04856230c92592129e8983528751d687ab9
tuned proofs;

diff -r 2461a0485623 -r 7e03c3ed1a18 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Wed Aug 09 00:12:40 2006 +0200
+++ b/src/HOL/Lambda/Type.thy	Wed Aug 09 00:14:28 2006 +0200
@@ -365,7 +365,7 @@
   show ?case by (rule prems) simp_all
 next
   case Fun
-  show ?case  by (rule prems) (insert Fun, simp_all)
+  show ?case by (rule prems) (insert Fun, simp_all)
 qed
 
 end
diff -r 2461a0485623 -r 7e03c3ed1a18 src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Wed Aug 09 00:12:40 2006 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Wed Aug 09 00:14:28 2006 +0200
@@ -25,14 +25,14 @@
   apply (drule StandardRes_SRStar_prop1a)+ defer 1
   apply (drule StandardRes_SRStar_prop1a)+
   apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
-  apply (drule notE, rule MultInv_zcong_prop1, auto)
-  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)
-  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
-  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
-  apply (drule MultInv_zcong_prop1, auto)
-  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
-  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
-  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
+  apply (drule notE, rule MultInv_zcong_prop1, auto)[]
+  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
+  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
+  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
+  apply (drule MultInv_zcong_prop1, auto)[]
+  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
+  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
+  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
   done
 
 lemma MultInvPair_prop1b:
@@ -60,8 +60,7 @@
                                 ~([j = 0] (mod p)); 
                                 ~(QuadRes p a) |]  ==> 
                              ~([j = a * MultInv p j] (mod p))"
-  apply auto
-proof -
+proof
   assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and 
     "~([j = 0] (mod p))" and "~(QuadRes p a)"
   assume "[j = a * MultInv p j] (mod p)"
@@ -93,7 +92,8 @@
   apply auto
   apply (simp only: StandardRes_prop2)
   apply (drule MultInvPair_distinct)
-by auto
+  apply auto back
+  done
 
 
 subsection {* Properties of SetS *}
@@ -313,8 +313,8 @@
 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
     a^(nat (((p) - 1) div 2))] (mod p)"
   apply (auto simp add: Legendre_def Euler_part2)
-  apply (frule Euler_part3, auto simp add: zcong_sym)
-  apply (frule Euler_part1, auto simp add: zcong_sym)
+  apply (frule Euler_part3, auto simp add: zcong_sym)[]
+  apply (frule Euler_part1, auto simp add: zcong_sym)[]
   done
 
 end
diff -r 2461a0485623 -r 7e03c3ed1a18 src/HOL/NumberTheory/EvenOdd.thy
--- a/src/HOL/NumberTheory/EvenOdd.thy	Wed Aug 09 00:12:40 2006 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed Aug 09 00:14:28 2006 +0200
@@ -165,12 +165,12 @@
 
 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
 proof -
-  assume 1: "x \<in> zEven" and 2: "0 \<le> x"
-  from 1 obtain a where 3: "x = 2 * a" ..
-  with 2 have "0 \<le> a" by simp
-  from 2 3 have "nat x = nat (2 * a)"
+  assume "x \<in> zEven" and "0 \<le> x"
+  from `x \<in> zEven` obtain a where "x = 2 * a" ..
+  with `0 \<le> x` have "0 \<le> a" by simp
+  from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
     by simp
-  also from 3 have "nat (2 * a) = 2 * nat a"
+  also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
     by (simp add: nat_mult_distrib)
   finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
     by simp
@@ -184,10 +184,10 @@
 
 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
 proof -
-  assume 1: "x \<in> zOdd" and 2: "0 \<le> x"
-  from 1 obtain a where 3: "x = 2 * a + 1" ..
-  with 2 have a: "0 \<le> a" by simp
-  with 2 3 have "nat x = nat (2 * a + 1)"
+  assume "x \<in> zOdd" and "0 \<le> x"
+  from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
+  with `0 \<le> x` have a: "0 \<le> a" by simp
+  with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
     by simp
   also from a have "nat (2 * a + 1) = 2 * nat a + 1"
     by (auto simp add: nat_mult_distrib nat_add_distrib)
@@ -202,7 +202,7 @@
 qed
 
 lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==>
-  (-1::int)^(nat x) = (-1::int)^(nat y)"
+    (-1::int)^(nat x) = (-1::int)^(nat y)"
   using even_odd_disj [of x] even_odd_disj [of y]
   by (auto simp add: neg_one_even_power neg_one_odd_power)
 
@@ -212,9 +212,9 @@
 
 lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
 proof -
-  assume 1: "y \<in> zEven" and 2: "x < y"
-  from 1 obtain k where k: "y = 2 * k" ..
-  with 2 have "x < 2 * k" by simp
+  assume "y \<in> zEven" and "x < y"
+  from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
+  with `x < y` have "x < 2 * k" by simp
   then have "x div 2 < k" by (auto simp add: div_prop1)
   also have "k = (2 * k) div 2" by simp
   finally have "x div 2 < 2 * k div 2" by simp
diff -r 2461a0485623 -r 7e03c3ed1a18 src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Wed Aug 09 00:12:40 2006 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy	Wed Aug 09 00:14:28 2006 +0200
@@ -98,10 +98,10 @@
 
 lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
 proof (induct x)
+  case 0
   show "card {y::nat . y < 0} = 0" by simp
 next
-  fix n::nat
-  assume "card {y. y < n} = n"
+  case (Suc n)
   have "{y. y < Suc n} = insert n {y. y < n}"
     by auto
   then have "card {y. y < Suc n} = card (insert n {y. y < n})"
@@ -109,7 +109,7 @@
   also have "... = Suc (card {y. y < n})"
     by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
   finally show "card {y. y < Suc n} = Suc n"
-    by (simp add: prems)
+    using `card {y. y < n} = n` by simp
 qed
 
 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
@@ -126,7 +126,7 @@
     by (auto simp add: inj_on_def)
   hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
     by (rule card_image)
-  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
+  also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
     apply (auto simp add: zless_nat_eq_int_zless image_def)
     apply (rule_tac x = "nat x" in exI)
     apply (auto simp add: nat_0_le)