--- 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
--- 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
--- 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
--- 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)