--- a/src/HOL/Equiv_Relations.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/Equiv_Relations.thy Thu Dec 09 18:30:59 2004 +0100
@@ -316,8 +316,8 @@
apply (rule Union_quotient [THEN subst])
apply assumption
apply (rule dvd_partition)
- prefer 4 apply (blast dest: quotient_disj)
- apply (simp_all add: Union_quotient equiv_type finite_quotient)
+ prefer 3 apply (blast dest: quotient_disj)
+ apply (simp_all add: Union_quotient equiv_type)
done
lemma card_quotient_disjoint:
--- a/src/HOL/Finite_Set.ML Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/Finite_Set.ML Thu Dec 09 18:30:59 2004 +0100
@@ -31,7 +31,6 @@
val [emptyI, insertI] = thms "foldSet.intros";
end;
-val Diff1_foldSet = thm "Diff1_foldSet";
val cardR_SucD = thm "cardR_SucD";
val cardR_determ = thm "cardR_determ";
val cardR_emptyE = thm "cardR_emptyE";
@@ -51,8 +50,8 @@
val card_bij_eq = thm "card_bij_eq";
val card_def = thm "card_def";
val card_empty = thm "card_empty";
+val card_equality = thm "card_equality";
val card_eq_setsum = thm "card_eq_setsum";
-val card_equality = thm "card_equality";
val card_image = thm "card_image";
val card_image_le = thm "card_image_le";
val card_inj_on_le = thm "card_inj_on_le";
@@ -66,6 +65,7 @@
val card_seteq = thm "card_seteq";
val choose_deconstruct = thm "choose_deconstruct";
val constr_bij = thm "constr_bij";
+val Diff1_foldSet = thm "Diff1_foldSet";
val dvd_partition = thm "dvd_partition";
val empty_foldSetE = thm "empty_foldSetE";
val endo_inj_surj = thm "endo_inj_surj";
@@ -74,6 +74,7 @@
val finite_Diff = thm "finite_Diff";
val finite_Diff_insert = thm "finite_Diff_insert";
val finite_Field = thm "finite_Field";
+val finite_imp_foldSet = thm "finite_imp_foldSet";
val finite_Int = thm "finite_Int";
val finite_Pow_iff = thm "finite_Pow_iff";
val finite_Prod_UNIV = thm "finite_Prod_UNIV";
@@ -87,25 +88,24 @@
val finite_imageD = thm "finite_imageD";
val finite_imageI = thm "finite_imageI";
val finite_imp_cardR = thm "finite_imp_cardR";
-val finite_imp_foldSet = thm "finite_imp_foldSet";
val finite_induct = thm "finite_induct";
val finite_insert = thm "finite_insert";
val finite_range_imageI = thm "finite_range_imageI";
val finite_subset = thm "finite_subset";
val finite_subset_induct = thm "finite_subset_induct";
val finite_trancl = thm "finite_trancl";
-val foldSet_determ = thm "LC.foldSet_determ";
+val foldSet_determ = thm "ACf.foldSet_determ";
val foldSet_imp_finite = thm "foldSet_imp_finite";
val fold_Un_Int = thm "ACe.fold_Un_Int";
val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
-val fold_Un_disjoint2 = thm "ACe.fold_o_Un_disjoint";
-val fold_commute = thm "LC.fold_commute";
+val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
+val fold_commute = thm "ACf.fold_commute";
val fold_def = thm "fold_def";
val fold_empty = thm "fold_empty";
-val fold_equality = thm "LC.fold_equality";
-val fold_insert = thm "LC.fold_insert";
-val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
-val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
+val fold_equality = thm "ACf.fold_equality";
+val fold_insert = thm "ACf.fold_insert";
+val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
+val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
val n_sub_lemma = thm "n_sub_lemma";
val n_subsets = thm "n_subsets";
val psubset_card_mono = thm "psubset_card_mono";
--- a/src/HOL/Finite_Set.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/Finite_Set.thy Thu Dec 09 18:30:59 2004 +0100
@@ -3,12 +3,7 @@
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
Additions by Jeremy Avigad in Feb 2004
-FIXME split up, get rid of LC, define foldSet f g e (instead of just f)
-
-Possible improvements: simplify card lemmas using the card_eq_setsum.
-Unfortunately it appears necessary to define card before foldSet
-because the uniqueness proof of foldSet uses card (but only very
-elementary properties).
+FIXME: define card via fold and derive as many lemmas as possible from fold.
*)
header {* Finite sets *}
@@ -17,7 +12,7 @@
imports Divides Power Inductive
begin
-subsection {* Collection of finite sets *}
+subsection {* Definition and basic properties *}
consts Finites :: "'a set set"
syntax
@@ -87,6 +82,49 @@
qed
qed
+text{* Finite sets are the images of initial segments of natural numbers: *}
+
+lemma finite_imp_nat_seg_image:
+assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}"
+using fin
+proof induct
+ case empty
+ show ?case
+ proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed
+next
+ case (insert a A)
+ from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast
+ hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}"
+ by (auto simp add:image_def Ball_def)
+ thus ?case by blast
+qed
+
+lemma nat_seg_image_imp_finite:
+ "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
+proof (induct n)
+ case 0 thus ?case by simp
+next
+ case (Suc n)
+ let ?B = "f ` {i. i < n}"
+ have finB: "finite ?B" by(rule Suc.hyps[OF refl])
+ show ?case
+ proof cases
+ assume "\<exists>k<n. f n = f k"
+ hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
+ thus ?thesis using finB by simp
+ next
+ assume "\<not>(\<exists> k<n. f n = f k)"
+ hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
+ thus ?thesis using finB by simp
+ qed
+qed
+
+lemma finite_conv_nat_seg_image:
+ "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
+by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite)
+
+subsubsection{* Finiteness and set theoretic constructions *}
+
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
-- {* The union of two finite sets is finite. *}
by (induct set: Finites) simp_all
@@ -177,7 +215,7 @@
done
-subsubsection {* Image and Inverse Image over Finite Sets *}
+text {* Image and Inverse Image over Finite Sets *}
lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
-- {* The image of a finite set is finite. *}
@@ -229,7 +267,7 @@
done
-subsubsection {* The finite UNION of finite sets *}
+text {* The finite UNION of finite sets *}
lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
by (induct set: Finites) simp_all
@@ -246,7 +284,7 @@
by (blast intro: finite_UN_I finite_subset)
-subsubsection {* Sigma of finite sets *}
+text {* Sigma of finite sets *}
lemma finite_SigmaI [simp]:
"finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
@@ -276,7 +314,7 @@
qed
-subsubsection {* The powerset of a finite set *}
+text {* The powerset of a finite set *}
lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
proof
@@ -289,6 +327,11 @@
by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
qed
+
+lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
+by(blast intro: finite_subset[OF subset_Pow_Union])
+
+
lemma finite_converse [iff]: "finite (r^-1) = finite r"
apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
apply simp
@@ -303,9 +346,8 @@
done
-subsubsection {* Finiteness of transitive closure *}
-
-text {* (Thanks to Sidi Ehmety) *}
+text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
+Ehmety) *}
lemma finite_Field: "finite r ==> finite (Field r)"
-- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
@@ -334,6 +376,442 @@
by (rule finite_SigmaI)
+subsection {* A fold functional for finite sets *}
+
+text {* The intended behaviour is
+@{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"}
+if @{text f} is associative-commutative. For an application of @{text fold}
+se the definitions of sums and products over finite sets.
+*}
+
+consts
+ foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
+
+inductive "foldSet f g e"
+intros
+emptyI [intro]: "({}, e) : foldSet f g e"
+insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk>
+ \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e"
+
+inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e"
+
+constdefs
+ fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
+ "fold f g e A == THE x. (A, x) : foldSet f g e"
+
+lemma Diff1_foldSet:
+ "(A - {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e"
+by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
+
+lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A"
+ by (induct set: foldSet) auto
+
+lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e"
+ by (induct set: Finites) auto
+
+
+subsubsection {* Commutative monoids *}
+
+locale ACf =
+ fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
+ assumes commute: "x \<cdot> y = y \<cdot> x"
+ and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+
+locale ACe = ACf +
+ fixes e :: 'a
+ assumes ident [simp]: "x \<cdot> e = x"
+
+lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+proof -
+ have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
+ also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
+ also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
+ finally show ?thesis .
+qed
+
+lemmas (in ACf) AC = assoc commute left_commute
+
+lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
+proof -
+ have "x \<cdot> e = x" by (rule ident)
+ thus ?thesis by (subst commute)
+qed
+
+subsubsection{*From @{term foldSet} to @{term fold}*}
+
+lemma (in ACf) foldSet_determ_aux:
+ "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
+ \<Longrightarrow> x' = x"
+proof (induct n)
+ case 0 thus ?case by auto
+next
+ case (Suc n)
+ have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
+ \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
+ and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
+ show ?case
+ proof cases
+ assume "EX k<n. h n = h k"
+ hence card': "A = h ` {i. i < n}"
+ using card by (auto simp:image_def less_Suc_eq)
+ show ?thesis by(rule IH[OF card' Afoldx Afoldy])
+ next
+ assume new: "\<not>(EX k<n. h n = h k)"
+ show ?thesis
+ proof (rule foldSet.cases[OF Afoldx])
+ assume "(A, x) = ({}, e)"
+ thus "x' = x" using Afoldy by (auto)
+ next
+ fix B b y
+ assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
+ and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
+ hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
+ show ?thesis
+ proof (rule foldSet.cases[OF Afoldy])
+ assume "(A,x') = ({}, e)"
+ thus ?thesis using A1 by auto
+ next
+ fix C c z
+ assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
+ and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
+ hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
+ let ?h = "%i. if h i = b then h n else h i"
+ have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
+(* move down? *)
+ have less: "B = ?h`{i. i<n}" (is "_ = ?r")
+ proof
+ show "B \<subseteq> ?r"
+ proof
+ fix u assume "u \<in> B"
+ hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
+ then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
+ using card by(auto simp:image_def)
+ show "u \<in> ?r"
+ proof cases
+ assume "i\<^isub>u < n"
+ thus ?thesis using unotb by(fastsimp)
+ next
+ assume "\<not> i\<^isub>u < n"
+ with below have [simp]: "i\<^isub>u = n" by arith
+ obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
+ using A1 card by blast
+ have "i\<^isub>k < n"
+ proof (rule ccontr)
+ assume "\<not> i\<^isub>k < n"
+ hence "i\<^isub>k = n" using i\<^isub>k by arith
+ thus False using unotb by simp
+ qed
+ thus ?thesis by(auto simp add:image_def)
+ qed
+ qed
+ next
+ show "?r \<subseteq> B"
+ proof
+ fix u assume "u \<in> ?r"
+ then obtain i\<^isub>u where below: "i\<^isub>u < n" and
+ or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
+ by(auto simp:image_def)
+ from or show "u \<in> B"
+ proof
+ assume [simp]: "b = h i\<^isub>u \<and> u = h n"
+ have "u \<in> A" using card by auto
+ moreover have "u \<noteq> b" using new below by auto
+ ultimately show "u \<in> B" using A1 by blast
+ next
+ assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
+ moreover hence "u \<in> A" using card below by auto
+ ultimately show "u \<in> B" using A1 by blast
+ qed
+ qed
+ qed
+ show ?thesis
+ proof cases
+ assume "b = c"
+ then moreover have "B = C" using A1 A2 notinB notinC by auto
+ ultimately show ?thesis using IH[OF less] y z x x' by auto
+ next
+ assume diff: "b \<noteq> c"
+ let ?D = "B - {c}"
+ have B: "B = insert c ?D" and C: "C = insert b ?D"
+ using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
+ have "finite ?D" using finA A1 by simp
+ then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
+ using finite_imp_foldSet by rules
+ moreover have cinB: "c \<in> B" using B by(auto)
+ ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
+ by(rule Diff1_foldSet)
+ hence "g c \<cdot> d = y" by(rule IH[OF less y])
+ moreover have "g b \<cdot> d = z"
+ proof (rule IH[OF _ z])
+ let ?h = "%i. if h i = c then h n else h i"
+ show "C = ?h`{i. i<n}" (is "_ = ?r")
+ proof
+ show "C \<subseteq> ?r"
+ proof
+ fix u assume "u \<in> C"
+ hence uinA: "u \<in> A" and unotc: "u \<noteq> c"
+ using A2 notinC by blast+
+ then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
+ using card by(auto simp:image_def)
+ show "u \<in> ?r"
+ proof cases
+ assume "i\<^isub>u < n"
+ thus ?thesis using unotc by(fastsimp)
+ next
+ assume "\<not> i\<^isub>u < n"
+ with below have [simp]: "i\<^isub>u = n" by arith
+ obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k"
+ using A2 card by blast
+ have "i\<^isub>k < n"
+ proof (rule ccontr)
+ assume "\<not> i\<^isub>k < n"
+ hence "i\<^isub>k = n" using i\<^isub>k by arith
+ thus False using unotc by simp
+ qed
+ thus ?thesis by(auto simp add:image_def)
+ qed
+ qed
+ next
+ show "?r \<subseteq> C"
+ proof
+ fix u assume "u \<in> ?r"
+ then obtain i\<^isub>u where below: "i\<^isub>u < n" and
+ or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
+ by(auto simp:image_def)
+ from or show "u \<in> C"
+ proof
+ assume [simp]: "c = h i\<^isub>u \<and> u = h n"
+ have "u \<in> A" using card by auto
+ moreover have "u \<noteq> c" using new below by auto
+ ultimately show "u \<in> C" using A2 by blast
+ next
+ assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
+ moreover hence "u \<in> A" using card below by auto
+ ultimately show "u \<in> C" using A2 by blast
+ qed
+ qed
+ qed
+ next
+ show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
+ by fastsimp
+ qed
+ ultimately show ?thesis using x x' by(auto simp:AC)
+ qed
+ qed
+ qed
+ qed
+qed
+
+(* The same proof, but using card
+lemma (in ACf) foldSet_determ_aux:
+ "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
+ \<Longrightarrow> x' = x"
+proof (induct n)
+ case 0 thus ?case by simp
+next
+ case (Suc n)
+ have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
+ \<Longrightarrow> x' = x" and card: "card A < Suc n"
+ and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
+ from card have "card A < n \<or> card A = n" by arith
+ thus ?case
+ proof
+ assume less: "card A < n"
+ show ?thesis by(rule IH[OF less Afoldx Afoldy])
+ next
+ assume cardA: "card A = n"
+ show ?thesis
+ proof (rule foldSet.cases[OF Afoldx])
+ assume "(A, x) = ({}, e)"
+ thus "x' = x" using Afoldy by (auto)
+ next
+ fix B b y
+ assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
+ and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
+ hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
+ show ?thesis
+ proof (rule foldSet.cases[OF Afoldy])
+ assume "(A,x') = ({}, e)"
+ thus ?thesis using A1 by auto
+ next
+ fix C c z
+ assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
+ and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
+ hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
+ have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
+ with cardA A1 notinB have less: "card B < n" by simp
+ show ?thesis
+ proof cases
+ assume "b = c"
+ then moreover have "B = C" using A1 A2 notinB notinC by auto
+ ultimately show ?thesis using IH[OF less] y z x x' by auto
+ next
+ assume diff: "b \<noteq> c"
+ let ?D = "B - {c}"
+ have B: "B = insert c ?D" and C: "C = insert b ?D"
+ using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
+ have "finite ?D" using finA A1 by simp
+ then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
+ using finite_imp_foldSet by rules
+ moreover have cinB: "c \<in> B" using B by(auto)
+ ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
+ by(rule Diff1_foldSet)
+ hence "g c \<cdot> d = y" by(rule IH[OF less y])
+ moreover have "g b \<cdot> d = z"
+ proof (rule IH[OF _ z])
+ show "card C < n" using C cardA A1 notinB finA cinB
+ by(auto simp:card_Diff1_less)
+ next
+ show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
+ by fastsimp
+ qed
+ ultimately show ?thesis using x x' by(auto simp:AC)
+ qed
+ qed
+ qed
+ qed
+qed
+*)
+
+lemma (in ACf) foldSet_determ:
+ "(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x"
+apply(frule foldSet_imp_finite)
+apply(simp add:finite_conv_nat_seg_image)
+apply(blast intro: foldSet_determ_aux [rule_format])
+done
+
+lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y"
+ by (unfold fold_def) (blast intro: foldSet_determ)
+
+text{* The base case for @{text fold}: *}
+
+lemma fold_empty [simp]: "fold f g e {} = e"
+ by (unfold fold_def) blast
+
+lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
+ ((insert x A, v) : foldSet f g e) =
+ (EX y. (A, y) : foldSet f g e & v = f (g x) y)"
+ apply auto
+ apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
+ apply (fastsimp dest: foldSet_imp_finite)
+ apply (blast intro: foldSet_determ)
+ done
+
+text{* The recursion equation for @{text fold}: *}
+
+lemma (in ACf) fold_insert[simp]:
+ "finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)"
+ apply (unfold fold_def)
+ apply (simp add: fold_insert_aux)
+ apply (rule the_equality)
+ apply (auto intro: finite_imp_foldSet
+ cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
+ done
+
+text{* Its definitional form: *}
+
+corollary (in ACf) fold_insert_def:
+ "\<lbrakk> F \<equiv> fold f g e; finite A; x \<notin> A \<rbrakk> \<Longrightarrow> F (insert x A) = f (g x) (F A)"
+by(simp)
+
+declare
+ empty_foldSetE [rule del] foldSet.intros [rule del]
+ -- {* Delete rules to do with @{text foldSet} relation. *}
+
+subsubsection{*Lemmas about @{text fold}*}
+
+lemma (in ACf) fold_commute:
+ "finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)"
+ apply (induct set: Finites, simp)
+ apply (simp add: left_commute)
+ done
+
+lemma (in ACf) fold_nest_Un_Int:
+ "finite A ==> finite B
+ ==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)"
+ apply (induct set: Finites, simp)
+ apply (simp add: fold_commute Int_insert_left insert_absorb)
+ done
+
+lemma (in ACf) fold_nest_Un_disjoint:
+ "finite A ==> finite B ==> A Int B = {}
+ ==> fold f g e (A Un B) = fold f g (fold f g e B) A"
+ by (simp add: fold_nest_Un_Int)
+
+lemma (in ACf) fold_reindex:
+assumes fin: "finite B"
+shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B"
+using fin apply (induct)
+ apply simp
+apply simp
+done
+
+lemma (in ACe) fold_Un_Int:
+ "finite A ==> finite B ==>
+ fold f g e A \<cdot> fold f g e B =
+ fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
+ apply (induct set: Finites, simp)
+ apply (simp add: AC insert_absorb Int_insert_left)
+ done
+
+corollary (in ACe) fold_Un_disjoint:
+ "finite A ==> finite B ==> A Int B = {} ==>
+ fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
+ by (simp add: fold_Un_Int)
+
+lemma (in ACe) fold_UN_disjoint:
+ "\<lbrakk> finite I; ALL i:I. finite (A i);
+ ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
+ \<Longrightarrow> fold f g e (UNION I A) =
+ fold f (%i. fold f g e (A i)) e I"
+ apply (induct set: Finites, simp, atomize)
+ apply (subgoal_tac "ALL i:F. x \<noteq> i")
+ prefer 2 apply blast
+ apply (subgoal_tac "A x Int UNION F A = {}")
+ prefer 2 apply blast
+ apply (simp add: fold_Un_disjoint)
+ done
+
+lemma (in ACf) fold_cong:
+ "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A"
+ apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g a C = fold f h a C")
+ apply simp
+ apply (erule finite_induct, simp)
+ apply (simp add: subset_insert_iff, clarify)
+ apply (subgoal_tac "finite C")
+ prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+ apply (subgoal_tac "C = insert x (C - {x})")
+ prefer 2 apply blast
+ apply (erule ssubst)
+ apply (drule spec)
+ apply (erule (1) notE impE)
+ apply (simp add: Ball_def del: insert_Diff_single)
+ done
+
+lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
+ fold f (%x. fold f (g x) e (B x)) e A =
+ fold f (split g) e (SIGMA x:A. B x)"
+apply (subst Sigma_def)
+apply (subst fold_UN_disjoint)
+ apply assumption
+ apply simp
+ apply blast
+apply (erule fold_cong)
+apply (subst fold_UN_disjoint)
+ apply simp
+ apply simp
+ apply blast
+apply (simp)
+done
+
+lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
+ fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
+apply (erule finite_induct)
+ apply simp
+apply (simp add:AC)
+done
+
+
subsection {* Finite cardinality *}
text {*
@@ -565,286 +1043,415 @@
apply (blast elim!: equalityE)
done
-text {*
- \medskip Relates to equivalence classes. Based on a theorem of
- F. Kammüller's. The @{prop "finite C"} premise is redundant.
-*}
+text {* Relates to equivalence classes. Based on a theorem of
+F. Kammüller's. *}
lemma dvd_partition:
- "finite C ==> finite (Union C) ==>
+ "finite (Union C) ==>
ALL c : C. k dvd card c ==>
(ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
k dvd card (Union C)"
+apply(frule finite_UnionD)
+apply(rotate_tac -1)
apply (induct set: Finites, simp_all, clarify)
apply (subst card_Un_disjoint)
apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
done
-subsection {* A fold functional for finite sets *}
+subsubsection {* Theorems about @{text "choose"} *}
text {*
- For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
- f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
+ \medskip Basic theorem about @{text "choose"}. By Florian
+ Kamm\"uller, tidied by LCP.
*}
-consts
- foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
-
-inductive "foldSet f e"
- intros
- emptyI [intro]: "({}, e) : foldSet f e"
- insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
-
-inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
-
-constdefs
- fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
- "fold f e A == THE x. (A, x) : foldSet f e"
-
-lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
-by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
-
-lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
- by (induct set: foldSet) auto
-
-lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
- by (induct set: Finites) auto
-
-
-subsubsection {* Left-commutative operations *}
-
-locale LC =
- fixes f :: "'b => 'a => 'a" (infixl "\<cdot>" 70)
- assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+lemma card_s_0_eq_empty:
+ "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
+ apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
+ apply (simp cong add: rev_conj_cong)
+ done
-lemma (in LC) foldSet_determ_aux:
- "ALL A x. card A < n --> (A, x) : foldSet f e -->
- (ALL y. (A, y) : foldSet f e --> y = x)"
- apply (induct n)
- apply (auto simp add: less_Suc_eq)
- apply (erule foldSet.cases, blast)
- apply (erule foldSet.cases, blast, clarify)
- txt {* force simplification of @{text "card A < card (insert ...)"}. *}
- apply (erule rev_mp)
- apply (simp add: less_Suc_eq_le)
- apply (rule impI)
- apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
- apply (subgoal_tac "Aa = Ab")
- prefer 2 apply (blast elim!: equalityE, blast)
- txt {* case @{prop "xa \<notin> xb"}. *}
- apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
- prefer 2 apply (blast elim!: equalityE, clarify)
- apply (subgoal_tac "Aa = insert xb Ab - {xa}")
- prefer 2 apply blast
- apply (subgoal_tac "card Aa <= card Ab")
- prefer 2
- apply (rule Suc_le_mono [THEN subst])
- apply (simp add: card_Suc_Diff1)
- apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
- apply (blast intro: foldSet_imp_finite finite_Diff)
- apply (frule (1) Diff1_foldSet)
- apply (subgoal_tac "ya = f xb x")
- prefer 2 apply (blast del: equalityCE)
- apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
- prefer 2 apply simp
- apply (subgoal_tac "yb = f xa x")
- prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
- apply (simp (no_asm_simp) add: left_commute)
+lemma choose_deconstruct: "finite M ==> x \<notin> M
+ ==> {s. s <= insert x M & card(s) = Suc k}
+ = {s. s <= M & card(s) = Suc k} Un
+ {s. EX t. t <= M & card(t) = k & s = insert x t}"
+ apply safe
+ apply (auto intro: finite_subset [THEN card_insert_disjoint])
+ apply (drule_tac x = "xa - {x}" in spec)
+ apply (subgoal_tac "x \<notin> xa", auto)
+ apply (erule rev_mp, subst card_Diff_singleton)
+ apply (auto intro: finite_subset)
done
-lemma (in LC) foldSet_determ:
- "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
-by (blast intro: foldSet_determ_aux [rule_format])
+lemma card_inj_on_le:
+ "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
+apply (subgoal_tac "finite A")
+ apply (force intro: card_mono simp add: card_image [symmetric])
+apply (blast intro: finite_imageD dest: finite_subset)
+done
-lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
- by (unfold fold_def) (blast intro: foldSet_determ)
+lemma card_bij_eq:
+ "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
+ finite A; finite B |] ==> card A = card B"
+ by (auto intro: le_anti_sym card_inj_on_le)
-lemma fold_empty [simp]: "fold f e {} = e"
- by (unfold fold_def) blast
-
-lemma (in LC) fold_insert_aux: "x \<notin> A ==>
- ((insert x A, v) : foldSet f e) =
- (EX y. (A, y) : foldSet f e & v = f x y)"
- apply auto
- apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
- apply (fastsimp dest: foldSet_imp_finite)
- apply (blast intro: foldSet_determ)
+text{*There are as many subsets of @{term A} having cardinality @{term k}
+ as there are sets obtained from the former by inserting a fixed element
+ @{term x} into each.*}
+lemma constr_bij:
+ "[|finite A; x \<notin> A|] ==>
+ card {B. EX C. C <= A & card(C) = k & B = insert x C} =
+ card {B. B <= A & card(B) = k}"
+ apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
+ apply (auto elim!: equalityE simp add: inj_on_def)
+ apply (subst Diff_insert0, auto)
+ txt {* finiteness of the two sets *}
+ apply (rule_tac [2] B = "Pow (A)" in finite_subset)
+ apply (rule_tac B = "Pow (insert x A)" in finite_subset)
+ apply fast+
done
-lemma (in LC) fold_insert[simp]:
- "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
- apply (unfold fold_def)
- apply (simp add: fold_insert_aux)
- apply (rule the_equality)
- apply (auto intro: finite_imp_foldSet
- cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
- done
+text {*
+ Main theorem: combinatorial statement about number of subsets of a set.
+*}
-corollary (in LC) fold_insert_def:
- "\<lbrakk> F \<equiv> fold f e; finite A; x \<notin> A \<rbrakk> \<Longrightarrow> F (insert x A) = f x (F A)"
-by(simp)
-
-lemma (in LC) fold_commute:
- "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
- apply (induct set: Finites, simp)
- apply (simp add: left_commute)
- done
-
-lemma (in LC) fold_nest_Un_Int:
- "finite A ==> finite B
- ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
- apply (induct set: Finites, simp)
- apply (simp add: fold_commute Int_insert_left insert_absorb)
+lemma n_sub_lemma:
+ "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
+ apply (induct k)
+ apply (simp add: card_s_0_eq_empty, atomize)
+ apply (rotate_tac -1, erule finite_induct)
+ apply (simp_all (no_asm_simp) cong add: conj_cong
+ add: card_s_0_eq_empty choose_deconstruct)
+ apply (subst card_Un_disjoint)
+ prefer 4 apply (force simp add: constr_bij)
+ prefer 3 apply force
+ prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
+ finite_subset [of _ "Pow (insert x F)", standard])
+ apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
done
-lemma (in LC) fold_nest_Un_disjoint:
- "finite A ==> finite B ==> A Int B = {}
- ==> fold f e (A Un B) = fold f (fold f e B) A"
- by (simp add: fold_nest_Un_Int)
+theorem n_subsets:
+ "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
+ by (simp add: n_sub_lemma)
+
+
+subsection{* A fold functional for non-empty sets *}
+
+text{* Does not require start value. *}
-declare foldSet_imp_finite [simp del]
- empty_foldSetE [rule del] foldSet.intros [rule del]
- -- {* Delete rules to do with @{text foldSet} relation. *}
+consts
+ foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
+
+inductive "foldSet1 f"
+intros
+foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f"
+foldSet1_insertI [intro]:
+ "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
+ \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
-lemma (in LC) o_closed: "LC(f o g)"
-by(insert prems, simp add:LC_def)
+constdefs
+ fold1 :: "('a => 'a => 'a) => 'a set => 'a"
+ "fold1 f A == THE x. (A, x) : foldSet1 f"
+
+lemma foldSet1_nonempty:
+ "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
+by(erule foldSet1.cases, simp_all)
+
-lemma (in LC) fold_reindex:
-assumes fin: "finite B"
-shows "inj_on g B \<Longrightarrow> fold f e (g ` B) = fold (f \<circ> g) e B"
-using fin apply (induct)
- apply simp
-apply simp
-apply(simp add:LC.fold_insert[OF o_closed])
+inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
+
+lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
+apply(rule iffI)
+ prefer 2 apply fast
+apply (erule foldSet1.cases)
+ apply blast
+apply (erule foldSet1.cases)
+ apply blast
+apply blast
done
-subsubsection {* Commutative monoids *}
-
-text {*
- We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
- instead of @{text "'b => 'a => 'a"}.
-*}
+lemma Diff1_foldSet1:
+ "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
+by (erule insert_Diff [THEN subst], rule foldSet1.intros,
+ auto dest!:foldSet1_nonempty)
-locale ACf =
- fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
- assumes commute: "x \<cdot> y = y \<cdot> x"
- and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A"
+ by (induct set: foldSet1) auto
-locale ACe = ACf +
- fixes e :: 'a
- assumes ident [simp]: "x \<cdot> e = x"
+lemma finite_nonempty_imp_foldSet1:
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
+ by (induct set: Finites) auto
-lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-proof -
- have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
- also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
- also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
- finally show ?thesis .
-qed
-
-corollary (in ACf) LC: "LC f"
-by(simp add:LC_def left_commute)
-
-lemmas (in ACf) AC = assoc commute left_commute
-
-lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
-proof -
- have "x \<cdot> e = x" by (rule ident)
- thus ?thesis by (subst commute)
+lemma (in ACf) foldSet1_determ_aux:
+ "!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x"
+proof (induct n)
+ case 0 thus ?case by simp
+next
+ case (Suc n)
+ have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk>
+ \<Longrightarrow> y = x" and card: "card A < Suc n"
+ and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" .
+ from card have "card A < n \<or> card A = n" by arith
+ thus ?case
+ proof
+ assume less: "card A < n"
+ show ?thesis by(rule IH[OF less Afoldx Afoldy])
+ next
+ assume cardA: "card A = n"
+ show ?thesis
+ proof (rule foldSet1.cases[OF Afoldx])
+ fix a assume "(A, x) = ({a}, a)"
+ thus "y = x" using Afoldy by (simp add:foldSet1_sing)
+ next
+ fix Ax ax x'
+ assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')"
+ and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax"
+ and Axnon: "Ax \<noteq> {}"
+ hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto
+ show ?thesis
+ proof (rule foldSet1.cases[OF Afoldy])
+ fix ay assume "(A, y) = ({ay}, ay)"
+ thus ?thesis using eq1 x' Axnon notinx
+ by (fastsimp simp:foldSet1_sing)
+ next
+ fix Ay ay y'
+ assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')"
+ and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay"
+ and Aynon: "Ay \<noteq> {}"
+ hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto
+ have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx])
+ with cardA A1 notinx have less: "card Ax < n" by simp
+ show ?thesis
+ proof cases
+ assume "ax = ay"
+ then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto
+ ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto
+ next
+ assume diff: "ax \<noteq> ay"
+ let ?B = "Ax - {ay}"
+ have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B"
+ using A1 A2 notinx notiny diff by(blast elim!:equalityE)+
+ show ?thesis
+ proof cases
+ assume "?B = {}"
+ with Ax Ay show ?thesis using x' y' x y by(simp add:commute)
+ next
+ assume Bnon: "?B \<noteq> {}"
+ moreover have "finite ?B" using finA A1 by simp
+ ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f"
+ using finite_nonempty_imp_foldSet1 by(blast)
+ moreover have ayinAx: "ay \<in> Ax" using Ax by(auto)
+ ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1)
+ hence "ay\<cdot>b = x'" by(rule IH[OF less x'])
+ moreover have "ax\<cdot>b = y'"
+ proof (rule IH[OF _ y'])
+ show "card Ay < n" using Ay cardA A1 notinx finA ayinAx
+ by(auto simp:card_Diff1_less)
+ next
+ show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon
+ by fastsimp
+ qed
+ ultimately show ?thesis using x y by(auto simp:AC)
+ qed
+ qed
+ qed
+ qed
+ qed
qed
-lemma (in ACe) fold_o_Un_Int:
- "finite A ==> finite B ==>
- fold (f o g) e A \<cdot> fold (f o g) e B =
- fold (f o g) e (A Un B) \<cdot> fold (f o g) e (A Int B)"
- apply (induct set: Finites, simp)
- apply (simp add: AC insert_absorb Int_insert_left
- LC.fold_insert [OF LC.intro])
- done
+
+lemma (in ACf) foldSet1_determ:
+ "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
+by (blast intro: foldSet1_determ_aux [rule_format])
+
+lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
+ by (unfold fold1_def) (blast intro: foldSet1_determ)
+
+lemma fold1_singleton: "fold1 f {a} = a"
+ by (unfold fold1_def) blast
-corollary (in ACe) fold_Un_Int:
- "finite A ==> finite B ==>
- fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
- by (rule fold_o_Un_Int[where g = id,simplified])
+lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow>
+ ((insert x A, v) : foldSet1 f) =
+ (EX y. (A, y) : foldSet1 f & v = f x y)"
+apply auto
+apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
+ apply (fastsimp dest: foldSet1_imp_finite)
+ apply blast
+apply (blast intro: foldSet1_determ)
+done
-corollary (in ACe) fold_o_Un_disjoint:
- "finite A ==> finite B ==> A Int B = {} ==>
- fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
- by (simp add: fold_o_Un_Int)
+lemma (in ACf) fold1_insert:
+ "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
+apply (unfold fold1_def)
+apply (simp add: foldSet1_insert_aux)
+apply (rule the_equality)
+apply (auto intro: finite_nonempty_imp_foldSet1
+ cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
+done
-corollary (in ACe) fold_Un_disjoint:
- "finite A ==> finite B ==> A Int B = {} ==>
- fold f e (A Un B) = fold f e A \<cdot> fold f e B"
- by (simp add: fold_Un_Int)
+locale ACIf = ACf +
+ assumes idem: "x \<cdot> x = x"
-lemma (in ACe) fold_o_UN_disjoint:
- "\<lbrakk> finite I; ALL i:I. finite (A i);
- ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
- \<Longrightarrow> fold (f o g) e (UNION I A) =
- fold (f o (%i. fold (f o g) e (A i))) e I"
- apply (induct set: Finites, simp, atomize)
- apply (subgoal_tac "ALL i:F. x \<noteq> i")
- prefer 2 apply blast
- apply (subgoal_tac "A x Int UNION F A = {}")
- prefer 2 apply blast
- apply (simp add: fold_o_Un_disjoint LC.fold_insert[OF LC.o_closed[OF LC]])
- done
+lemma (in ACIf) fold1_insert2:
+assumes finA: "finite A" and nonA: "A \<noteq> {}"
+shows "fold1 f (insert a A) = f a (fold1 f A)"
+proof cases
+ assume "a \<in> A"
+ then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
+ by(blast dest: mk_disjoint_insert)
+ show ?thesis
+ proof cases
+ assume "B = {}"
+ thus ?thesis using A by(simp add:idem fold1_singleton)
+ next
+ assume nonB: "B \<noteq> {}"
+ from finA A have finB: "finite B" by(blast intro: finite_subset)
+ have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
+ also have "\<dots> = f a (fold1 f B)"
+ using finB nonB disj by(simp add: fold1_insert)
+ also have "\<dots> = f a (fold1 f A)"
+ using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric])
+ finally show ?thesis .
+ qed
+next
+ assume "a \<notin> A"
+ with finA nonA show ?thesis by(simp add:fold1_insert)
+qed
+
-lemma (in ACf) fold_cong:
- "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold (f o g) a A = fold (f o h) a A"
- apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold (f o g) a C = fold (f o h) a C")
- apply simp
- apply (erule finite_induct, simp)
- apply (simp add: subset_insert_iff, clarify)
- apply (subgoal_tac "finite C")
- prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
- apply (subgoal_tac "C = insert x (C - {x})")
- prefer 2 apply blast
- apply (erule ssubst)
- apply (drule spec)
- apply (erule (1) notE impE)
- apply (fold o_def)
- apply (simp add: Ball_def LC.fold_insert[OF LC.o_closed[OF LC]]
- del: insert_Diff_single)
- done
+text{* Now the recursion rules for definitions: *}
+
+lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
+by(simp add:fold1_singleton)
+
+lemma (in ACf) fold1_insert_def:
+ "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
+by(simp add:fold1_insert)
+
+lemma (in ACIf) fold1_insert2_def:
+ "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
+by(simp add:fold1_insert2)
+
-lemma (in ACe) fold_o_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
-fold (f o (%x. fold (f o g x) e (B x))) e A =
-fold (f o (split g)) e (SIGMA x:A. B x)"
-apply (subst Sigma_def)
-apply (subst fold_o_UN_disjoint)
- apply assumption
- apply simp
- apply blast
-apply (erule fold_cong)
-apply (subst fold_o_UN_disjoint)
- apply simp
- apply simp
- apply blast
-apply (simp add: LC.fold_insert [OF LC.o_closed[OF LC]])
-apply(simp add:o_def)
+subsection{*Min and Max*}
+
+text{* As an application of @{text fold1} we define the minimal and
+maximal element of a (non-empty) set over a linear order. First we
+show that @{text min} and @{text max} are ACI: *}
+
+lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
+apply(rule ACf.intro)
+apply(auto simp:min_def)
+done
+
+lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
+apply(rule ACIf.intro[OF ACf_min])
+apply(rule ACIf_axioms.intro)
+apply(auto simp:min_def)
done
-lemma (in ACe) fold_o_distrib: "finite A \<Longrightarrow>
- fold (f o (%x. f (g x) (h x))) e A =
- f (fold (f o g) e A) (fold (f o h) e A)"
-apply (erule finite_induct)
- apply simp
-apply(simp add: LC.fold_insert[OF LC.o_closed[OF LC]] del:o_apply)
-apply(subgoal_tac "(%x. f(g x)) = (%u ua. f ua (g u))")
- prefer 2 apply(rule ext, rule ext, simp add:AC)
-apply(subgoal_tac "(%x. f(h x)) = (%u ua. f ua (h u))")
- prefer 2 apply(rule ext, rule ext, simp add:AC)
-apply (simp add:AC o_def)
+lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
+apply(rule ACf.intro)
+apply(auto simp:max_def)
+done
+
+lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
+apply(rule ACIf.intro[OF ACf_max])
+apply(rule ACIf_axioms.intro)
+apply(auto simp:max_def)
done
+text{* Now we make the definitions: *}
+
+constdefs
+ Min :: "('a::linorder)set => 'a"
+ "Min == fold1 min"
+
+ Max :: "('a::linorder)set => 'a"
+ "Max == fold1 max"
+
+text{* Now we instantiate the recursiuon equations and declare them
+simplification rules: *}
+
+declare
+ fold1_singleton_def[OF Min_def, simp]
+ ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp]
+ fold1_singleton_def[OF Max_def, simp]
+ ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
+
+text{* Now we prove some properties by induction: *}
+
+lemma Min_in [simp]:
+ assumes a: "finite S"
+ shows "S \<noteq> {} \<Longrightarrow> Min S \<in> S"
+using a
+proof induct
+ case empty thus ?case by simp
+next
+ case (insert x S)
+ show ?case
+ proof cases
+ assume "S = {}" thus ?thesis by simp
+ next
+ assume "S \<noteq> {}" thus ?thesis using insert by (simp add:min_def)
+ qed
+qed
+
+lemma Min_le [simp]:
+ assumes a: "finite S"
+ shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> Min S \<le> x"
+using a
+proof induct
+ case empty thus ?case by simp
+next
+ case (insert y S)
+ show ?case
+ proof cases
+ assume "S = {}" thus ?thesis using insert by simp
+ next
+ assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:min_def)
+ qed
+qed
+
+lemma Max_in [simp]:
+ assumes a: "finite S"
+ shows "S \<noteq> {} \<Longrightarrow> Max S \<in> S"
+using a
+proof induct
+ case empty thus ?case by simp
+next
+ case (insert x S)
+ show ?case
+ proof cases
+ assume "S = {}" thus ?thesis by simp
+ next
+ assume "S \<noteq> {}" thus ?thesis using insert by (simp add:max_def)
+ qed
+qed
+
+lemma Max_le [simp]:
+ assumes a: "finite S"
+ shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> x \<le> Max S"
+using a
+proof induct
+ case empty thus ?case by simp
+next
+ case (insert y S)
+ show ?case
+ proof cases
+ assume "S = {}" thus ?thesis using insert by simp
+ next
+ assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def)
+ qed
+qed
+
subsection {* Generalized summation over a set *}
constdefs
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
- "setsum f A == if finite A then fold (op + o f) 0 A else 0"
+ "setsum f A == if finite A then fold (op +) f 0 A else 0"
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
written @{text"\<Sum>x\<in>A. e"}. *}
@@ -874,14 +1481,26 @@
"SUM x|P. t" => "setsum (%x. t) {x. P}"
"\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
+text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
+
+syntax
+ "_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\<Sum>_" [1000] 999)
+
+parse_translation {*
+ let
+ fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
+ in [("_Setsum", Setsum_tr)] end;
+*}
+
print_translation {*
let
- fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] =
- (if x<>y then raise Match
- else let val x' = Syntax.mark_bound x
- val t' = subst_bound(x',t)
- val P' = subst_bound(x',P)
- in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end)
+ fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
+ | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] =
+ if x<>y then raise Match
+ else let val x' = Syntax.mark_bound x
+ val t' = subst_bound(x',t)
+ val P' = subst_bound(x',P)
+ in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
in
[("setsum", setsum_tr')]
end
@@ -895,38 +1514,34 @@
lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
-corollary LC_add_o: "LC(op + o f :: 'a \<Rightarrow> 'b::comm_monoid_add \<Rightarrow> 'b)"
-by(rule LC.o_closed[OF ACf.LC[OF ACf_add]])
-
lemma setsum_empty [simp]: "setsum f {} = 0"
by (simp add: setsum_def)
lemma setsum_insert [simp]:
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
- by (simp add: setsum_def LC.fold_insert [OF LC_add_o])
+ by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
lemma setsum_reindex:
- "finite B ==> inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
-by (simp add: setsum_def LC.fold_reindex[OF LC_add_o] o_assoc)
+ "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
+by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
lemma setsum_reindex_id:
- "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
-by (auto simp add: setsum_reindex id_o)
+ "inj_on f B ==> setsum f B = setsum id (f ` B)"
+by (auto simp add: setsum_reindex)
lemma setsum_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
lemma setsum_reindex_cong:
- "[|finite A; inj_on f A; B = f ` A; !!a. g a = h (f a)|]
+ "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|]
==> setsum h B = setsum g A"
by (simp add: setsum_reindex cong: setsum_cong)
lemma setsum_0: "setsum (%i. 0) A = 0"
- apply (case_tac "finite A")
- prefer 2 apply (simp add: setsum_def)
- apply (erule finite_induct, auto)
- done
+apply (clarsimp simp: setsum_def)
+apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
+done
lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
@@ -938,10 +1553,10 @@
-- {* Could allow many @{text "card"} proofs to be simplified. *}
by (induct set: Finites) auto
-lemma setsum_Un_Int: "finite A ==> finite B
- ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
+lemma setsum_Un_Int: "finite A ==> finite B ==>
+ setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-by(simp add: setsum_def ACe.fold_o_Un_Int[OF ACe_add,symmetric])
+by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
lemma setsum_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
@@ -951,7 +1566,7 @@
"finite I ==> (ALL i:I. finite (A i)) ==>
(ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
-by(simp add: setsum_def ACe.fold_o_UN_disjoint[OF ACe_add] cong: setsum_cong)
+by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
lemma setsum_Union_disjoint:
@@ -965,7 +1580,7 @@
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
(\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
-by(simp add:setsum_def ACe.fold_o_Sigma[OF ACe_add] split_def cong:setsum_cong)
+by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
lemma setsum_cartesian_product: "finite A ==> finite B ==>
(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) =
@@ -973,7 +1588,7 @@
by (erule setsum_Sigma, auto)
lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
-by(simp add:setsum_def ACe.fold_o_distrib[OF ACe_add])
+by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
subsubsection {* Properties in more restricted classes of structures *}
@@ -1198,7 +1813,7 @@
constdefs
setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
- "setprod f A == if finite A then fold (op * o f) 1 A else 1"
+ "setprod f A == if finite A then fold (op *) f 1 A else 1"
syntax
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
@@ -1210,6 +1825,23 @@
translations
"\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}
+syntax
+ "_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\<Prod>_" [1000] 999)
+
+parse_translation {*
+ let
+ fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
+ in [("_Setprod", Setprod_tr)] end;
+*}
+print_translation {*
+let fun setprod_tr' [Abs(x,Tx,t), A] =
+ if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
+in
+[("setprod", setprod_tr')]
+end
+*}
+
+
text{* Instantiation of locales: *}
lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
@@ -1218,31 +1850,27 @@
lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
-corollary LC_mult_o: "LC(op * o f :: 'a \<Rightarrow> 'b::comm_monoid_mult \<Rightarrow> 'b)"
-by(rule LC.o_closed[OF ACf.LC[OF ACf_mult]])
-
lemma setprod_empty [simp]: "setprod f {} = 1"
by (auto simp add: setprod_def)
lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
setprod f (insert a A) = f a * setprod f A"
-by (simp add: setprod_def LC.fold_insert [OF LC_mult_o])
+by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
lemma setprod_reindex:
- "finite B ==> inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
-by (simp add: setprod_def LC.fold_reindex[OF LC_mult_o] o_assoc)
+ "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
+by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
-lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
- setprod f B = setprod id (f ` B)"
-by (auto simp add: setprod_reindex id_o)
+lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
+by (auto simp add: setprod_reindex)
lemma setprod_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
-lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
+lemma setprod_reindex_cong: "inj_on f A ==>
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
- by (frule setprod_reindex, assumption, simp)
+ by (frule setprod_reindex, simp)
lemma setprod_1: "setprod (%i. 1) A = 1"
@@ -1259,7 +1887,7 @@
lemma setprod_Un_Int: "finite A ==> finite B
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
-by(simp add: setprod_def ACe.fold_o_Un_Int[OF ACe_mult,symmetric])
+by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
lemma setprod_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
@@ -1269,7 +1897,7 @@
"finite I ==> (ALL i:I. finite (A i)) ==>
(ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
-by(simp add: setprod_def ACe.fold_o_UN_disjoint[OF ACe_mult] cong: setprod_cong)
+by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
lemma setprod_Union_disjoint:
"finite C ==> (ALL A:C. finite A) ==>
@@ -1282,7 +1910,7 @@
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
(\<Prod>x:A. (\<Prod>y: B x. f x y)) =
(\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
-by(simp add:setprod_def ACe.fold_o_Sigma[OF ACe_mult] split_def cong:setprod_cong)
+by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
lemma setprod_cartesian_product: "finite A ==> finite B ==>
(\<Prod>x:A. (\<Prod>y: B. f x y)) =
@@ -1291,7 +1919,7 @@
lemma setprod_timesf:
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
-by(simp add:setprod_def ACe.fold_o_distrib[OF ACe_mult])
+by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
subsubsection {* Properties in more restricted classes of structures *}
@@ -1392,319 +2020,4 @@
apply (subst divide_inverse, auto)
done
-
-subsection{* Min and Max of finite linearly ordered sets *}
-
-consts
- foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
-
-inductive "foldSet1 f"
-intros
-fold1_singletonI [intro]: "({a}, a) : foldSet1 f"
-fold1_insertI [intro]:
- "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
- \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
-
-constdefs
- fold1 :: "('a => 'a => 'a) => 'a set => 'a"
- "fold1 f A == THE x. (A, x) : foldSet1 f"
-
-lemma foldSet1_nonempty:
- "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
-by(erule foldSet1.cases, simp_all)
-
-
-inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
-
-lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
-apply(rule iffI)
- prefer 2 apply fast
-apply (erule foldSet1.cases)
- apply blast
-apply (erule foldSet1.cases)
- apply blast
-apply blast
-done
-
-lemma Diff1_foldSet1:
- "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
-by (erule insert_Diff [THEN subst], rule foldSet1.intros,
- auto dest!:foldSet1_nonempty)
-
-lemma foldSet_imp_finite [simp]: "(A, x) : foldSet1 f ==> finite A"
- by (induct set: foldSet1) auto
-
-lemma finite_nonempty_imp_foldSet1:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
- by (induct set: Finites) auto
-
-lemma lem: "(A \<subseteq> {a}) = (A = {} \<or> A = {a})"
-by blast
-
-(* FIXME structured proof to avoid ML hack and speed things up *)
-ML"simp_depth_limit := 3"
-lemma (in ACf) foldSet1_determ_aux:
- "ALL A x. card A < n --> (A, x) : foldSet1 f -->
- (ALL y. (A, y) : foldSet1 f --> y = x)"
-apply (induct n)
- apply (auto simp add: less_Suc_eq)
-apply (erule foldSet1.cases)
- apply (simp add:foldSet1_sing)
-apply (erule foldSet1.cases)
- apply (fastsimp simp:foldSet1_sing lem)
-apply (clarify)
- txt {* force simplification of @{text "card A < card (insert ...)"}. *}
-apply (erule rev_mp)
-apply (simp add: less_Suc_eq_le)
-apply (rule impI)
-apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
- apply (subgoal_tac "Aa = Ab")
- prefer 2 apply (blast elim!: equalityE, blast)
- txt {* case @{prop "xa \<notin> xb"}. *}
-apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
- prefer 2 apply (blast elim!: equalityE, clarify)
-apply (subgoal_tac "Aa = insert xb Ab - {xa}")
- prefer 2 apply blast
-apply (subgoal_tac "card Aa <= card Ab")
- prefer 2
- apply (rule Suc_le_mono [THEN subst])
- apply (simp add: card_Suc_Diff1)
-apply(case_tac "Aa - {xb} = {}")
- apply(subgoal_tac "Aa = {xb}")
- prefer 2 apply (fast elim!: equalityE)
- apply(subgoal_tac "Ab = {xa}")
- prefer 2 apply (fast elim!: equalityE)
- apply (simp add:insert_Diff_if AC)
-apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
- apply (blast intro: foldSet_imp_finite finite_Diff)
- apply assumption
-apply (frule (1) Diff1_foldSet1)
-apply (subgoal_tac "ya = f xb x")
- prefer 2 apply (blast del: equalityCE)
-apply (subgoal_tac "(Ab - {xa}, x) : foldSet1 f")
- prefer 2 apply (simp)
-apply (subgoal_tac "yb = f xa x")
- prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet1)
-apply (simp (no_asm_simp) add: left_commute)
-done
-ML"simp_depth_limit := 1000"
-
-lemma (in ACf) foldSet1_determ:
- "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
-by (blast intro: foldSet1_determ_aux [rule_format])
-
-lemma (in ACf) fold1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
- by (unfold fold1_def) (blast intro: foldSet1_determ)
-
-lemma fold1_singleton [simp]: "fold1 f {a} = a"
- by (unfold fold1_def) blast
-
-lemma (in ACf) fold1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow>
- ((insert x A, v) : foldSet1 f) =
- (EX y. (A, y) : foldSet1 f & v = f x y)"
-apply auto
-apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
- apply (fastsimp dest: foldSet_imp_finite)
- apply blast
-apply (blast intro: foldSet1_determ)
-done
-
-lemma (in ACf) fold1_insert:
- "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
-apply (unfold fold1_def)
-apply (simp add: fold1_insert_aux)
-apply (rule the_equality)
-apply (auto intro: finite_nonempty_imp_foldSet1
- cong add: conj_cong simp add: fold1_def [symmetric] fold1_equality)
-done
-
-locale ACIf = ACf +
- assumes idem: "x \<cdot> x = x"
-
-lemma (in ACIf) fold1_insert2:
-assumes finA: "finite A" and nonA: "A \<noteq> {}"
-shows "fold1 f (insert a A) = f a (fold1 f A)"
-proof cases
- assume "a \<in> A"
- then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
- by(blast dest: mk_disjoint_insert)
- show ?thesis
- proof cases
- assume "B = {}"
- thus ?thesis using A by(simp add:idem)
- next
- assume nonB: "B \<noteq> {}"
- from finA A have finB: "finite B" by(blast intro: finite_subset)
- have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
- also have "\<dots> = f a (fold1 f B)"
- using finB nonB disj by(simp add: fold1_insert)
- also have "\<dots> = f a (fold1 f A)"
- using A finB nonB disj by(simp add: idem fold1_insert assoc[symmetric])
- finally show ?thesis .
- qed
-next
- assume "a \<notin> A"
- with finA nonA show ?thesis by(simp add:fold1_insert)
-qed
-
-text{* Seemed easier to define directly than via fold. *}
-
-(* FIXME define Min/Max via fold1 *)
-
-lemma ex_Max: fixes S :: "('a::linorder)set"
- assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
-using fin
-proof (induct)
- case empty thus ?case by simp
-next
- case (insert x S)
- show ?case
- proof (cases)
- assume "S = {}" thus ?thesis by simp
- next
- assume nonempty: "S \<noteq> {}"
- then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
- show ?thesis
- proof (cases)
- assume "x \<le> m" thus ?thesis using m by blast
- next
- assume "~ x \<le> m" thus ?thesis using m
- by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
- qed
- qed
-qed
-
-lemma ex_Min: fixes S :: "('a::linorder)set"
- assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
-using fin
-proof (induct)
- case empty thus ?case by simp
-next
- case (insert x S)
- show ?case
- proof (cases)
- assume "S = {}" thus ?thesis by simp
- next
- assume nonempty: "S \<noteq> {}"
- then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
- show ?thesis
- proof (cases)
- assume "m \<le> x" thus ?thesis using m by blast
- next
- assume "~ m \<le> x" thus ?thesis using m
- by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
- qed
- qed
-qed
-
-constdefs
- Min :: "('a::linorder)set => 'a"
- "Min S == THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
-
- Max :: "('a::linorder)set => 'a"
- "Max S == THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
-
-lemma Min [simp]:
- assumes a: "finite S" "S \<noteq> {}"
- shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
-proof (unfold Min_def, rule theI')
- show "\<exists>!m. ?P m"
- proof (rule ex_ex1I)
- show "\<exists>m. ?P m" using ex_Min[OF a] by blast
- next
- fix m1 m2 assume "?P m1" and "?P m2"
- thus "m1 = m2" by (blast dest: order_antisym)
- qed
-qed
-
-lemma Max [simp]:
- assumes a: "finite S" "S \<noteq> {}"
- shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
-proof (unfold Max_def, rule theI')
- show "\<exists>!m. ?P m"
- proof (rule ex_ex1I)
- show "\<exists>m. ?P m" using ex_Max[OF a] by blast
- next
- fix m1 m2 assume "?P m1" "?P m2"
- thus "m1 = m2" by (blast dest: order_antisym)
- qed
-qed
-
-
-subsection {* Theorems about @{text "choose"} *}
-
-text {*
- \medskip Basic theorem about @{text "choose"}. By Florian
- Kamm\"uller, tidied by LCP.
-*}
-
-lemma card_s_0_eq_empty:
- "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
- apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
- apply (simp cong add: rev_conj_cong)
- done
-
-lemma choose_deconstruct: "finite M ==> x \<notin> M
- ==> {s. s <= insert x M & card(s) = Suc k}
- = {s. s <= M & card(s) = Suc k} Un
- {s. EX t. t <= M & card(t) = k & s = insert x t}"
- apply safe
- apply (auto intro: finite_subset [THEN card_insert_disjoint])
- apply (drule_tac x = "xa - {x}" in spec)
- apply (subgoal_tac "x \<notin> xa", auto)
- apply (erule rev_mp, subst card_Diff_singleton)
- apply (auto intro: finite_subset)
- done
-
-lemma card_inj_on_le:
- "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
-apply (subgoal_tac "finite A")
- apply (force intro: card_mono simp add: card_image [symmetric])
-apply (blast intro: finite_imageD dest: finite_subset)
-done
-
-lemma card_bij_eq:
- "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
- finite A; finite B |] ==> card A = card B"
- by (auto intro: le_anti_sym card_inj_on_le)
-
-text{*There are as many subsets of @{term A} having cardinality @{term k}
- as there are sets obtained from the former by inserting a fixed element
- @{term x} into each.*}
-lemma constr_bij:
- "[|finite A; x \<notin> A|] ==>
- card {B. EX C. C <= A & card(C) = k & B = insert x C} =
- card {B. B <= A & card(B) = k}"
- apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
- apply (auto elim!: equalityE simp add: inj_on_def)
- apply (subst Diff_insert0, auto)
- txt {* finiteness of the two sets *}
- apply (rule_tac [2] B = "Pow (A)" in finite_subset)
- apply (rule_tac B = "Pow (insert x A)" in finite_subset)
- apply fast+
- done
-
-text {*
- Main theorem: combinatorial statement about number of subsets of a set.
-*}
-
-lemma n_sub_lemma:
- "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
- apply (induct k)
- apply (simp add: card_s_0_eq_empty, atomize)
- apply (rotate_tac -1, erule finite_induct)
- apply (simp_all (no_asm_simp) cong add: conj_cong
- add: card_s_0_eq_empty choose_deconstruct)
- apply (subst card_Un_disjoint)
- prefer 4 apply (force simp add: constr_bij)
- prefer 3 apply force
- prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
- finite_subset [of _ "Pow (insert x F)", standard])
- apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
- done
-
-theorem n_subsets:
- "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
- by (simp add: n_sub_lemma)
-
end
--- a/src/HOL/List.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/List.thy Thu Dec 09 18:30:59 2004 +0100
@@ -13,7 +13,7 @@
Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
-section{*Basic list processing functions*}
+subsection{*Basic list processing functions*}
consts
"@" :: "'a list => 'a list => 'a list" (infixr 65)
@@ -237,7 +237,7 @@
by (rule measure_induct [of length]) rules
-subsection {* @{text length} *}
+subsubsection {* @{text length} *}
text {*
Needs to come before @{text "@"} because of theorem @{text
@@ -289,7 +289,7 @@
apply(simp)
done
-subsection {* @{text "@"} -- append *}
+subsubsection {* @{text "@"} -- append *}
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
by (induct xs) auto
@@ -444,7 +444,7 @@
*}
-subsection {* @{text map} *}
+subsubsection {* @{text map} *}
lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
by (induct xs) simp_all
@@ -553,7 +553,7 @@
by (induct rule:list_induct2, simp_all)
-subsection {* @{text rev} *}
+subsubsection {* @{text rev} *}
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
by (induct xs) auto
@@ -587,7 +587,7 @@
lemmas rev_cases = rev_exhaust
-subsection {* @{text set} *}
+subsubsection {* @{text set} *}
lemma finite_set [iff]: "finite (set xs)"
by (induct xs) auto
@@ -650,7 +650,7 @@
by (induct xs) (auto simp add: card_insert_if)
-subsection {* @{text mem} *}
+subsubsection {* @{text mem} *}
text{* Only use @{text mem} for generating executable code. Otherwise
use @{prop"x : set xs"} instead --- it is much easier to reason
@@ -660,7 +660,7 @@
by (induct xs) auto
-subsection {* @{text list_all} *}
+subsubsection {* @{text list_all} *}
lemma list_all_conv: "list_all P xs = (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
@@ -670,7 +670,7 @@
by (induct xs) auto
-subsection {* @{text filter} *}
+subsubsection {* @{text filter} *}
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
by (induct xs) auto
@@ -739,7 +739,7 @@
qed
-subsection {* @{text concat} *}
+subsubsection {* @{text concat} *}
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
by (induct xs) auto
@@ -763,7 +763,7 @@
by (induct xs) auto
-subsection {* @{text nth} *}
+subsubsection {* @{text nth} *}
lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
by auto
@@ -815,7 +815,7 @@
by (auto simp add: set_conv_nth)
-subsection {* @{text list_update} *}
+subsubsection {* @{text list_update} *}
lemma length_list_update [simp]: "!!i. length(xs[i:=x]) = length xs"
by (induct xs) (auto split: nat.split)
@@ -865,7 +865,7 @@
by (blast dest!: set_update_subset_insert [THEN subsetD])
-subsection {* @{text last} and @{text butlast} *}
+subsubsection {* @{text last} and @{text butlast} *}
lemma last_snoc [simp]: "last (xs @ [x]) = x"
by (induct xs) auto
@@ -908,7 +908,7 @@
by (auto dest: in_set_butlastD simp add: butlast_append)
-subsection {* @{text take} and @{text drop} *}
+subsubsection {* @{text take} and @{text drop} *}
lemma take_0 [simp]: "take 0 xs = []"
by (induct xs) auto
@@ -1084,7 +1084,7 @@
done
-subsection {* @{text takeWhile} and @{text dropWhile} *}
+subsubsection {* @{text takeWhile} and @{text dropWhile} *}
lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
by (induct xs) auto
@@ -1124,7 +1124,7 @@
by(induct xs, auto)
-subsection {* @{text zip} *}
+subsubsection {* @{text zip} *}
lemma zip_Nil [simp]: "zip [] ys = []"
by (induct ys) auto
@@ -1189,7 +1189,7 @@
done
-subsection {* @{text list_all2} *}
+subsubsection {* @{text list_all2} *}
lemma list_all2_lengthD [intro?]:
"list_all2 P xs ys ==> length xs = length ys"
@@ -1332,7 +1332,7 @@
done
-subsection {* @{text foldl} and @{text foldr} *}
+subsubsection {* @{text foldl} and @{text foldr} *}
lemma foldl_append [simp]:
"!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
@@ -1363,7 +1363,7 @@
by (induct ns) auto
-subsection {* @{text upto} *}
+subsubsection {* @{text upto} *}
lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
-- {* Does not terminate! *}
@@ -1474,7 +1474,7 @@
nth_Cons'[of _ _ "number_of v",standard]
-subsection {* @{text "distinct"} and @{text remdups} *}
+subsubsection {* @{text "distinct"} and @{text remdups} *}
lemma distinct_append [simp]:
"distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
@@ -1572,7 +1572,7 @@
done
-subsection {* @{text remove1} *}
+subsubsection {* @{text remove1} *}
lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
apply(induct xs)
@@ -1597,7 +1597,7 @@
by (induct xs) simp_all
-subsection {* @{text replicate} *}
+subsubsection {* @{text replicate} *}
lemma length_replicate [simp]: "length (replicate n x) = n"
by (induct n) auto
@@ -1644,7 +1644,7 @@
by (simp add: set_replicate_conv_if split: split_if_asm)
-subsection{*@{text rotate1} and @{text rotate}*}
+subsubsection{*@{text rotate1} and @{text rotate}*}
lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
by(simp add:rotate1_def)
@@ -1722,7 +1722,7 @@
by (induct n) (simp_all add:rotate_def)
-subsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
+subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
lemma sublist_empty [simp]: "sublist xs {} = []"
by (auto simp add: sublist_def)
@@ -1800,9 +1800,9 @@
done
-subsection{*Sets of Lists*}
-
-subsection {* @{text lists}: the list-forming operator over sets *}
+subsubsection{*Sets of Lists*}
+
+subsubsection {* @{text lists}: the list-forming operator over sets *}
consts lists :: "'a set => 'a list set"
inductive "lists A"
@@ -1842,7 +1842,7 @@
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto
-subsection{*Lists as Cartesian products*}
+subsubsection{*Lists as Cartesian products*}
text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
@{term A} and tail drawn from @{term Xs}.*}
@@ -1863,9 +1863,9 @@
"listset(A#As) = set_Cons A (listset As)"
-section{*Relations on lists*}
-
-subsection {* Lexicographic orderings on lists *}
+subsection{*Relations on lists*}
+
+subsubsection {* Lexicographic orderings on lists *}
consts
lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
@@ -1946,7 +1946,7 @@
done
-subsection{*Lifting a Relation on List Elements to the Lists*}
+subsubsection{*Lifting a Relation on List Elements to the Lists*}
consts listrel :: "('a * 'a)set => ('a list * 'a list)set"
@@ -2004,9 +2004,9 @@
by (auto simp add: set_Cons_def intro: listrel.intros)
-section{*Miscellany*}
-
-subsection {* Characters and strings *}
+subsection{*Miscellany*}
+
+subsubsection {* Characters and strings *}
datatype nibble =
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
@@ -2084,7 +2084,7 @@
in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
*}
-subsection {* Code generator setup *}
+subsubsection {* Code generator setup *}
ML {*
local
--- a/src/HOL/Matrix/MatrixGeneral.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy Thu Dec 09 18:30:59 2004 +0100
@@ -41,7 +41,8 @@
from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
have "m \<notin> ?S"
proof -
- have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max[OF c b])
+ have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_le[OF
+ c b])
moreover from d have "~(m <= Max ?S)" by (simp)
ultimately show "m \<notin> ?S" by (auto)
qed
--- a/src/HOL/NumberTheory/Euler.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Thu Dec 09 18:30:59 2004 +0100
@@ -150,7 +150,7 @@
lemma SetS_setprod_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); x \<in> (SetS a p) |] ==>
- [setprod x = a] (mod p)";
+ [\<Prod>x = a] (mod p)";
apply (auto simp add: SetS_def MultInvPair_def)
apply (frule StandardRes_SRStar_prop1a)
apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)");
@@ -186,49 +186,49 @@
done
lemma Union_SetS_setprod_prop1: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
- [setprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)";
-proof -;
- assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)";
- then have "[setprod (Union (SetS a p)) =
- gsetprod setprod (SetS a p)] (mod p)";
+ [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
+proof -
+ assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
+ then have "[\<Prod>(Union (SetS a p)) =
+ setprod (setprod (%x. x)) (SetS a p)] (mod p)"
by (auto simp add: SetS_finite SetS_elems_finite
- MultInvPair_prop1c setprod_disj_sets)
- also; have "[gsetprod setprod (SetS a p) =
- gsetprod (%x. a) (SetS a p)] (mod p)";
- apply (rule gsetprod_same_function_zcong)
+ 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)
- also (zcong_trans) have "[gsetprod (%x. a) (SetS a p) =
- a^(card (SetS a p))] (mod p)";
- by (auto simp add: prems SetS_finite gsetprod_const)
- finally (zcong_trans) show ?thesis;
+ 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)
+ finally (zcong_trans) show ?thesis
apply (rule zcong_trans)
- 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 (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
-qed;
+qed
lemma Union_SetS_setprod_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==>
- setprod (Union (SetS a p)) = zfact (p - 1)";
+ \<Prod>(Union (SetS a p)) = zfact (p - 1)";
proof -;
assume "p \<in> zprime" and "2 < p" and "~([a = 0](mod p))";
- then have "setprod (Union (SetS a p)) = setprod (SRStar p)";
+ then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
by (auto simp add: MultInvPair_prop2)
- also have "... = setprod ({1} \<union> (d22set (p - 1)))";
+ also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
by (auto simp add: prems SRStar_d22set_prop)
- also have "... = zfact(p - 1)";
- proof -;
- have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))";
+ also have "... = zfact(p - 1)"
+ proof -
+ have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
apply (insert prems, auto)
apply (drule d22set_g_1)
apply (auto simp add: d22set_fin)
done
- then have "setprod({1} \<union> (d22set (p - 1))) = setprod (d22set (p - 1))";
+ then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))";
by auto
then show ?thesis
by (auto simp add: d22set_prod_zfact)
qed;
- finally show ?thesis .;
+ finally show ?thesis .
qed;
lemma zfact_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
--- a/src/HOL/NumberTheory/EulerFermat.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Dec 09 18:30:59 2004 +0100
@@ -255,8 +255,8 @@
by (unfold inj_on_def, auto)
lemma Bnor_prod_power [rule_format]:
- "x \<noteq> 0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) =
- setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))"
+ "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
+ \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (subst BnorRset.simps)
@@ -273,7 +273,7 @@
subsection {* Fermat *}
lemma bijzcong_zcong_prod:
- "(A, B) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)"
+ "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
apply (unfold zcongm_def)
apply (erule bijR.induct)
apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
@@ -281,7 +281,7 @@
done
lemma Bnor_prod_zgcd [rule_format]:
- "a < m --> zgcd (setprod (BnorRset (a, m)), m) = 1"
+ "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (subst BnorRset.simps)
@@ -296,7 +296,7 @@
apply (case_tac "x = 0")
apply (case_tac [2] "m = 1")
apply (rule_tac [3] iffD1)
- apply (rule_tac [3] k = "setprod (BnorRset (m - 1, m))"
+ apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
in zcong_cancel2)
prefer 5
apply (subst Bnor_prod_power [symmetric])
--- a/src/HOL/NumberTheory/Finite2.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy Thu Dec 09 18:30:59 2004 +0100
@@ -5,7 +5,9 @@
header {*Finite Sets and Finite Sums*}
-theory Finite2 = Main + IntFact:;
+theory Finite2
+imports IntFact
+begin
text{*These are useful for combinatorial and number-theoretic counting
arguments.*}
@@ -15,208 +17,163 @@
(******************************************************************)
(* *)
-(* gsetprod: A generalized set product function, for ints only. *)
-(* Note that "setprod", as defined in IntFact, is equivalent to *)
-(* our "gsetprod id". *)
+(* Useful properties of sums and products *)
(* *)
(******************************************************************)
-consts
- gsetprod :: "('a => int) => 'a set => int"
-
-defs
- gsetprod_def: "gsetprod f A == if finite A then fold (op * o f) 1 A else 1";
-
-lemma gsetprod_empty [simp]: "gsetprod f {} = 1";
- by (auto simp add: gsetprod_def)
-
-lemma gsetprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
- gsetprod f (insert a A) = f a * gsetprod f A";
- by (simp add: gsetprod_def LC_def LC.fold_insert)
-
-(******************************************************************)
-(* *)
-(* Useful properties of sums and products *)
-(* *)
-(******************************************************************);
-
subsection {* Useful properties of sums and products *}
-lemma setprod_gsetprod_id: "setprod A = gsetprod id A";
- by (auto simp add: setprod_def gsetprod_def)
-
-lemma setsum_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==>
- setsum f S = setsum g S";
-by (induct set: Finites, auto)
-
-lemma gsetprod_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==>
- gsetprod f S = gsetprod g S";
-by (induct set: Finites, auto)
-
lemma setsum_same_function_zcong:
- "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |]
- ==> [setsum f S = setsum g S] (mod m)";
- by (induct set: Finites, auto simp add: zcong_zadd)
+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)
+next
+ assume "infinite S" thus ?thesis by(simp add:setsum_def)
+qed
-lemma gsetprod_same_function_zcong:
- "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |]
- ==> [gsetprod f S = gsetprod g S] (mod m)";
-by (induct set: Finites, auto simp add: zcong_zmult)
+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)"
+proof cases
+ assume "finite S"
+ thus ?thesis using a by induct (simp_all add: zcong_zmult)
+next
+ assume "infinite S" thus ?thesis by(simp add:setprod_def)
+qed
-lemma gsetprod_Un_Int: "finite A ==> finite B
- ==> gsetprod g (A \<union> B) * gsetprod g (A \<inter> B) =
- gsetprod g A * gsetprod g B";
- apply (induct set: Finites)
-by (auto simp add: Int_insert_left insert_absorb)
-
-lemma gsetprod_Un_disjoint: "[| finite A; finite B; A \<inter> B = {} |] ==>
- gsetprod g (A \<union> B) = gsetprod g A * gsetprod g B";
- apply (subst gsetprod_Un_Int [symmetric])
-by auto
-
-lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
+lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
apply (induct set: Finites)
apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
done
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
- int(c) * int(card X)";
+ int(c) * int(card X)"
apply (induct set: Finites)
apply (auto simp add: zadd_zmult_distrib2)
done
-lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A =
- setsum f A - setsum g A";
- by (induct set: Finites, auto)
-
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
- c * setsum f A";
+ c * setsum f A"
apply (induct set: Finites, auto)
- by (auto simp only: zadd_zmult_distrib2)
-
-lemma setsum_non_neg: "[| finite A; \<forall>x \<in> A. (0::int) \<le> f x |] ==>
- 0 \<le> setsum f A";
- by (induct set: Finites, auto)
-
-lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)";
- apply (induct set: Finites)
-by auto
+ by (auto simp only: 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";
+lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
by (simp add: finite_subset finite_imageI)
-lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
+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_le_finite: "finite { y::nat . y \<le> x }";
+lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x }"
apply (subgoal_tac "{ y::nat . y \<le> x } = { y::nat . y < Suc x}")
by (auto simp add: bdd_nat_set_l_finite)
-lemma bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}";
+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}");
+ 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}";
+lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
apply (erule ssubst)
apply (rule bdd_int_set_l_finite)
by auto
-lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
+lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
by (auto simp add: bdd_int_set_l_finite finite_subset)
-lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}";
+lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
by (auto simp add: bdd_int_set_le_finite finite_subset)
-lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
+lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
apply (induct_tac x, force)
-proof -;
- fix n::nat;
- assume "card {y. y < n} = n";
- have "{y. y < Suc n} = insert n {y. y < n}";
+proof -
+ fix n::nat
+ 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})";
+ then have "card {y. y < Suc n} = card (insert n {y. y < n})"
by auto
- also have "... = Suc (card {y. y < n})";
+ 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";
+ finally show "card {y. y < Suc n} = Suc n"
by (simp add: prems)
-qed;
+qed
-lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x";
+lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
by (auto simp add: card_bdd_nat_set_l)
-lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n";
-proof -;
- fix n::int;
- assume "0 \<le> n";
- have "finite {y. y < nat n}";
+lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
+proof -
+ fix n::int
+ assume "0 \<le> n"
+ have "finite {y. y < nat n}"
by (rule bdd_nat_set_l_finite)
- moreover have "inj_on (%y. int y) {y. y < nat n}";
+ moreover have "inj_on (%y. int y) {y. y < nat n}"
by (auto simp add: inj_on_def)
- ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
+ ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}"
by (rule card_image)
- also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}";
+ also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
apply (auto simp add: zless_nat_eq_int_zless image_def)
apply (rule_tac x = "nat x" in exI)
by (auto simp add: nat_0_le)
- also; have "card {y. y < nat n} = nat n"
+ also have "card {y. y < nat n} = nat n"
by (rule card_bdd_nat_set_l)
- finally show "card {y. 0 \<le> y & y < n} = nat n"; .;
-qed;
+ finally show "card {y. 0 \<le> y & y < n} = nat n" .
+qed
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
- nat n + 1";
+ nat n + 1"
apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
apply (insert card_bdd_int_set_l [of "n+1"])
by (auto simp add: nat_add_distrib)
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
- card {x. 0 < x & x \<le> n} = nat n";
-proof -;
- fix n::int;
- assume "0 \<le> n";
- have "finite {x. 0 \<le> x & x < n}";
+ card {x. 0 < x & x \<le> n} = nat n"
+proof -
+ fix n::int
+ assume "0 \<le> n"
+ have "finite {x. 0 \<le> x & x < n}"
by (rule bdd_int_set_l_finite)
- moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}";
+ moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
by (auto simp add: inj_on_def)
ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
- card {x. 0 \<le> x & x < n}";
+ card {x. 0 \<le> x & x < n}"
by (rule card_image)
- also from prems have "... = nat n";
+ also from prems have "... = nat n"
by (rule card_bdd_int_set_l)
- also; have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}";
+ also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
apply (auto simp add: image_def)
apply (rule_tac x = "x - 1" in exI)
by arith
- finally; show "card {x. 0 < x & x \<le> n} = nat n";.;
-qed;
+ finally show "card {x. 0 < x & x \<le> n} = nat n".
+qed
lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
- card {x. 0 < x & x < n} = nat n - 1";
+ card {x. 0 < x & x < n} = nat n - 1"
apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
apply (insert card_bdd_int_set_l_le [of "n - 1"])
by (auto simp add: nat_diff_distrib)
lemma int_card_bdd_int_set_l_l: "0 < n ==>
- int(card {x. 0 < x & x < n}) = n - 1";
+ int(card {x. 0 < x & x < n}) = n - 1"
apply (auto simp add: card_bdd_int_set_l_l)
apply (subgoal_tac "Suc 0 \<le> nat n")
apply (auto simp add: zdiff_int [THEN sym])
@@ -224,7 +181,7 @@
by (simp add: zero_less_nat_eq)
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
- int(card {x. 0 < x & x \<le> n}) = n";
+ int(card {x. 0 < x & x \<le> n}) = n"
by (auto simp add: card_bdd_int_set_l_le)
(******************************************************************)
@@ -236,23 +193,23 @@
subsection {* Cardinality of finite cartesian products *}
lemma insert_Sigma [simp]: "~(A = {}) ==>
- (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)";
+ (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
by blast
lemma cartesian_product_finite: "[| finite A; finite B |] ==>
- finite (A <*> B)";
+ finite (A <*> B)"
apply (rule_tac F = A in finite_induct)
by auto
lemma cartesian_product_card_a [simp]: "finite A ==>
- card({x} <*> A) = card(A)";
- apply (subgoal_tac "inj_on (%y .(x,y)) A");
+ card({x} <*> A) = card(A)"
+ apply (subgoal_tac "inj_on (%y .(x,y)) A")
apply (frule card_image, assumption)
- apply (subgoal_tac "(Pair x ` A) = {x} <*> A");
+ apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
by (auto simp add: inj_on_def)
lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==>
- card (A <*> B) = card(A) * card(B)";
+ card (A <*> B) = card(A) * card(B)"
apply (rule_tac F = A in finite_induct, auto)
done
@@ -262,101 +219,61 @@
(* *)
(******************************************************************)
-subsection {* Reindexing sums and products *}
-
-lemma sum_prop [rule_format]: "finite B ==>
- inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
-by (rule finite_induct, auto)
-
-lemma sum_prop_id: "finite B ==> inj_on f B ==>
- setsum f B = setsum id (f ` B)";
-by (auto simp add: sum_prop id_o)
-
-lemma prod_prop [rule_format]: "finite B ==>
- inj_on f B --> gsetprod h (f ` B) = gsetprod (h \<circ> f) B";
- apply (rule finite_induct, assumption, force)
- apply (rule impI)
- apply (auto simp add: inj_on_def)
- apply (subgoal_tac "f x \<notin> f ` F")
- apply (subgoal_tac "finite (f ` F)");
-by (auto simp add: gsetprod_insert)
-
-lemma prod_prop_id: "[| finite B; inj_on f B |] ==>
- gsetprod id (f ` B) = (gsetprod f B)";
- by (simp add: prod_prop id_o)
-
subsection {* Lemmas for counting arguments *}
lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==>
- finite (Union A)";
+ finite (Union A)"
apply (induct set: Finites)
by auto
lemma finite_index_UNION_finite_sets: "finite A ==>
- (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)";
+ (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)"
by (induct_tac rule: finite_induct, auto)
lemma card_union_disjoint_sets: "finite A ==>
((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==>
- card (Union A) = setsum card A";
+ card (Union A) = setsum card A"
apply auto
apply (induct set: Finites, auto)
apply (frule_tac B = "Union F" and A = x in card_Un_Int)
by (auto simp add: finite_union_finite_subsets)
-(*
- We just duplicated something in the standard library: the next lemma
- is setsum_UN_disjoint in Finite_Set
-
-lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==>
- ((\<forall>x \<in> A. finite (g x)) &
- (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) -->
- setsum f (UNION A g) = setsum (%x. setsum f (g x)) A";
-apply (induct_tac rule: finite_induct)
-apply (assumption, simp, clarify)
-apply (subgoal_tac "g x \<inter> (UNION F g) = {}");
-apply (subgoal_tac "finite (UNION F g)");
-apply (simp add: setsum_Un_disjoint)
-by (auto simp add: finite_index_UNION_finite_sets)
-
-*)
-
lemma int_card_eq_setsum [rule_format]: "finite A ==>
- int (card A) = setsum (%x. 1) A";
+ int (card A) = setsum (%x. 1) A"
by (erule finite_induct, auto)
lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==>
((\<forall>x \<in> A. finite (g x)) &
(\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) -->
- card (UNION A g) = setsum (%x. card (g x)) A";
+ card (UNION A g) = setsum (%x. card (g x)) A"
apply clarify
apply (frule_tac f = "%x.(1::nat)" and A = g in
- setsum_UN_disjoint);
-apply assumption+;
-apply (subgoal_tac "finite (UNION A g)");
-apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
+ setsum_UN_disjoint)
+apply assumption+
+apply (subgoal_tac "finite (UNION A g)")
+apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)")
apply (auto simp only: card_eq_setsum)
-apply (erule setsum_same_function)
-by auto;
+apply (rule setsum_cong)
+by auto
lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==>
((\<forall>x \<in> A. finite (g x)) &
(\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) -->
- int(card (UNION A g)) = setsum (%x. int( card (g x))) A";
+ int(card (UNION A g)) = setsum (%x. int( card (g x))) A"
apply clarify
apply (frule_tac f = "%x.(1::int)" and A = g in
- setsum_UN_disjoint);
-apply assumption+;
-apply (subgoal_tac "finite (UNION A g)");
-apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
+ setsum_UN_disjoint)
+apply assumption+
+apply (subgoal_tac "finite (UNION A g)")
+apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)")
apply (auto simp only: int_card_eq_setsum)
-apply (erule setsum_same_function)
+apply (rule setsum_cong)
by (auto simp add: int_card_eq_setsum)
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 sum_prop, auto)
-apply (subgoal_tac "setsum g B = setsum g (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)
@@ -365,10 +282,10 @@
apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
by auto
-lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
- g ` B \<subseteq> A; inj_on g B |] ==> gsetprod g B = gsetprod (g \<circ> f) A";
- apply (frule_tac h = g and f = f in prod_prop, auto)
- apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)");
+lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
+ g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
+ apply (frule_tac h = g and f = f in setprod_reindex)
+ apply (subgoal_tac "setprod g B = setprod g (f ` A)")
apply (simp add: inj_on_def)
apply (subgoal_tac "card A = card B")
apply (drule_tac A = "f ` A" and B = B in card_seteq)
@@ -376,40 +293,4 @@
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)
-lemma setsum_union_disjoint_sets [rule_format]: "finite A ==>
- ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {}))
- --> setsum f (Union A) = setsum (%x. setsum f x) A";
-apply (induct_tac rule: finite_induct)
-apply (assumption, simp, clarify)
-apply (subgoal_tac "x \<inter> (Union F) = {}");
-apply (subgoal_tac "finite (Union F)");
- by (auto simp add: setsum_Un_disjoint Union_def)
-
-lemma gsetprod_union_disjoint_sets [rule_format]: "[|
- finite (A :: int set set);
- (\<forall>X \<in> A. finite (X :: int set));
- (\<forall>X \<in> A. (\<forall>Y \<in> A. (X :: int set) \<noteq> (Y :: int set) -->
- (X \<inter> Y) = {})) |] ==>
- ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)";
- apply (induct set: Finites)
- apply (auto simp add: gsetprod_empty)
- apply (subgoal_tac "gsetprod f (x \<union> Union F) =
- gsetprod f x * gsetprod f (Union F)");
- apply simp
- apply (rule gsetprod_Un_disjoint)
-by (auto simp add: gsetprod_Un_disjoint Union_def)
-
-lemma gsetprod_disjoint_sets: "[| finite A;
- \<forall>X \<in> A. finite X;
- \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==>
- gsetprod id (Union A) = gsetprod (gsetprod id) A";
- apply (rule_tac f = id in gsetprod_union_disjoint_sets)
- by auto
-
-lemma setprod_disj_sets: "[| finite (A::int set set);
- \<forall>X \<in> A. finite X;
- \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==>
- setprod (Union A) = gsetprod (%x. setprod x) A";
- by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets)
-
-end;
+end
\ No newline at end of file
--- a/src/HOL/NumberTheory/Gauss.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Thu Dec 09 18:30:59 2004 +0100
@@ -274,7 +274,7 @@
apply (insert p_prime p_minus_one_l)
by (auto simp add: A_def zless_zprime_imp_zrelprime)
-lemma (in GAUSS) A_prod_relprime: "zgcd((gsetprod id A),p) = 1";
+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)
subsection {* Relationships Between Gauss Sets *}
@@ -303,17 +303,16 @@
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: "gsetprod id E * gsetprod id D = gsetprod 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 gsetprod_Un_disjoint [of D E id])
+ apply (frule setprod_Un_disjoint [of D E id])
by auto
-lemma (in GAUSS) C_B_zcong_prod: "[gsetprod id C = gsetprod id B] (mod p)";
-thm gsetprod_same_function_zcong;
+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 f = "StandardRes p" in prod_prop_id, auto)
- apply (rule gsetprod_same_function_zcong)
+ apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id[THEN sym], auto)
+ apply (rule setprod_same_function_zcong)
by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
@@ -384,127 +383,127 @@
by (auto simp add: card_seteq)
lemma (in GAUSS) prod_D_F_eq_prod_A:
- "(gsetprod id D) * (gsetprod id F) = gsetprod id A";
+ "(setprod id D) * (setprod id F) = setprod id A";
apply (insert F_D_disj finite_D finite_F)
- apply (frule gsetprod_Un_disjoint [of F D id])
+ apply (frule setprod_Un_disjoint [of F D id])
by (auto simp add: F_Un_D_eq_A)
lemma (in GAUSS) prod_F_zcong:
- "[gsetprod id F = ((-1) ^ (card E)) * (gsetprod id E)] (mod p)";
- proof -;
- have "gsetprod id F = gsetprod id (op - p ` E)";
+ "[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 "gsetprod id F = gsetprod (op - p) E";
+ 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 prod_prop_id, auto)
+ by (frule_tac f = "op - p" in setprod_reindex_id, auto)
then have one:
- "[gsetprod id F = gsetprod (StandardRes p o (op - p)) E] (mod p)";
+ "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
apply simp
apply (insert p_g_0 finite_E)
by (auto simp add: StandardRes_prod)
- moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)";
+ moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
apply clarify
apply (insert zcong_id [of p])
by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
- moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)";
+ moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
apply clarify
by (simp add: StandardRes_prop1 zcong_sym)
- moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)";
+ moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
apply clarify
apply (insert a b)
by (rule_tac b = "p - x" in zcong_trans, auto)
ultimately have c:
- "[gsetprod (StandardRes p o (op - p)) E = gsetprod (uminus) E](mod p)";
+ "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
apply simp
apply (insert finite_E p_g_0)
- by (frule gsetprod_same_function_zcong [of E "StandardRes p o (op - p)"
- uminus p], auto);
- then have two: "[gsetprod id F = gsetprod (uminus) E](mod p)";
+ by (rule setprod_same_function_zcong [of E "StandardRes p o (op - p)"
+ uminus p], auto)
+ then have two: "[setprod id F = setprod (uminus) E](mod p)"
apply (insert one c)
- by (rule zcong_trans [of "gsetprod id F"
- "gsetprod (StandardRes p o op - p) E" p
- "gsetprod uminus E"], auto);
- also have "gsetprod uminus E = (gsetprod id E) * (-1)^(card E)";
+ by (rule zcong_trans [of "setprod id F"
+ "setprod (StandardRes p o op - p) E" p
+ "setprod uminus E"], auto)
+ also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
apply (insert finite_E)
by (induct set: Finites, auto)
- then have "gsetprod uminus E = (-1) ^ (card E) * (gsetprod id E)";
+ then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
by (simp add: zmult_commute)
with two show ?thesis
by simp
-qed;
+qed
subsection {* Gauss' Lemma *}
-lemma (in GAUSS) aux: "gsetprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = gsetprod id A * a ^ card A";
+lemma (in GAUSS) aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
by (auto simp add: finite_E neg_one_special)
theorem (in GAUSS) pre_gauss_lemma:
- "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)";
- proof -;
- have "[gsetprod id A = gsetprod id F * gsetprod id D](mod p)";
+ "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
+ proof -
+ have "[setprod id A = setprod id F * setprod id D](mod p)"
by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
- then have "[gsetprod id A = ((-1)^(card E) * gsetprod id E) *
- gsetprod id D] (mod p)";
+ then have "[setprod id A = ((-1)^(card E) * setprod id E) *
+ setprod id D] (mod p)"
apply (rule zcong_trans)
by (auto simp add: prod_F_zcong zcong_scalar)
- then have "[gsetprod id A = ((-1)^(card E) * gsetprod id C)] (mod p)";
+ then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
apply (rule zcong_trans)
apply (insert C_prod_eq_D_times_E, erule subst)
by (subst zmult_assoc, auto)
- then have "[gsetprod id A = ((-1)^(card E) * gsetprod id B)] (mod p)"
+ then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
apply (rule zcong_trans)
by (simp add: C_B_zcong_prod zcong_scalar2)
- then have "[gsetprod id A = ((-1)^(card E) *
- (gsetprod id ((%x. x * a) ` A)))] (mod p)";
+ then have "[setprod id A = ((-1)^(card E) *
+ (setprod id ((%x. x * a) ` A)))] (mod p)"
by (simp add: B_def)
- then have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. x * a) A))]
- (mod p)";
+ then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
+ (mod p)"
apply (rule zcong_trans)
- by (simp add: finite_A inj_on_xa_A prod_prop_id zcong_scalar2)
- moreover have "gsetprod (%x. x * a) A =
- gsetprod (%x. a) A * gsetprod id A";
+ by (simp add: finite_A inj_on_xa_A setprod_reindex_id zcong_scalar2)
+ moreover have "setprod (%x. x * a) A =
+ setprod (%x. a) A * setprod id A"
by (insert finite_A, induct set: Finites, auto)
- ultimately have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. a) A *
- gsetprod id A))] (mod p)";
+ ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
+ setprod id A))] (mod p)"
by simp
- then have "[gsetprod id A = ((-1)^(card E) * a^(card A) *
- gsetprod id A)](mod p)";
+ then have "[setprod id A = ((-1)^(card E) * a^(card A) *
+ setprod id A)](mod p)"
apply (rule zcong_trans)
- by (simp add: zcong_scalar2 zcong_scalar finite_A gsetprod_const
+ by (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant
zmult_assoc)
- then have a: "[gsetprod id A * (-1)^(card E) =
- ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)";
+ then have a: "[setprod id A * (-1)^(card E) =
+ ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
by (rule zcong_scalar)
- then have "[gsetprod id A * (-1)^(card E) = gsetprod id A *
- (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
+ then have "[setprod id A * (-1)^(card E) = setprod id A *
+ (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
apply (rule zcong_trans)
by (simp add: a mult_commute mult_left_commute)
- then have "[gsetprod id A * (-1)^(card E) = gsetprod id A *
- a^(card A)](mod p)";
+ then have "[setprod id A * (-1)^(card E) = setprod id A *
+ a^(card A)](mod p)"
apply (rule zcong_trans)
by (simp add: aux)
- with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"]
- p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)";
+ with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
+ p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
by (simp add: order_less_imp_le)
from this show ?thesis
by (simp add: A_card_eq zcong_sym)
-qed;
+qed
-theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)";
-proof -;
+theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
+proof -
from Euler_Criterion p_prime p_g_2 have
- "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)";
+ "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
by auto
- moreover note pre_gauss_lemma;
- ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)";
+ moreover note pre_gauss_lemma
+ ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
by (rule zcong_trans)
- moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)";
+ moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
by (auto simp add: Legendre_def)
- moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1";
+ moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
by (rule neg_one_power)
- ultimately show ?thesis;
+ ultimately show ?thesis
by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
-qed;
+qed
-end;
\ No newline at end of file
+end
\ No newline at end of file
--- a/src/HOL/NumberTheory/Int2.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Int2.thy Thu Dec 09 18:30:59 2004 +0100
@@ -178,7 +178,7 @@
by (frule_tac m = m in zcong_not_zero, auto)
lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
- ==> zgcd (gsetprod id A,y) = 1";
+ ==> zgcd (setprod id A,y) = 1";
by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
(*****************************************************************)
--- a/src/HOL/NumberTheory/IntFact.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy Thu Dec 09 18:30:59 2004 +0100
@@ -18,29 +18,15 @@
consts
zfact :: "int => int"
- setprod :: "int set => int"
d22set :: "int => int set"
recdef zfact "measure ((\<lambda>n. nat n) :: int => nat)"
"zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
-defs
- setprod_def: "setprod A == (if finite A then fold (op *) 1 A else 1)"
-
recdef d22set "measure ((\<lambda>a. nat a) :: int => nat)"
"d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
-text {* \medskip @{term setprod} --- product of finite set *}
-
-lemma setprod_empty [simp]: "setprod {} = 1"
- apply (simp add: setprod_def)
- done
-
-lemma setprod_insert [simp]:
- "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
- by (simp add: setprod_def mult_left_commute LC.fold_insert [OF LC.intro])
-
text {*
\medskip @{term d22set} --- recursively defined set including all
integers from @{text 2} up to @{text a}
@@ -100,7 +86,7 @@
declare zfact.simps [simp del]
-lemma d22set_prod_zfact: "setprod (d22set a) = zfact a"
+lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
apply (induct a rule: d22set.induct)
apply safe
apply (simp add: d22set.simps zfact.simps)
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Dec 09 18:30:59 2004 +0100
@@ -5,7 +5,9 @@
header {* The law of Quadratic reciprocity *}
-theory Quadratic_Reciprocity = Gauss:;
+theory Quadratic_Reciprocity
+imports Gauss
+begin
(***************************************************************)
(* *)
@@ -15,137 +17,137 @@
(***************************************************************)
lemma (in GAUSS) QRLemma1: "a * setsum id A =
- p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
-proof -;
- from finite_A have "a * setsum id A = setsum (%x. a * x) A";
+ p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
+proof -
+ from finite_A have "a * setsum id A = setsum (%x. a * x) A"
by (auto simp add: setsum_const_mult id_def)
- also have "setsum (%x. a * x) = setsum (%x. x * a)";
+ also have "setsum (%x. a * x) = setsum (%x. x * a)"
by (auto simp add: zmult_commute)
- also; have "setsum (%x. x * a) A = setsum id B";
- by (auto simp add: B_def sum_prop_id finite_A inj_on_xa_A)
- also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
- apply (rule setsum_same_function)
+ also have "setsum (%x. x * a) A = setsum id B"
+ by (auto simp add: B_def setsum_reindex_id finite_A inj_on_xa_A)
+ also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
+ apply (rule setsum_cong)
by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
- also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B";
+ also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B"
by (rule setsum_addf)
- also; have "setsum (StandardRes p) B = setsum id C";
- by (auto simp add: C_def sum_prop_id [THEN sym] finite_B
+ also have "setsum (StandardRes p) B = setsum id C"
+ by (auto simp add: C_def setsum_reindex_id [THEN sym] finite_B
SR_B_inj)
- also; from C_eq have "... = setsum id (D \<union> E)";
+ also from C_eq have "... = setsum id (D \<union> E)"
by auto
- also; from finite_D finite_E have "... = setsum id D + setsum id E";
+ also from finite_D finite_E have "... = setsum id D + setsum id E"
apply (rule setsum_Un_disjoint)
by (auto simp add: D_def E_def)
also have "setsum (%x. p * (x div p)) B =
- setsum ((%x. p * (x div p)) o (%x. (x * a))) A";
- by (auto simp add: B_def sum_prop finite_A inj_on_xa_A)
- also have "... = setsum (%x. p * ((x * a) div p)) A";
+ setsum ((%x. p * (x div p)) o (%x. (x * a))) A"
+ by (auto simp add: B_def setsum_reindex finite_A inj_on_xa_A)
+ also have "... = setsum (%x. p * ((x * a) div p)) A"
by (auto simp add: o_def)
also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
- p * setsum (%x. ((x * a) div p)) A";
+ p * setsum (%x. ((x * a) div p)) A"
by (auto simp add: setsum_const_mult)
finally show ?thesis by arith
-qed;
+qed
lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
- setsum id D";
-proof -;
- from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)";
+ setsum id D"
+proof -
+ from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
by (simp add: Un_commute)
also from F_D_disj finite_D finite_F have
- "... = setsum id D + setsum id F";
+ "... = setsum id D + setsum id F"
apply (simp add: Int_commute)
by (intro setsum_Un_disjoint)
- also from F_def have "F = (%x. (p - x)) ` E";
+ also from F_def have "F = (%x. (p - x)) ` E"
by auto
also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
- setsum (%x. (p - x)) E";
- by (auto simp add: sum_prop)
- also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
- by (auto simp add: setsum_minus id_def)
- also from finite_E have "setsum (%x. p) E = p * int(card E)";
+ setsum (%x. (p - x)) E"
+ by (auto simp add: setsum_reindex)
+ also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E"
+ by (auto simp add: setsum_subtractf id_def)
+ also from finite_E have "setsum (%x. p) E = p * int(card E)"
by (intro setsum_const)
- finally show ?thesis;
+ finally show ?thesis
by arith
-qed;
+qed
lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
- p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
-proof -;
- have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
+ p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
+proof -
+ have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
by (auto simp add: zdiff_zmult_distrib)
- also note QRLemma1;
- also; from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
+ also note QRLemma1
+ also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
setsum id E - setsum id A =
p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
- setsum id E - (p * int (card E) - setsum id E + setsum id D)";
+ setsum id E - (p * int (card E) - setsum id E + setsum id D)"
by auto
- also; have "... = p * (\<Sum>x \<in> A. x * a div p) -
- p * int (card E) + 2 * setsum id E";
+ also have "... = p * (\<Sum>x \<in> A. x * a div p) -
+ p * int (card E) + 2 * setsum id E"
by arith
- finally show ?thesis;
+ finally show ?thesis
by (auto simp only: zdiff_zmult_distrib2)
-qed;
+qed
lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
- (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)";
-proof -;
- assume a_odd: "a \<in> zOdd";
+ (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
+proof -
+ assume a_odd: "a \<in> zOdd"
from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
- (a - 1) * setsum id A - 2 * setsum id E";
+ (a - 1) * setsum id A - 2 * setsum id E"
by arith
from a_odd have "a - 1 \<in> zEven"
by (rule odd_minus_one_even)
- hence "(a - 1) * setsum id A \<in> zEven";
+ hence "(a - 1) * setsum id A \<in> zEven"
by (rule even_times_either)
- moreover have "2 * setsum id E \<in> zEven";
+ moreover have "2 * setsum id E \<in> zEven"
by (auto simp add: zEven_def)
ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
by (rule even_minus_even)
- with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
+ with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
by simp
- hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
+ hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
by (rule EvenOdd.even_product)
- with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
+ with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
by (auto simp add: odd_iff_not_even)
- thus ?thesis;
+ thus ?thesis
by (auto simp only: even_diff [THEN sym])
-qed;
+qed
lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
- (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
-proof -;
- assume "a \<in> zOdd";
+ (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
+proof -
+ assume "a \<in> zOdd"
from QRLemma4 have
- "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)";..;
- moreover have "0 \<le> int(card E)";
+ "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)"..
+ moreover have "0 \<le> int(card E)"
by auto
- moreover have "0 \<le> setsum (%x. ((x * a) div p)) A";
- proof (intro setsum_non_neg);
- from finite_A show "finite A";.;
- next show "\<forall>x \<in> A. 0 \<le> x * a div p";
- proof;
- fix x;
- assume "x \<in> A";
- then have "0 \<le> x";
+ moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
+ proof (intro setsum_nonneg)
+ from finite_A show "finite A".
+ next show "\<forall>x \<in> A. 0 \<le> x * a div p"
+ proof
+ fix x
+ assume "x \<in> A"
+ then have "0 \<le> x"
by (auto simp add: A_def)
- with a_nonzero have "0 \<le> x * a";
+ with a_nonzero have "0 \<le> x * a"
by (auto simp add: zero_le_mult_iff)
- with p_g_2 show "0 \<le> x * a div p";
+ with p_g_2 show "0 \<le> x * a div p"
by (auto simp add: pos_imp_zdiv_nonneg_iff)
- qed;
- qed;
+ qed
+ qed
ultimately have "(-1::int)^nat((int (card E))) =
- (-1)^nat(((\<Sum>x \<in> A. x * a div p)))";
+ (-1)^nat(((\<Sum>x \<in> A. x * a div p)))"
by (intro neg_one_power_parity, auto)
- also have "nat (int(card E)) = card E";
+ also have "nat (int(card E)) = card E"
by auto
- finally show ?thesis;.;
-qed;
+ finally show ?thesis .
+qed
lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 2 < p;
A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
- (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
+ (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
apply (subst GAUSS.gauss_lemma)
apply (auto simp add: GAUSS_def)
apply (subst GAUSS.QRLemma5)
@@ -182,34 +184,34 @@
defines f1_def: "f1 j == { (j1, y). (j1, y):S & j1 = j &
(y \<le> (q * j) div p) }"
defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j &
- (x \<le> (p * j) div q) }";
+ (x \<le> (p * j) div q) }"
-lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
-proof -;
+lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
+proof -
from prems have "2 < p" by (simp add: QRTEMP_def)
then have "2 \<le> p - 1" by arith
then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
then show ?thesis by auto
-qed;
+qed
-lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
-proof -;
+lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2"
+proof -
from prems have "2 < q" by (simp add: QRTEMP_def)
then have "2 \<le> q - 1" by arith
then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
then show ?thesis by auto
-qed;
+qed
lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
- (p * b \<noteq> q * a)";
-proof;
- assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2";
+ (p * b \<noteq> q * a)"
+proof
+ assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
then have "q dvd (p * b)" by (auto simp add: dvd_def)
- with q_prime p_g_2 have "q dvd p | q dvd b";
+ with q_prime p_g_2 have "q dvd p | q dvd b"
by (auto simp add: zprime_zdvd_zmult)
- moreover have "~ (q dvd p)";
- proof;
- assume "q dvd p";
+ moreover have "~ (q dvd p)"
+ proof
+ assume "q dvd p"
with p_prime have "q = 1 | q = p"
apply (auto simp add: zprime_def QRTEMP_def)
apply (drule_tac x = q and R = False in allE)
@@ -218,410 +220,404 @@
apply (insert prems)
by (auto simp add: QRTEMP_def)
with q_g_2 p_neq_q show False by auto
- qed;
+ qed
ultimately have "q dvd b" by auto
- then have "q \<le> b";
- proof -;
- assume "q dvd b";
+ then have "q \<le> b"
+ proof -
+ assume "q dvd b"
moreover from prems have "0 < b" by auto
ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
- qed;
+ qed
with prems have "q \<le> (q - 1) div 2" by auto
then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
- then have "2 * q \<le> q - 1";
- proof -;
- assume "2 * q \<le> 2 * ((q - 1) div 2)";
+ then have "2 * q \<le> q - 1"
+ proof -
+ assume "2 * q \<le> 2 * ((q - 1) div 2)"
with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
with odd_minus_one_even have "(q - 1):zEven" by auto
with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
with prems show ?thesis by auto
- qed;
+ qed
then have p1: "q \<le> -1" by arith
with q_g_2 show False by auto
-qed;
+qed
-lemma (in QRTEMP) P_set_finite: "finite (P_set)";
+lemma (in QRTEMP) P_set_finite: "finite (P_set)"
by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
-lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
+lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
-lemma (in QRTEMP) S_finite: "finite S";
+lemma (in QRTEMP) S_finite: "finite S"
by (auto simp add: S_def P_set_finite Q_set_finite cartesian_product_finite)
-lemma (in QRTEMP) S1_finite: "finite S1";
-proof -;
+lemma (in QRTEMP) S1_finite: "finite S1"
+proof -
have "finite S" by (auto simp add: S_finite)
moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
ultimately show ?thesis by (auto simp add: finite_subset)
-qed;
+qed
-lemma (in QRTEMP) S2_finite: "finite S2";
-proof -;
+lemma (in QRTEMP) S2_finite: "finite S2"
+proof -
have "finite S" by (auto simp add: S_finite)
moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
ultimately show ?thesis by (auto simp add: finite_subset)
-qed;
+qed
-lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
+lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))"
by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
-lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
+lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
-lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
+lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
apply (auto simp add: S_def zmult_int setsum_constant_nat)
done
-lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
+lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
by (auto simp add: S1_def S2_def)
-lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2";
+lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2"
apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
- proof -;
- fix a and b;
- assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2";
+ proof -
+ fix a and b
+ assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
ultimately show "p * b < q * a" by auto
- qed;
+ qed
lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
- int(card(S1)) + int(card(S2))";
-proof-;
- have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
+ int(card(S1)) + int(card(S2))"
+proof-
+ have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
by (auto simp add: S_card)
- also have "... = int( card(S1) + card(S2))";
+ also have "... = int( card(S1) + card(S2))"
apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
apply (drule card_Un_disjoint, auto)
done
also have "... = int(card(S1)) + int(card(S2))" by auto
- finally show ?thesis .;
-qed;
+ finally show ?thesis .
+qed
lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
0 < b; b \<le> (q - 1) div 2 |] ==>
- (p * b < q * a) = (b \<le> q * a div p)";
-proof -;
- assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
- have "p * b < q * a ==> b \<le> q * a div p";
- proof -;
- assume "p * b < q * a";
+ (p * b < q * a) = (b \<le> q * a div p)"
+proof -
+ assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
+ have "p * b < q * a ==> b \<le> q * a div p"
+ proof -
+ assume "p * b < q * a"
then have "p * b \<le> q * a" by auto
- then have "(p * b) div p \<le> (q * a) div p";
+ then have "(p * b) div p \<le> (q * a) div p"
by (rule zdiv_mono1, insert p_g_2, auto)
- then show "b \<le> (q * a) div p";
+ then show "b \<le> (q * a) div p"
apply (subgoal_tac "p \<noteq> 0")
apply (frule zdiv_zmult_self2, force)
by (insert p_g_2, auto)
- qed;
- moreover have "b \<le> q * a div p ==> p * b < q * a";
- proof -;
- assume "b \<le> q * a div p";
- then have "p * b \<le> p * ((q * a) div p)";
+ qed
+ moreover have "b \<le> q * a div p ==> p * b < q * a"
+ proof -
+ assume "b \<le> q * a div p"
+ then have "p * b \<le> p * ((q * a) div p)"
by (insert p_g_2, auto simp add: mult_le_cancel_left)
- also have "... \<le> q * a";
+ also have "... \<le> q * a"
by (rule zdiv_leq_prop, insert p_g_2, auto)
- finally have "p * b \<le> q * a" .;
- then have "p * b < q * a | p * b = q * a";
+ finally have "p * b \<le> q * a" .
+ then have "p * b < q * a | p * b = q * a"
by (simp only: order_le_imp_less_or_eq)
- moreover have "p * b \<noteq> q * a";
+ moreover have "p * b \<noteq> q * a"
by (rule pb_neq_qa, insert prems, auto)
ultimately show ?thesis by auto
- qed;
- ultimately show ?thesis ..;
-qed;
+ qed
+ ultimately show ?thesis ..
+qed
lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
0 < b; b \<le> (q - 1) div 2 |] ==>
- (q * a < p * b) = (a \<le> p * b div q)";
-proof -;
- assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
- have "q * a < p * b ==> a \<le> p * b div q";
- proof -;
- assume "q * a < p * b";
+ (q * a < p * b) = (a \<le> p * b div q)"
+proof -
+ assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
+ have "q * a < p * b ==> a \<le> p * b div q"
+ proof -
+ assume "q * a < p * b"
then have "q * a \<le> p * b" by auto
- then have "(q * a) div q \<le> (p * b) div q";
+ then have "(q * a) div q \<le> (p * b) div q"
by (rule zdiv_mono1, insert q_g_2, auto)
- then show "a \<le> (p * b) div q";
+ then show "a \<le> (p * b) div q"
apply (subgoal_tac "q \<noteq> 0")
apply (frule zdiv_zmult_self2, force)
by (insert q_g_2, auto)
- qed;
- moreover have "a \<le> p * b div q ==> q * a < p * b";
- proof -;
- assume "a \<le> p * b div q";
- then have "q * a \<le> q * ((p * b) div q)";
+ qed
+ moreover have "a \<le> p * b div q ==> q * a < p * b"
+ proof -
+ assume "a \<le> p * b div q"
+ then have "q * a \<le> q * ((p * b) div q)"
by (insert q_g_2, auto simp add: mult_le_cancel_left)
- also have "... \<le> p * b";
+ also have "... \<le> p * b"
by (rule zdiv_leq_prop, insert q_g_2, auto)
- finally have "q * a \<le> p * b" .;
- then have "q * a < p * b | q * a = p * b";
+ finally have "q * a \<le> p * b" .
+ then have "q * a < p * b | q * a = p * b"
by (simp only: order_le_imp_less_or_eq)
- moreover have "p * b \<noteq> q * a";
+ moreover have "p * b \<noteq> q * a"
by (rule pb_neq_qa, insert prems, auto)
ultimately show ?thesis by auto
- qed;
- ultimately show ?thesis ..;
-qed;
+ qed
+ ultimately show ?thesis ..
+qed
lemma aux2: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==>
- (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2";
-proof-;
- assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q";
+ (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
+proof-
+ assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q"
(* Set up what's even and odd *)
- then have "p \<in> zOdd & q \<in> zOdd";
+ then have "p \<in> zOdd & q \<in> zOdd"
by (auto simp add: zprime_zOdd_eq_grt_2)
- then have even1: "(p - 1):zEven & (q - 1):zEven";
+ then have even1: "(p - 1):zEven & (q - 1):zEven"
by (auto simp add: odd_minus_one_even)
- then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
+ then have even2: "(2 * p):zEven & ((q - 1) * p):zEven"
by (auto simp add: zEven_def)
- then have even3: "(((q - 1) * p) + (2 * p)):zEven";
+ then have even3: "(((q - 1) * p) + (2 * p)):zEven"
by (auto simp: EvenOdd.even_plus_even)
(* using these prove it *)
- from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
+ from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
by (auto simp add: int_distrib)
- then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2";
- apply (rule_tac x = "((p - 1) * q)" in even_div_2_l);
+ then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
+ apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
by (auto simp add: even3, auto simp add: zmult_ac)
- also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)";
+ also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
by (auto simp add: even1 even_prod_div_2)
- also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p";
+ also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
finally show ?thesis
apply (rule_tac x = " q * ((p - 1) div 2)" and
- y = "(q - 1) div 2" in div_prop2);
+ y = "(q - 1) div 2" in div_prop2)
by (insert prems, auto)
-qed;
+qed
-lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p";
-proof;
- fix j;
- assume j_fact: "j \<in> P_set";
- have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})";
- proof -;
- have "finite (f1 j)";
- proof -;
+lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
+proof
+ fix j
+ assume j_fact: "j \<in> P_set"
+ have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})"
+ proof -
+ have "finite (f1 j)"
+ proof -
have "(f1 j) \<subseteq> S" by (auto simp add: f1_def)
with S_finite show ?thesis by (auto simp add: finite_subset)
- qed;
- moreover have "inj_on (%(x,y). y) (f1 j)";
+ qed
+ moreover have "inj_on (%(x,y). y) (f1 j)"
by (auto simp add: f1_def inj_on_def)
- ultimately have "card ((%(x,y). y) ` (f1 j)) = card (f1 j)";
+ ultimately have "card ((%(x,y). y) ` (f1 j)) = card (f1 j)"
by (auto simp add: f1_def card_image)
- moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}";
+ moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def
image_def)
ultimately show ?thesis by (auto simp add: f1_def)
- qed;
- also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})";
- proof -;
+ qed
+ also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
+ proof -
have "{y. y \<in> Q_set & y \<le> (q * j) div p} =
- {y. 0 < y & y \<le> (q * j) div p}";
+ {y. 0 < y & y \<le> (q * j) div p}"
apply (auto simp add: Q_set_def)
- proof -;
- fix x;
- assume "0 < x" and "x \<le> q * j div p";
- with j_fact P_set_def have "j \<le> (p - 1) div 2"; by auto
- with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
+ proof -
+ fix x
+ assume "0 < x" and "x \<le> q * j div p"
+ with j_fact P_set_def have "j \<le> (p - 1) div 2" by auto
+ with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
by (auto simp add: mult_le_cancel_left)
- with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
+ with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
by (auto simp add: zdiv_mono1)
- also from prems have "... \<le> (q - 1) div 2";
+ also from prems have "... \<le> (q - 1) div 2"
apply simp apply (insert aux2) by (simp add: QRTEMP_def)
finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
- qed;
+ qed
then show ?thesis by auto
- qed;
- also have "... = (q * j) div p";
- proof -;
+ qed
+ also have "... = (q * j) div p"
+ proof -
from j_fact P_set_def have "0 \<le> j" by auto
with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: mult_left_mono)
then have "0 \<le> q * j" by auto
- then have "0 div p \<le> (q * j) div p";
+ then have "0 div p \<le> (q * j) div p"
apply (rule_tac a = 0 in zdiv_mono1)
by (insert p_g_2, auto)
also have "0 div p = 0" by auto
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
- qed;
- finally show "int (card (f1 j)) = q * j div p" .;
-qed;
+ qed
+ finally show "int (card (f1 j)) = q * j div p" .
+qed
-lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q";
-proof;
- fix j;
- assume j_fact: "j \<in> Q_set";
- have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})";
- proof -;
- have "finite (f2 j)";
- proof -;
+lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
+proof
+ fix j
+ assume j_fact: "j \<in> Q_set"
+ have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})"
+ proof -
+ have "finite (f2 j)"
+ proof -
have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
with S_finite show ?thesis by (auto simp add: finite_subset)
- qed;
- moreover have "inj_on (%(x,y). x) (f2 j)";
+ qed
+ moreover have "inj_on (%(x,y). x) (f2 j)"
by (auto simp add: f2_def inj_on_def)
- ultimately have "card ((%(x,y). x) ` (f2 j)) = card (f2 j)";
+ ultimately have "card ((%(x,y). x) ` (f2 j)) = card (f2 j)"
by (auto simp add: f2_def card_image)
- moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}";
+ moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
by (insert prems, auto simp add: f2_def S_def Q_set_def
P_set_def image_def)
ultimately show ?thesis by (auto simp add: f2_def)
- qed;
- also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})";
- proof -;
+ qed
+ also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
+ proof -
have "{y. y \<in> P_set & y \<le> (p * j) div q} =
- {y. 0 < y & y \<le> (p * j) div q}";
+ {y. 0 < y & y \<le> (p * j) div q}"
apply (auto simp add: P_set_def)
- proof -;
- fix x;
- assume "0 < x" and "x \<le> p * j div q";
- with j_fact Q_set_def have "j \<le> (q - 1) div 2"; by auto
- with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
+ proof -
+ fix x
+ assume "0 < x" and "x \<le> p * j div q"
+ with j_fact Q_set_def have "j \<le> (q - 1) div 2" by auto
+ with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
by (auto simp add: mult_le_cancel_left)
- with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
+ with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
by (auto simp add: zdiv_mono1)
- also from prems have "... \<le> (p - 1) div 2";
+ also from prems have "... \<le> (p - 1) div 2"
by (auto simp add: aux2 QRTEMP_def)
finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
- qed;
+ qed
then show ?thesis by auto
- qed;
- also have "... = (p * j) div q";
- proof -;
+ qed
+ also have "... = (p * j) div q"
+ proof -
from j_fact Q_set_def have "0 \<le> j" by auto
with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: mult_left_mono)
then have "0 \<le> p * j" by auto
- then have "0 div q \<le> (p * j) div q";
+ then have "0 div q \<le> (p * j) div q"
apply (rule_tac a = 0 in zdiv_mono1)
by (insert q_g_2, auto)
also have "0 div q = 0" by auto
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
- qed;
- finally show "int (card (f2 j)) = p * j div q" .;
-qed;
+ qed
+ finally show "int (card (f2 j)) = p * j div q" .
+qed
-lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
-proof -;
- have "\<forall>x \<in> P_set. finite (f1 x)";
- proof;
- fix x;
+lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
+proof -
+ have "\<forall>x \<in> P_set. finite (f1 x)"
+ proof
+ fix x
have "f1 x \<subseteq> S" by (auto simp add: f1_def)
with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
- qed;
- moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})";
+ qed
+ moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})"
by (auto simp add: f1_def)
- moreover note P_set_finite;
+ moreover note P_set_finite
ultimately have "int(card (UNION P_set f1)) =
- setsum (%x. int(card (f1 x))) P_set";
+ setsum (%x. int(card (f1 x))) P_set"
by (rule_tac A = P_set in int_card_indexed_union_disjoint_sets, auto)
- moreover have "S1 = UNION P_set f1";
+ moreover have "S1 = UNION P_set f1"
by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
by auto
- also have "... = setsum (%j. q * j div p) P_set";
- proof -;
- note aux3a
- with P_set_finite show ?thesis by (rule setsum_same_function)
- qed;
- finally show ?thesis .;
-qed;
+ also have "... = setsum (%j. q * j div p) P_set"
+ using aux3a by(fastsimp intro: setsum_cong)
+ finally show ?thesis .
+qed
-lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set";
-proof -;
- have "\<forall>x \<in> Q_set. finite (f2 x)";
- proof;
- fix x;
+lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
+proof -
+ have "\<forall>x \<in> Q_set. finite (f2 x)"
+ proof
+ fix x
have "f2 x \<subseteq> S" by (auto simp add: f2_def)
with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
- qed;
+ qed
moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y -->
- (f2 x) \<inter> (f2 y) = {})";
+ (f2 x) \<inter> (f2 y) = {})"
by (auto simp add: f2_def)
- moreover note Q_set_finite;
+ moreover note Q_set_finite
ultimately have "int(card (UNION Q_set f2)) =
- setsum (%x. int(card (f2 x))) Q_set";
+ setsum (%x. int(card (f2 x))) Q_set"
by (rule_tac A = Q_set in int_card_indexed_union_disjoint_sets, auto)
- moreover have "S2 = UNION Q_set f2";
+ moreover have "S2 = UNION Q_set f2"
by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
by auto
- also have "... = setsum (%j. p * j div q) Q_set";
- proof -;
- note aux3b;
- with Q_set_finite show ?thesis by (rule setsum_same_function)
- qed;
- finally show ?thesis .;
-qed;
+ also have "... = setsum (%j. p * j div q) Q_set"
+ using aux3b by(fastsimp intro: setsum_cong)
+ finally show ?thesis .
+qed
lemma (in QRTEMP) S1_carda: "int (card(S1)) =
- setsum (%j. (j * q) div p) P_set";
+ setsum (%j. (j * q) div p) P_set"
by (auto simp add: S1_card zmult_ac)
lemma (in QRTEMP) S2_carda: "int (card(S2)) =
- setsum (%j. (j * p) div q) Q_set";
+ setsum (%j. (j * p) div q) Q_set"
by (auto simp add: S2_card zmult_ac)
lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
- (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
-proof -;
+ (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
+proof -
have "(setsum (%j. (j * p) div q) Q_set) +
- (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
+ (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)"
by (auto simp add: S1_carda S2_carda)
- also have "... = int (card S1) + int (card S2)";
+ also have "... = int (card S1) + int (card S2)"
by auto
- also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
+ also have "... = ((p - 1) div 2) * ((q - 1) div 2)"
by (auto simp add: card_sum_S1_S2)
- finally show ?thesis .;
-qed;
+ finally show ?thesis .
+qed
-lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))";
+lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))"
apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
apply (drule_tac x = q in allE)
apply (drule_tac x = p in allE)
by auto
lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
- (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
-proof -;
- from prems have "~([p = 0] (mod q))";
+ (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
+proof -
+ from prems have "~([p = 0] (mod q))"
by (auto simp add: pq_prime_neq QRTEMP_def)
with prems have a1: "(Legendre p q) = (-1::int) ^
- nat(setsum (%x. ((x * p) div q)) Q_set)";
+ nat(setsum (%x. ((x * p) div q)) Q_set)"
apply (rule_tac p = q in MainQRLemma)
by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
- from prems have "~([q = 0] (mod p))";
+ from prems have "~([q = 0] (mod p))"
apply (rule_tac p = q and q = p in pq_prime_neq)
- apply (simp add: QRTEMP_def)+;
+ apply (simp add: QRTEMP_def)+
by arith
with prems have a2: "(Legendre q p) =
- (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
+ (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
apply (rule_tac p = p in MainQRLemma)
by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
from a1 a2 have "(Legendre p q) * (Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
- (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
+ (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
by auto
also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
- nat(setsum (%x. ((x * q) div p)) P_set))";
+ nat(setsum (%x. ((x * q) div p)) P_set))"
by (auto simp add: zpower_zadd_distrib)
also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set) =
nat((setsum (%x. ((x * p) div q)) Q_set) +
- (setsum (%x. ((x * q) div p)) P_set))";
+ (setsum (%x. ((x * q) div p)) P_set))"
apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
- nat_add_distrib [THEN sym]);
+ nat_add_distrib [THEN sym])
by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
- also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
+ also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))"
by (auto simp add: pq_sum_prop)
- finally show ?thesis .;
-qed;
+ finally show ?thesis .
+qed
theorem Quadratic_Reciprocity:
"[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime;
p \<noteq> q |]
==> (Legendre p q) * (Legendre q p) =
- (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
+ (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym]
QRTEMP_def)
--- a/src/HOL/NumberTheory/Residues.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Residues.thy Thu Dec 09 18:30:59 2004 +0100
@@ -168,7 +168,7 @@
by (auto simp add: zcong_zmod)
lemma StandardRes_prod: "[| finite X; 0 < m |]
- ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
+ ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)";
apply (rule_tac F = X in finite_induct)
by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
--- a/src/HOL/NumberTheory/WilsonBij.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.thy Thu Dec 09 18:30:59 2004 +0100
@@ -229,7 +229,7 @@
subsection {* Wilson *}
lemma bijER_zcong_prod_1:
- "p \<in> zprime ==> A \<in> bijER (reciR p) ==> [setprod A = 1] (mod p)"
+ "p \<in> zprime ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
apply (unfold reciR_def)
apply (erule bijER.induct)
apply (subgoal_tac [2] "a = 1 \<or> a = p - 1")
@@ -239,7 +239,7 @@
prefer 3
apply (subst setprod_insert)
apply (auto simp add: fin_bijER)
- apply (subgoal_tac "zcong ((a * b) * setprod A) (1 * 1) p")
+ apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
apply (simp add: zmult_assoc)
apply (rule zcong_zmult)
apply auto
--- a/src/HOL/NumberTheory/WilsonRuss.thy Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Thu Dec 09 18:30:59 2004 +0100
@@ -261,7 +261,7 @@
lemma wset_zcong_prod_1 [rule_format]:
"p \<in> zprime -->
- 5 \<le> p --> a < p - 1 --> [setprod (wset (a, p)) = 1] (mod p)"
+ 5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
apply (induct a p rule: wset_induct)
prefer 2
apply (subst wset.simps)
@@ -269,7 +269,7 @@
apply (subst setprod_insert)
apply (tactic {* stac (thm "setprod_insert") 3 *})
apply (subgoal_tac [5]
- "zcong (a * inv p a * setprod (wset (a - 1, p))) (1 * 1) p")
+ "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
prefer 5
apply (simp add: zmult_assoc)
apply (rule_tac [5] zcong_zmult)