prime is a predicate now.
--- a/src/HOL/Algebra/Exponent.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/Algebra/Exponent.thy Fri Jul 01 17:41:10 2005 +0200
@@ -11,15 +11,15 @@
constdefs
exponent :: "[nat, nat] => nat"
- "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
+ "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
subsection{*Prime Theorems*}
-lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
+lemma prime_imp_one_less: "prime p ==> Suc 0 < p"
by (unfold prime_def, force)
lemma prime_iff:
- "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
+ "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
apply (auto simp add: prime_imp_one_less)
apply (blast dest!: prime_dvd_mult)
apply (auto simp add: prime_def)
@@ -30,7 +30,7 @@
apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
done
-lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
+lemma zero_less_prime_power: "prime p ==> 0 < p^a"
by (force simp add: prime_iff)
@@ -39,7 +39,7 @@
lemma prime_dvd_cases:
- "[| p*k dvd m*n; p \<in> prime |]
+ "[| p*k dvd m*n; prime p |]
==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
apply (simp add: prime_iff)
apply (frule dvd_mult_left)
@@ -56,7 +56,7 @@
done
-lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime
+lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
==> \<forall>m n. p^c dvd m*n -->
(\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
apply (induct_tac "c")
@@ -89,7 +89,7 @@
(*needed in this form in Sylow.ML*)
lemma div_combine:
- "[| p \<in> prime; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
+ "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
==> p ^ a dvd k"
by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
@@ -117,7 +117,7 @@
subsection{*Exponent Theorems*}
lemma exponent_ge [rule_format]:
- "[|p^k dvd n; p \<in> prime; 0<n|] ==> k <= exponent p n"
+ "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n"
apply (simp add: exponent_def)
apply (erule Greatest_le)
apply (blast dest: prime_imp_one_less power_dvd_bound)
@@ -131,14 +131,14 @@
done
lemma power_Suc_exponent_Not_dvd:
- "[|(p * p ^ exponent p s) dvd s; p \<in> prime |] ==> s=0"
+ "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0"
apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
prefer 2 apply simp
apply (rule ccontr)
apply (drule exponent_ge, auto)
done
-lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
+lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a"
apply (simp (no_asm_simp) add: exponent_def)
apply (rule Greatest_equality, simp)
apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
@@ -148,7 +148,7 @@
"!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
by (simp (no_asm_simp) add: exponent_def)
-lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
+lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
by (simp (no_asm_simp) add: exponent_def)
@@ -156,7 +156,7 @@
lemma exponent_mult_add1:
"[| 0 < a; 0 < b |]
==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
-apply (case_tac "p \<in> prime")
+apply (case_tac "prime p")
apply (rule exponent_ge)
apply (auto simp add: power_add)
apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
@@ -165,7 +165,7 @@
(* exponent_mult_add, opposite inclusion *)
lemma exponent_mult_add2: "[| 0 < a; 0 < b |]
==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
-apply (case_tac "p \<in> prime")
+apply (case_tac "prime p")
apply (rule leI, clarify)
apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
@@ -191,7 +191,7 @@
done
lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
-apply (case_tac "p \<in> prime")
+apply (case_tac "prime p")
apply (auto simp add: prime_iff not_divides_exponent_0)
done
@@ -258,7 +258,7 @@
lemma p_not_div_choose_lemma [rule_format]:
"[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
==> k<K --> exponent p ((j+k) choose k) = 0"
-apply (case_tac "p \<in> prime")
+apply (case_tac "prime p")
prefer 2 apply simp
apply (induct_tac "k")
apply (simp (no_asm))
@@ -293,7 +293,7 @@
lemma const_p_fac_right:
"0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
-apply (case_tac "p \<in> prime")
+apply (case_tac "prime p")
prefer 2 apply simp
apply (frule_tac a = a in zero_less_prime_power)
apply (rule_tac K = "p^a" in p_not_div_choose)
@@ -311,7 +311,7 @@
lemma const_p_fac:
"0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
-apply (case_tac "p \<in> prime")
+apply (case_tac "prime p")
prefer 2 apply simp
apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
prefer 2 apply (force simp add: prime_iff)
--- a/src/HOL/Algebra/Sylow.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/Algebra/Sylow.thy Fri Jul 01 17:41:10 2005 +0200
@@ -15,7 +15,7 @@
locale sylow = group +
fixes p and a and m and calM and RelM
- assumes prime_p: "p \<in> prime"
+ assumes prime_p: "prime p"
and order_G: "order(G) = (p^a) * m"
and finite_G [iff]: "finite (carrier G)"
defines "calM == {s. s \<subseteq> carrier(G) & card(s) = p^a}"
@@ -363,7 +363,7 @@
by (simp add: sylow_def group_def)
theorem sylow_thm:
- "[|p \<in> prime; group(G); order(G) = (p^a) * m; finite (carrier G)|]
+ "[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|]
==> \<exists>H. subgroup H G & card(H) = p^a"
apply (rule sylow.sylow_thm [of G p a m])
apply (simp add: sylow_eq sylow_axioms_def)
--- a/src/HOL/Complex/ex/NSPrimes.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy Fri Jul 01 17:41:10 2005 +0200
@@ -22,7 +22,7 @@
constdefs
starprime :: "hypnat set"
- "starprime == ( *sNat* prime)"
+ "starprime == ( *sNat* {p. prime p})"
constdefs
choicefun :: "'a set => 'a"
@@ -149,7 +149,7 @@
apply (drule_tac x = f in spec, auto, ultra+)
done
-lemma prime_two: "2 : prime"
+lemma prime_two: "prime 2"
apply (unfold prime_def, auto)
apply (frule dvd_imp_le)
apply (auto dest: dvd_0_left)
@@ -158,13 +158,13 @@
declare prime_two [simp]
(* proof uses course-of-value induction *)
-lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k \<in> prime. k dvd n)"
+lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k. prime k & k dvd n)"
apply (rule_tac n = n in nat_less_induct, auto)
-apply (case_tac "n \<in> prime")
-apply (rule_tac x = n in bexI, auto)
+apply (case_tac "prime n")
+apply (rule_tac x = n in exI, auto)
apply (drule conjI [THEN not_prime_ex_mk], auto)
apply (drule_tac x = m in spec, auto)
-apply (rule_tac x = ka in bexI)
+apply (rule_tac x = ka in exI)
apply (auto intro: dvd_mult2)
done
@@ -173,7 +173,7 @@
apply (rule_tac z = n in eq_Abs_hypnat)
apply (auto simp add: hypnat_one_def hypnat_less starprime_def
lemma_hypnat_P_EX lemma_hypnat_P_ALL hdvd starsetNat_def Ball_def UF_if)
-apply (rule_tac x = "%n. @y. y \<in> prime & y dvd x n" in exI, auto, ultra)
+apply (rule_tac x = "%n. @y. prime y & y dvd x n" in exI, auto, ultra)
apply (drule sym, simp (no_asm_simp))
prefer 2 apply ultra
apply (rule_tac [!] someI2_ex)
@@ -372,7 +372,7 @@
apply (auto simp add: hypnat_less hypnat_add)
done
-lemma zero_not_prime: "0 \<notin> prime"
+lemma zero_not_prime: "\<not> prime 0"
apply safe
apply (drule prime_g_zero, auto)
done
@@ -389,13 +389,13 @@
done
declare hypnat_zero_not_prime [simp]
-lemma one_not_prime: "1 \<notin> prime"
+lemma one_not_prime: "\<not> prime 1"
apply safe
apply (drule prime_g_one, auto)
done
declare one_not_prime [simp]
-lemma one_not_prime2: "Suc 0 \<notin> prime"
+lemma one_not_prime2: "\<not> prime(Suc 0)"
apply safe
apply (drule prime_g_one, auto)
done
@@ -428,7 +428,7 @@
apply (auto simp add: hdvd)
done
-theorem not_finite_prime: "~ finite prime"
+theorem not_finite_prime: "~ finite {p. prime p}"
apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
apply (cut_tac hypnat_dvd_all_hypnat_of_nat)
apply (erule exE)
@@ -437,7 +437,7 @@
prefer 2 apply (blast intro: hypnat_add_one_gt_one)
apply (drule hyperprime_factor_exists)
apply (auto intro: NatStar_mem)
-apply (subgoal_tac "k \<notin> hypnat_of_nat ` prime")
+apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
apply (force simp add: starprime_def, safe)
apply (drule_tac x = x in bspec)
apply (rule ccontr, simp)
--- a/src/HOL/Complex/ex/Sqrt.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy Fri Jul 01 17:41:10 2005 +0200
@@ -74,9 +74,9 @@
irrational.
*}
-theorem sqrt_prime_irrational: "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
+theorem sqrt_prime_irrational: "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
proof
- assume p_prime: "p \<in> prime"
+ assume p_prime: "prime p"
then have p: "1 < p" by (simp add: prime_def)
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
@@ -119,9 +119,9 @@
structure, it is probably closer to proofs seen in mathematics.
*}
-theorem "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
+theorem "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
proof
- assume p_prime: "p \<in> prime"
+ assume p_prime: "prime p"
then have p: "1 < p" by (simp add: prime_def)
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy Fri Jul 01 17:41:10 2005 +0200
@@ -17,16 +17,16 @@
subsection {* Preliminaries *}
-lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p \<noteq> 0"
+lemma prime_nonzero: "prime p \<Longrightarrow> p \<noteq> 0"
by (force simp add: prime_def)
lemma prime_dvd_other_side:
- "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
+ "n * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
apply (rule_tac j = "k * k" in dvd_mult_left, simp)
done
-lemma reduction: "p \<in> prime \<Longrightarrow>
+lemma reduction: "prime p \<Longrightarrow>
0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
apply (rule ccontr)
apply (simp add: linorder_not_less)
@@ -40,7 +40,7 @@
by (simp add: mult_ac)
lemma prime_not_square:
- "p \<in> prime \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
+ "prime p \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
apply (induct m rule: nat_less_induct)
apply clarify
apply (frule prime_dvd_other_side, assumption)
@@ -65,7 +65,7 @@
*}
theorem prime_sqrt_irrational:
- "p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
+ "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
apply (simp add: rationals_def real_abs_def)
apply clarify
apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
--- a/src/HOL/Library/Primes.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/Library/Primes.thy Fri Jul 01 17:41:10 2005 +0200
@@ -29,8 +29,8 @@
coprime :: "nat => nat => bool"
"coprime m n == gcd (m, n) = 1"
- prime :: "nat set"
- "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
+ prime :: "nat \<Rightarrow> bool"
+ "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)"
lemma gcd_induct:
@@ -172,7 +172,7 @@
apply (blast intro: relprime_dvd_mult dvd_trans)
done
-lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
+lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
apply (auto simp add: prime_def)
apply (drule_tac x = "gcd (p, n)" in spec)
apply auto
@@ -180,7 +180,7 @@
apply simp
done
-lemma two_is_prime: "2 \<in> prime"
+lemma two_is_prime: "prime 2"
apply (auto simp add: prime_def)
apply (case_tac m)
apply (auto dest!: dvd_imp_le)
@@ -192,13 +192,13 @@
one of those primes.
*}
-lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
+lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
by (blast intro: relprime_dvd_mult prime_imp_relprime)
-lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m"
+lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
by (auto dest: prime_dvd_mult)
-lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
+lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
by (rule prime_dvd_square) (simp_all add: power2_eq_square)
--- a/src/HOL/NumberTheory/Euler.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Euler.thy Fri Jul 01 17:41:10 2005 +0200
@@ -19,7 +19,7 @@
(* *)
(****************************************************************)
-lemma MultInvPair_prop1a: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
+lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
X \<in> (SetS a p); Y \<in> (SetS a p);
~((X \<inter> Y) = {}) |] ==>
X = Y";
@@ -37,7 +37,7 @@
apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
done
-lemma MultInvPair_prop1b: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
+lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
X \<in> (SetS a p); Y \<in> (SetS a p);
X \<noteq> Y |] ==>
X \<inter> Y = {}";
@@ -46,11 +46,11 @@
apply (drule MultInvPair_prop1a, auto)
done
-lemma MultInvPair_prop1c: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==>
+lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
\<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
by (auto simp add: MultInvPair_prop1b)
-lemma MultInvPair_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==>
+lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
Union ( SetS a p) = SRStar p";
apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4
SRStar_mult_prop2)
@@ -58,13 +58,13 @@
apply (rule bexI, auto)
done
-lemma MultInvPair_distinct: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
+lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~([j = 0] (mod p));
~(QuadRes p a) |] ==>
~([j = a * MultInv p j] (mod p))";
apply auto
proof -;
- assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and
+ assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
"~([j = 0] (mod p))" and "~(QuadRes p a)";
assume "[j = a * MultInv p j] (mod p)";
then have "[j * j = (a * MultInv p j) * j] (mod p)";
@@ -87,7 +87,7 @@
by (simp add: QuadRes_def)
qed;
-lemma MultInvPair_card_two: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
+lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); ~([j = 0] (mod p)) |] ==>
card (MultInvPair a p j) = 2";
apply (auto simp add: MultInvPair_def)
@@ -109,7 +109,7 @@
lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X";
by (auto simp add: SetS_def MultInvPair_def)
-lemma SetS_elems_card: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
+lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a) |] ==>
\<forall>X \<in> SetS a p. card X = 2";
apply (auto simp add: SetS_def)
@@ -124,10 +124,10 @@
\<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S";
by (induct set: Finites, auto)
-lemma SetS_card: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
+lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
int(card(SetS a p)) = (p - 1) div 2";
proof -;
- assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)";
+ assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)";
then have "(p - 1) = 2 * int(card(SetS a p))";
proof -;
have "p - 1 = int(card(Union (SetS a p)))";
@@ -148,7 +148,7 @@
by auto
qed;
-lemma SetS_setprod_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
+lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); x \<in> (SetS a p) |] ==>
[\<Prod>x = a] (mod p)";
apply (auto simp add: SetS_def MultInvPair_def)
@@ -185,10 +185,10 @@
apply (frule d22set_g_1, auto)
done
-lemma Union_SetS_setprod_prop1: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
+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)"
proof -
- assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
+ assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
then have "[\<Prod>(Union (SetS a p)) =
setprod (setprod (%x. x)) (SetS a p)] (mod p)"
by (auto simp add: SetS_finite SetS_elems_finite
@@ -208,10 +208,10 @@
done
qed
-lemma Union_SetS_setprod_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==>
+lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
\<Prod>(Union (SetS a p)) = zfact (p - 1)";
proof -;
- assume "p \<in> zprime" and "2 < p" and "~([a = 0](mod p))";
+ assume "zprime p" and "2 < p" and "~([a = 0](mod p))";
then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
by (auto simp add: MultInvPair_prop2)
also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
@@ -231,7 +231,7 @@
finally show ?thesis .
qed;
-lemma zfact_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
+lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
[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)
@@ -245,7 +245,7 @@
(* *)
(****************************************************************)
-lemma Euler_part1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p));
+lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
~(QuadRes p x) |] ==>
[x^(nat (((p) - 1) div 2)) = -1](mod p)";
apply (frule zfact_prop, auto)
@@ -289,7 +289,7 @@
then show ?thesis by auto
qed;
-lemma Euler_part2: "[| 2 < p; p \<in> zprime; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)";
+lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)";
apply (frule zprime_zOdd_eq_grt_2)
apply (frule aux_2, auto)
apply (frule_tac a = a in aux_1, auto)
@@ -314,7 +314,7 @@
lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))";
by (auto simp add: nat_mult_distrib)
-lemma Euler_part3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); QuadRes p x |] ==>
+lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==>
[x^(nat (((p) - 1) div 2)) = 1](mod p)";
apply (subgoal_tac "p \<in> zOdd")
apply (auto simp add: QuadRes_def)
@@ -335,7 +335,7 @@
(* *)
(********************************************************************)
-theorem Euler_Criterion: "[| 2 < p; p \<in> zprime |] ==> [(Legendre a p) =
+theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
a^(nat (((p) - 1) div 2))] (mod p)";
apply (auto simp add: Legendre_def Euler_part2)
apply (frule Euler_part3, auto simp add: zcong_sym)
--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Fri Jul 01 17:41:10 2005 +0200
@@ -316,7 +316,7 @@
done
lemma Bnor_prime [rule_format (no_asm)]:
- "p \<in> zprime ==>
+ "zprime p ==>
a < p --> (\<forall>b. 0 < b \<and> b \<le> a --> zgcd (b, p) = 1)
--> card (BnorRset (a, p)) = nat a"
apply (auto simp add: zless_zprime_imp_zrelprime)
@@ -330,14 +330,14 @@
apply (frule Bnor_fin)
done
-lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - 1)"
+lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
apply (unfold phi_def norRRset_def)
apply (rule Bnor_prime, auto)
apply (erule zless_zprime_imp_zrelprime, simp_all)
done
theorem Little_Fermat:
- "p \<in> zprime ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
+ "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
apply (subst phi_prime [symmetric])
apply (rule_tac [2] Euler_Fermat)
apply (erule_tac [3] zprime_imp_zrelprime)
--- a/src/HOL/NumberTheory/EvenOdd.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy Fri Jul 01 17:41:10 2005 +0200
@@ -219,7 +219,7 @@
(* An odd prime is greater than 2 *)
-lemma zprime_zOdd_eq_grt_2: "p \<in> zprime ==> (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])
--- a/src/HOL/NumberTheory/Factorization.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy Fri Jul 01 17:41:10 2005 +0200
@@ -19,7 +19,7 @@
sort :: "nat list => nat list"
defs
- primel_def: "primel xs == set xs \<subseteq> prime"
+ primel_def: "primel xs == \<forall>p \<in> set xs. prime p"
primrec
"nondec [] = True"
@@ -83,12 +83,12 @@
apply auto
done
-lemma prime_primel: "n \<in> prime ==> primel [n] \<and> prod [n] = n"
+lemma prime_primel: "prime n ==> primel [n] \<and> prod [n] = n"
apply (unfold primel_def)
apply auto
done
-lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd Suc 0"
+lemma prime_nd_one: "prime p ==> \<not> p dvd Suc 0"
apply (unfold prime_def dvd_def)
apply auto
done
@@ -105,12 +105,12 @@
apply auto
done
-lemma primel_hd_tl: "(primel (x # xs)) = (x \<in> prime \<and> primel xs)"
+lemma primel_hd_tl: "(primel (x # xs)) = (prime x \<and> primel xs)"
apply (unfold primel_def)
apply auto
done
-lemma primes_eq: "p \<in> prime ==> q \<in> prime ==> p dvd q ==> p = q"
+lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"
apply (unfold prime_def)
apply auto
done
@@ -121,12 +121,12 @@
apply simp_all
done
-lemma prime_g_one: "p \<in> prime ==> Suc 0 < p"
+lemma prime_g_one: "prime p ==> Suc 0 < p"
apply (unfold prime_def)
apply auto
done
-lemma prime_g_zero: "p \<in> prime ==> 0 < p"
+lemma prime_g_zero: "prime p ==> 0 < p"
apply (unfold prime_def)
apply auto
done
@@ -186,7 +186,11 @@
lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
apply (unfold primel_def)
apply (erule perm.induct)
- apply simp_all
+ apply simp
+ apply simp
+ apply (simp (no_asm))
+ apply blast
+ apply blast
done
lemma perm_prod [rule_format]: "xs <~~> ys ==> prod xs = prod ys"
@@ -223,7 +227,7 @@
done
lemma not_prime_ex_mk:
- "Suc 0 < n \<and> n \<notin> prime ==>
+ "Suc 0 < n \<and> \<not> prime n ==>
\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
apply (unfold prime_def dvd_def)
apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
@@ -240,7 +244,7 @@
lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
apply (induct n rule: nat_less_induct)
apply (rule impI)
- apply (case_tac "n \<in> prime")
+ apply (case_tac "prime n")
apply (rule exI)
apply (erule prime_primel)
apply (cut_tac n = n in not_prime_ex_mk)
@@ -256,7 +260,7 @@
subsection {* Uniqueness *}
lemma prime_dvd_mult_list [rule_format]:
- "p \<in> prime ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
+ "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
apply (induct xs)
apply (force simp add: prime_def)
apply (force dest: prime_dvd_mult)
@@ -300,7 +304,7 @@
done
lemma prod_one_empty:
- "primel xs ==> p * prod xs = p ==> p \<in> prime ==> xs = []"
+ "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
apply (auto intro: primel_one_empty simp add: prime_def)
done
--- a/src/HOL/NumberTheory/Gauss.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Fri Jul 01 17:41:10 2005 +0200
@@ -17,7 +17,7 @@
fixes E :: "int set"
fixes F :: "int set"
- assumes p_prime: "p \<in> zprime"
+ assumes p_prime: "zprime p"
assumes p_g_2: "2 < p"
assumes p_a_relprime: "~[a = 0](mod p)"
assumes a_nonzero: "0 < a"
--- a/src/HOL/NumberTheory/Int2.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Int2.thy Fri Jul 01 17:41:10 2005 +0200
@@ -37,13 +37,13 @@
lemma aux4: " -(m * n) = (-m) * (n::int)";
by auto
-lemma zprime_zdvd_zmult_better: "[| p \<in> zprime; p dvd (m * n) |] ==>
+lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==>
(p dvd m) | (p dvd n)";
apply (case_tac "0 \<le> m")
apply (simp add: zprime_zdvd_zmult)
by (insert zprime_zdvd_zmult [of "-m" p n], auto)
-lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n)
+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)
@@ -124,7 +124,7 @@
([c = d * a](mod m) = [c = d * b] (mod m))";
by (auto simp add: zmult_ac zcong_zmult_prop1)
-lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p);
+lemma zcong_zmult_prop3: "[| zprime p; ~[x = 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)
@@ -160,11 +160,11 @@
lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
by (auto simp add: zcong_def)
-lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==>
+lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==>
[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: "[| p \<in> zprime; 0 < a |] ==>
+lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
~[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)
@@ -191,10 +191,10 @@
[(MultInv p x) = (MultInv p y)] (mod p)";
by (auto simp add: MultInv_def zcong_zpower)
-lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==>
+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 "p \<in> zprime" and "~ p dvd x";
+ 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)";
@@ -207,7 +207,7 @@
finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
qed;
-lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==>
+lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
[(MultInv p x) * x = 1] (mod p)";
by (auto simp add: MultInv_prop2 zmult_ac)
@@ -217,14 +217,14 @@
lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
by auto
-lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==>
+lemma MultInv_prop3: "[| 2 < p; zprime 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
-lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
+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)";
apply (drule MultInv_prop2, auto)
@@ -232,7 +232,7 @@
apply (auto simp add: zcong_sym)
done
-lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
+lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](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)
@@ -241,14 +241,14 @@
apply (auto simp add: zmult_ac)
done
-lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==>
+lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](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
-lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p));
+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)";
apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
@@ -271,7 +271,7 @@
[j * k = a * MultInv p k * k] (mod p)";
by (auto simp add: zcong_scalar)
-lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p));
+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)";
apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
[of "MultInv p k * k" 1 p "j * k" a])
@@ -282,7 +282,7 @@
(MultInv p j) * a] (mod p)";
by (auto simp add: zmult_assoc zcong_scalar2)
-lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p));
+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)";
apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
@@ -290,14 +290,14 @@
apply (auto simp add: zmult_ac zcong_sym)
done
-lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p));
+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)";
apply (drule aux___1)
apply (frule aux___2, auto)
by (drule aux___3, drule aux___4, auto)
-lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p));
+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)";
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Jul 01 17:41:10 2005 +0200
@@ -40,8 +40,8 @@
zgcd :: "int * int => int"
"zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
- zprime :: "int set"
- "zprime == {p. 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)}"
+ zprime :: "int \<Rightarrow> bool"
+ "zprime p == 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)"
xzgcd :: "int => int => int * int * int"
"xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
@@ -159,14 +159,14 @@
text{*This is merely a sanity check on zprime, since the previous version
denoted the empty set.*}
-lemma "2 \<in> zprime"
+lemma "zprime 2"
apply (auto simp add: zprime_def)
apply (frule zdvd_imp_le, simp)
apply (auto simp add: order_le_less dvd_def)
done
lemma zprime_imp_zrelprime:
- "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = 1"
+ "zprime p ==> \<not> p dvd n ==> zgcd (n, p) = 1"
apply (auto simp add: zprime_def)
apply (drule_tac x = "zgcd(n, p)" in allE)
apply (auto simp add: zgcd_zdvd2 [of n p] zgcd_geq_zero)
@@ -174,13 +174,13 @@
done
lemma zless_zprime_imp_zrelprime:
- "p \<in> zprime ==> 0 < n ==> n < p ==> zgcd (n, p) = 1"
+ "zprime p ==> 0 < n ==> n < p ==> zgcd (n, p) = 1"
apply (erule zprime_imp_zrelprime)
apply (erule zdvd_not_zless, assumption)
done
lemma zprime_zdvd_zmult:
- "0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
+ "0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
apply safe
apply (rule zrelprime_zdvd_zmult)
apply (rule zprime_imp_zrelprime, auto)
@@ -282,7 +282,7 @@
done
lemma zcong_square:
- "[|p \<in> zprime; 0 < a; [a * a = 1] (mod p)|]
+ "[| zprime p; 0 < a; [a * a = 1] (mod p)|]
==> [a = 1] (mod p) \<or> [a = p - 1] (mod p)"
apply (unfold zcong_def)
apply (rule zprime_zdvd_zmult)
@@ -346,7 +346,7 @@
done
lemma zcong_square_zless:
- "p \<in> zprime ==> 0 < a ==> a < p ==>
+ "zprime p ==> 0 < a ==> a < p ==>
[a * a = 1] (mod p) ==> a = 1 \<or> a = p - 1"
apply (cut_tac p = p and a = a in zcong_square)
apply (simp add: zprime_def)
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Fri Jul 01 17:41:10 2005 +0200
@@ -144,7 +144,7 @@
finally show ?thesis .
qed
-lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 2 < p;
+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} |] ==>
(Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
apply (subst GAUSS.gauss_lemma)
@@ -169,9 +169,9 @@
fixes f1 :: "int => (int * int) set"
fixes f2 :: "int => (int * int) set"
- assumes p_prime: "p \<in> zprime"
+ assumes p_prime: "zprime p"
assumes p_g_2: "2 < p"
- assumes q_prime: "q \<in> zprime"
+ assumes q_prime: "zprime q"
assumes q_g_2: "2 < q"
assumes p_neq_q: "p \<noteq> q"
@@ -367,10 +367,10 @@
ultimately show ?thesis ..
qed
-lemma aux2: "[| p \<in> zprime; q \<in> zprime; 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 "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q"
+ assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
(* Set up what's even and odd *)
then have "p \<in> zOdd & q \<in> zOdd"
by (auto simp add: zprime_zOdd_eq_grt_2)
@@ -570,7 +570,7 @@
finally show ?thesis .
qed
-lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))"
+lemma pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
apply (drule_tac x = q in allE)
apply (drule_tac x = p in allE)
@@ -613,7 +613,7 @@
qed
theorem Quadratic_Reciprocity:
- "[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime;
+ "[| 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))"
--- a/src/HOL/NumberTheory/Residues.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Residues.thy Fri Jul 01 17:41:10 2005 +0200
@@ -96,7 +96,7 @@
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; p \<in> zprime; x \<in> SRStar p |]
+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);
apply (rule MultInv_prop3)
@@ -106,18 +106,18 @@
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: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |]
+lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \<in> SRStar p |]
==> StandardRes p x \<in> SRStar p";
by (frule StandardRes_SRStar_prop3, auto)
-lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|]
+lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \<in> SRStar p; y \<in> 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
-lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
+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";
apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
--- a/src/HOL/NumberTheory/WilsonBij.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy Fri Jul 01 17:41:10 2005 +0200
@@ -23,7 +23,7 @@
\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1"
inv :: "int => int => int"
"inv p a ==
- if p \<in> zprime \<and> 0 < a \<and> a < p then
+ if zprime p \<and> 0 < a \<and> a < p then
(SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
else 0"
@@ -31,7 +31,7 @@
text {* \medskip Inverse *}
lemma inv_correct:
- "p \<in> zprime ==> 0 < a ==> a < p
+ "zprime p ==> 0 < a ==> a < p
==> 0 \<le> inv p a \<and> inv p a < p \<and> [a * inv p a = 1] (mod p)"
apply (unfold inv_def)
apply (simp (no_asm_simp))
@@ -46,7 +46,7 @@
lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard]
lemma inv_not_0:
- "p \<in> zprime ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
+ "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
-- {* same as @{text WilsonRuss} *}
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
@@ -61,7 +61,7 @@
done
lemma inv_not_1:
- "p \<in> zprime ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1"
+ "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1"
-- {* same as @{text WilsonRuss} *}
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
@@ -86,7 +86,7 @@
done
lemma inv_not_p_minus_1:
- "p \<in> zprime ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1"
+ "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1"
-- {* same as @{text WilsonRuss} *}
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
@@ -102,7 +102,7 @@
but use ``@{text correct}'' theorems.
*}
-lemma inv_g_1: "p \<in> zprime ==> 1 < a ==> a < p - 1 ==> 1 < inv p a"
+lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a"
apply (subgoal_tac "inv p a \<noteq> 1")
apply (subgoal_tac "inv p a \<noteq> 0")
apply (subst order_less_le)
@@ -116,7 +116,7 @@
done
lemma inv_less_p_minus_1:
- "p \<in> zprime ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1"
+ "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1"
-- {* ditto *}
apply (subst order_less_le)
apply (simp add: inv_not_p_minus_1 inv_less)
@@ -141,7 +141,7 @@
apply auto
done
-lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - 2))"
+lemma inv_inj: "zprime p ==> inj_on (inv p) (d22set (p - 2))"
apply (unfold inj_on_def)
apply auto
apply (rule zcong_zless_imp_eq)
@@ -160,7 +160,7 @@
done
lemma inv_d22set_d22set:
- "p \<in> zprime ==> inv p ` d22set (p - 2) = d22set (p - 2)"
+ "zprime p ==> inv p ` d22set (p - 2) = d22set (p - 2)"
apply (rule endo_inj_surj)
apply (rule d22set_fin)
apply (erule_tac [2] inv_inj)
@@ -173,7 +173,7 @@
done
lemma d22set_d22set_bij:
- "p \<in> zprime ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
+ "zprime p ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
apply (unfold reciR_def)
apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst)
apply (simp add: inv_d22set_d22set)
@@ -187,14 +187,14 @@
apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4)
done
-lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - 2))"
+lemma reciP_bijP: "zprime p ==> bijP (reciR p) (d22set (p - 2))"
apply (unfold reciR_def bijP_def)
apply auto
apply (rule d22set_mem)
apply auto
done
-lemma reciP_uniq: "p \<in> zprime ==> uniqP (reciR p)"
+lemma reciP_uniq: "zprime p ==> uniqP (reciR p)"
apply (unfold reciR_def uniqP_def)
apply auto
apply (rule zcong_zless_imp_eq)
@@ -211,13 +211,13 @@
apply auto
done
-lemma reciP_sym: "p \<in> zprime ==> symP (reciR p)"
+lemma reciP_sym: "zprime p ==> symP (reciR p)"
apply (unfold reciR_def symP_def)
apply (simp add: zmult_commute)
apply auto
done
-lemma bijER_d22set: "p \<in> zprime ==> d22set (p - 2) \<in> bijER (reciR p)"
+lemma bijER_d22set: "zprime p ==> d22set (p - 2) \<in> bijER (reciR p)"
apply (rule bijR_bijER)
apply (erule d22set_d22set_bij)
apply (erule reciP_bijP)
@@ -229,7 +229,7 @@
subsection {* Wilson *}
lemma bijER_zcong_prod_1:
- "p \<in> zprime ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
+ "zprime p ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
apply (unfold reciR_def)
apply (erule bijER.induct)
apply (subgoal_tac [2] "a = 1 \<or> a = p - 1")
@@ -245,7 +245,7 @@
apply auto
done
-theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - 1) = -1] (mod p)"
+theorem Wilson_Bij: "zprime p ==> [zfact (p - 1) = -1] (mod p)"
apply (subgoal_tac "zcong ((p - 1) * zfact (p - 2)) (-1 * 1) p")
apply (rule_tac [2] zcong_zmult)
apply (simp add: zprime_def)
--- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Fri Jul 01 17:41:10 2005 +0200
@@ -39,7 +39,7 @@
by (subst int_int_eq [symmetric], auto)
lemma inv_is_inv:
- "p \<in> zprime \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
+ "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
apply (unfold inv_def)
apply (subst zcong_zmod)
apply (subst zmod_zmult1_eq [symmetric])
@@ -52,7 +52,7 @@
done
lemma inv_distinct:
- "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a"
+ "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a"
apply safe
apply (cut_tac a = a and p = p in zcong_square)
apply (cut_tac [3] a = a and p = p in inv_is_inv, auto)
@@ -63,7 +63,7 @@
done
lemma inv_not_0:
- "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0"
+ "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0"
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
apply (unfold zcong_def, auto)
@@ -75,7 +75,7 @@
done
lemma inv_not_1:
- "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1"
+ "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1"
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
prefer 4
@@ -96,7 +96,7 @@
done
lemma inv_not_p_minus_1:
- "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1"
+ "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1"
apply safe
apply (cut_tac a = a and p = p in inv_is_inv, auto)
apply (simp add: inv_not_p_minus_1_aux)
@@ -105,7 +105,7 @@
done
lemma inv_g_1:
- "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a"
+ "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a"
apply (case_tac "0\<le> inv p a")
apply (subgoal_tac "inv p a \<noteq> 1")
apply (subgoal_tac "inv p a \<noteq> 0")
@@ -118,7 +118,7 @@
done
lemma inv_less_p_minus_1:
- "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1"
+ "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1"
apply (case_tac "inv p a < p")
apply (subst order_less_le)
apply (simp add: inv_not_p_minus_1, auto)
@@ -140,7 +140,7 @@
apply (rule_tac [2] zcong_zmult, simp_all)
done
-lemma inv_inv: "p \<in> zprime \<Longrightarrow>
+lemma inv_inv: "zprime p \<Longrightarrow>
5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
apply (unfold inv_def)
apply (subst zpower_zmod)
@@ -197,7 +197,7 @@
done
lemma wset_g_1 [rule_format]:
- "p \<in> zprime --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
+ "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
apply (induct a p rule: wset_induct, auto)
apply (case_tac "b = a")
apply (case_tac [2] "b = inv p a")
@@ -209,7 +209,7 @@
done
lemma wset_less [rule_format]:
- "p \<in> zprime --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
+ "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
apply (induct a p rule: wset_induct, auto)
apply (case_tac "b = a")
apply (case_tac [2] "b = inv p a")
@@ -221,7 +221,7 @@
done
lemma wset_mem [rule_format]:
- "p \<in> zprime -->
+ "zprime p -->
a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
apply (induct a p rule: wset.induct, auto)
apply (rule_tac wset_subset)
@@ -230,7 +230,7 @@
done
lemma wset_mem_inv_mem [rule_format]:
- "p \<in> zprime --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
+ "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
--> inv p b \<in> wset (a, p)"
apply (induct a p rule: wset_induct, auto)
apply (case_tac "b = a")
@@ -245,7 +245,7 @@
done
lemma wset_inv_mem_mem:
- "p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
+ "zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
\<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
apply (rule_tac [2] wset_mem_inv_mem)
@@ -260,7 +260,7 @@
done
lemma wset_zcong_prod_1 [rule_format]:
- "p \<in> zprime -->
+ "zprime p -->
5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
apply (induct a p rule: wset_induct)
prefer 2
@@ -281,7 +281,7 @@
apply (rule inv_distinct, auto)
done
-lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
+lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)"
apply safe
apply (erule wset_mem)
apply (rule_tac [2] d22set_g_1)
@@ -298,7 +298,7 @@
subsection {* Wilson *}
-lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
+lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
apply (unfold zprime_def dvd_def)
apply (case_tac "p = 4", auto)
apply (rule notE)
@@ -311,7 +311,7 @@
done
theorem Wilson_Russ:
- "p \<in> zprime ==> [zfact (p - 1) = -1] (mod p)"
+ "zprime p ==> [zfact (p - 1) = -1] (mod p)"
apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)")
apply (rule_tac [2] zcong_zmult)
apply (simp only: zprime_def)