--- a/src/HOL/NumberTheory/BijectionRel.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/BijectionRel.thy Thu Dec 08 12:50:04 2005 +0100
@@ -63,19 +63,16 @@
done
lemma aux_induct:
- "finite F ==> F \<subseteq> A ==> P {} ==>
- (!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
- ==> P F"
-proof -
- case rule_context
- assume major: "finite F"
+ assumes major: "finite F"
and subs: "F \<subseteq> A"
- show ?thesis
- apply (rule subs [THEN rev_mp])
- apply (rule major [THEN finite_induct])
- apply (blast intro: rule_context)+
- done
-qed
+ and cases: "P {}"
+ "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
+ shows "P F"
+ using major subs
+ apply (induct set: Finites)
+ apply (blast intro: cases)+
+ done
+
lemma inj_func_bijR_aux1:
"A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
--- a/src/HOL/NumberTheory/Euler.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Thu Dec 08 12:50:04 2005 +0100
@@ -122,7 +122,7 @@
lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);
\<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
-by (induct set: Finites, auto)
+ by (induct set: Finites) auto
lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
int(card(SetS a p)) = (p - 1) div 2"
@@ -172,9 +172,9 @@
lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
by auto
-lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union>
- (d22set (p - 1))"
- apply (induct p rule: d22set.induct, auto)
+lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
+ apply (induct p rule: d22set.induct)
+ apply auto
apply (simp add: SRStar_def d22set.simps)
apply (simp add: SRStar_def d22set.simps, clarify)
apply (frule aux1)
@@ -183,7 +183,7 @@
apply (simp add: d22set.simps)
apply (frule d22set_le)
apply (frule d22set_g_1, auto)
-done
+ done
lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
@@ -195,8 +195,8 @@
MultInvPair_prop1c setprod_Union_disjoint)
also have "[setprod (setprod (%x. x)) (SetS a p) =
setprod (%x. a) (SetS a p)] (mod p)"
- apply (rule setprod_same_function_zcong)
- by (auto simp add: prems SetS_setprod_prop SetS_finite)
+ by (rule setprod_same_function_zcong)
+ (auto simp add: prems SetS_setprod_prop SetS_finite)
also (zcong_trans) have "[setprod (%x. a) (SetS a p) =
a^(card (SetS a p))] (mod p)"
by (auto simp add: prems SetS_finite setprod_constant)
@@ -205,7 +205,7 @@
apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
apply (auto simp add: prems SetS_card)
- done
+ done
qed
lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
@@ -218,15 +218,15 @@
by (auto simp add: prems SRStar_d22set_prop)
also have "... = zfact(p - 1)"
proof -
- have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
+ have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
apply (insert prems, auto)
apply (drule d22set_g_1)
apply (auto simp add: d22set_fin)
- done
- then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
- by auto
- then show ?thesis
- by (auto simp add: d22set_prod_zfact)
+ done
+ then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
+ by auto
+ then show ?thesis
+ by (auto simp add: d22set_prod_zfact)
qed
finally show ?thesis .
qed
@@ -235,7 +235,7 @@
[zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
apply (frule Union_SetS_setprod_prop1)
apply (auto simp add: Union_SetS_setprod_prop2)
-done
+ done
(****************************************************************)
(* *)
@@ -252,7 +252,7 @@
apply (frule Wilson_Russ)
apply (auto simp add: zcong_sym)
apply (rule zcong_trans, auto)
-done
+ done
(********************************************************************)
(* *)
@@ -294,7 +294,7 @@
apply (frule aux_2, auto)
apply (frule_tac a = a in aux_1, auto)
apply (frule zcong_zmult_prop1, auto)
-done
+ done
(****************************************************************)
(* *)
@@ -309,7 +309,7 @@
~([y ^ 2 = 0] (mod p))")
apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
-done
+ done
lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))"
by (auto simp add: nat_mult_distrib)
@@ -327,7 +327,7 @@
apply (frule odd_minus_one_even)
apply (frule even_div_2_prop2)
apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
-done
+ done
(********************************************************************)
(* *)
@@ -340,6 +340,6 @@
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)
-done
+ done
-end
\ No newline at end of file
+end
--- a/src/HOL/NumberTheory/EulerFermat.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Dec 08 12:50:04 2005 +0100
@@ -2,9 +2,6 @@
ID: $Id$
Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
-
-Changes by Jeremy Avigad, 2003/02/21:
- repaired proof of Bnor_prime (removed use of zprime_def)
*)
header {* Fermat's Little Theorem extended to Euler's Totient function *}
@@ -60,7 +57,7 @@
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
-- {* LCP: not sure why this lemma is needed now *}
-by (auto simp add: abs_if)
+ by (auto simp add: abs_if)
text {* \medskip @{text norRRset} *}
@@ -68,29 +65,27 @@
declare BnorRset.simps [simp del]
lemma BnorRset_induct:
- "(!!a m. P {} a m) ==>
- (!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
- ==> P (BnorRset(a,m)) a m)
- ==> P (BnorRset(u,v)) u v"
-proof -
- case rule_context
- show ?thesis
- apply (rule BnorRset.induct, safe)
- apply (case_tac [2] "0 < a")
- apply (rule_tac [2] rule_context, simp_all)
- apply (simp_all add: BnorRset.simps rule_context)
+ assumes "!!a m. P {} a m"
+ and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
+ ==> P (BnorRset(a,m)) a m"
+ shows "P (BnorRset(u,v)) u v"
+ apply (rule BnorRset.induct)
+ apply safe
+ apply (case_tac [2] "0 < a")
+ apply (rule_tac [2] prems)
+ apply simp_all
+ apply (simp_all add: BnorRset.simps prems)
done
-qed
-lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) --> b \<le> a"
+lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
apply (induct a m rule: BnorRset_induct)
- prefer 2
- apply (subst BnorRset.simps)
+ apply simp
+ apply (subst BnorRset.simps)
apply (unfold Let_def, auto)
done
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
-by (auto dest: Bnor_mem_zle)
+ by (auto dest: Bnor_mem_zle)
lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
apply (induct a m rule: BnorRset_induct)
@@ -210,7 +205,7 @@
RRset2norRR_correct [THEN conjunct2, standard]
lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
-by (erule RsetR.induct, auto)
+ by (induct set: RsetR) auto
lemma RRset_zcong_eq [rule_format]:
"1 < m ==>
--- a/src/HOL/NumberTheory/EvenOdd.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy Thu Dec 08 12:50:04 2005 +0100
@@ -5,14 +5,14 @@
header {*Parity: Even and Odd Integers*}
-theory EvenOdd imports Int2 begin;
+theory EvenOdd imports Int2 begin
text{*Note. This theory is being revised. See the web page
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
constdefs
zOdd :: "int set"
- "zOdd == {x. \<exists>k. x = 2*k + 1}"
+ "zOdd == {x. \<exists>k. x = 2 * k + 1}"
zEven :: "int set"
"zEven == {x. \<exists>k. x = 2 * k}"
@@ -22,223 +22,239 @@
(* *)
(***********************************************************)
-lemma one_not_even: "~(1 \<in> zEven)";
- apply (simp add: zEven_def)
- apply (rule allI, case_tac "k \<le> 0", auto)
-done
+lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
+ and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
+ by (auto simp add: zOdd_def)
-lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)";
- apply (auto simp add: zOdd_def zEven_def)
- proof -;
- fix a b;
- assume "2 * (a::int) = 2 * (b::int) + 1";
- then have "2 * (a::int) - 2 * (b :: int) = 1";
- by arith
- then have "2 * (a - b) = 1";
- by (auto simp add: zdiff_zmult_distrib)
- moreover have "(2 * (a - b)):zEven";
- by (auto simp only: zEven_def)
- ultimately show "False";
- by (auto simp add: one_not_even)
- qed;
+lemma zEvenI [intro?]: "x = 2 * k \<Longrightarrow> x \<in> zEven"
+ and zEvenE [elim?]: "x \<in> zEven \<Longrightarrow> (!!k. x = 2 * k \<Longrightarrow> C) \<Longrightarrow> C"
+ by (auto simp add: zEven_def)
+
+lemma one_not_even: "~(1 \<in> zEven)"
+proof
+ assume "1 \<in> zEven"
+ then obtain k :: int where "1 = 2 * k" ..
+ then show False by arith
+qed
-lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
- by (simp add: zOdd_def zEven_def, presburger)
+lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)"
+proof -
+ {
+ fix a b
+ assume "2 * (a::int) = 2 * (b::int) + 1"
+ then have "2 * (a::int) - 2 * (b :: int) = 1"
+ by arith
+ then have "2 * (a - b) = 1"
+ by (auto simp add: zdiff_zmult_distrib)
+ moreover have "(2 * (a - b)):zEven"
+ by (auto simp only: zEven_def)
+ ultimately have False
+ by (auto simp add: one_not_even)
+ }
+ then show ?thesis
+ by (auto simp add: zOdd_def zEven_def)
+qed
-lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
- by (insert even_odd_disj, auto)
+lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)"
+ by (simp add: zOdd_def zEven_def) arith
-lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd";
- apply (case_tac "x \<in> zOdd", auto)
- apply (drule not_odd_impl_even)
- apply (auto simp add: zEven_def zOdd_def)
- proof -;
- fix a b;
- assume "2 * a * y = 2 * b + 1";
- then have "2 * a * y - 2 * b = 1";
- by arith
- then have "2 * (a * y - b) = 1";
- by (auto simp add: zdiff_zmult_distrib)
- moreover have "(2 * (a * y - b)):zEven";
- by (auto simp only: zEven_def)
- ultimately show "False";
- by (auto simp add: one_not_even)
- qed;
+lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven"
+ using even_odd_disj by auto
-lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven";
+lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd"
+proof (rule classical)
+ assume "\<not> ?thesis"
+ then have "x \<in> zEven" by (rule not_odd_impl_even)
+ then obtain a where a: "x = 2 * a" ..
+ assume "x * y : zOdd"
+ then obtain b where "x * y = 2 * b + 1" ..
+ with a have "2 * a * y = 2 * b + 1" by simp
+ then have "2 * a * y - 2 * b = 1"
+ by arith
+ then have "2 * (a * y - b) = 1"
+ by (auto simp add: zdiff_zmult_distrib)
+ moreover have "(2 * (a * y - b)):zEven"
+ by (auto simp only: zEven_def)
+ ultimately have False
+ by (auto simp add: one_not_even)
+ then show ?thesis ..
+qed
+
+lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven"
by (auto simp add: zOdd_def zEven_def)
-lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0";
+lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0"
by (auto simp add: zEven_def)
-lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x";
+lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x"
by (auto simp add: zEven_def)
-lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven";
+lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
apply (auto simp add: zEven_def)
- by (auto simp only: zadd_zmult_distrib2 [THEN sym])
+ apply (auto simp only: zadd_zmult_distrib2 [symmetric])
+ done
-lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven";
+lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
by (auto simp add: zEven_def)
-lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven";
+lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"
apply (auto simp add: zEven_def)
- by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
+ apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
+ done
-lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven";
+lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
apply (auto simp add: zOdd_def zEven_def)
- by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
+ apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
+ done
-lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd";
+lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
apply (auto simp add: zOdd_def zEven_def)
apply (rule_tac x = "k - ka - 1" in exI)
- by auto
+ apply auto
+ done
-lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd";
+lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
apply (auto simp add: zOdd_def zEven_def)
- by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
+ apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
+ done
-lemma odd_times_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x * y \<in> zOdd";
+lemma odd_times_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x * y \<in> zOdd"
apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
apply (rule_tac x = "2 * ka * k + ka + k" in exI)
- by (auto simp add: zadd_zmult_distrib)
-
-lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))";
- by (insert even_odd_conj even_odd_disj, auto)
-
-lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven";
- by (insert odd_iff_not_even odd_times_odd, auto)
+ apply (auto simp add: zadd_zmult_distrib)
+ done
-lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))";
- apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
- even_minus_odd odd_minus_even)
- proof -;
- assume "x - y \<in> zEven" and "x \<in> zEven";
- show "y \<in> zEven";
- proof (rule classical);
- assume "~(y \<in> zEven)";
- then have "y \<in> zOdd"
- by (auto simp add: odd_iff_not_even)
- with prems have "x - y \<in> zOdd";
- by (simp add: even_minus_odd)
- with prems have "False";
- by (auto simp add: odd_iff_not_even)
- thus ?thesis;
- by auto
- qed;
- next assume "x - y \<in> zEven" and "y \<in> zEven";
- show "x \<in> zEven";
- proof (rule classical);
- assume "~(x \<in> zEven)";
- then have "x \<in> zOdd"
- by (auto simp add: odd_iff_not_even)
- with prems have "x - y \<in> zOdd";
- by (simp add: odd_minus_even)
- with prems have "False";
- by (auto simp add: odd_iff_not_even)
- thus ?thesis;
- by auto
- qed;
- qed;
+lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
+ using even_odd_conj even_odd_disj by auto
+
+lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"
+ using odd_iff_not_even odd_times_odd by auto
-lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1";
-proof -;
- assume "x \<in> zEven" and "0 \<le> x";
- then have "\<exists>k. x = 2 * k";
- by (auto simp only: zEven_def)
- then show ?thesis;
- proof;
- fix a;
- assume "x = 2 * a";
- from prems have a: "0 \<le> a";
- by arith
- from prems have "nat x = nat(2 * a)";
- by auto
- also from a have "nat (2 * a) = 2 * nat a";
- by (auto simp add: nat_mult_distrib)
- finally have "(-1::int)^nat x = (-1)^(2 * nat a)";
- by auto
- also have "... = ((-1::int)^2)^ (nat a)";
- by (auto simp add: zpower_zpower [THEN sym])
- also have "(-1::int)^2 = 1";
- by auto
- finally; show ?thesis;
- by auto
- qed;
-qed;
+lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))"
+proof
+ assume xy: "x - y \<in> zEven"
+ {
+ assume x: "x \<in> zEven"
+ have "y \<in> zEven"
+ proof (rule classical)
+ assume "\<not> ?thesis"
+ then have "y \<in> zOdd"
+ by (simp add: odd_iff_not_even)
+ with x have "x - y \<in> zOdd"
+ by (simp add: even_minus_odd)
+ with xy have False
+ by (auto simp add: odd_iff_not_even)
+ then show ?thesis ..
+ qed
+ } moreover {
+ assume y: "y \<in> zEven"
+ have "x \<in> zEven"
+ proof (rule classical)
+ assume "\<not> ?thesis"
+ then have "x \<in> zOdd"
+ by (auto simp add: odd_iff_not_even)
+ with y have "x - y \<in> zOdd"
+ by (simp add: odd_minus_even)
+ with xy have False
+ by (auto simp add: odd_iff_not_even)
+ then show ?thesis ..
+ qed
+ }
+ ultimately show "(x \<in> zEven) = (y \<in> zEven)"
+ by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
+ even_minus_odd odd_minus_even)
+next
+ assume "(x \<in> zEven) = (y \<in> zEven)"
+ then show "x - y \<in> zEven"
+ by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
+ even_minus_odd odd_minus_even)
+qed
-lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
-proof -;
- assume "x \<in> zOdd" and "0 \<le> x";
- then have "\<exists>k. x = 2 * k + 1";
- by (auto simp only: zOdd_def)
- then show ?thesis;
- proof;
- fix a;
- assume "x = 2 * a + 1";
- from prems have a: "0 \<le> a";
- by arith
- from prems have "nat x = nat(2 * a + 1)";
- by auto
- also from a have "nat (2 * a + 1) = 2 * nat a + 1";
- by (auto simp add: nat_mult_distrib nat_add_distrib)
- finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)";
- by auto
- also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
- by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
- also have "(-1::int)^2 = 1";
- by auto
- finally; show ?thesis;
- by auto
- qed;
-qed;
+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)"
+ by simp
+ also from 3 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
+ also have "... = ((-1::int)^2)^ (nat a)"
+ by (simp add: zpower_zpower [symmetric])
+ also have "(-1::int)^2 = 1"
+ by simp
+ finally show ?thesis
+ by simp
+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)";
- apply (insert even_odd_disj [of x])
- apply (insert even_odd_disj [of y])
+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)"
+ by simp
+ also from a have "nat (2 * a + 1) = 2 * nat a + 1"
+ by (auto simp add: nat_mult_distrib nat_add_distrib)
+ finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
+ by simp
+ also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
+ by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib)
+ also have "(-1::int)^2 = 1"
+ by simp
+ finally show ?thesis
+ by simp
+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)"
+ using even_odd_disj [of x] even_odd_disj [of y]
by (auto simp add: neg_one_even_power neg_one_odd_power)
-lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))";
+
+lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))"
by (auto simp add: zcong_def zdvd_not_zless)
-lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2";
- apply (auto simp only: zEven_def)
- proof -;
- fix k assume "x < 2 * k";
- then have "x div 2 < k" by (auto simp add: div_prop1)
- also have "k = (2 * k) div 2"; by auto
- finally show "x div 2 < 2 * k div 2" by auto
- qed;
+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
+ 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
+ with k show ?thesis by simp
+qed
-lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2";
+lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
-lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y";
+lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
by (auto simp add: zEven_def)
(* An odd prime is greater than 2 *)
-lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)";
+lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)"
apply (auto simp add: zOdd_def zprime_def)
apply (drule_tac x = 2 in allE)
- apply (insert odd_iff_not_even [of p])
-by (auto simp add: zOdd_def zEven_def)
+ using odd_iff_not_even [of p]
+ apply (auto simp add: zOdd_def zEven_def)
+ done
(* Powers of -1 and parity *)
-lemma neg_one_special: "finite A ==>
- ((-1 :: int) ^ card A) * (-1 ^ card A) = 1";
- by (induct set: Finites, auto)
+lemma neg_one_special: "finite A ==>
+ ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
+ by (induct set: Finites) auto
-lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1";
- apply (induct_tac n)
- by auto
+lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
+ by (induct n) auto
lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
- ==> ((-1::int)^j = (-1::int)^k)";
- apply (insert neg_one_power [of j])
- apply (insert neg_one_power [of k])
+ ==> ((-1::int)^j = (-1::int)^k)"
+ using neg_one_power [of j] and insert neg_one_power [of k]
by (auto simp add: one_not_neg_one_mod_m zcong_sym)
-end;
+end
--- a/src/HOL/NumberTheory/Finite2.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy Thu Dec 08 12:50:04 2005 +0100
@@ -23,7 +23,7 @@
subsection {* Useful properties of sums and products *}
-lemma setsum_same_function_zcong:
+lemma setsum_same_function_zcong:
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
shows "[setsum f S = setsum g S] (mod m)"
proof cases
@@ -48,16 +48,16 @@
apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
done
-lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
+lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)"
apply (induct set: Finites)
apply (auto simp add: zadd_zmult_distrib2)
-done
+ done
-lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
+lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A"
- apply (induct set: Finites, auto)
- by (auto simp only: zadd_zmult_distrib2)
+ by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
+
(******************************************************************)
(* *)
@@ -68,61 +68,71 @@
subsection {* Cardinality of explicit finite sets *}
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
-by (simp add: finite_subset finite_imageI)
+ by (simp add: finite_subset finite_imageI)
-lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}"
-apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
-by auto
+lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
+ by (rule bounded_nat_set_is_finite) blast
-lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x }"
-apply (subgoal_tac "{ y::nat . y \<le> x } = { y::nat . y < Suc x}")
-by (auto simp add: bdd_nat_set_l_finite)
+lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
+proof -
+ have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
+ then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
+qed
-lemma bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}"
-apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
+lemma bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
+apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
int ` {(x :: nat). x < nat n}")
apply (erule finite_surjI)
apply (auto simp add: bdd_nat_set_l_finite image_def)
-apply (rule_tac x = "nat x" in exI, simp)
+apply (rule_tac x = "nat x" in exI, simp)
done
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
apply (erule ssubst)
apply (rule bdd_int_set_l_finite)
-by auto
+apply auto
+done
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
-apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
-by (auto simp add: bdd_int_set_l_finite finite_subset)
+proof -
+ have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
+ by auto
+ then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
+qed
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
-apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
-by (auto simp add: bdd_int_set_le_finite finite_subset)
+proof -
+ have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
+ by auto
+ then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
+qed
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
-apply (induct_tac x, force)
-proof -
+proof (induct x)
+ show "card {y::nat . y < 0} = 0" by simp
+next
fix n::nat
- assume "card {y. y < n} = n"
+ assume "card {y. y < n} = 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})"
by auto
also have "... = Suc (card {y. y < n})"
- apply (rule card_insert_disjoint)
- by (auto simp add: bdd_nat_set_l_finite)
- finally show "card {y. y < Suc n} = Suc 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)
qed
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
-apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
-by (auto simp add: card_bdd_nat_set_l)
+proof -
+ have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
+ by auto
+ then show ?thesis by (auto simp add: card_bdd_nat_set_l)
+qed
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
proof -
- fix n::int
assume "0 \<le> n"
have "inj_on (%y. int y) {y. y < nat n}"
by (auto simp add: inj_on_def)
@@ -131,52 +141,63 @@
also from prems 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)
- by (auto simp add: nat_0_le)
- also have "card {y. y < nat n} = nat n"
+ apply (auto simp add: nat_0_le)
+ done
+ also have "card {y. y < nat n} = nat n"
by (rule card_bdd_nat_set_l)
finally show "card {y. 0 \<le> y & y < n} = nat n" .
qed
-lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
+lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
nat n + 1"
-apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
-apply (insert card_bdd_int_set_l [of "n+1"])
-by (auto simp add: nat_add_distrib)
+proof -
+ assume "0 \<le> n"
+ moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
+ ultimately show ?thesis
+ using card_bdd_int_set_l [of "n + 1"]
+ by (auto simp add: nat_add_distrib)
+qed
-lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
+lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
card {x. 0 < x & x \<le> n} = nat n"
proof -
- fix n::int
assume "0 \<le> n"
have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
by (auto simp add: inj_on_def)
- hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
+ hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
card {x. 0 \<le> x & x < n}"
by (rule card_image)
- also from prems have "... = nat n"
+ also from `0 \<le> n` have "... = nat n"
by (rule card_bdd_int_set_l)
also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
apply (auto simp add: image_def)
apply (rule_tac x = "x - 1" in exI)
- by arith
- finally show "card {x. 0 < x & x \<le> n} = nat n".
+ apply arith
+ done
+ finally show "card {x. 0 < x & x \<le> n} = nat n" .
qed
-lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
- card {x. 0 < x & x < n} = nat n - 1"
- apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
- apply (insert card_bdd_int_set_l_le [of "n - 1"])
- by (auto simp add: nat_diff_distrib)
+lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
+ card {x. 0 < x & x < n} = nat n - 1"
+proof -
+ assume "0 < n"
+ moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
+ by simp
+ ultimately show ?thesis
+ using insert card_bdd_int_set_l_le [of "n - 1"]
+ by (auto simp add: nat_diff_distrib)
+qed
-lemma int_card_bdd_int_set_l_l: "0 < n ==>
+lemma int_card_bdd_int_set_l_l: "0 < n ==>
int(card {x. 0 < x & x < n}) = n - 1"
apply (auto simp add: card_bdd_int_set_l_l)
apply (subgoal_tac "Suc 0 \<le> nat n")
- apply (auto simp add: zdiff_int [THEN sym])
+ apply (auto simp add: zdiff_int [symmetric])
apply (subgoal_tac "0 < nat n", arith)
- by (simp add: zero_less_nat_eq)
+ apply (simp add: zero_less_nat_eq)
+ done
-lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
+lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
int(card {x. 0 < x & x \<le> n}) = n"
by (auto simp add: card_bdd_int_set_l_le)
@@ -201,7 +222,7 @@
subsection {* Lemmas for counting arguments *}
-lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
+lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
apply (frule_tac h = g and f = f in setsum_reindex)
apply (subgoal_tac "setsum g B = setsum g (f ` A)")
@@ -211,17 +232,19 @@
apply (auto simp add: card_image)
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
-by auto
+apply auto
+done
-lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
+lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
apply (frule_tac h = g and f = f in setprod_reindex)
- apply (subgoal_tac "setprod g B = setprod g (f ` A)")
+ apply (subgoal_tac "setprod g B = setprod g (f ` A)")
apply (simp add: inj_on_def)
apply (subgoal_tac "card A = card B")
apply (drule_tac A = "f ` A" and B = B in card_seteq)
apply (auto simp add: card_image)
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
-by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
+ apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
+ done
-end
\ No newline at end of file
+end
--- a/src/HOL/NumberTheory/Gauss.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Thu Dec 08 12:50:04 2005 +0100
@@ -5,7 +5,7 @@
header {* Gauss' Lemma *}
-theory Gauss imports Euler begin;
+theory Gauss imports Euler begin
locale GAUSS =
fixes p :: "int"
@@ -27,410 +27,417 @@
defines C_def: "C == (StandardRes p) ` B"
defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
- defines F_def: "F == (%x. (p - x)) ` E";
+ defines F_def: "F == (%x. (p - x)) ` E"
subsection {* Basic properties of p *}
-lemma (in GAUSS) p_odd: "p \<in> zOdd";
+lemma (in GAUSS) p_odd: "p \<in> zOdd"
by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
-lemma (in GAUSS) p_g_0: "0 < p";
- by (insert p_g_2, auto)
+lemma (in GAUSS) p_g_0: "0 < p"
+ using p_g_2 by auto
-lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2";
- by (insert p_g_2, auto simp add: pos_imp_zdiv_nonneg_iff)
+lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
+ using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
-lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p";
- proof -;
- have "p - 1 = (p - 1) div 1" by auto
- then have "(p - 1) div 2 \<le> p - 1"
- apply (rule ssubst) back;
- apply (rule zdiv_mono2)
- by (auto simp add: p_g_0)
- then have "(p - 1) div 2 \<le> p - 1";
- by auto
- then show ?thesis by simp
-qed;
+lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p"
+proof -
+ have "(p - 1) div 2 \<le> (p - 1) div 1"
+ by (rule zdiv_mono2) (auto simp add: p_g_0)
+ also have "\<dots> = p - 1" by simp
+ finally show ?thesis by simp
+qed
-lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1";
- apply (insert zdiv_zmult_self2 [of 2 "p - 1"])
-by auto
+lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1"
+ using zdiv_zmult_self2 [of 2 "p - 1"] by auto
-lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)";
+lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
apply (frule odd_minus_one_even)
apply (simp add: zEven_def)
apply (subgoal_tac "2 \<noteq> 0")
- apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
-by (auto simp add: even_div_2_prop2)
+ apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
+ apply (auto simp add: even_div_2_prop2)
+ done
-lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1";
+lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
-by (frule zodd_imp_zdiv_eq, auto)
+ apply (frule zodd_imp_zdiv_eq, auto)
+ done
subsection {* Basic Properties of the Gauss Sets *}
-lemma (in GAUSS) finite_A: "finite (A)";
- apply (auto simp add: A_def)
-thm bdd_int_set_l_finite;
- apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}");
-by (auto simp add: bdd_int_set_l_finite finite_subset)
+lemma (in GAUSS) finite_A: "finite (A)"
+ apply (auto simp add: A_def)
+ apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
+ apply (auto simp add: bdd_int_set_l_finite finite_subset)
+ done
-lemma (in GAUSS) finite_B: "finite (B)";
+lemma (in GAUSS) finite_B: "finite (B)"
by (auto simp add: B_def finite_A finite_imageI)
-lemma (in GAUSS) finite_C: "finite (C)";
+lemma (in GAUSS) finite_C: "finite (C)"
by (auto simp add: C_def finite_B finite_imageI)
-lemma (in GAUSS) finite_D: "finite (D)";
+lemma (in GAUSS) finite_D: "finite (D)"
by (auto simp add: D_def finite_Int finite_C)
-lemma (in GAUSS) finite_E: "finite (E)";
+lemma (in GAUSS) finite_E: "finite (E)"
by (auto simp add: E_def finite_Int finite_C)
-lemma (in GAUSS) finite_F: "finite (F)";
+lemma (in GAUSS) finite_F: "finite (F)"
by (auto simp add: F_def finite_E finite_imageI)
-lemma (in GAUSS) C_eq: "C = D \<union> E";
+lemma (in GAUSS) C_eq: "C = D \<union> E"
by (auto simp add: C_def D_def E_def)
-lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)";
- apply (auto simp add: A_def)
+lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)"
+ apply (auto simp add: A_def)
apply (insert int_nat)
apply (erule subst)
- by (auto simp add: card_bdd_int_set_l_le)
+ apply (auto simp add: card_bdd_int_set_l_le)
+ done
-lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A";
- apply (insert a_nonzero)
-by (simp add: A_def inj_on_def)
+lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A"
+ using a_nonzero by (simp add: A_def inj_on_def)
-lemma (in GAUSS) A_res: "ResSet p A";
- apply (auto simp add: A_def ResSet_def)
- apply (rule_tac m = p in zcong_less_eq)
- apply (insert p_g_2, auto)
- apply (subgoal_tac [1-2] "(p - 1) div 2 < p");
-by (auto, auto simp add: p_minus_one_l)
+lemma (in GAUSS) A_res: "ResSet p A"
+ apply (auto simp add: A_def ResSet_def)
+ apply (rule_tac m = p in zcong_less_eq)
+ apply (insert p_g_2, auto)
+ apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
+ apply (auto, auto simp add: p_minus_one_l)
+ done
-lemma (in GAUSS) B_res: "ResSet p B";
+lemma (in GAUSS) B_res: "ResSet p B"
apply (insert p_g_2 p_a_relprime p_minus_one_l)
- apply (auto simp add: B_def)
+ apply (auto simp add: B_def)
apply (rule ResSet_image)
- apply (auto simp add: A_res)
+ apply (auto simp add: A_res)
apply (auto simp add: A_def)
- proof -;
- fix x fix y
- assume a: "[x * a = y * a] (mod p)"
- assume b: "0 < x"
- assume c: "x \<le> (p - 1) div 2"
- assume d: "0 < y"
- assume e: "y \<le> (p - 1) div 2"
- from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
- have "[x = y](mod p)";
- by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
- with zcong_less_eq [of x y p] p_minus_one_l
- order_le_less_trans [of x "(p - 1) div 2" p]
- order_le_less_trans [of y "(p - 1) div 2" p] show "x = y";
- by (simp add: prems p_minus_one_l p_g_0)
-qed;
+proof -
+ fix x fix y
+ assume a: "[x * a = y * a] (mod p)"
+ assume b: "0 < x"
+ assume c: "x \<le> (p - 1) div 2"
+ assume d: "0 < y"
+ assume e: "y \<le> (p - 1) div 2"
+ from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
+ have "[x = y](mod p)"
+ by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
+ with zcong_less_eq [of x y p] p_minus_one_l
+ order_le_less_trans [of x "(p - 1) div 2" p]
+ order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
+ by (simp add: prems p_minus_one_l p_g_0)
+qed
-lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B";
+lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B"
apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
- proof -;
- fix x fix y
- assume a: "x * a mod p = y * a mod p"
- assume b: "0 < x"
- assume c: "x \<le> (p - 1) div 2"
- assume d: "0 < y"
- assume e: "y \<le> (p - 1) div 2"
- assume f: "x \<noteq> y"
- from a have "[x * a = y * a](mod p)";
- by (simp add: zcong_zmod_eq p_g_0)
- with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
- have "[x = y](mod p)";
- by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
- with zcong_less_eq [of x y p] p_minus_one_l
- order_le_less_trans [of x "(p - 1) div 2" p]
- order_le_less_trans [of y "(p - 1) div 2" p] have "x = y";
- by (simp add: prems p_minus_one_l p_g_0)
- then have False;
- by (simp add: f)
- then show "a = 0";
- by simp
-qed;
+proof -
+ fix x fix y
+ assume a: "x * a mod p = y * a mod p"
+ assume b: "0 < x"
+ assume c: "x \<le> (p - 1) div 2"
+ assume d: "0 < y"
+ assume e: "y \<le> (p - 1) div 2"
+ assume f: "x \<noteq> y"
+ from a have "[x * a = y * a](mod p)"
+ by (simp add: zcong_zmod_eq p_g_0)
+ with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
+ have "[x = y](mod p)"
+ by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
+ with zcong_less_eq [of x y p] p_minus_one_l
+ order_le_less_trans [of x "(p - 1) div 2" p]
+ order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
+ by (simp add: prems p_minus_one_l p_g_0)
+ then have False
+ by (simp add: f)
+ then show "a = 0"
+ by simp
+qed
-lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E";
+lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E"
apply (auto simp add: E_def C_def B_def A_def)
- apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI);
-by auto
+ apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
+ apply auto
+ done
-lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)";
+lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
apply (auto simp add: A_def)
apply (frule_tac m = p in zcong_not_zero)
apply (insert p_minus_one_l)
-by auto
+ apply auto
+ done
-lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x";
+lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x"
by (auto simp add: A_def)
-lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)";
+lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
apply (auto simp add: B_def)
- apply (frule A_ncong_p)
+ apply (frule A_ncong_p)
apply (insert p_a_relprime p_prime a_nonzero)
apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
-by (auto simp add: A_greater_zero)
+ apply (auto simp add: A_greater_zero)
+ done
-lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
- apply (insert a_nonzero)
-by (auto simp add: B_def mult_pos_pos A_greater_zero)
+lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x"
+ using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
-lemma (in GAUSS) C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)";
+lemma (in GAUSS) C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)"
apply (auto simp add: C_def)
apply (frule B_ncong_p)
- apply (subgoal_tac "[x = StandardRes p x](mod p)");
- defer; apply (simp add: StandardRes_prop1)
+ apply (subgoal_tac "[x = StandardRes p x](mod p)")
+ defer apply (simp add: StandardRes_prop1)
apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
-by auto
+ apply auto
+ done
-lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y";
+lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y"
apply (auto simp add: C_def)
- proof -;
- fix x;
- assume a: "x \<in> B";
- from p_g_0 have "0 \<le> StandardRes p x";
- by (simp add: StandardRes_lbound)
- moreover have "~[x = 0] (mod p)";
- by (simp add: a B_ncong_p)
- then have "StandardRes p x \<noteq> 0";
- by (simp add: StandardRes_prop3)
- ultimately show "0 < StandardRes p x";
- by (simp add: order_le_less)
-qed;
+proof -
+ fix x
+ assume a: "x \<in> B"
+ from p_g_0 have "0 \<le> StandardRes p x"
+ by (simp add: StandardRes_lbound)
+ moreover have "~[x = 0] (mod p)"
+ by (simp add: a B_ncong_p)
+ then have "StandardRes p x \<noteq> 0"
+ by (simp add: StandardRes_prop3)
+ ultimately show "0 < StandardRes p x"
+ by (simp add: order_le_less)
+qed
-lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)";
+lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
by (auto simp add: D_def C_ncong_p)
-lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)";
+lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
by (auto simp add: E_def C_ncong_p)
-lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)";
- apply (auto simp add: F_def)
- proof -;
- fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
- from E_ncong_p have "~[x = 0] (mod p)";
- by (simp add: a)
- moreover from a have "0 < x";
- by (simp add: a E_def C_greater_zero)
- moreover from a have "x < p";
- by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
- ultimately have "~[p - x = 0] (mod p)";
- by (simp add: zcong_not_zero)
- from this show False by (simp add: b)
-qed;
+lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
+ apply (auto simp add: F_def)
+proof -
+ fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
+ from E_ncong_p have "~[x = 0] (mod p)"
+ by (simp add: a)
+ moreover from a have "0 < x"
+ by (simp add: a E_def C_greater_zero)
+ moreover from a have "x < p"
+ by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
+ ultimately have "~[p - x = 0] (mod p)"
+ by (simp add: zcong_not_zero)
+ from this show False by (simp add: b)
+qed
-lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
- apply (auto simp add: F_def E_def)
+lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
+ apply (auto simp add: F_def E_def)
apply (insert p_g_0)
apply (frule_tac x = xa in StandardRes_ubound)
apply (frule_tac x = x in StandardRes_ubound)
apply (subgoal_tac "xa = StandardRes p xa")
apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
- proof -;
- from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
- "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)";
- by simp
- with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
- ==> p - StandardRes p x \<le> (p - 1) div 2";
- by simp
-qed;
+proof -
+ from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
+ "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)"
+ by simp
+ with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
+ ==> p - StandardRes p x \<le> (p - 1) div 2"
+ by simp
+qed
-lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
+lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
by (auto simp add: D_def C_greater_zero)
-lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}";
+lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
by (auto simp add: F_def E_def D_def C_def B_def A_def)
-lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}";
+lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
by (auto simp add: D_def C_def B_def A_def)
-lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2";
+lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
by (auto simp add: D_eq)
-lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2";
+lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
apply (auto simp add: F_eq A_def)
- proof -;
- fix y;
- assume "(p - 1) div 2 < StandardRes p (y * a)";
- then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)";
- by arith
- also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)";
- by (rule subst, auto)
- also; have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1";
- by arith
- finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2";
- by (insert zless_add1_eq [of "p - StandardRes p (y * a)"
- "(p - 1) div 2"],auto);
-qed;
+proof -
+ fix y
+ assume "(p - 1) div 2 < StandardRes p (y * a)"
+ then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)"
+ by arith
+ also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"
+ by auto
+ also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1"
+ by arith
+ finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2"
+ using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
+qed
-lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x,p) = 1";
- apply (insert p_prime p_minus_one_l)
-by (auto simp add: A_def zless_zprime_imp_zrelprime)
+lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
+ using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
-lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1";
- by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)
+lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1"
+ using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
subsection {* Relationships Between Gauss Sets *}
-lemma (in GAUSS) B_card_eq_A: "card B = card A";
- apply (insert finite_A)
-by (simp add: finite_A B_def inj_on_xa_A card_image)
+lemma (in GAUSS) B_card_eq_A: "card B = card A"
+ using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
-lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)";
- by (auto simp add: B_card_eq_A A_card_eq)
+lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)"
+ by (simp add: B_card_eq_A A_card_eq)
-lemma (in GAUSS) F_card_eq_E: "card F = card E";
- apply (insert finite_E)
-by (simp add: F_def inj_on_pminusx_E card_image)
+lemma (in GAUSS) F_card_eq_E: "card F = card E"
+ using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
-lemma (in GAUSS) C_card_eq_B: "card C = card B";
+lemma (in GAUSS) C_card_eq_B: "card C = card B"
apply (insert finite_B)
- apply (subgoal_tac "inj_on (StandardRes p) B");
+ apply (subgoal_tac "inj_on (StandardRes p) B")
apply (simp add: B_def C_def card_image)
apply (rule StandardRes_inj_on_ResSet)
-by (simp add: B_res)
+ apply (simp add: B_res)
+ done
-lemma (in GAUSS) D_E_disj: "D \<inter> E = {}";
+lemma (in GAUSS) D_E_disj: "D \<inter> E = {}"
by (auto simp add: D_def E_def)
-lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
+lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E"
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
-lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C";
+lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
apply (insert D_E_disj finite_D finite_E C_eq)
apply (frule setprod_Un_disjoint [of D E id])
-by auto
+ apply auto
+ done
-lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)";
+lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
apply (auto simp add: C_def)
- apply (insert finite_B SR_B_inj)
- apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id[THEN sym], auto)
+ apply (insert finite_B SR_B_inj)
+ apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id [symmetric], auto)
apply (rule setprod_same_function_zcong)
-by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
+ apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
+ done
-lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
+lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A"
apply (rule Un_least)
-by (auto simp add: A_def F_subset D_subset)
+ apply (auto simp add: A_def F_subset D_subset)
+ done
-lemma two_eq: "2 * (x::int) = x + x";
+lemma two_eq: "2 * (x::int) = x + x"
by arith
-lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}";
+lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}"
apply (simp add: F_eq D_eq)
apply (auto simp add: F_eq D_eq)
- proof -;
- fix y; fix ya;
- assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
- then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
- by arith
- moreover have "p dvd p";
- by auto
- ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
- by auto
- then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
- by (auto simp add: zcong_def)
- have "[y * a = StandardRes p (y * a)] (mod p)";
- by (simp only: zcong_sym StandardRes_prop1)
- moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
- by (simp only: zcong_sym StandardRes_prop1)
- ultimately have "[y * a + ya * a =
- StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
- by (rule zcong_zadd)
- with a have "[y * a + ya * a = 0] (mod p)";
- apply (elim zcong_trans)
- by (simp only: zcong_refl)
- also have "y * a + ya * a = a * (y + ya)";
- by (simp add: zadd_zmult_distrib2 zmult_commute)
- finally have "[a * (y + ya) = 0] (mod p)";.;
- with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
- p_a_relprime
- have a: "[y + ya = 0] (mod p)";
- by auto
- assume b: "y \<in> A" and c: "ya: A";
- with A_def have "0 < y + ya";
- by auto
- moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2";
- by auto
- moreover from b c p_eq2 A_def have "y + ya < p";
- by auto
- ultimately show False;
- apply simp
- apply (frule_tac m = p in zcong_not_zero)
- by (auto simp add: a)
-qed;
+proof -
+ fix y fix ya
+ assume "p - StandardRes p (y * a) = StandardRes p (ya * a)"
+ then have "p = StandardRes p (y * a) + StandardRes p (ya * a)"
+ by arith
+ moreover have "p dvd p"
+ by auto
+ ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))"
+ by auto
+ then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)"
+ by (auto simp add: zcong_def)
+ have "[y * a = StandardRes p (y * a)] (mod p)"
+ by (simp only: zcong_sym StandardRes_prop1)
+ moreover have "[ya * a = StandardRes p (ya * a)] (mod p)"
+ by (simp only: zcong_sym StandardRes_prop1)
+ ultimately have "[y * a + ya * a =
+ StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)"
+ by (rule zcong_zadd)
+ with a have "[y * a + ya * a = 0] (mod p)"
+ apply (elim zcong_trans)
+ by (simp only: zcong_refl)
+ also have "y * a + ya * a = a * (y + ya)"
+ by (simp add: zadd_zmult_distrib2 zmult_commute)
+ finally have "[a * (y + ya) = 0] (mod p)" .
+ with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
+ p_a_relprime
+ have a: "[y + ya = 0] (mod p)"
+ by auto
+ assume b: "y \<in> A" and c: "ya: A"
+ with A_def have "0 < y + ya"
+ by auto
+ moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2"
+ by auto
+ moreover from b c p_eq2 A_def have "y + ya < p"
+ by auto
+ ultimately show False
+ apply simp
+ apply (frule_tac m = p in zcong_not_zero)
+ apply (auto simp add: a)
+ done
+qed
-lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)";
+lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
apply (insert F_D_disj finite_F finite_D)
- proof -;
- have "card (F \<union> D) = card E + card D";
- by (auto simp add: finite_F finite_D F_D_disj
- card_Un_disjoint F_card_eq_E)
- then have "card (F \<union> D) = card C";
- by (simp add: C_card_eq_D_plus_E)
- from this show "card (F \<union> D) = nat ((p - 1) div 2)";
- by (simp add: C_card_eq_B B_card_eq)
-qed;
+proof -
+ have "card (F \<union> D) = card E + card D"
+ by (auto simp add: finite_F finite_D F_D_disj
+ card_Un_disjoint F_card_eq_E)
+ then have "card (F \<union> D) = card C"
+ by (simp add: C_card_eq_D_plus_E)
+ from this show "card (F \<union> D) = nat ((p - 1) div 2)"
+ by (simp add: C_card_eq_B B_card_eq)
+qed
-lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A";
- apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card)
-by (auto simp add: card_seteq)
+lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A"
+ using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
-lemma (in GAUSS) prod_D_F_eq_prod_A:
- "(setprod id D) * (setprod id F) = setprod id A";
+lemma (in GAUSS) prod_D_F_eq_prod_A:
+ "(setprod id D) * (setprod id F) = setprod id A"
apply (insert F_D_disj finite_D finite_F)
apply (frule setprod_Un_disjoint [of F D id])
-by (auto simp add: F_Un_D_eq_A)
+ apply (auto simp add: F_Un_D_eq_A)
+ done
lemma (in GAUSS) prod_F_zcong:
- "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
- proof -
- have "setprod id F = setprod id (op - p ` E)"
- by (auto simp add: F_def)
- then have "setprod id F = setprod (op - p) E"
- apply simp
- apply (insert finite_E inj_on_pminusx_E)
- by (frule_tac f = "op - p" in setprod_reindex_id, auto)
- then have one:
- "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
- apply simp
- apply (insert p_g_0 finite_E)
- by (auto simp add: StandardRes_prod)
- moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
- apply clarify
- apply (insert zcong_id [of p])
- by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
- moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
- apply clarify
- by (simp add: StandardRes_prop1 zcong_sym)
- moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
- apply clarify
- apply (insert a b)
- by (rule_tac b = "p - x" in zcong_trans, auto)
- ultimately have c:
- "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
- apply simp
- apply (insert finite_E p_g_0)
- by (rule setprod_same_function_zcong [of E "StandardRes p o (op - p)"
- uminus p], auto)
- then have two: "[setprod id F = setprod (uminus) E](mod p)"
- apply (insert one c)
- by (rule zcong_trans [of "setprod id F"
+ "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
+proof -
+ have "setprod id F = setprod id (op - p ` E)"
+ by (auto simp add: F_def)
+ then have "setprod id F = setprod (op - p) E"
+ apply simp
+ apply (insert finite_E inj_on_pminusx_E)
+ apply (frule_tac f = "op - p" in setprod_reindex_id, auto)
+ done
+ then have one:
+ "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
+ apply simp
+ apply (insert p_g_0 finite_E)
+ by (auto simp add: StandardRes_prod)
+ moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
+ apply clarify
+ apply (insert zcong_id [of p])
+ apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
+ done
+ moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
+ apply clarify
+ apply (simp add: StandardRes_prop1 zcong_sym)
+ done
+ moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
+ apply clarify
+ apply (insert a b)
+ apply (rule_tac b = "p - x" in zcong_trans, auto)
+ done
+ ultimately have c:
+ "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
+ apply simp
+ apply (insert finite_E p_g_0)
+ apply (rule setprod_same_function_zcong
+ [of E "StandardRes p o (op - p)" uminus p], auto)
+ done
+ then have two: "[setprod id F = setprod (uminus) E](mod p)"
+ apply (insert one c)
+ apply (rule zcong_trans [of "setprod id F"
"setprod (StandardRes p o op - p) E" p
- "setprod uminus E"], auto)
- also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
- apply (insert finite_E)
- by (induct set: Finites, auto)
- then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
- by (simp add: zmult_commute)
- with two show ?thesis
- by simp
+ "setprod uminus E"], auto)
+ done
+ also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
+ using finite_E by (induct set: Finites) auto
+ then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
+ by (simp add: zmult_commute)
+ with two show ?thesis
+ by simp
qed
subsection {* Gauss' Lemma *}
@@ -439,60 +446,65 @@
by (auto simp add: finite_E neg_one_special)
theorem (in GAUSS) pre_gauss_lemma:
- "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
- proof -
- have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
- then have "[setprod id A = ((-1)^(card E) * setprod id E) *
- setprod id D] (mod p)"
- apply (rule zcong_trans)
- by (auto simp add: prod_F_zcong zcong_scalar)
- then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
- apply (rule zcong_trans)
- apply (insert C_prod_eq_D_times_E, erule subst)
- by (subst zmult_assoc, auto)
- then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
- apply (rule zcong_trans)
- by (simp add: C_B_zcong_prod zcong_scalar2)
- then have "[setprod id A = ((-1)^(card E) *
- (setprod id ((%x. x * a) ` A)))] (mod p)"
- by (simp add: B_def)
- then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
- (mod p)"
- by(simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
- moreover have "setprod (%x. x * a) A =
- setprod (%x. a) A * setprod id A"
- by (insert finite_A, induct set: Finites, auto)
- ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
- setprod id A))] (mod p)"
- by simp
- then have "[setprod id A = ((-1)^(card E) * a^(card A) *
- setprod id A)](mod p)"
- apply (rule zcong_trans)
- by (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant
- zmult_assoc)
- then have a: "[setprod id A * (-1)^(card E) =
- ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
- by (rule zcong_scalar)
- then have "[setprod id A * (-1)^(card E) = setprod id A *
- (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
- apply (rule zcong_trans)
- by (simp add: a mult_commute mult_left_commute)
- then have "[setprod id A * (-1)^(card E) = setprod id A *
- a^(card A)](mod p)"
- apply (rule zcong_trans)
- by (simp add: aux)
- with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
- p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
- by (simp add: order_less_imp_le)
- from this show ?thesis
- by (simp add: A_card_eq zcong_sym)
+ "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
+proof -
+ have "[setprod id A = setprod id F * setprod id D](mod p)"
+ by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
+ then have "[setprod id A = ((-1)^(card E) * setprod id E) *
+ setprod id D] (mod p)"
+ apply (rule zcong_trans)
+ apply (auto simp add: prod_F_zcong zcong_scalar)
+ done
+ then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
+ apply (rule zcong_trans)
+ apply (insert C_prod_eq_D_times_E, erule subst)
+ apply (subst zmult_assoc, auto)
+ done
+ then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
+ apply (rule zcong_trans)
+ apply (simp add: C_B_zcong_prod zcong_scalar2)
+ done
+ then have "[setprod id A = ((-1)^(card E) *
+ (setprod id ((%x. x * a) ` A)))] (mod p)"
+ by (simp add: B_def)
+ then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
+ (mod p)"
+ by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
+ moreover have "setprod (%x. x * a) A =
+ setprod (%x. a) A * setprod id A"
+ using finite_A by (induct set: Finites) auto
+ ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
+ setprod id A))] (mod p)"
+ by simp
+ then have "[setprod id A = ((-1)^(card E) * a^(card A) *
+ setprod id A)](mod p)"
+ apply (rule zcong_trans)
+ apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant zmult_assoc)
+ done
+ then have a: "[setprod id A * (-1)^(card E) =
+ ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
+ by (rule zcong_scalar)
+ then have "[setprod id A * (-1)^(card E) = setprod id A *
+ (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
+ apply (rule zcong_trans)
+ apply (simp add: a mult_commute mult_left_commute)
+ done
+ then have "[setprod id A * (-1)^(card E) = setprod id A *
+ a^(card A)](mod p)"
+ apply (rule zcong_trans)
+ apply (simp add: aux)
+ done
+ with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
+ p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
+ by (simp add: order_less_imp_le)
+ from this show ?thesis
+ by (simp add: A_card_eq zcong_sym)
qed
theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
proof -
from Euler_Criterion p_prime p_g_2 have
- "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
+ "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
by auto
moreover note pre_gauss_lemma
ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
--- a/src/HOL/NumberTheory/Int2.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/Int2.thy Thu Dec 08 12:50:04 2005 +0100
@@ -5,14 +5,14 @@
header {*Integers: Divisibility and Congruences*}
-theory Int2 imports Finite2 WilsonRuss begin;
+theory Int2 imports Finite2 WilsonRuss begin
text{*Note. This theory is being revised. See the web page
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
constdefs
MultInv :: "int => int => int"
- "MultInv p x == x ^ nat (p - 2)";
+ "MultInv p x == x ^ nat (p - 2)"
(*****************************************************************)
(* *)
@@ -20,69 +20,68 @@
(* *)
(*****************************************************************)
-lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) -->
- p dvd ((y::int) ^ n)";
- by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
+lemma zpower_zdvd_prop1:
+ "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
+ by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
-lemma zdvd_bounds: "n dvd m ==> (m \<le> (0::int) | n \<le> m)";
-proof -;
- assume "n dvd m";
- then have "~(0 < m & m < n)";
- apply (insert zdvd_not_zless [of m n])
- by (rule contrapos_pn, auto)
- then have "(~0 < m | ~m < n)" by auto
+lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
+proof -
+ assume "n dvd m"
+ then have "~(0 < m & m < n)"
+ using zdvd_not_zless [of m n] by auto
then show ?thesis by auto
-qed;
-
-lemma aux4: " -(m * n) = (-m) * (n::int)";
- by auto
+qed
lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==>
- (p dvd m) | (p dvd n)";
- apply (case_tac "0 \<le> m")
+ (p dvd m) | (p dvd n)"
+ apply (cases "0 \<le> m")
apply (simp add: zprime_zdvd_zmult)
- by (insert zprime_zdvd_zmult [of "-m" p n], auto)
+ apply (insert zprime_zdvd_zmult [of "-m" p n])
+ apply auto
+ done
-lemma zpower_zdvd_prop2 [rule_format]: "zprime p --> p dvd ((y::int) ^ n)
- --> 0 < n --> p dvd y";
- apply (induct_tac n, auto)
- apply (frule zprime_zdvd_zmult_better, auto)
-done
-
-lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y";
- by arith
+lemma zpower_zdvd_prop2:
+ "zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y"
+ apply (induct n)
+ apply simp
+ apply (frule zprime_zdvd_zmult_better)
+ apply simp
+ apply force
+ done
-lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
-proof -;
- assume "0 < z";
- then have "(x div z) * z \<le> (x div z) * z + x mod z";
- apply (rule_tac x = "x div z * z" in stupid)
- by (simp add: pos_mod_sign)
- also have "... = x";
- by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
- also assume "x < y * z";
- finally show ?thesis;
+lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
+proof -
+ assume "0 < z"
+ then have "(x div z) * z \<le> (x div z) * z + x mod z"
+ by arith
+ also have "... = x"
+ by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
+ also assume "x < y * z"
+ finally show ?thesis
by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
-qed;
+qed
-lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";
-proof -;
- assume "0 < z" and "x < (y * z) + z";
+lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"
+proof -
+ assume "0 < z" and "x < (y * z) + z"
then have "x < (y + 1) * z" by (auto simp add: int_distrib)
- then have "x div z < y + 1";
- by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
+ then have "x div z < y + 1"
+ apply -
+ apply (rule_tac y = "y + 1" in div_prop1)
+ apply (auto simp add: prems)
+ done
then show ?thesis by auto
-qed;
+qed
-lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)";
-proof-;
- assume "0 < y";
+lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"
+proof-
+ assume "0 < y"
from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
- moreover have "0 \<le> x mod y";
+ moreover have "0 \<le> x mod y"
by (auto simp add: prems pos_mod_sign)
- ultimately show ?thesis;
+ ultimately show ?thesis
by arith
-qed;
+qed
(*****************************************************************)
(* *)
@@ -90,96 +89,102 @@
(* *)
(*****************************************************************)
-lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
+lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
by (auto simp add: zcong_def)
-lemma zcong_id: "[m = 0] (mod m)";
+lemma zcong_id: "[m = 0] (mod m)"
by (auto simp add: zcong_def zdvd_0_right)
-lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";
+lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
by (auto simp add: zcong_refl zcong_zadd)
-lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
- by (induct_tac z, auto simp add: zcong_zmult)
+lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
+ by (induct z) (auto simp add: zcong_zmult)
lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
- [a = d](mod m)";
- by (auto, rule_tac b = c in zcong_trans)
+ [a = d](mod m)"
+ apply (erule zcong_trans)
+ apply simp
+ done
-lemma aux1: "a - b = (c::int) ==> a = c + b";
+lemma aux1: "a - b = (c::int) ==> a = c + b"
by auto
lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
- [c = b * d] (mod m))";
+ [c = b * d] (mod m))"
apply (auto simp add: zcong_def dvd_def)
apply (rule_tac x = "ka + k * d" in exI)
- apply (drule aux1)+;
+ apply (drule aux1)+
apply (auto simp add: int_distrib)
apply (rule_tac x = "ka - k * d" in exI)
- apply (drule aux1)+;
+ apply (drule aux1)+
apply (auto simp add: int_distrib)
-done
+ done
lemma zcong_zmult_prop2: "[a = b](mod m) ==>
- ([c = d * a](mod m) = [c = d * b] (mod m))";
+ ([c = d * a](mod m) = [c = d * b] (mod m))"
by (auto simp add: zmult_ac zcong_zmult_prop1)
lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
- ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
+ ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
apply (auto simp add: zcong_def)
apply (drule zprime_zdvd_zmult_better, auto)
-done
+ done
lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
- x < m; y < m |] ==> x = y";
+ x < m; y < m |] ==> x = y"
apply (simp add: zcong_zmod_eq)
- apply (subgoal_tac "(x mod m) = x");
- apply (subgoal_tac "(y mod m) = y");
+ apply (subgoal_tac "(x mod m) = x")
+ apply (subgoal_tac "(y mod m) = y")
apply simp
apply (rule_tac [1-2] mod_pos_pos_trivial)
-by auto
+ apply auto
+ done
lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
- ~([x = 1] (mod p))";
-proof;
+ ~([x = 1] (mod p))"
+proof
assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
- then have "[1 = -1] (mod p)";
+ then have "[1 = -1] (mod p)"
apply (auto simp add: zcong_sym)
apply (drule zcong_trans, auto)
- done
- then have "[1 + 1 = -1 + 1] (mod p)";
+ done
+ then have "[1 + 1 = -1 + 1] (mod p)"
by (simp only: zcong_shift)
- then have "[2 = 0] (mod p)";
+ then have "[2 = 0] (mod p)"
by auto
- then have "p dvd 2";
+ then have "p dvd 2"
by (auto simp add: dvd_def zcong_def)
- with prems show False;
+ with prems show False
by (auto simp add: zdvd_not_zless)
-qed;
+qed
-lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
+lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"
by (auto simp add: zcong_def)
lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==>
- [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)";
+ [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"
by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
- ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
+ ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"
apply auto
apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
-by auto
+ apply auto
+ done
-lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)";
+lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"
by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
-lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0";
+lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"
apply (drule order_le_imp_less_or_eq, auto)
-by (frule_tac m = m in zcong_not_zero, auto)
+ apply (frule_tac m = m in zcong_not_zero)
+ apply auto
+ done
lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
- ==> zgcd (setprod id A,y) = 1";
- by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
+ ==> zgcd (setprod id A,y) = 1"
+ by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
(*****************************************************************)
(* *)
@@ -188,69 +193,69 @@
(*****************************************************************)
lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
- [(MultInv p x) = (MultInv p y)] (mod p)";
+ [(MultInv p x) = (MultInv p y)] (mod p)"
by (auto simp add: MultInv_def zcong_zpower)
lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
- [(x * (MultInv p x)) = 1] (mod p)";
-proof (simp add: MultInv_def zcong_eq_zdvd_prop);
- assume "2 < p" and "zprime p" and "~ p dvd x";
- have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
+ [(x * (MultInv p x)) = 1] (mod p)"
+proof (simp add: MultInv_def zcong_eq_zdvd_prop)
+ assume "2 < p" and "zprime p" and "~ p dvd x"
+ have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
by auto
- also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
+ also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
by (simp only: nat_add_distrib, auto)
also have "p - 2 + 1 = p - 1" by arith
- finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
+ finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
by (rule ssubst, auto)
- also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
+ also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
by (auto simp add: Little_Fermat)
- finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
-qed;
+ finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
+qed
lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
- [(MultInv p x) * x = 1] (mod p)";
+ [(MultInv p x) * x = 1] (mod p)"
by (auto simp add: MultInv_prop2 zmult_ac)
-lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
+lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
by (simp add: nat_diff_distrib)
-lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
+lemma aux_2: "2 < p ==> 0 < nat (p - 2)"
by auto
lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
- ~([MultInv p x = 0](mod p))";
+ ~([MultInv p x = 0](mod p))"
apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
apply (drule aux_2)
apply (drule zpower_zdvd_prop2, auto)
-done
+ done
lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
[(MultInv p (MultInv p x)) = (x * (MultInv p x) *
- (MultInv p (MultInv p x)))] (mod p)";
+ (MultInv p (MultInv p x)))] (mod p)"
apply (drule MultInv_prop2, auto)
- apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
+ apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto)
apply (auto simp add: zcong_sym)
-done
+ done
lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
- [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
+ [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)"
apply (frule MultInv_prop3, auto)
apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
apply (drule MultInv_prop2, auto)
apply (drule_tac k = x in zcong_scalar2, auto)
apply (auto simp add: zmult_ac)
-done
+ done
lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
- [(MultInv p (MultInv p x)) = x] (mod p)";
+ [(MultInv p (MultInv p x)) = x] (mod p)"
apply (frule aux__1, auto)
apply (drule aux__2, auto)
apply (drule zcong_trans, auto)
-done
+ done
lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p));
~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==>
- [x = y] (mod p)";
+ [x = y] (mod p)"
apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
m = p and k = x in zcong_scalar)
apply (insert MultInv_prop2 [of p x], simp)
@@ -261,38 +266,38 @@
apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
apply (auto simp add: zcong_sym)
-done
+ done
lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>
- [a * MultInv p j = a * MultInv p k] (mod p)";
+ [a * MultInv p j = a * MultInv p k] (mod p)"
by (drule MultInv_prop1, auto simp add: zcong_scalar2)
lemma aux___1: "[j = a * MultInv p k] (mod p) ==>
- [j * k = a * MultInv p k * k] (mod p)";
+ [j * k = a * MultInv p k * k] (mod p)"
by (auto simp add: zcong_scalar)
lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p));
- [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
+ [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
[of "MultInv p k * k" 1 p "j * k" a])
apply (auto simp add: zmult_ac)
-done
+ done
lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
- (MultInv p j) * a] (mod p)";
+ (MultInv p j) * a] (mod p)"
by (auto simp add: zmult_assoc zcong_scalar2)
lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
[(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
- ==> [k = a * (MultInv p j)] (mod p)";
+ ==> [k = a * (MultInv p j)] (mod p)"
apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
[of "MultInv p j * j" 1 p "MultInv p j * a" k])
apply (auto simp add: zmult_ac zcong_sym)
-done
+ done
lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==>
- [k = a * MultInv p j] (mod p)";
+ [k = a * MultInv p j] (mod p)"
apply (drule aux___1)
apply (frule aux___2, auto)
by (drule aux___3, drule aux___4, auto)
@@ -300,11 +305,11 @@
lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p));
~([k = 0](mod p)); ~([j = 0](mod p));
[a * MultInv p j = a * MultInv p k] (mod p) |] ==>
- [j = k] (mod p)";
+ [j = k] (mod p)"
apply (auto simp add: zcong_eq_zdvd_prop [of a p])
apply (frule zprime_imp_zrelprime, auto)
apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
apply (drule MultInv_prop5, auto)
-done
+ done
end
--- a/src/HOL/NumberTheory/IntFact.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy Thu Dec 08 12:50:04 2005 +0100
@@ -36,41 +36,36 @@
lemma d22set_induct:
- "(!!a. P {} a) ==>
- (!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1)
- ==> P (d22set a) a)
- ==> P (d22set u) u"
-proof -
- case rule_context
- show ?thesis
- apply (rule d22set.induct)
- apply safe
- apply (case_tac [2] "1 < a")
- apply (rule_tac [2] rule_context)
- apply (simp_all (no_asm_simp))
- apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
- done
-qed
+ assumes "!!a. P {} a"
+ and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
+ shows "P (d22set u) u"
+ apply (rule d22set.induct)
+ apply safe
+ prefer 2
+ apply (case_tac "1 < a")
+ apply (rule_tac prems)
+ apply (simp_all (no_asm_simp))
+ apply (simp_all (no_asm_simp) add: d22set.simps prems)
+ done
lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
apply (induct a rule: d22set_induct)
- prefer 2
- apply (subst d22set.simps)
- apply auto
+ apply simp
+ apply (subst d22set.simps)
+ apply auto
done
lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
apply (induct a rule: d22set_induct)
- prefer 2
+ apply simp
apply (subst d22set.simps)
apply auto
done
lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
- apply (auto dest: d22set_le)
- done
+ by (auto dest: d22set_le)
-lemma d22set_mem [rule_format]: "1 < b --> b \<le> a --> b \<in> d22set a"
+lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
apply (induct a rule: d22set.induct)
apply auto
apply (simp_all add: d22set.simps)
--- a/src/HOL/NumberTheory/IntPrimes.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Thu Dec 08 12:50:04 2005 +0100
@@ -2,11 +2,6 @@
ID: $Id$
Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
-
-Changes by Jeremy Avigad, 2003/02/21:
- Repaired definition of zprime_def, added "0 <= m &"
- Added lemma zgcd_geq_zero
- Repaired proof of zprime_imp_zrelprime
*)
header {* Divisibility and prime numbers (on integers) *}
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Dec 08 12:50:04 2005 +0100
@@ -16,12 +16,12 @@
(* *)
(***************************************************************)
-lemma (in GAUSS) QRLemma1: "a * setsum id A =
+lemma (in GAUSS) QRLemma1: "a * setsum id A =
p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
proof -
- from finite_A have "a * setsum id A = setsum (%x. a * x) A"
+ from finite_A have "a * setsum id A = setsum (%x. a * x) A"
by (auto simp add: setsum_const_mult id_def)
- also have "setsum (%x. a * x) = setsum (%x. x * a)"
+ also have "setsum (%x. a * x) = setsum (%x. x * a)"
by (auto simp add: zmult_commute)
also have "setsum (%x. x * a) A = setsum id B"
by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
@@ -34,28 +34,26 @@
also from C_eq have "... = setsum id (D \<union> E)"
by auto
also from finite_D finite_E have "... = setsum id D + setsum id E"
- apply (rule setsum_Un_disjoint)
- by (auto simp add: D_def E_def)
- also have "setsum (%x. p * (x div p)) B =
+ by (rule setsum_Un_disjoint) (auto simp add: D_def E_def)
+ also have "setsum (%x. p * (x div p)) B =
setsum ((%x. p * (x div p)) o (%x. (x * a))) A"
by (auto simp add: B_def setsum_reindex inj_on_xa_A)
also have "... = setsum (%x. p * ((x * a) div p)) A"
by (auto simp add: o_def)
- also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
+ also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
p * setsum (%x. ((x * a) div p)) A"
by (auto simp add: setsum_const_mult)
finally show ?thesis by arith
qed
-lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
- setsum id D"
+lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
+ setsum id D"
proof -
from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
by (simp add: Un_commute)
- also from F_D_disj finite_D finite_F have
- "... = setsum id D + setsum id F"
- apply (simp add: Int_commute)
- by (intro setsum_Un_disjoint)
+ also from F_D_disj finite_D finite_F
+ have "... = setsum id D + setsum id F"
+ by (auto simp add: Int_commute intro: setsum_Un_disjoint)
also from F_def have "F = (%x. (p - x)) ` E"
by auto
also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
@@ -69,30 +67,30 @@
by arith
qed
-lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
+lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
proof -
have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
- by (auto simp add: zdiff_zmult_distrib)
+ by (auto simp add: zdiff_zmult_distrib)
also note QRLemma1
- also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
- setsum id E - setsum id A =
- p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
+ also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
+ setsum id E - setsum id A =
+ p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
setsum id E - (p * int (card E) - setsum id E + setsum id D)"
by auto
- also have "... = p * (\<Sum>x \<in> A. x * a div p) -
- p * int (card E) + 2 * setsum id E"
+ also have "... = p * (\<Sum>x \<in> A. x * a div p) -
+ p * int (card E) + 2 * setsum id E"
by arith
finally show ?thesis
by (auto simp only: zdiff_zmult_distrib2)
qed
-lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
+lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
(setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
proof -
assume a_odd: "a \<in> zOdd"
from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
- (a - 1) * setsum id A - 2 * setsum id E"
+ (a - 1) * setsum id A - 2 * setsum id E"
by arith
from a_odd have "a - 1 \<in> zEven"
by (rule odd_minus_one_even)
@@ -109,10 +107,10 @@
with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
by (auto simp add: odd_iff_not_even)
thus ?thesis
- by (auto simp only: even_diff [THEN sym])
+ by (auto simp only: even_diff [symmetric])
qed
-lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
+lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
(-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
proof -
assume "a \<in> zOdd"
@@ -130,7 +128,7 @@
by (auto simp add: A_def)
with a_nonzero have "0 \<le> x * a"
by (auto simp add: zero_le_mult_iff)
- with p_g_2 show "0 \<le> x * a div p"
+ with p_g_2 show "0 \<le> x * a div p"
by (auto simp add: pos_imp_zdiv_nonneg_iff)
qed
qed
@@ -143,12 +141,13 @@
qed
lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p;
- A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
+ A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
(Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
apply (subst GAUSS.gauss_lemma)
apply (auto simp add: GAUSS_def)
apply (subst GAUSS.QRLemma5)
-by (auto simp add: GAUSS_def)
+ apply (auto simp add: GAUSS_def)
+ done
(******************************************************************)
(* *)
@@ -178,9 +177,9 @@
defines S_def: "S == P_set <*> Q_set"
defines S1_def: "S1 == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
defines S2_def: "S2 == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
- defines f1_def: "f1 j == { (j1, y). (j1, y):S & j1 = j &
+ defines f1_def: "f1 j == { (j1, y). (j1, y):S & j1 = j &
(y \<le> (q * j) div p) }"
- defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j &
+ defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j &
(x \<le> (p * j) div q) }"
lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
@@ -199,7 +198,7 @@
then show ?thesis by auto
qed
-lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
+lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
(p * b \<noteq> q * a)"
proof
assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
@@ -212,10 +211,11 @@
with p_prime have "q = 1 | q = p"
apply (auto simp add: zprime_def QRTEMP_def)
apply (drule_tac x = q and R = False in allE)
- apply (simp add: QRTEMP_def)
+ apply (simp add: QRTEMP_def)
apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
apply (insert prems)
- by (auto simp add: QRTEMP_def)
+ apply (auto simp add: QRTEMP_def)
+ done
with q_g_2 p_neq_q show False by auto
qed
ultimately have "q dvd b" by auto
@@ -223,7 +223,7 @@
proof -
assume "q dvd b"
moreover from prems have "0 < b" by auto
- ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
+ ultimately show ?thesis using zdvd_bounds [of q b] by auto
qed
with prems have "q \<le> (q - 1) div 2" by auto
then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
@@ -240,10 +240,10 @@
qed
lemma (in QRTEMP) P_set_finite: "finite (P_set)"
- by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
+ using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
- by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
+ using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite)
lemma (in QRTEMP) S_finite: "finite S"
by (auto simp add: S_def P_set_finite Q_set_finite finite_cartesian_product)
@@ -263,43 +263,42 @@
qed
lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))"
- by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
+ using p_fact by (auto simp add: P_set_def card_bdd_int_set_l_le)
lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
- by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
+ using q_fact by (auto simp add: Q_set_def card_bdd_int_set_l_le)
lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
- apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
- apply (auto simp add: S_def zmult_int setsum_constant)
-done
+ using P_set_card Q_set_card P_set_finite Q_set_finite
+ by (auto simp add: S_def zmult_int setsum_constant)
lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
by (auto simp add: S1_def S2_def)
lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2"
apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
- proof -
- fix a and b
- assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
- with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
- moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
- ultimately show "p * b < q * a" by auto
- qed
+proof -
+ fix a and b
+ assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
+ with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
+ moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
+ ultimately show "p * b < q * a" by auto
+qed
-lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
+lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
int(card(S1)) + int(card(S2))"
-proof-
+proof -
have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
by (auto simp add: S_card)
also have "... = int( card(S1) + card(S2))"
apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
apply (drule card_Un_disjoint, auto)
- done
+ done
also have "... = int(card(S1)) + int(card(S2))" by auto
finally show ?thesis .
qed
-lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
+lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
0 < b; b \<le> (q - 1) div 2 |] ==>
(p * b < q * a) = (b \<le> q * a div p)"
proof -
@@ -309,30 +308,31 @@
assume "p * b < q * a"
then have "p * b \<le> q * a" by auto
then have "(p * b) div p \<le> (q * a) div p"
- by (rule zdiv_mono1, insert p_g_2, auto)
+ by (rule zdiv_mono1) (insert p_g_2, auto)
then show "b \<le> (q * a) div p"
apply (subgoal_tac "p \<noteq> 0")
apply (frule zdiv_zmult_self2, force)
- by (insert p_g_2, auto)
+ apply (insert p_g_2, auto)
+ done
qed
moreover have "b \<le> q * a div p ==> p * b < q * a"
proof -
assume "b \<le> q * a div p"
then have "p * b \<le> p * ((q * a) div p)"
- by (insert p_g_2, auto simp add: mult_le_cancel_left)
+ using p_g_2 by (auto simp add: mult_le_cancel_left)
also have "... \<le> q * a"
- by (rule zdiv_leq_prop, insert p_g_2, auto)
+ by (rule zdiv_leq_prop) (insert p_g_2, auto)
finally have "p * b \<le> q * a" .
then have "p * b < q * a | p * b = q * a"
by (simp only: order_le_imp_less_or_eq)
moreover have "p * b \<noteq> q * a"
- by (rule pb_neq_qa, insert prems, auto)
+ by (rule pb_neq_qa) (insert prems, auto)
ultimately show ?thesis by auto
qed
ultimately show ?thesis ..
qed
-lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
+lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
0 < b; b \<le> (q - 1) div 2 |] ==>
(q * a < p * b) = (a \<le> p * b div q)"
proof -
@@ -342,30 +342,31 @@
assume "q * a < p * b"
then have "q * a \<le> p * b" by auto
then have "(q * a) div q \<le> (p * b) div q"
- by (rule zdiv_mono1, insert q_g_2, auto)
+ by (rule zdiv_mono1) (insert q_g_2, auto)
then show "a \<le> (p * b) div q"
apply (subgoal_tac "q \<noteq> 0")
apply (frule zdiv_zmult_self2, force)
- by (insert q_g_2, auto)
+ apply (insert q_g_2, auto)
+ done
qed
moreover have "a \<le> p * b div q ==> q * a < p * b"
proof -
assume "a \<le> p * b div q"
then have "q * a \<le> q * ((p * b) div q)"
- by (insert q_g_2, auto simp add: mult_le_cancel_left)
+ using q_g_2 by (auto simp add: mult_le_cancel_left)
also have "... \<le> p * b"
- by (rule zdiv_leq_prop, insert q_g_2, auto)
+ by (rule zdiv_leq_prop) (insert q_g_2, auto)
finally have "q * a \<le> p * b" .
then have "q * a < p * b | q * a = p * b"
by (simp only: order_le_imp_less_or_eq)
moreover have "p * b \<noteq> q * a"
- by (rule pb_neq_qa, insert prems, auto)
+ by (rule pb_neq_qa) (insert prems, auto)
ultimately show ?thesis by auto
qed
ultimately show ?thesis ..
qed
-lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
+lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
(q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
proof-
assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
@@ -388,10 +389,10 @@
by (auto simp add: even1 even_prod_div_2)
also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
- finally show ?thesis
- apply (rule_tac x = " q * ((p - 1) div 2)" and
+ finally show ?thesis
+ apply (rule_tac x = " q * ((p - 1) div 2)" and
y = "(q - 1) div 2" in div_prop2)
- by (insert prems, auto)
+ using prems by auto
qed
lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
@@ -410,27 +411,29 @@
ultimately have "card ((%(x,y). y) ` (f1 j)) = card (f1 j)"
by (auto simp add: f1_def card_image)
moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
- by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def
- image_def)
+ using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
ultimately show ?thesis by (auto simp add: f1_def)
qed
also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
proof -
- have "{y. y \<in> Q_set & y \<le> (q * j) div p} =
+ have "{y. y \<in> Q_set & y \<le> (q * j) div p} =
{y. 0 < y & y \<le> (q * j) div p}"
apply (auto simp add: Q_set_def)
- proof -
- fix x
- assume "0 < x" and "x \<le> q * j div p"
- with j_fact P_set_def have "j \<le> (p - 1) div 2" by auto
- with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
- by (auto simp add: mult_le_cancel_left)
- with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
- by (auto simp add: zdiv_mono1)
- also from prems have "... \<le> (q - 1) div 2"
- apply simp apply (insert aux2) by (simp add: QRTEMP_def)
- finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
- qed
+ proof -
+ fix x
+ assume "0 < x" and "x \<le> q * j div p"
+ with j_fact P_set_def have "j \<le> (p - 1) div 2" by auto
+ with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
+ by (auto simp add: mult_le_cancel_left)
+ with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
+ by (auto simp add: zdiv_mono1)
+ also from prems have "... \<le> (q - 1) div 2"
+ apply simp
+ apply (insert aux2)
+ apply (simp add: QRTEMP_def)
+ done
+ finally show "x \<le> (q - 1) div 2" using prems by auto
+ qed
then show ?thesis by auto
qed
also have "... = (q * j) div p"
@@ -440,7 +443,8 @@
then have "0 \<le> q * j" by auto
then have "0 div p \<le> (q * j) div p"
apply (rule_tac a = 0 in zdiv_mono1)
- by (insert p_g_2, auto)
+ apply (insert p_g_2, auto)
+ done
also have "0 div p = 0" by auto
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
qed
@@ -463,26 +467,25 @@
ultimately have "card ((%(x,y). x) ` (f2 j)) = card (f2 j)"
by (auto simp add: f2_def card_image)
moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
- by (insert prems, auto simp add: f2_def S_def Q_set_def
- P_set_def image_def)
+ using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
ultimately show ?thesis by (auto simp add: f2_def)
qed
also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
proof -
- have "{y. y \<in> P_set & y \<le> (p * j) div q} =
+ have "{y. y \<in> P_set & y \<le> (p * j) div q} =
{y. 0 < y & y \<le> (p * j) div q}"
apply (auto simp add: P_set_def)
- proof -
- fix x
- assume "0 < x" and "x \<le> p * j div q"
- with j_fact Q_set_def have "j \<le> (q - 1) div 2" by auto
- with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
- by (auto simp add: mult_le_cancel_left)
- with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
- by (auto simp add: zdiv_mono1)
- also from prems have "... \<le> (p - 1) div 2"
- by (auto simp add: aux2 QRTEMP_def)
- finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
+ proof -
+ fix x
+ assume "0 < x" and "x \<le> p * j div q"
+ with j_fact Q_set_def have "j \<le> (q - 1) div 2" by auto
+ with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
+ by (auto simp add: mult_le_cancel_left)
+ with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
+ by (auto simp add: zdiv_mono1)
+ also from prems have "... \<le> (p - 1) div 2"
+ by (auto simp add: aux2 QRTEMP_def)
+ finally show "x \<le> (p - 1) div 2" using prems by auto
qed
then show ?thesis by auto
qed
@@ -493,7 +496,8 @@
then have "0 \<le> p * j" by auto
then have "0 div q \<le> (p * j) div q"
apply (rule_tac a = 0 in zdiv_mono1)
- by (insert q_g_2, auto)
+ apply (insert q_g_2, auto)
+ done
also have "0 div q = 0" by auto
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
qed
@@ -511,12 +515,12 @@
moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})"
by (auto simp add: f1_def)
moreover note P_set_finite
- ultimately have "int(card (UNION P_set f1)) =
+ ultimately have "int(card (UNION P_set f1)) =
setsum (%x. int(card (f1 x))) P_set"
by(simp add:card_UN_disjoint int_setsum o_def)
moreover have "S1 = UNION P_set f1"
by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
- ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
+ ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
by auto
also have "... = setsum (%j. q * j div p) P_set"
using aux3a by(fastsimp intro: setsum_cong)
@@ -531,34 +535,34 @@
have "f2 x \<subseteq> S" by (auto simp add: f2_def)
with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
qed
- moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y -->
+ moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y -->
(f2 x) \<inter> (f2 y) = {})"
by (auto simp add: f2_def)
moreover note Q_set_finite
- ultimately have "int(card (UNION Q_set f2)) =
+ ultimately have "int(card (UNION Q_set f2)) =
setsum (%x. int(card (f2 x))) Q_set"
by(simp add:card_UN_disjoint int_setsum o_def)
moreover have "S2 = UNION Q_set f2"
by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
- ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
+ ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
by auto
also have "... = setsum (%j. p * j div q) Q_set"
using aux3b by(fastsimp intro: setsum_cong)
finally show ?thesis .
qed
-lemma (in QRTEMP) S1_carda: "int (card(S1)) =
+lemma (in QRTEMP) S1_carda: "int (card(S1)) =
setsum (%j. (j * q) div p) P_set"
by (auto simp add: S1_card zmult_ac)
-lemma (in QRTEMP) S2_carda: "int (card(S2)) =
+lemma (in QRTEMP) S2_carda: "int (card(S2)) =
setsum (%j. (j * p) div q) Q_set"
by (auto simp add: S2_card zmult_ac)
-lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
+lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
proof -
- have "(setsum (%j. (j * p) div q) Q_set) +
+ have "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)"
by (auto simp add: S1_carda S2_carda)
also have "... = int (card S1) + int (card S2)"
@@ -572,50 +576,54 @@
apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
apply (drule_tac x = q in allE)
apply (drule_tac x = p in allE)
-by auto
+ apply auto
+ done
-lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
+lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
proof -
from prems have "~([p = 0] (mod q))"
by (auto simp add: pq_prime_neq QRTEMP_def)
- with prems have a1: "(Legendre p q) = (-1::int) ^
+ with prems have a1: "(Legendre p q) = (-1::int) ^
nat(setsum (%x. ((x * p) div q)) Q_set)"
apply (rule_tac p = q in MainQRLemma)
- by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
+ apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
+ done
from prems have "~([q = 0] (mod p))"
apply (rule_tac p = q and q = p in pq_prime_neq)
apply (simp add: QRTEMP_def)+
done
- with prems have a2: "(Legendre q p) =
+ with prems have a2: "(Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
apply (rule_tac p = p in MainQRLemma)
- by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
- from a1 a2 have "(Legendre p q) * (Legendre q p) =
+ apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
+ done
+ from a1 a2 have "(Legendre p q) * (Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
(-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
by auto
- also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
+ also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set))"
by (auto simp add: zpower_zadd_distrib)
- also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
+ also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set) =
- nat((setsum (%x. ((x * p) div q)) Q_set) +
+ nat((setsum (%x. ((x * p) div q)) Q_set) +
(setsum (%x. ((x * q) div p)) P_set))"
- apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
- nat_add_distrib [THEN sym])
- by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
+ apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
+ nat_add_distrib [symmetric])
+ apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric])
+ done
also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))"
by (auto simp add: pq_sum_prop)
finally show ?thesis .
qed
theorem Quadratic_Reciprocity:
- "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
- p \<noteq> q |]
- ==> (Legendre p q) * (Legendre q p) =
+ "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
+ p \<noteq> q |]
+ ==> (Legendre p q) * (Legendre q p) =
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
- by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym]
+ by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [symmetric]
QRTEMP_def)
end
--- a/src/HOL/NumberTheory/Residues.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/Residues.thy Thu Dec 08 12:50:04 2005 +0100
@@ -5,7 +5,7 @@
header {* Residue Sets *}
-theory Residues imports Int2 begin;
+theory Residues imports Int2 begin
text{*Note. This theory is being revised. See the web page
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
@@ -37,7 +37,7 @@
"SR p == {x. (0 \<le> x) & (x < p)}"
SRStar :: "int => int set"
- "SRStar p == {x. (0 < x) & (x < p)}";
+ "SRStar p == {x. (0 < x) & (x < p)}"
(******************************************************************)
(* *)
@@ -47,29 +47,29 @@
subsection {* Properties of StandardRes *}
-lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
+lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod)
lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
- = ([x1 = x2] (mod m))";
+ = ([x1 = x2] (mod m))"
by (auto simp add: StandardRes_def zcong_zmod_eq)
-lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
+lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"
by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
lemma StandardRes_prop4: "2 < m
- ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
+ ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod_eq
zmod_zmult_distrib [of x y m])
-lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x";
+lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
by (auto simp add: StandardRes_def pos_mod_sign)
-lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
+lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"
by (auto simp add: StandardRes_def pos_mod_bound)
lemma StandardRes_eq_zcong:
- "(StandardRes m x = 0) = ([x = 0](mod m))";
+ "(StandardRes m x = 0) = ([x = 0](mod m))"
by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def)
(******************************************************************)
@@ -80,55 +80,56 @@
subsection {* Relations between StandardRes, SRStar, and SR *}
-lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p";
+lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
by (auto simp add: SRStar_def SR_def)
-lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x";
+lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x"
by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p)
- = (~[x = 0] (mod p))";
+ = (~[x = 0] (mod p))"
apply (auto simp add: StandardRes_prop3 StandardRes_def
SRStar_def pos_mod_bound)
apply (subgoal_tac "0 < p")
-by (drule_tac a = x in pos_mod_sign, arith, simp)
+ apply (drule_tac a = x in pos_mod_sign, arith, simp)
+ done
-lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
+lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))"
by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \<in> SRStar p |]
- ==> StandardRes p (MultInv p x) \<in> SRStar p";
- apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
+ ==> StandardRes p (MultInv p x) \<in> SRStar p"
+ apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp)
apply (rule MultInv_prop3)
apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
-done
+ done
-lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
+lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x"
by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \<in> SRStar p |]
- ==> StandardRes p x \<in> SRStar p";
+ ==> StandardRes p x \<in> SRStar p"
by (frule StandardRes_SRStar_prop3, auto)
lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \<in> SRStar p; y \<in> SRStar p|]
- ==> (StandardRes p (x * y)):SRStar p";
+ ==> (StandardRes p (x * y)):SRStar p"
apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
-done
+ done
lemma SRStar_mult_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p));
x \<in> SRStar p |]
- ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
+ ==> StandardRes p (a * MultInv p x) \<in> SRStar p"
apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
-done
+ done
-lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
+lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1"
by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
-lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
+lemma SRStar_finite: "2 < p ==> finite( SRStar p)"
by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
(******************************************************************)
@@ -139,40 +140,42 @@
subsection {* Properties relating ResSets with StandardRes *}
-lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
- apply (subgoal_tac "x = y ==> [x = y](mod m)");
- apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
+lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
+ apply (subgoal_tac "x = y ==> [x = y](mod m)")
+ apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)")
apply (auto simp add: zcong_zmod [of x y m])
-done
+ done
-lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
+lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)"
apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
apply (drule_tac m = m in aux, auto)
-done
+ done
lemma StandardRes_Sum: "[| finite X; 0 < m |]
- ==> [setsum f X = setsum (StandardRes m o f) X](mod m)";
+ ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"
apply (rule_tac F = X in finite_induct)
apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
-done
+ done
-lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
+lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}"
by (auto simp add: StandardRes_ubound StandardRes_lbound)
-lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
+lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X"
apply (rule_tac f = "StandardRes m" in finite_imageD)
- apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
-by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
+ apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset)
+ apply (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
+ done
-lemma mod_mod_is_mod: "[x = x mod m](mod m)";
+lemma mod_mod_is_mod: "[x = x mod m](mod m)"
by (auto simp add: zcong_zmod)
lemma StandardRes_prod: "[| finite X; 0 < m |]
- ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)";
+ ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)"
apply (rule_tac F = X in finite_induct)
-by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
+ apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
+ done
-lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)";
+lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)"
by (auto simp add: ResSet_def)
(****************************************************************)
@@ -181,7 +184,7 @@
(* *)
(****************************************************************)
-lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
+lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
-end;
\ No newline at end of file
+end
--- a/src/HOL/NumberTheory/WilsonRuss.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Thu Dec 08 12:50:04 2005 +0100
@@ -2,9 +2,6 @@
ID: $Id$
Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
-
-Changes by Jeremy Avigad, 2003/02/21:
- repaired proof of prime_g_5
*)
header {* Wilson's Theorem according to Russinoff *}
@@ -165,19 +162,16 @@
declare wset.simps [simp del]
lemma wset_induct:
- "(!!a p. P {} a p) \<Longrightarrow>
- (!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p
- ==> P (wset (a, p)) a p)
- ==> P (wset (u, v)) u v"
-proof -
- case rule_context
- show ?thesis
- apply (rule wset.induct, safe)
- apply (case_tac [2] "1 < a")
- apply (rule_tac [2] rule_context, simp_all)
- apply (simp_all add: wset.simps rule_context)
- done
-qed
+ assumes "!!a p. P {} a p"
+ and "!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
+ shows "P (wset (u, v)) u v"
+ apply (rule wset.induct, safe)
+ prefer 2
+ apply (case_tac "1 < a")
+ apply (rule prems)
+ apply simp_all
+ apply (simp_all add: wset.simps prems)
+ done
lemma wset_mem_imp_or [rule_format]:
"1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)