--- a/src/HOL/NumberTheory/BijectionRel.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy Wed May 17 01:23:41 2006 +0200
@@ -29,15 +29,15 @@
(and similar for @{term A}).
*}
-constdefs
+definition
bijP :: "('a => 'a => bool) => 'a set => bool"
- "bijP P F == \<forall>a b. a \<in> F \<and> P a b --> b \<in> F"
+ "bijP P F = (\<forall>a b. a \<in> F \<and> P a b --> b \<in> F)"
uniqP :: "('a => 'a => bool) => bool"
- "uniqP P == \<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d)"
+ "uniqP P = (\<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d))"
symP :: "('a => 'a => bool) => bool"
- "symP P == \<forall>a b. P a b = P b a"
+ "symP P = (\<forall>a b. P a b = P b a)"
consts
bijER :: "('a => 'a => bool) => 'a set set"
--- a/src/HOL/NumberTheory/Chinese.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Wed May 17 01:23:41 2006 +0200
@@ -31,43 +31,34 @@
"funsum f i 0 = f i"
"funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
-consts
+definition
m_cond :: "nat => (nat => int) => bool"
+ "m_cond n mf =
+ ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
+ (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
+
km_cond :: "nat => (nat => int) => (nat => int) => bool"
+ "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
+
lincong_sol ::
"nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
+ "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
mhf :: "(nat => int) => nat => nat => int"
+ "mhf mf n i =
+ (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
+ else if i = n then funprod mf 0 (n - Suc 0)
+ else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
+
xilin_sol ::
"nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
- x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
-
-defs
- m_cond_def:
- "m_cond n mf ==
- (\<forall>i. i \<le> n --> 0 < mf i) \<and>
- (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
-
- km_cond_def:
- "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
-
- lincong_sol_def:
- "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
+ "xilin_sol i n kf bf mf =
+ (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
+ (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
+ else 0)"
- mhf_def:
- "mhf mf n i ==
- if i = 0 then funprod mf (Suc 0) (n - Suc 0)
- else if i = n then funprod mf 0 (n - Suc 0)
- else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)"
-
- xilin_sol_def:
- "xilin_sol i n kf bf mf ==
- if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
- (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
- else 0"
-
- x_sol_def:
- "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
+ x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
+ "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
text {* \medskip @{term funprod} and @{term funsum} *}
--- a/src/HOL/NumberTheory/Euler.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Euler.thy Wed May 17 01:23:41 2006 +0200
@@ -7,22 +7,20 @@
theory Euler imports Residues EvenOdd begin
-constdefs
+definition
MultInvPair :: "int => int => int => int set"
- "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+ "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+
SetS :: "int => int => int set set"
- "SetS a p == ((MultInvPair a p) ` (SRStar p))"
+ "SetS a p = (MultInvPair a p ` SRStar p)"
-(****************************************************************)
-(* *)
-(* Property for MultInvPair *)
-(* *)
-(****************************************************************)
+
+subsection {* Property for MultInvPair *}
-lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
- X \<in> (SetS a p); Y \<in> (SetS a p);
- ~((X \<inter> Y) = {}) |] ==>
- X = Y"
+lemma MultInvPair_prop1a:
+ "[| zprime p; 2 < p; ~([a = 0](mod p));
+ X \<in> (SetS a p); Y \<in> (SetS a p);
+ ~((X \<inter> Y) = {}) |] ==> X = Y"
apply (auto simp add: SetS_def)
apply (drule StandardRes_SRStar_prop1a)+ defer 1
apply (drule StandardRes_SRStar_prop1a)+
@@ -35,16 +33,16 @@
apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
-done
+ done
-lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
- X \<in> (SetS a p); Y \<in> (SetS a p);
- X \<noteq> Y |] ==>
- X \<inter> Y = {}"
+lemma MultInvPair_prop1b:
+ "[| zprime p; 2 < p; ~([a = 0](mod p));
+ X \<in> (SetS a p); Y \<in> (SetS a p);
+ X \<noteq> Y |] ==> X \<inter> Y = {}"
apply (rule notnotD)
apply (rule notI)
apply (drule MultInvPair_prop1a, auto)
-done
+ done
lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
\<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
@@ -56,7 +54,7 @@
SRStar_mult_prop2)
apply (frule StandardRes_SRStar_prop3)
apply (rule bexI, auto)
-done
+ done
lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~([j = 0] (mod p));
@@ -97,11 +95,8 @@
apply (drule MultInvPair_distinct)
by auto
-(****************************************************************)
-(* *)
-(* Properties of SetS *)
-(* *)
-(****************************************************************)
+
+subsection {* Properties of SetS *}
lemma SetS_finite: "2 < p ==> finite (SetS a p)"
by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
@@ -115,7 +110,7 @@
apply (auto simp add: SetS_def)
apply (frule StandardRes_SRStar_prop1a)
apply (rule MultInvPair_card_two, auto)
-done
+ done
lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
@@ -136,10 +131,9 @@
by (auto simp add: prems SetS_finite SetS_elems_finite
MultInvPair_prop1c [of p a] card_Union_disjoint)
also have "... = int(setsum (%x.2) (SetS a p))"
- apply (insert prems)
- apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
+ using prems
+ by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
card_setsum_aux simp del: setsum_constant)
- done
also have "... = 2 * int(card( SetS a p))"
by (auto simp add: prems SetS_finite setsum_const2)
finally show ?thesis .
@@ -164,7 +158,7 @@
apply (frule_tac p = p and x = x in MultInv_prop2, auto)
apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
apply (auto simp add: zmult_ac)
-done
+ done
lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
by arith
@@ -237,13 +231,7 @@
apply (auto simp add: Union_SetS_setprod_prop2)
done
-(****************************************************************)
-(* *)
-(* Prove the first part of Euler's Criterion: *)
-(* ~(QuadRes p x) |] ==> *)
-(* [x^(nat (((p) - 1) div 2)) = -1](mod p) *)
-(* *)
-(****************************************************************)
+text {* \medskip Prove the first part of Euler's Criterion: *}
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
~(QuadRes p x) |] ==>
@@ -254,12 +242,7 @@
apply (rule zcong_trans, auto)
done
-(********************************************************************)
-(* *)
-(* Prove another part of Euler Criterion: *)
-(* [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
-(* *)
-(********************************************************************)
+text {* \medskip Prove another part of Euler Criterion: *}
lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
proof -
@@ -289,20 +272,15 @@
then show ?thesis by auto
qed
-lemma Euler_part2: "[| 2 < p; zprime p; [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)
apply (frule zcong_zmult_prop1, auto)
done
-(****************************************************************)
-(* *)
-(* Prove the final part of Euler's Criterion: *)
-(* QuadRes p x |] ==> *)
-(* [x^(nat (((p) - 1) div 2)) = 1](mod p) *)
-(* *)
-(****************************************************************)
+text {* \medskip Prove the final part of Euler's Criterion: *}
lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==>
@@ -329,11 +307,8 @@
apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
done
-(********************************************************************)
-(* *)
-(* Finally show Euler's Criterion *)
-(* *)
-(********************************************************************)
+
+text {* \medskip Finally show Euler's Criterion: *}
theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
a^(nat (((p) - 1) div 2))] (mod p)"
--- a/src/HOL/NumberTheory/EulerFermat.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Wed May 17 01:23:41 2006 +0200
@@ -19,12 +19,6 @@
consts
RsetR :: "int => int set set"
- BnorRset :: "int * int => int set"
- norRRset :: "int => int set"
- noXRRset :: "int => int => int set"
- phi :: "int => nat"
- is_RRset :: "int set => int => bool"
- RRset2norRR :: "int set => int => int => int"
inductive "RsetR m"
intros
@@ -32,6 +26,9 @@
insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
\<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
+consts
+ BnorRset :: "int * int => int set"
+
recdef BnorRset
"measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
"BnorRset (a, m) =
@@ -40,20 +37,27 @@
in (if zgcd (a, m) = 1 then insert a na else na)
else {})"
-defs
- norRRset_def: "norRRset m == BnorRset (m - 1, m)"
- noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m"
- phi_def: "phi m == card (norRRset m)"
- is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
- RRset2norRR_def:
- "RRset2norRR A m a ==
+definition
+ norRRset :: "int => int set"
+ "norRRset m = BnorRset (m - 1, m)"
+
+ noXRRset :: "int => int => int set"
+ "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
+
+ phi :: "int => nat"
+ "phi m = card (norRRset m)"
+
+ is_RRset :: "int set => int => bool"
+ "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
+
+ RRset2norRR :: "int set => int => int => int"
+ "RRset2norRR A m a =
(if 1 < m \<and> is_RRset A m \<and> a \<in> A then
SOME b. zcong a b m \<and> b \<in> norRRset m
else 0)"
-constdefs
zcongm :: "int => int => int => bool"
- "zcongm m == \<lambda>a b. zcong a b m"
+ "zcongm m = (\<lambda>a b. zcong a b m)"
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
-- {* LCP: not sure why this lemma is needed now *}
--- a/src/HOL/NumberTheory/EvenOdd.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy Wed May 17 01:23:41 2006 +0200
@@ -7,20 +7,13 @@
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
+definition
zOdd :: "int set"
- "zOdd == {x. \<exists>k. x = 2 * k + 1}"
+ "zOdd = {x. \<exists>k. x = 2 * k + 1}"
zEven :: "int set"
- "zEven == {x. \<exists>k. x = 2 * k}"
+ "zEven = {x. \<exists>k. x = 2 * k}"
-(***********************************************************)
-(* *)
-(* Some useful properties about even and odd *)
-(* *)
-(***********************************************************)
+subsection {* Some useful properties about even and odd *}
lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
--- a/src/HOL/NumberTheory/Factorization.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy Wed May 17 01:23:41 2006 +0200
@@ -11,16 +11,16 @@
subsection {* Definitions *}
+definition
+ primel :: "nat list => bool "
+ "primel xs = (\<forall>p \<in> set xs. prime p)"
+
consts
- primel :: "nat list => bool "
nondec :: "nat list => bool "
prod :: "nat list => nat"
oinsert :: "nat => nat list => nat list"
sort :: "nat list => nat list"
-defs
- primel_def: "primel xs == \<forall>p \<in> set xs. prime p"
-
primrec
"nondec [] = True"
"nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
@@ -41,12 +41,12 @@
subsection {* Arithmetic *}
lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
- apply (case_tac m)
+ apply (cases m)
apply auto
done
lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
- apply (case_tac k)
+ apply (cases k)
apply auto
done
@@ -55,7 +55,7 @@
done
lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
- apply (case_tac n)
+ apply (cases n)
apply auto
done
@@ -116,9 +116,8 @@
done
lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
- apply (unfold primel_def prime_def)
- apply (case_tac xs)
- apply simp_all
+ apply (cases xs)
+ apply (simp_all add: primel_def prime_def)
done
lemma prime_g_one: "prime p ==> Suc 0 < p"
@@ -131,25 +130,25 @@
apply auto
done
-lemma primel_nempty_g_one [rule_format]:
- "primel xs --> xs \<noteq> [] --> Suc 0 < prod xs"
- apply (unfold primel_def prime_def)
+lemma primel_nempty_g_one:
+ "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
apply (induct xs)
- apply (auto elim: one_less_mult)
+ apply simp
+ apply (fastsimp simp: primel_def prime_def elim: one_less_mult)
done
lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
- apply (unfold primel_def prime_def)
apply (induct xs)
- apply auto
+ apply (auto simp: primel_def prime_def)
done
subsection {* Sorting *}
-lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
+lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
apply (induct xs)
- apply (case_tac [2] xs)
+ apply simp
+ apply (case_tac xs)
apply (simp_all cong del: list.weak_case_cong)
done
@@ -163,7 +162,7 @@
apply simp_all
done
-lemma nondec_sort_eq [rule_format]: "nondec xs --> xs = sort xs"
+lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
apply (induct xs)
apply safe
apply simp_all
@@ -185,7 +184,7 @@
lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
apply (unfold primel_def)
- apply (erule perm.induct)
+ apply (induct set: perm)
apply simp
apply simp
apply (simp (no_asm))
@@ -193,13 +192,13 @@
apply blast
done
-lemma perm_prod [rule_format]: "xs <~~> ys ==> prod xs = prod ys"
- apply (erule perm.induct)
+lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
+ apply (induct set: perm)
apply (simp_all add: mult_ac)
done
lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
- apply (erule perm.induct)
+ apply (induct set: perm)
apply auto
done
@@ -214,7 +213,7 @@
done
lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
- apply (erule perm.induct)
+ apply (induct set: perm)
apply (simp_all add: oinsert_x_y)
done
--- a/src/HOL/NumberTheory/Finite2.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy Wed May 17 01:23:41 2006 +0200
@@ -9,23 +9,17 @@
imports IntFact
begin
-text{*These are useful for combinatorial and number-theoretic counting
-arguments.*}
-
-text{*Note. This theory is being revised. See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+text{*
+ These are useful for combinatorial and number-theoretic counting
+ arguments.
+*}
-(******************************************************************)
-(* *)
-(* Useful properties of sums and products *)
-(* *)
-(******************************************************************)
subsection {* Useful properties of sums and products *}
lemma setsum_same_function_zcong:
-assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
-shows "[setsum f S = setsum g S] (mod m)"
+ assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
+ shows "[setsum f S = setsum g S] (mod m)"
proof cases
assume "finite S"
thus ?thesis using a by induct (simp_all add: zcong_zadd)
@@ -34,8 +28,8 @@
qed
lemma setprod_same_function_zcong:
-assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
-shows "[setprod f S = setprod g S] (mod m)"
+ assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
+ shows "[setprod f S = setprod g S] (mod m)"
proof cases
assume "finite S"
thus ?thesis using a by induct (simp_all add: zcong_zmult)
@@ -59,12 +53,6 @@
by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
-(******************************************************************)
-(* *)
-(* Cardinality of some explicit finite sets *)
-(* *)
-(******************************************************************)
-
subsection {* Cardinality of explicit finite sets *}
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
@@ -80,19 +68,19 @@
qed
lemma bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
-apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
- 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)
-done
+ apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
+ int ` {(x :: nat). x < nat n}")
+ apply (erule finite_surjI)
+ apply (auto simp add: bdd_nat_set_l_finite image_def)
+ apply (rule_tac x = "nat x" in exI, simp)
+ done
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
-apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
-apply (erule ssubst)
-apply (rule bdd_int_set_l_finite)
-apply auto
-done
+ apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
+ apply (erule ssubst)
+ apply (rule bdd_int_set_l_finite)
+ apply auto
+ done
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
proof -
@@ -192,7 +180,7 @@
int(card {x. 0 < x & x < n}) = n - 1"
apply (auto simp add: card_bdd_int_set_l_l)
apply (subgoal_tac "Suc 0 \<le> nat n")
- apply (auto simp add: zdiff_int [symmetric])
+ apply (auto simp add: zdiff_int [symmetric])
apply (subgoal_tac "0 < nat n", arith)
apply (simp add: zero_less_nat_eq)
done
@@ -201,11 +189,6 @@
int(card {x. 0 < x & x \<le> n}) = n"
by (auto simp add: card_bdd_int_set_l_le)
-(******************************************************************)
-(* *)
-(* Cartesian products of finite sets *)
-(* *)
-(******************************************************************)
subsection {* Cardinality of finite cartesian products *}
@@ -214,35 +197,29 @@
by blast
*)
-(******************************************************************)
-(* *)
-(* Sums and products over finite sets *)
-(* *)
-(******************************************************************)
-
-subsection {* Lemmas for counting arguments *}
+text {* Lemmas for counting arguments. *}
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
-apply (frule_tac h = g and f = f in setsum_reindex)
-apply (subgoal_tac "setsum g B = setsum g (f ` A)")
-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)
-apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
-apply auto
-done
+ apply (frule_tac h = g and f = f in setsum_reindex)
+ apply (subgoal_tac "setsum g B = setsum 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)
+ apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
+ apply auto
+ done
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
apply (frule_tac h = g and f = f in setprod_reindex)
apply (subgoal_tac "setprod g B = setprod g (f ` A)")
- apply (simp add: inj_on_def)
+ 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 (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)
apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
done
--- a/src/HOL/NumberTheory/Int2.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Int2.thy Wed May 17 01:23:41 2006 +0200
@@ -7,18 +7,12 @@
theory Int2 imports Finite2 WilsonRuss begin
-text{*Note. This theory is being revised. See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+definition
+ MultInv :: "int => int => int"
+ "MultInv p x = x ^ nat (p - 2)"
-constdefs
- MultInv :: "int => int => int"
- "MultInv p x == x ^ nat (p - 2)"
-(*****************************************************************)
-(* *)
-(* Useful lemmas about dvd and powers *)
-(* *)
-(*****************************************************************)
+subsection {* Useful lemmas about dvd and powers *}
lemma zpower_zdvd_prop1:
"0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
@@ -32,7 +26,7 @@
then show ?thesis by auto
qed
-lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==>
+lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==>
(p dvd m) | (p dvd n)"
apply (cases "0 \<le> m")
apply (simp add: zprime_zdvd_zmult)
@@ -83,11 +77,8 @@
by arith
qed
-(*****************************************************************)
-(* *)
-(* Useful properties of congruences *)
-(* *)
-(*****************************************************************)
+
+subsection {* Useful properties of congruences *}
lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
by (auto simp add: zcong_def)
@@ -101,7 +92,7 @@
lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
by (induct z) (auto simp add: zcong_zmult)
-lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
+lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
[a = d](mod m)"
apply (erule zcong_trans)
apply simp
@@ -110,7 +101,7 @@
lemma aux1: "a - b = (c::int) ==> a = c + b"
by auto
-lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
+lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
[c = b * d] (mod m))"
apply (auto simp add: zcong_def dvd_def)
apply (rule_tac x = "ka + k * d" in exI)
@@ -121,17 +112,17 @@
apply (auto simp add: int_distrib)
done
-lemma zcong_zmult_prop2: "[a = b](mod m) ==>
+lemma zcong_zmult_prop2: "[a = b](mod m) ==>
([c = d * a](mod m) = [c = d * b] (mod m))"
by (auto simp add: zmult_ac zcong_zmult_prop1)
-lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
+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)
done
-lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
+lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
x < m; y < m |] ==> x = y"
apply (simp add: zcong_zmod_eq)
apply (subgoal_tac "(x mod m) = x")
@@ -141,7 +132,7 @@
apply auto
done
-lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
+lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
~([x = 1] (mod p))"
proof
assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
@@ -162,18 +153,18 @@
lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"
by (auto simp add: zcong_def)
-lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==>
- [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"
+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: "[| zprime p; 0 < a |] ==>
~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"
- apply auto
+ apply auto
apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
apply auto
done
-lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"
+lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"
by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"
@@ -186,17 +177,14 @@
==> zgcd (setprod id A,y) = 1"
by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
-(*****************************************************************)
-(* *)
-(* Some properties of MultInv *)
-(* *)
-(*****************************************************************)
-lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
+subsection {* Some properties of MultInv *}
+
+lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
[(MultInv p x) = (MultInv p y)] (mod p)"
by (auto simp add: MultInv_def zcong_zpower)
-lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
+lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
[(x * (MultInv p x)) = 1] (mod p)"
proof (simp add: MultInv_def zcong_eq_zdvd_prop)
assume "2 < p" and "zprime p" and "~ p dvd x"
@@ -208,11 +196,11 @@
finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
by (rule ssubst, auto)
also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
- by (auto simp add: Little_Fermat)
+ by (auto simp add: Little_Fermat)
finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
qed
-lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([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)
@@ -222,15 +210,15 @@
lemma aux_2: "2 < p ==> 0 < nat (p - 2)"
by auto
-lemma MultInv_prop3: "[| 2 < p; zprime p; ~([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; zprime p; ~([x = 0](mod p))|] ==>
- [(MultInv p (MultInv p x)) = (x * (MultInv p x) *
+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)
apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto)
@@ -246,17 +234,17 @@
apply (auto simp add: zmult_ac)
done
-lemma MultInv_prop4: "[| 2 < p; zprime p; ~([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; zprime p; ~([x = 0](mod p));
- ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (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
+ apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
m = p and k = x in zcong_scalar)
apply (insert MultInv_prop2 [of p x], simp)
apply (auto simp only: zcong_sym [of "MultInv p x * x"])
@@ -268,43 +256,43 @@
apply (auto simp add: zcong_sym)
done
-lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>
+lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>
[a * MultInv p j = a * MultInv p k] (mod p)"
by (drule MultInv_prop1, auto simp add: zcong_scalar2)
-lemma aux___1: "[j = a * MultInv p k] (mod p) ==>
+lemma aux___1: "[j = a * MultInv p k] (mod p) ==>
[j * k = a * MultInv p k * k] (mod p)"
by (auto simp add: zcong_scalar)
-lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p));
+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
+ apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
[of "MultInv p k * k" 1 p "j * k" a])
apply (auto simp add: zmult_ac)
done
-lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
+lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
(MultInv p j) * a] (mod p)"
by (auto simp add: zmult_assoc zcong_scalar2)
-lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
+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
+ apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
[of "MultInv p j * j" 1 p "MultInv p j * a" k])
apply (auto simp add: zmult_ac zcong_sym)
done
-lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
- ~([j = 0](mod p)); [j = a * MultInv p k] (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; zprime p; ~([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) |] ==>
+ [a * MultInv p j = a * MultInv p k] (mod p) |] ==>
[j = k] (mod p)"
apply (auto simp add: zcong_eq_zdvd_prop [of a p])
apply (frule zprime_imp_zrelprime, auto)
--- a/src/HOL/NumberTheory/IntPrimes.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Wed May 17 01:23:41 2006 +0200
@@ -31,18 +31,18 @@
s, s' - (r' div r) * s,
t, t' - (r' div r) * t))"
-constdefs
+definition
zgcd :: "int * int => int"
- "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
+ "zgcd = (\<lambda>(x,y). int (gcd (nat (abs x), nat (abs y))))"
zprime :: "int \<Rightarrow> bool"
- "zprime p == 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)"
+ "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
xzgcd :: "int => int => int * int * int"
- "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
+ "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)"
zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))")
- "[a = b] (mod m) == m dvd (a - b)"
+ "[a = b] (mod m) = (m dvd (a - b))"
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed May 17 01:23:41 2006 +0200
@@ -9,12 +9,10 @@
imports Gauss
begin
-(***************************************************************)
-(* *)
-(* Lemmas leading up to the proof of theorem 3.3 in *)
-(* Niven and Zuckerman's presentation *)
-(* *)
-(***************************************************************)
+text {*
+ Lemmas leading up to the proof of theorem 3.3 in Niven and
+ Zuckerman's presentation.
+*}
lemma (in GAUSS) QRLemma1: "a * setsum id A =
p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
@@ -149,11 +147,8 @@
apply (auto simp add: GAUSS_def)
done
-(******************************************************************)
-(* *)
-(* Stuff about S, S1 and S2... *)
-(* *)
-(******************************************************************)
+
+subsection {* Stuff about S, S1 and S2 *}
locale QRTEMP =
fixes p :: "int"
--- a/src/HOL/NumberTheory/Residues.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Residues.thy Wed May 17 01:23:41 2006 +0200
@@ -7,45 +7,33 @@
theory Residues imports Int2 begin
-text{*Note. This theory is being revised. See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+text {*
+ \medskip Define the residue of a set, the standard residue,
+ quadratic residues, and prove some basic properties. *}
-(*****************************************************************)
-(* *)
-(* Define the residue of a set, the standard residue, quadratic *)
-(* residues, and prove some basic properties. *)
-(* *)
-(*****************************************************************)
-
-constdefs
+definition
ResSet :: "int => int set => bool"
- "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) -->
- y1 = y2)"
+ "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
StandardRes :: "int => int => int"
- "StandardRes m x == x mod m"
+ "StandardRes m x = x mod m"
QuadRes :: "int => int => bool"
- "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
+ "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
Legendre :: "int => int => int"
- "Legendre a p == (if ([a = 0] (mod p)) then 0
+ "Legendre a p = (if ([a = 0] (mod p)) then 0
else if (QuadRes p a) then 1
else -1)"
SR :: "int => int set"
- "SR p == {x. (0 \<le> x) & (x < p)}"
+ "SR p = {x. (0 \<le> x) & (x < p)}"
SRStar :: "int => int set"
- "SRStar p == {x. (0 < x) & (x < p)}"
+ "SRStar p = {x. (0 < x) & (x < p)}"
-(******************************************************************)
-(* *)
-(* Some useful properties of StandardRes *)
-(* *)
-(******************************************************************)
-subsection {* Properties of StandardRes *}
+subsection {* Some useful properties of StandardRes *}
lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod)
@@ -72,11 +60,6 @@
"(StandardRes m x = 0) = ([x = 0](mod m))"
by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def)
-(******************************************************************)
-(* *)
-(* Some useful stuff relating StandardRes and SRStar and SR *)
-(* *)
-(******************************************************************)
subsection {* Relations between StandardRes, SRStar, and SR *}
@@ -132,11 +115,6 @@
lemma SRStar_finite: "2 < p ==> finite( SRStar p)"
by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
-(******************************************************************)
-(* *)
-(* Some useful stuff about ResSet and StandardRes *)
-(* *)
-(******************************************************************)
subsection {* Properties relating ResSets with StandardRes *}
@@ -175,14 +153,13 @@
apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
done
-lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)"
+lemma ResSet_image:
+ "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==>
+ ResSet m (f ` A)"
by (auto simp add: ResSet_def)
-(****************************************************************)
-(* *)
-(* Property for SRStar *)
-(* *)
-(****************************************************************)
+
+subsection {* Property for SRStar *}
lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
--- a/src/HOL/NumberTheory/WilsonBij.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy Wed May 17 01:23:41 2006 +0200
@@ -17,15 +17,14 @@
subsection {* Definitions and lemmas *}
-constdefs
+definition
reciR :: "int => int => int => bool"
- "reciR p ==
- \<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1"
+ "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
inv :: "int => int => int"
- "inv p a ==
- if zprime p \<and> 0 < a \<and> a < p then
+ "inv p a =
+ (if zprime p \<and> 0 < a \<and> a < p then
(SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
- else 0"
+ else 0)"
text {* \medskip Inverse *}
--- a/src/HOL/NumberTheory/WilsonRuss.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Wed May 17 01:23:41 2006 +0200
@@ -15,13 +15,13 @@
subsection {* Definitions and lemmas *}
+definition
+ inv :: "int => int => int"
+ "inv p a = (a^(nat (p - 2))) mod p"
+
consts
- inv :: "int => int => int"
wset :: "int * int => int set"
-defs
- inv_def: "inv p a == (a^(nat (p - 2))) mod p"
-
recdef wset
"measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
"wset (a, p) =
@@ -81,7 +81,8 @@
apply (rule_tac [2] zcong_zless_imp_eq, auto)
done
-lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
+lemma inv_not_p_minus_1_aux:
+ "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
apply (unfold zcong_def)
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -163,7 +164,8 @@
lemma wset_induct:
assumes "!!a p. P {} a p"
- and "!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
+ and "!!a p. 1 < (a::int) \<Longrightarrow>
+ P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
shows "P (wset (u, v)) u v"
apply (rule wset.induct, safe)
prefer 2