# HG changeset patch # User nipkow # Date 1120232470 -7200 # Node ID 13e9c402308ba85aaf7fc5d6ce8e67bf386c884c # Parent 0836569a8ffcc50a5b59a3598b96de5a8a88ee5f prime is a predicate now. diff -r 0836569a8ffc -r 13e9c402308b src/HOL/Algebra/Exponent.thy --- 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 \ 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 \ prime ==> Suc 0 < p" +lemma prime_imp_one_less: "prime p ==> Suc 0 < p" by (unfold prime_def, force) lemma prime_iff: - "(p \ prime) = (Suc 0 (p dvd a) | (p dvd b)))" + "(prime p) = (Suc 0 (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 \ 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 \ prime |] + "[| p*k dvd m*n; prime p |] ==> (\x. k dvd x*n & m = p*x) | (\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 \ prime +lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p ==> \m n. p^c dvd m*n --> (\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 \ 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 \ prime; 0 k <= exponent p n" + "[|p^k dvd n; prime p; 0 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 \ 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 \ 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 \ prime ==> exponent p s = 0" +lemma exponent_eq_0 [simp]: "\ 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 (exponent p a) + (exponent p b) <= exponent p (a * b)" -apply (case_tac "p \ 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 exponent p (a * b) <= (exponent p a) + (exponent p b)" -apply (case_tac "p \ 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 \ 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]: "[| \i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] ==> k exponent p ((j+k) choose k) = 0" -apply (case_tac "p \ 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 \ 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 \ 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) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/Algebra/Sylow.thy --- 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 \ 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 \ carrier(G) & card(s) = p^a}" @@ -363,7 +363,7 @@ by (simp add: sylow_def group_def) theorem sylow_thm: - "[|p \ prime; group(G); order(G) = (p^a) * m; finite (carrier G)|] + "[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|] ==> \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) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/Complex/ex/NSPrimes.thy --- 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 --> (\k \ prime. k dvd n)" +lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\k. prime k & k dvd n)" apply (rule_tac n = n in nat_less_induct, auto) -apply (case_tac "n \ 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 \ 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 \ prime" +lemma zero_not_prime: "\ 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 \ prime" +lemma one_not_prime: "\ prime 1" apply safe apply (drule prime_g_one, auto) done declare one_not_prime [simp] -lemma one_not_prime2: "Suc 0 \ prime" +lemma one_not_prime2: "\ 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 \ hypnat_of_nat ` prime") +apply (subgoal_tac "k \ hypnat_of_nat ` {p. prime p}") apply (force simp add: starprime_def, safe) apply (drule_tac x = x in bspec) apply (rule ccontr, simp) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/Complex/ex/Sqrt.thy --- 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 \ prime \ sqrt (real p) \ \" +theorem sqrt_prime_irrational: "prime p \ sqrt (real p) \ \" proof - assume p_prime: "p \ prime" + assume p_prime: "prime p" then have p: "1 < p" by (simp add: prime_def) assume "sqrt (real p) \ \" then obtain m n where @@ -119,9 +119,9 @@ structure, it is probably closer to proofs seen in mathematics. *} -theorem "p \ prime \ sqrt (real p) \ \" +theorem "prime p \ sqrt (real p) \ \" proof - assume p_prime: "p \ prime" + assume p_prime: "prime p" then have p: "1 < p" by (simp add: prime_def) assume "sqrt (real p) \ \" then obtain m n where diff -r 0836569a8ffc -r 13e9c402308b src/HOL/Complex/ex/Sqrt_Script.thy --- 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 \ prime \ p \ 0" +lemma prime_nonzero: "prime p \ p \ 0" by (force simp add: prime_def) lemma prime_dvd_other_side: - "n * n = p * (k * k) \ p \ prime \ p dvd n" + "n * n = p * (k * k) \ prime p \ 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 \ prime \ +lemma reduction: "prime p \ 0 < k \ k * k = p * (j * j) \ k < p * j \ 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 \ prime \ (\k. 0 < k \ m * m \ p * (k * k))" + "prime p \ (\k. 0 < k \ m * m \ 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 \ prime \ x * x = real p \ 0 \ x \ x \ \" + "prime p \ x * x = real p \ 0 \ x \ x \ \" apply (simp add: rationals_def real_abs_def) apply clarify apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/Library/Primes.thy --- 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 m = 1 \ m = p)}" + prime :: "nat \ bool" + "prime p == 1 m = 1 \ m = p)" lemma gcd_induct: @@ -172,7 +172,7 @@ apply (blast intro: relprime_dvd_mult dvd_trans) done -lemma prime_imp_relprime: "p \ prime ==> \ p dvd n ==> gcd (p, n) = 1" +lemma prime_imp_relprime: "prime p ==> \ 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 \ 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 \ prime ==> p dvd m * n ==> p dvd m \ p dvd n" +lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \ p dvd n" by (blast intro: relprime_dvd_mult prime_imp_relprime) -lemma prime_dvd_square: "p \ 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 \ prime ==> p dvd m\ ==> p dvd m" +lemma prime_dvd_power_two: "prime p ==> p dvd m\ ==> p dvd m" by (rule prime_dvd_square) (simp_all add: power2_eq_square) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/Euler.thy --- 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 \ zprime; 2 < p; ~([a = 0](mod p)); +lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p)); X \ (SetS a p); Y \ (SetS a p); ~((X \ Y) = {}) |] ==> X = Y"; @@ -37,7 +37,7 @@ apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym) done -lemma MultInvPair_prop1b: "[| p \ zprime; 2 < p; ~([a = 0](mod p)); +lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p)); X \ (SetS a p); Y \ (SetS a p); X \ Y |] ==> X \ Y = {}"; @@ -46,11 +46,11 @@ apply (drule MultInvPair_prop1a, auto) done -lemma MultInvPair_prop1c: "[| p \ zprime; 2 < p; ~([a = 0](mod p)) |] ==> +lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> \X \ SetS a p. \Y \ SetS a p. X \ Y --> X\Y = {}" by (auto simp add: MultInvPair_prop1b) -lemma MultInvPair_prop2: "[| p \ 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 \ 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 \ 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 \ 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: "\X \ SetS a p. finite X"; by (auto simp add: SetS_def MultInvPair_def) -lemma SetS_elems_card: "[| p \ zprime; 2 < p; ~([a = 0] (mod p)); +lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> \X \ SetS a p. card X = 2"; apply (auto simp add: SetS_def) @@ -124,10 +124,10 @@ \X \ S. card X = n |] ==> setsum card S = setsum (%x. n) S"; by (induct set: Finites, auto) -lemma SetS_card: "[| p \ 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 \ 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 \ zprime; 2 < p; ~([a = 0] (mod p)); +lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a); x \ (SetS a p) |] ==> [\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 \ 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) |] ==> [\(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)" proof - - assume "p \ 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 "[\(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 \ zprime; 2 < p; ~([a = 0](mod p)) |] ==> +lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> \(Union (SetS a p)) = zfact (p - 1)"; proof -; - assume "p \ zprime" and "2 < p" and "~([a = 0](mod p))"; + assume "zprime p" and "2 < p" and "~([a = 0](mod p))"; then have "\(Union (SetS a p)) = \(SRStar p)" by (auto simp add: MultInvPair_prop2) also have "... = \({1} \ (d22set (p - 1)))" @@ -231,7 +231,7 @@ finally show ?thesis . qed; -lemma zfact_prop: "[| p \ 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 \ 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 \ 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 \ 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 \ zOdd") apply (auto simp add: QuadRes_def) @@ -335,7 +335,7 @@ (* *) (********************************************************************) -theorem Euler_Criterion: "[| 2 < p; p \ 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) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/EulerFermat.thy --- 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 \ zprime ==> + "zprime p ==> a (\b. 0 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 \ 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 \ zprime ==> \ p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)" + "zprime p ==> \ 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) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/EvenOdd.thy --- 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 \ zprime ==> (p \ zOdd) = (2 < p)"; +lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \ 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]) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/Factorization.thy --- 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 \ prime" + primel_def: "primel xs == \p \ set xs. prime p" primrec "nondec [] = True" @@ -83,12 +83,12 @@ apply auto done -lemma prime_primel: "n \ prime ==> primel [n] \ prod [n] = n" +lemma prime_primel: "prime n ==> primel [n] \ prod [n] = n" apply (unfold primel_def) apply auto done -lemma prime_nd_one: "p \ prime ==> \ p dvd Suc 0" +lemma prime_nd_one: "prime p ==> \ 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 \ prime \ primel xs)" +lemma primel_hd_tl: "(primel (x # xs)) = (prime x \ primel xs)" apply (unfold primel_def) apply auto done -lemma primes_eq: "p \ prime ==> q \ 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 \ 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 \ 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 \ n \ prime ==> + "Suc 0 < n \ \ prime n ==> \m k. Suc 0 < m \ Suc 0 < k \ m < n \ k < n \ 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 --> (\l. primel l \ prod l = n)" apply (induct n rule: nat_less_induct) apply (rule impI) - apply (case_tac "n \ 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 \ prime ==> p dvd (prod xs) --> (\m. m:set xs \ p dvd m)" + "prime p ==> p dvd (prod xs) --> (\m. m:set xs \ 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 \ prime ==> xs = []" + "primel xs ==> p * prod xs = p ==> prime p ==> xs = []" apply (auto intro: primel_one_empty simp add: prime_def) done diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/Gauss.thy --- 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 \ 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" diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/Int2.thy --- 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 \ 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 \ m") apply (simp add: zprime_zdvd_zmult) by (insert zprime_zdvd_zmult [of "-m" p n], auto) -lemma zpower_zdvd_prop2 [rule_format]: "p \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 0 < nat (p - 2)"; by auto -lemma MultInv_prop3: "[| 2 < p; p \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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)"; diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/IntPrimes.thy --- 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 == \(x,y). int (gcd (nat (abs x), nat (abs y)))" - zprime :: "int set" - "zprime == {p. 1 m = 1 \ m = p)}" + zprime :: "int \ bool" + "zprime p == 1 m = 1 \ 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 \ 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 \ zprime ==> \ p dvd n ==> zgcd (n, p) = 1" + "zprime p ==> \ 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 \ zprime ==> 0 < n ==> n zgcd (n, p) = 1" + "zprime p ==> 0 < n ==> n zgcd (n, p) = 1" apply (erule zprime_imp_zrelprime) apply (erule zdvd_not_zless, assumption) done lemma zprime_zdvd_zmult: - "0 \ (m::int) ==> p \ zprime ==> p dvd m * n ==> p dvd m \ p dvd n" + "0 \ (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \ 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 \ zprime; 0 < a; [a * a = 1] (mod p)|] + "[| zprime p; 0 < a; [a * a = 1] (mod p)|] ==> [a = 1] (mod p) \ [a = p - 1] (mod p)" apply (unfold zcong_def) apply (rule zprime_zdvd_zmult) @@ -346,7 +346,7 @@ done lemma zcong_square_zless: - "p \ zprime ==> 0 < a ==> a + "zprime p ==> 0 < a ==> a [a * a = 1] (mod p) ==> a = 1 \ a = p - 1" apply (cut_tac p = p and a = a in zcong_square) apply (simp add: zprime_def) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/Quadratic_Reciprocity.thy --- 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 \ zOdd; 0 < a; ~([a = 0] (mod p));p \ zprime; 2 < p; +lemma MainQRLemma: "[| a \ zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p; A = {x. 0 < x & x \ (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 \ zprime" + assumes p_prime: "zprime p" assumes p_g_2: "2 < p" - assumes q_prime: "q \ zprime" + assumes q_prime: "zprime q" assumes q_g_2: "2 < q" assumes p_neq_q: "p \ q" @@ -367,10 +367,10 @@ ultimately show ?thesis .. qed -lemma aux2: "[| p \ zprime; q \ zprime; 2 < p; 2 < q |] ==> +lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==> (q * ((p - 1) div 2)) div p \ (q - 1) div 2" proof- - assume "p \ zprime" and "q \ 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 \ zOdd & q \ zOdd" by (auto simp add: zprime_zOdd_eq_grt_2) @@ -570,7 +570,7 @@ finally show ?thesis . qed -lemma pq_prime_neq: "[| p \ zprime; q \ zprime; p \ q |] ==> (~[p = 0] (mod q))" +lemma pq_prime_neq: "[| zprime p; zprime q; p \ 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 \ zOdd; p \ zprime; q \ zOdd; q \ zprime; + "[| p \ zOdd; zprime p; q \ zOdd; zprime q; p \ q |] ==> (Legendre p q) * (Legendre q p) = (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))" diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/Residues.thy --- 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 \ SRStar p ==> ~([x = 0] (mod p))"; by (auto simp add: SRStar_def zcong_def zdvd_not_zless) -lemma StandardRes_SRStar_prop2: "[| 2 < p; p \ zprime; x \ SRStar p |] +lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \ SRStar p |] ==> StandardRes p (MultInv p x) \ 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 \ SRStar p ==> StandardRes p x = x"; by (auto simp add: SRStar_SR_prop StandardRes_SR_prop) -lemma StandardRes_SRStar_prop4: "[| p \ zprime; 2 < p; x \ SRStar p |] +lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \ SRStar p |] ==> StandardRes p x \ SRStar p"; by (frule StandardRes_SRStar_prop3, auto) -lemma SRStar_mult_prop1: "[| p \ zprime; 2 < p; x \ SRStar p; y \ SRStar p|] +lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \ SRStar p; 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 -lemma SRStar_mult_prop2: "[| p \ zprime; 2 < p; ~([a = 0](mod p)); +lemma SRStar_mult_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)); x \ SRStar p |] ==> StandardRes p (a * MultInv p x) \ SRStar p"; apply (frule_tac x = x in StandardRes_SRStar_prop2, auto) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/WilsonBij.thy --- 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 @@ \a b. zcong (a * b) 1 p \ 1 < a \ a int => int" "inv p a == - if p \ zprime \ 0 < a \ a 0 < a ==> a 0 < a ==> a 0 \ inv p a \ inv p a < p \ [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 \ zprime ==> 1 < a ==> a inv p a \ 0" + "zprime p ==> 1 < a ==> a inv p a \ 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 \ zprime ==> 1 < a ==> a inv p a \ 1" + "zprime p ==> 1 < a ==> a inv p a \ 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 \ zprime ==> 1 < a ==> a inv p a \ p - 1" + "zprime p ==> 1 < a ==> a inv p a \ 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 \ zprime ==> 1 < a ==> a 1 < inv p a" +lemma inv_g_1: "zprime p ==> 1 < a ==> a 1 < inv p a" apply (subgoal_tac "inv p a \ 1") apply (subgoal_tac "inv p a \ 0") apply (subst order_less_le) @@ -116,7 +116,7 @@ done lemma inv_less_p_minus_1: - "p \ zprime ==> 1 < a ==> a inv p a 1 < a ==> a inv p a 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 \ 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 \ zprime ==> (d22set (p - 2), d22set (p - 2)) \ bijR (reciR p)" + "zprime p ==> (d22set (p - 2), d22set (p - 2)) \ 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 \ 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 \ 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 \ 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 \ zprime ==> d22set (p - 2) \ bijER (reciR p)" +lemma bijER_d22set: "zprime p ==> d22set (p - 2) \ 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 \ zprime ==> A \ bijER (reciR p) ==> [\A = 1] (mod p)" + "zprime p ==> A \ bijER (reciR p) ==> [\A = 1] (mod p)" apply (unfold reciR_def) apply (erule bijER.induct) apply (subgoal_tac [2] "a = 1 \ a = p - 1") @@ -245,7 +245,7 @@ apply auto done -theorem Wilson_Bij: "p \ 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) diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/WilsonRuss.thy --- 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 \ zprime \ 0 < a \ a [a * inv p a = 1] (mod p)" + "zprime p \ 0 < a \ a [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 \ zprime \ 1 < a \ a a \ inv p a" + "zprime p \ 1 < a \ a a \ 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 \ zprime \ 1 < a \ a inv p a \ 0" + "zprime p \ 1 < a \ a inv p a \ 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 \ zprime \ 1 < a \ a inv p a \ 1" + "zprime p \ 1 < a \ a inv p a \ 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 \ zprime \ 1 < a \ a inv p a \ p - 1" + "zprime p \ 1 < a \ a inv p a \ 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 \ zprime \ 1 < a \ a 1 < inv p a" + "zprime p \ 1 < a \ a 1 < inv p a" apply (case_tac "0\ inv p a") apply (subgoal_tac "inv p a \ 1") apply (subgoal_tac "inv p a \ 0") @@ -118,7 +118,7 @@ done lemma inv_less_p_minus_1: - "p \ zprime \ 1 < a \ a inv p a 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 \ zprime \ +lemma inv_inv: "zprime p \ 5 \ p \ 0 < a \ a 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 \ zprime --> a b \