# HG changeset patch # User wenzelm # Date 1134042604 -3600 # Node ID 694ea14ab4f25a6f81da1cade4683be038789d59 # Parent 2f9b2539c5bbf87ef6bb52b90dae81ad2b52a9db tuned sources and proofs diff -r 2f9b2539c5bb -r 694ea14ab4f2 src/HOL/NumberTheory/BijectionRel.thy --- 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 \ A ==> P {} ==> - (!!F a. F \ A ==> a \ A ==> a \ F ==> P F ==> P (insert a F)) - ==> P F" -proof - - case rule_context - assume major: "finite F" + assumes major: "finite F" and subs: "F \ 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 \ A ==> a \ A ==> a \ 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 \ B ==> a \ A ==> a \ B ==> inj_on f B ==> f a \ f ` A" diff -r 2f9b2539c5bb -r 694ea14ab4f2 src/HOL/NumberTheory/Euler.thy --- 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; \X \ S. finite (X::int set); \X \ 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 \ b | b \ a)" by auto -lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \ - (d22set (p - 1))" - apply (induct p rule: d22set.induct, auto) +lemma SRStar_d22set_prop: "2 < p \ (SRStar p) = {1} \ (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) |] ==> [\(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 \ d22set (p - 1)) & finite( d22set (p - 1))" + have "~(1 \ 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 "\({1} \ (d22set (p - 1))) = \(d22set (p - 1))" - by auto - then show ?thesis - by (auto simp add: d22set_prod_zfact) + done + then have "\({1} \ (d22set (p - 1))) = \(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 diff -r 2f9b2539c5bb -r 694ea14ab4f2 src/HOL/NumberTheory/EulerFermat.thy --- 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 \ 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 \ BnorRset (a, m) --> b \ a" +lemma Bnor_mem_zle [rule_format]: "b \ BnorRset (a, m) \ b \ 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 \ BnorRset (a, m)" -by (auto dest: Bnor_mem_zle) + by (auto dest: Bnor_mem_zle) lemma Bnor_mem_zg [rule_format]: "b \ 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 \ RsetR m ==> finite A" -by (erule RsetR.induct, auto) + by (induct set: RsetR) auto lemma RRset_zcong_eq [rule_format]: "1 < m ==> diff -r 2f9b2539c5bb -r 694ea14ab4f2 src/HOL/NumberTheory/EvenOdd.thy --- 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. \k. x = 2*k + 1}" + "zOdd == {x. \k. x = 2 * k + 1}" zEven :: "int set" "zEven == {x. \k. x = 2 * k}" @@ -22,223 +22,239 @@ (* *) (***********************************************************) -lemma one_not_even: "~(1 \ zEven)"; - apply (simp add: zEven_def) - apply (rule allI, case_tac "k \ 0", auto) -done +lemma zOddI [intro?]: "x = 2 * k + 1 \ x \ zOdd" + and zOddE [elim?]: "x \ zOdd \ (!!k. x = 2 * k + 1 \ C) \ C" + by (auto simp add: zOdd_def) -lemma even_odd_conj: "~(x \ zOdd & x \ 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 \ x \ zEven" + and zEvenE [elim?]: "x \ zEven \ (!!k. x = 2 * k \ C) \ C" + by (auto simp add: zEven_def) + +lemma one_not_even: "~(1 \ zEven)" +proof + assume "1 \ zEven" + then obtain k :: int where "1 = 2 * k" .. + then show False by arith +qed -lemma even_odd_disj: "(x \ zOdd | x \ zEven)"; - by (simp add: zOdd_def zEven_def, presburger) +lemma even_odd_conj: "~(x \ zOdd & x \ 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 \ zOdd) ==> x \ zEven"; - by (insert even_odd_disj, auto) +lemma even_odd_disj: "(x \ zOdd | x \ zEven)" + by (simp add: zOdd_def zEven_def) arith -lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \ zOdd"; - apply (case_tac "x \ 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 \ zOdd) ==> x \ zEven" + using even_odd_disj by auto -lemma odd_minus_one_even: "x \ zOdd ==> (x - 1):zEven"; +lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \ zOdd" +proof (rule classical) + assume "\ ?thesis" + then have "x \ 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 \ zOdd ==> (x - 1):zEven" by (auto simp add: zOdd_def zEven_def) -lemma even_div_2_prop1: "x \ zEven ==> (x mod 2) = 0"; +lemma even_div_2_prop1: "x \ zEven ==> (x mod 2) = 0" by (auto simp add: zEven_def) -lemma even_div_2_prop2: "x \ zEven ==> (2 * (x div 2)) = x"; +lemma even_div_2_prop2: "x \ zEven ==> (2 * (x div 2)) = x" by (auto simp add: zEven_def) -lemma even_plus_even: "[| x \ zEven; y \ zEven |] ==> x + y \ zEven"; +lemma even_plus_even: "[| x \ zEven; y \ zEven |] ==> x + y \ 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 \ zEven ==> x * y \ zEven"; +lemma even_times_either: "x \ zEven ==> x * y \ zEven" by (auto simp add: zEven_def) -lemma even_minus_even: "[| x \ zEven; y \ zEven |] ==> x - y \ zEven"; +lemma even_minus_even: "[| x \ zEven; y \ zEven |] ==> x - y \ 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 \ zOdd; y \ zOdd |] ==> x - y \ zEven"; +lemma odd_minus_odd: "[| x \ zOdd; y \ zOdd |] ==> x - y \ 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 \ zEven; y \ zOdd |] ==> x - y \ zOdd"; +lemma even_minus_odd: "[| x \ zEven; y \ zOdd |] ==> x - y \ 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 \ zOdd; y \ zEven |] ==> x - y \ zOdd"; +lemma odd_minus_even: "[| x \ zOdd; y \ zEven |] ==> x - y \ 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 \ zOdd; y \ zOdd |] ==> x * y \ zOdd"; +lemma odd_times_odd: "[| x \ zOdd; y \ zOdd |] ==> x * y \ 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 \ zOdd) = (~ (x \ zEven))"; - by (insert even_odd_conj even_odd_disj, auto) - -lemma even_product: "x * y \ zEven ==> x \ zEven | y \ zEven"; - by (insert odd_iff_not_even odd_times_odd, auto) + apply (auto simp add: zadd_zmult_distrib) + done -lemma even_diff: "x - y \ zEven = ((x \ zEven) = (y \ 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 \ zEven" and "x \ zEven"; - show "y \ zEven"; - proof (rule classical); - assume "~(y \ zEven)"; - then have "y \ zOdd" - by (auto simp add: odd_iff_not_even) - with prems have "x - y \ 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 \ zEven" and "y \ zEven"; - show "x \ zEven"; - proof (rule classical); - assume "~(x \ zEven)"; - then have "x \ zOdd" - by (auto simp add: odd_iff_not_even) - with prems have "x - y \ 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 \ zOdd) = (~ (x \ zEven))" + using even_odd_conj even_odd_disj by auto + +lemma even_product: "x * y \ zEven ==> x \ zEven | y \ zEven" + using odd_iff_not_even odd_times_odd by auto -lemma neg_one_even_power: "[| x \ zEven; 0 \ x |] ==> (-1::int)^(nat x) = 1"; -proof -; - assume "x \ zEven" and "0 \ x"; - then have "\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 \ 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 \ zEven = ((x \ zEven) = (y \ zEven))" +proof + assume xy: "x - y \ zEven" + { + assume x: "x \ zEven" + have "y \ zEven" + proof (rule classical) + assume "\ ?thesis" + then have "y \ zOdd" + by (simp add: odd_iff_not_even) + with x have "x - y \ 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 \ zEven" + have "x \ zEven" + proof (rule classical) + assume "\ ?thesis" + then have "x \ zOdd" + by (auto simp add: odd_iff_not_even) + with y have "x - y \ 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 \ zEven) = (y \ zEven)" + by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd + even_minus_odd odd_minus_even) +next + assume "(x \ zEven) = (y \ zEven)" + then show "x - y \ 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 \ zOdd; 0 \ x |] ==> (-1::int)^(nat x) = -1"; -proof -; - assume "x \ zOdd" and "0 \ x"; - then have "\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 \ 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 \ zEven; 0 \ x |] ==> (-1::int)^(nat x) = 1" +proof - + assume 1: "x \ zEven" and 2: "0 \ x" + from 1 obtain a where 3: "x = 2 * a" .. + with 2 have "0 \ 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 \ x; 0 \ y; (x \ zEven) = (y \ 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 \ zOdd; 0 \ x |] ==> (-1::int)^(nat x) = -1" +proof - + assume 1: "x \ zOdd" and 2: "0 \ x" + from 1 obtain a where 3: "x = 2 * a + 1" .. + with 2 have a: "0 \ 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 \ x; 0 \ y; (x \ zEven) = (y \ 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 \ 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 \ zEven; x < y |] ==> x div 2 < y div 2" +proof - + assume 1: "y \ 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 \ zEven; y \ zEven |] ==> (x + y) div 2 = x div 2 + y div 2"; +lemma even_sum_div_2: "[| x \ zEven; y \ 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 \ zEven |] ==> (x * y) div 2 = (x div 2) * y"; +lemma even_prod_div_2: "[| x \ 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 \ 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]) -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 diff -r 2f9b2539c5bb -r 694ea14ab4f2 src/HOL/NumberTheory/Finite2.thy --- 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: "\x \ 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 \ 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 \ x }" -apply (subgoal_tac "{ y::nat . y \ 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 \ x}" +proof - + have "{y::nat . y \ 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 \ x & x < n}" -apply (subgoal_tac " {(x :: int). 0 \ x & x < n} \ +lemma bdd_int_set_l_finite: "finite {x::int. 0 \ x & x < n}" +apply (subgoal_tac " {(x :: int). 0 \ x & x < n} \ 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 \ x & x \ n}" apply (subgoal_tac "{x. 0 \ x & x \ n} = {x. 0 \ 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} \ {x::int. 0 \ x & x < n}") -by (auto simp add: bdd_int_set_l_finite finite_subset) +proof - + have "{x::int. 0 < x & x < n} \ {x::int. 0 \ 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 \ n}" -apply (subgoal_tac "{x::int. 0 < x & x \ n} \ {x::int. 0 \ x & x \ n}") -by (auto simp add: bdd_int_set_le_finite finite_subset) +proof - + have "{x::int. 0 < x & x \ n} \ {x::int. 0 \ x & x \ 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 \ x} = Suc x" -apply (subgoal_tac "{ y::nat. y \ x} = { y::nat. y < Suc x}") -by (auto simp add: card_bdd_nat_set_l) +proof - + have "{y::nat. y \ 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 \ (n::int) ==> card {y. 0 \ y & y < n} = nat n" proof - - fix n::int assume "0 \ 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 \ 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 \ y & y < n} = nat n" . qed -lemma card_bdd_int_set_le: "0 \ (n::int) ==> card {y. 0 \ y & y \ n} = +lemma card_bdd_int_set_le: "0 \ (n::int) ==> card {y. 0 \ y & y \ n} = nat n + 1" -apply (subgoal_tac "{y. 0 \ y & y \ n} = {y. 0 \ y & y < n+1}") -apply (insert card_bdd_int_set_l [of "n+1"]) -by (auto simp add: nat_add_distrib) +proof - + assume "0 \ n" + moreover have "{y. 0 \ y & y \ n} = {y. 0 \ 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 \ (n::int) ==> +lemma card_bdd_int_set_l_le: "0 \ (n::int) ==> card {x. 0 < x & x \ n} = nat n" proof - - fix n::int assume "0 \ n" have "inj_on (%x. x+1) {x. 0 \ x & x < n}" by (auto simp add: inj_on_def) - hence "card ((%x. x+1) ` {x. 0 \ x & x < n}) = + hence "card ((%x. x+1) ` {x. 0 \ x & x < n}) = card {x. 0 \ x & x < n}" by (rule card_image) - also from prems have "... = nat n" + also from `0 \ n` have "... = nat n" by (rule card_bdd_int_set_l) also have "(%x. x + 1) ` {x. 0 \ 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 \ n} = nat n". + apply arith + done + finally show "card {x. 0 < x & x \ 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 \ 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 \ 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 \ 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 \ n ==> +lemma int_card_bdd_int_set_l_le: "0 \ n ==> int(card {x. 0 < x & x \ 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 \ B; inj_on f A; +lemma setsum_bij_eq: "[| finite A; finite B; f ` A \ B; inj_on f A; g ` B \ A; inj_on g B |] ==> setsum g B = setsum (g \ 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 \ B; inj_on f A; +lemma setprod_bij_eq: "[| finite A; finite B; f ` A \ B; inj_on f A; g ` B \ A; inj_on g B |] ==> setprod g B = setprod (g \ 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 diff -r 2f9b2539c5bb -r 694ea14ab4f2 src/HOL/NumberTheory/Gauss.thy --- 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 \ {x. x \ ((p - 1) div 2)}" defines E_def: "E == C \ {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 \ zOdd"; +lemma (in GAUSS) p_odd: "p \ 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 \ p - 1" - apply (rule ssubst) back; - apply (rule zdiv_mono2) - by (auto simp add: p_g_0) - then have "(p - 1) div 2 \ 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 \ (p - 1) div 1" + by (rule zdiv_mono2) (auto simp add: p_g_0) + also have "\ = 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 \ zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"; +lemma zodd_imp_zdiv_eq: "x \ 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 \ 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 \ (p - 1) div 2} \ {x. 0 \ 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 \ (p - 1) div 2} \ {x. 0 \ 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 \ E"; +lemma (in GAUSS) C_eq: "C = D \ 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 \ (p - 1) div 2" - assume d: "0 < y" - assume e: "y \ (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 \ (p - 1) div 2" + assume d: "0 < y" + assume e: "y \ (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 \ (p - 1) div 2" - assume d: "0 < y" - assume e: "y \ (p - 1) div 2" - assume f: "x \ 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 \ (p - 1) div 2" + assume d: "0 < y" + assume e: "y \ (p - 1) div 2" + assume f: "x \ 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 \ A ==> ~[x = 0](mod p)"; +lemma (in GAUSS) A_ncong_p: "x \ 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 \ A ==> 0 < x"; +lemma (in GAUSS) A_greater_zero: "x \ A ==> 0 < x" by (auto simp add: A_def) -lemma (in GAUSS) B_ncong_p: "x \ B ==> ~[x = 0](mod p)"; +lemma (in GAUSS) B_ncong_p: "x \ 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 \ 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 \ 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 \ C ==> ~[x = 0](mod p)"; +lemma (in GAUSS) C_ncong_p: "x \ 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 \ C ==> 0 < y"; +lemma (in GAUSS) C_greater_zero: "y \ C ==> 0 < y" apply (auto simp add: C_def) - proof -; - fix x; - assume a: "x \ B"; - from p_g_0 have "0 \ 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 \ 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 \ B" + from p_g_0 have "0 \ 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 \ 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 \ D ==> ~[x = 0](mod p)"; +lemma (in GAUSS) D_ncong_p: "x \ D ==> ~[x = 0](mod p)" by (auto simp add: D_def C_ncong_p) -lemma (in GAUSS) E_ncong_p: "x \ E ==> ~[x = 0](mod p)"; +lemma (in GAUSS) E_ncong_p: "x \ E ==> ~[x = 0](mod p)" by (auto simp add: E_def C_ncong_p) -lemma (in GAUSS) F_ncong_p: "x \ F ==> ~[x = 0](mod p)"; - apply (auto simp add: F_def) - proof -; - fix x assume a: "x \ 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 \ F ==> ~[x = 0](mod p)" + apply (auto simp add: F_def) +proof - + fix x assume a: "x \ 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 \ {x. 0 < x & x \ ((p - 1) div 2)}"; - apply (auto simp add: F_def E_def) +lemma (in GAUSS) F_subset: "F \ {x. 0 < x & x \ ((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 \ B |] - ==> p - StandardRes p x \ (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 \ B |] + ==> p - StandardRes p x \ (p - 1) div 2" + by simp +qed -lemma (in GAUSS) D_subset: "D \ {x. 0 < x & x \ ((p - 1) div 2)}"; +lemma (in GAUSS) D_subset: "D \ {x. 0 < x & x \ ((p - 1) div 2)}" by (auto simp add: D_def C_greater_zero) -lemma (in GAUSS) F_eq: "F = {x. \y \ A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"; +lemma (in GAUSS) F_eq: "F = {x. \y \ 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. \y \ A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \ (p - 1) div 2)}"; +lemma (in GAUSS) D_eq: "D = {x. \y \ A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \ (p - 1) div 2)}" by (auto simp add: D_def C_def B_def A_def) -lemma (in GAUSS) D_leq: "x \ D ==> x \ (p - 1) div 2"; +lemma (in GAUSS) D_leq: "x \ D ==> x \ (p - 1) div 2" by (auto simp add: D_eq) -lemma (in GAUSS) F_ge: "x \ F ==> x \ (p - 1) div 2"; +lemma (in GAUSS) F_ge: "x \ F ==> x \ (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) \ (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) \ (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: "\x \ 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: "\x \ 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 \ E = {}"; +lemma (in GAUSS) D_E_disj: "D \ 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 \ D) \ A"; +lemma (in GAUSS) F_Un_D_subset: "(F \ D) \ 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 \ D) = {}"; +lemma (in GAUSS) F_D_disj: "(F \ 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 \ A" and c: "ya: A"; - with A_def have "0 < y + ya"; - by auto - moreover from b c A_def have "y + ya \ (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 \ A" and c: "ya: A" + with A_def have "0 < y + ya" + by auto + moreover from b c A_def have "y + ya \ (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 \ D) = nat ((p - 1) div 2)"; +lemma (in GAUSS) F_Un_D_card: "card (F \ D) = nat ((p - 1) div 2)" apply (insert F_D_disj finite_F finite_D) - proof -; - have "card (F \ 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 \ D) = card C"; - by (simp add: C_card_eq_D_plus_E) - from this show "card (F \ D) = nat ((p - 1) div 2)"; - by (simp add: C_card_eq_B B_card_eq) -qed; +proof - + have "card (F \ 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 \ D) = card C" + by (simp add: C_card_eq_D_plus_E) + from this show "card (F \ 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 \ 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 \ 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: "\x \ 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: "\