# HG changeset patch # User nipkow # Date 1102613459 -3600 # Node ID 290bc97038c704c4cf60b20f5c8e4b51065d6459 # Parent 797ed46d724b038eae090c96e8e8a83123f31539 First step in reorganizing Finite_Set diff -r 797ed46d724b -r 290bc97038c7 src/HOL/Equiv_Relations.thy --- 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: diff -r 797ed46d724b -r 290bc97038c7 src/HOL/Finite_Set.ML --- 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"; diff -r 797ed46d724b -r 290bc97038c7 src/HOL/Finite_Set.thy --- 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 "\ (n::nat) f. A = f ` {i::nat. if. {} = 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 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 "\k(\ k (n::nat) f. A = f ` {i::nat. i 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(\A) \ 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 \ 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) (\ (f (g x\<^isub>n) e)\)"} +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 \ 'a) set" + +inductive "foldSet f g e" +intros +emptyI [intro]: "({}, e) : foldSet f g e" +insertI [intro]: "\ x \ A; (A, y) : foldSet f g e \ + \ (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 "\" 70) + assumes commute: "x \ y = y \ x" + and assoc: "(x \ y) \ z = x \ (y \ z)" + +locale ACe = ACf + + fixes e :: 'a + assumes ident [simp]: "x \ e = x" + +lemma (in ACf) left_commute: "x \ (y \ z) = y \ (x \ z)" +proof - + have "x \ (y \ z) = (y \ z) \ x" by (simp only: commute) + also have "... = y \ (z \ x)" by (simp only: assoc) + also have "z \ x = x \ z" by (simp only: commute) + finally show ?thesis . +qed + +lemmas (in ACf) AC = assoc commute left_commute + +lemma (in ACe) left_ident [simp]: "e \ x = x" +proof - + have "x \ 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. \ A = h`{i::nat. i + \ x' = x" +proof (induct n) + case 0 thus ?case by auto +next + case (Suc n) + have IH: "!!A x x' h. \A = h`{i::nat. i foldSet f g e; (A,x') \ foldSet f g e\ + \ x' = x" and card: "A = h`{i. i foldSet f g e" and Afoldy: "(A,x') \ foldSet f g e" . + show ?case + proof cases + assume "EX k(EX k y)" + and y: "(B,y) \ foldSet f g e" and notinB: "b \ B" + hence A1: "A = insert b B" and x: "x = g b \ 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 \ z)" + and z: "(C,z) \ foldSet f g e" and notinC: "c \ C" + hence A2: "A = insert c C" and x': "x' = g c \ 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 ?r" + proof + fix u assume "u \ B" + hence uinA: "u \ A" and unotb: "u \ 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 \ ?r" + proof cases + assume "i\<^isub>u < n" + thus ?thesis using unotb by(fastsimp) + next + assume "\ 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 "\ 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 \ B" + proof + fix u assume "u \ ?r" + then obtain i\<^isub>u where below: "i\<^isub>u < n" and + or: "b = h i\<^isub>u \ u = h n \ h i\<^isub>u \ b \ h i\<^isub>u = u" + by(auto simp:image_def) + from or show "u \ B" + proof + assume [simp]: "b = h i\<^isub>u \ u = h n" + have "u \ A" using card by auto + moreover have "u \ b" using new below by auto + ultimately show "u \ B" using A1 by blast + next + assume "h i\<^isub>u \ b \ h i\<^isub>u = u" + moreover hence "u \ A" using card below by auto + ultimately show "u \ 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 \ 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) \ foldSet f g e" + using finite_imp_foldSet by rules + moreover have cinB: "c \ B" using B by(auto) + ultimately have "(B,g c \ d) \ foldSet f g e" + by(rule Diff1_foldSet) + hence "g c \ d = y" by(rule IH[OF less y]) + moreover have "g b \ 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 ?r" + proof + fix u assume "u \ C" + hence uinA: "u \ A" and unotc: "u \ 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 \ ?r" + proof cases + assume "i\<^isub>u < n" + thus ?thesis using unotc by(fastsimp) + next + assume "\ 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 "\ 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 \ C" + proof + fix u assume "u \ ?r" + then obtain i\<^isub>u where below: "i\<^isub>u < n" and + or: "c = h i\<^isub>u \ u = h n \ h i\<^isub>u \ c \ h i\<^isub>u = u" + by(auto simp:image_def) + from or show "u \ C" + proof + assume [simp]: "c = h i\<^isub>u \ u = h n" + have "u \ A" using card by auto + moreover have "u \ c" using new below by auto + ultimately show "u \ C" using A2 by blast + next + assume "h i\<^isub>u \ c \ h i\<^isub>u = u" + moreover hence "u \ A" using card below by auto + ultimately show "u \ C" using A2 by blast + qed + qed + qed + next + show "(C,g b \ d) \ 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'. \ card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \ + \ x' = x" +proof (induct n) + case 0 thus ?case by simp +next + case (Suc n) + have IH: "!!A x x'. \card A < n; (A,x) \ foldSet f g e; (A,x') \ foldSet f g e\ + \ x' = x" and card: "card A < Suc n" + and Afoldx: "(A, x) \ foldSet f g e" and Afoldy: "(A,x') \ foldSet f g e" . + from card have "card A < n \ 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 \ y)" + and y: "(B,y) \ foldSet f g e" and notinB: "b \ B" + hence A1: "A = insert b B" and x: "x = g b \ 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 \ z)" + and z: "(C,z) \ foldSet f g e" and notinC: "c \ C" + hence A2: "A = insert c C" and x': "x' = g c \ 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 \ 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) \ foldSet f g e" + using finite_imp_foldSet by rules + moreover have cinB: "c \ B" using B by(auto) + ultimately have "(B,g c \ d) \ foldSet f g e" + by(rule Diff1_foldSet) + hence "g c \ d = y" by(rule IH[OF less y]) + moreover have "g b \ 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 \ d) \ 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 \ 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 \ 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: + "\ F \ fold f g e; finite A; x \ A \ \ 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 \ fold f g e (h ` B) = fold f (g \ 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 \ fold f g e B = + fold f g e (A Un B) \ 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 \ fold f g e B" + by (simp add: fold_Un_Int) + +lemma (in ACe) fold_UN_disjoint: + "\ finite I; ALL i:I. finite (A i); + ALL i:I. ALL j:I. i \ j --> A i Int A j = {} \ + \ 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 \ 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 \ (!!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 \ + 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 \ 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 \ 'a) set" - -inductive "foldSet f e" - intros - emptyI [intro]: "({}, e) : foldSet f e" - insertI [intro]: "x \ 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 "\" 70) - assumes left_commute: "x \ (y \ z) = y \ (x \ z)" +lemma card_s_0_eq_empty: + "finite A ==> card {B. B \ 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 \ 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 \ 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 \ 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 \ B; finite B |] ==> card A \ 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 \ B; inj_on g B; g ` B \ 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 \ 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 \ 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 \ 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: - "\ F \ fold f e; finite A; x \ A \ \ 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 \ 'a) set" + +inductive "foldSet1 f" +intros +foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f" +foldSet1_insertI [intro]: + "\ (A, x) : foldSet1 f; a \ A; A \ {} \ + \ (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 \ A \ {}" +by(erule foldSet1.cases, simp_all) + -lemma (in LC) fold_reindex: -assumes fin: "finite B" -shows "inj_on g B \ fold f e (g ` B) = fold (f \ 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 "\" 70) - assumes commute: "x \ y = y \ x" - and assoc: "(x \ y) \ z = x \ (y \ 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 \ e = x" +lemma finite_nonempty_imp_foldSet1: + "\ finite A; A \ {} \ \ EX x. (A, x) : foldSet1 f" + by (induct set: Finites) auto -lemma (in ACf) left_commute: "x \ (y \ z) = y \ (x \ z)" -proof - - have "x \ (y \ z) = (y \ z) \ x" by (simp only: commute) - also have "... = y \ (z \ x)" by (simp only: assoc) - also have "z \ x = x \ 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 \ x = x" -proof - - have "x \ e = x" by (rule ident) - thus ?thesis by (subst commute) +lemma (in ACf) foldSet1_determ_aux: + "!!A x y. \ card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \ \ y = x" +proof (induct n) + case 0 thus ?case by simp +next + case (Suc n) + have IH: "!!A x y. \card A < n; (A, x) \ foldSet1 f; (A, y) \ foldSet1 f\ + \ y = x" and card: "card A < Suc n" + and Afoldx: "(A, x) \ foldSet1 f" and Afoldy: "(A, y) \ foldSet1 f" . + from card have "card A < n \ 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 \ x')" + and x': "(Ax, x') \ foldSet1 f" and notinx: "ax \ Ax" + and Axnon: "Ax \ {}" + hence A1: "A = insert ax Ax" and x: "x = ax \ 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 \ y')" + and y': "(Ay, y') \ foldSet1 f" and notiny: "ay \ Ay" + and Aynon: "Ay \ {}" + hence A2: "A = insert ay Ay" and y: "y = ay \ 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 \ 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 \ {}" + moreover have "finite ?B" using finA A1 by simp + ultimately obtain b where Bfoldb: "(?B,b) \ foldSet1 f" + using finite_nonempty_imp_foldSet1 by(blast) + moreover have ayinAx: "ay \ Ax" using Ax by(auto) + ultimately have "(Ax,ay\b) \ foldSet1 f" by(rule Diff1_foldSet1) + hence "ay\b = x'" by(rule IH[OF less x']) + moreover have "ax\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\b) \ 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 \ fold (f o g) e B = - fold (f o g) e (A Un B) \ 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 \ fold f e B = fold f e (A Un B) \ fold f e (A Int B)" - by (rule fold_o_Un_Int[where g = id,simplified]) +lemma (in ACf) foldSet1_insert_aux: "x \ A ==> A \ {} \ + ((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 \ fold (f o g) e B" - by (simp add: fold_o_Un_Int) +lemma (in ACf) fold1_insert: + "finite A ==> x \ A ==> A \ {} \ 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 \ fold f e B" - by (simp add: fold_Un_Int) +locale ACIf = ACf + + assumes idem: "x \ x = x" -lemma (in ACe) fold_o_UN_disjoint: - "\ finite I; ALL i:I. finite (A i); - ALL i:I. ALL j:I. i \ j --> A i Int A j = {} \ - \ 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 \ 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 \ {}" +shows "fold1 f (insert a A) = f a (fold1 f A)" +proof cases + assume "a \ A" + then obtain B where A: "A = insert a B" and disj: "a \ 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 \ {}" + 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 "\ = f a (fold1 f B)" + using finB nonB disj by(simp add: fold1_insert) + also have "\ = 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 \ A" + with finA nonA show ?thesis by(simp add:fold1_insert) +qed + -lemma (in ACf) fold_cong: - "finite A \ (!!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 \ fold1 f \ g {a} = a" +by(simp add:fold1_singleton) + +lemma (in ACf) fold1_insert_def: + "\ g \ fold1 f; finite A; x \ A; A \ {} \ \ g(insert x A) = x \ (g A)" +by(simp add:fold1_insert) + +lemma (in ACIf) fold1_insert2_def: + "\ g \ fold1 f; finite A; A \ {} \ \ g(insert x A) = x \ (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 \ 'a \ 'a)" +apply(rule ACf.intro) +apply(auto simp:min_def) +done + +lemma ACIf_min: "ACIf(min:: 'a::linorder \ 'a \ '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 \ - 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 \ 'a \ 'a)" +apply(rule ACf.intro) +apply(auto simp:max_def) +done + +lemma ACIf_max: "ACIf(max:: 'a::linorder \ 'a \ '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 \ {} \ Min S \ 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 \ {}" thus ?thesis using insert by (simp add:min_def) + qed +qed + +lemma Min_le [simp]: + assumes a: "finite S" + shows "\ S \ {}; x \ S \ \ Min S \ 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 \ {}" thus ?thesis using insert by (auto simp add:min_def) + qed +qed + +lemma Max_in [simp]: + assumes a: "finite S" + shows "S \ {} \ Max S \ 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 \ {}" thus ?thesis using insert by (simp add:max_def) + qed +qed + +lemma Max_le [simp]: + assumes a: "finite S" + shows "\ S \ {}; x \ S \ \ x \ 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 \ {}" 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"\x\A. e"}. *} @@ -874,14 +1481,26 @@ "SUM x|P. t" => "setsum (%x. t) {x. P}" "\x|P. t" => "setsum (%x. t) {x. P}" +text{* Finally we abbreviate @{term"\x\A. x"} by @{text"\A"}. *} + +syntax + "_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\_" [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 \ 'b::comm_monoid_add \ '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 \ 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 \ 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 \ 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 \ 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) ==> (\x\A. (\y\B x. f x y)) = (\z\(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 ==> (\x\A. (\y\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\_:_. _)" [0, 51, 10] 10) @@ -1210,6 +1825,23 @@ translations "\i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *} +syntax + "_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\_" [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 \ 'a \ '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 \ 'b::comm_monoid_mult \ '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 \ 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 \ 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 \ 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 \ 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 \ 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) ==> (\x:A. (\y: B x. f x y)) = (\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 ==> (\x:A. (\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 \ 'a) set" - -inductive "foldSet1 f" -intros -fold1_singletonI [intro]: "({a}, a) : foldSet1 f" -fold1_insertI [intro]: - "\ (A, x) : foldSet1 f; a \ A; A \ {} \ - \ (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 \ A \ {}" -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: - "\ finite A; A \ {} \ \ EX x. (A, x) : foldSet1 f" - by (induct set: Finites) auto - -lemma lem: "(A \ {a}) = (A = {} \ 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 \ 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 \ A ==> A \ {} \ - ((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 \ A ==> A \ {} \ 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 \ x = x" - -lemma (in ACIf) fold1_insert2: -assumes finA: "finite A" and nonA: "A \ {}" -shows "fold1 f (insert a A) = f a (fold1 f A)" -proof cases - assume "a \ A" - then obtain B where A: "A = insert a B" and disj: "a \ 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 \ {}" - 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 "\ = f a (fold1 f B)" - using finB nonB disj by(simp add: fold1_insert) - also have "\ = 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 \ 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 \ {} ==> \m\S. \s \ S. s \ 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 \ {}" - then obtain m where m: "m\S" "\s\S. s \ m" using insert by blast - show ?thesis - proof (cases) - assume "x \ m" thus ?thesis using m by blast - next - assume "~ x \ 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 \ {} ==> \m\S. \s \ S. m \ 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 \ {}" - then obtain m where m: "m\S" "\s\S. m \ s" using insert by blast - show ?thesis - proof (cases) - assume "m \ x" thus ?thesis using m by blast - next - assume "~ m \ 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 \ S \ (\s \ S. m \ s)" - - Max :: "('a::linorder)set => 'a" - "Max S == THE m. m \ S \ (\s \ S. s \ m)" - -lemma Min [simp]: - assumes a: "finite S" "S \ {}" - shows "Min S \ S \ (\s \ S. Min S \ s)" (is "?P(Min S)") -proof (unfold Min_def, rule theI') - show "\!m. ?P m" - proof (rule ex_ex1I) - show "\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 \ {}" - shows "Max S \ S \ (\s \ S. s \ Max S)" (is "?P(Max S)") -proof (unfold Max_def, rule theI') - show "\!m. ?P m" - proof (rule ex_ex1I) - show "\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 \ 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 \ 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 \ 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 \ B; finite B |] ==> card A \ 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 \ B; inj_on g B; g ` B \ 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 \ 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 diff -r 797ed46d724b -r 290bc97038c7 src/HOL/List.thy --- 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 = (\x \ 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 distinct ys \ set xs \ 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 [] = [] \ 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 diff -r 797ed46d724b -r 290bc97038c7 src/HOL/Matrix/MatrixGeneral.thy --- 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 \ ?S" proof - - have "m \ ?S \ m <= Max(?S)" by (simp add: Max[OF c b]) + have "m \ ?S \ m <= Max(?S)" by (simp add:Max_le[OF + c b]) moreover from d have "~(m <= Max ?S)" by (simp) ultimately show "m \ ?S" by (auto) qed diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Euler.thy --- 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 \ zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a); x \ (SetS a p) |] ==> - [setprod x = a] (mod p)"; + [\x = a] (mod p)"; apply (auto simp add: SetS_def MultInvPair_def) apply (frule StandardRes_SRStar_prop1a) apply (subgoal_tac "StandardRes p x \ StandardRes p (a * MultInv p x)"); @@ -186,49 +186,49 @@ done lemma Union_SetS_setprod_prop1: "[| p \ 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 \ 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)"; + [\(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)" +proof - + assume "p \ zprime" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" + then have "[\(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 \ zprime; 2 < p; ~([a = 0](mod p)) |] ==> - setprod (Union (SetS a p)) = zfact (p - 1)"; + \(Union (SetS a p)) = zfact (p - 1)"; proof -; assume "p \ zprime" and "2 < p" and "~([a = 0](mod p))"; - then have "setprod (Union (SetS a p)) = setprod (SRStar p)"; + then have "\(Union (SetS a p)) = \(SRStar p)" by (auto simp add: MultInvPair_prop2) - also have "... = setprod ({1} \ (d22set (p - 1)))"; + also have "... = \({1} \ (d22set (p - 1)))" by (auto simp add: prems SRStar_d22set_prop) - also have "... = zfact(p - 1)"; - proof -; - have "~(1 \ d22set (p - 1)) & finite( d22set (p - 1))"; + also have "... = zfact(p - 1)" + proof - + have "~(1 \ d22set (p - 1)) & finite( d22set (p - 1))" apply (insert prems, auto) apply (drule d22set_g_1) apply (auto simp add: d22set_fin) done - then have "setprod({1} \ (d22set (p - 1))) = setprod (d22set (p - 1))"; + then have "\({1} \ (d22set (p - 1))) = \(d22set (p - 1))"; by auto then show ?thesis by (auto simp add: d22set_prod_zfact) qed; - finally show ?thesis .; + finally show ?thesis . qed; lemma zfact_prop: "[| p \ zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/EulerFermat.thy --- 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 \ 0 ==> a < m --> setprod ((\a. a * x) ` BnorRset (a, m)) = - setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))" + "x \ 0 ==> a < m --> \((\a. a * x) ` BnorRset (a, m)) = + \(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) \ bijR (zcongm m) ==> [setprod A = setprod B] (mod m)" + "(A, B) \ bijR (zcongm m) ==> [\A = \B] (mod m)" apply (unfold zcongm_def) apply (erule bijR.induct) apply (subgoal_tac [2] "a \ A \ b \ B \ finite A \ 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 (\(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 = "\(BnorRset(m - 1, m))" in zcong_cancel2) prefer 5 apply (subst Bnor_prod_power [symmetric]) diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Finite2.thy --- 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 \ 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; \x \ S. f x = g x |] ==> - setsum f S = setsum g S"; -by (induct set: Finites, auto) - -lemma gsetprod_same_function: "[| finite S; \x \ S. f x = g x |] ==> - gsetprod f S = gsetprod g S"; -by (induct set: Finites, auto) - lemma setsum_same_function_zcong: - "[| finite S; \x \ 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: "\x \ 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; \x \ 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: "\x \ 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 \ B) * gsetprod g (A \ 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 \ B = {} |] ==> - gsetprod g (A \ 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; \x \ A. (0::int) \ f x |] ==> - 0 \ 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 \ f ` A; finite A |] ==> finite B"; +lemma finite_surjI: "[| B \ 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 \ x }"; +lemma bdd_nat_set_le_finite: "finite { y::nat . y \ x }" apply (subgoal_tac "{ y::nat . y \ x } = { y::nat . y < Suc x}") by (auto simp add: bdd_nat_set_l_finite) -lemma bdd_int_set_l_finite: "finite { x::int . 0 \ x & x < n}"; +lemma bdd_int_set_l_finite: "finite { x::int . 0 \ x & x < n}" apply (subgoal_tac " {(x :: int). 0 \ x & x < n} \ - int ` {(x :: nat). x < nat n}"); + 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 \ x & x \ n}"; +lemma bdd_int_set_le_finite: "finite {x::int. 0 \ x & x \ n}" apply (subgoal_tac "{x. 0 \ x & x \ n} = {x. 0 \ x & x < n + 1}") apply (erule ssubst) apply (rule bdd_int_set_l_finite) by auto -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} \ {x::int. 0 \ 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 \ n}"; +lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \ n}" apply (subgoal_tac "{x::int. 0 < x & x \ n} \ {x::int. 0 \ x & x \ n}") by (auto simp add: bdd_int_set_le_finite finite_subset) -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 \ x} = Suc x"; +lemma card_bdd_nat_set_le: "card { y::nat. y \ x} = Suc x" apply (subgoal_tac "{ y::nat. y \ x} = { y::nat. y < Suc x}") by (auto simp add: card_bdd_nat_set_l) -lemma card_bdd_int_set_l: "0 \ (n::int) ==> card {y. 0 \ y & y < n} = nat n"; -proof -; - fix n::int; - assume "0 \ n"; - have "finite {y. y < nat n}"; +lemma card_bdd_int_set_l: "0 \ (n::int) ==> card {y. 0 \ y & y < n} = nat n" +proof - + fix n::int + assume "0 \ n" + have "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 \ y & y < n}"; + also from prems have "int ` {y. y < nat n} = {y. 0 \ y & y < n}" apply (auto simp add: zless_nat_eq_int_zless image_def) apply (rule_tac x = "nat x" in exI) by (auto simp add: nat_0_le) - also; have "card {y. y < nat n} = nat n" + also have "card {y. y < nat n} = nat n" by (rule card_bdd_nat_set_l) - finally show "card {y. 0 \ y & y < n} = nat n"; .; -qed; + finally show "card {y. 0 \ y & y < n} = nat n" . +qed lemma card_bdd_int_set_le: "0 \ (n::int) ==> card {y. 0 \ y & y \ n} = - nat n + 1"; + nat n + 1" apply (subgoal_tac "{y. 0 \ y & y \ n} = {y. 0 \ y & y < n+1}") apply (insert card_bdd_int_set_l [of "n+1"]) by (auto simp add: nat_add_distrib) lemma card_bdd_int_set_l_le: "0 \ (n::int) ==> - card {x. 0 < x & x \ n} = nat n"; -proof -; - fix n::int; - assume "0 \ n"; - have "finite {x. 0 \ x & x < n}"; + card {x. 0 < x & x \ n} = nat n" +proof - + fix n::int + assume "0 \ n" + have "finite {x. 0 \ x & x < n}" by (rule bdd_int_set_l_finite) - moreover have "inj_on (%x. x+1) {x. 0 \ x & x < n}"; + moreover have "inj_on (%x. x+1) {x. 0 \ x & x < n}" by (auto simp add: inj_on_def) ultimately have "card ((%x. x+1) ` {x. 0 \ x & x < n}) = - card {x. 0 \ x & x < n}"; + card {x. 0 \ 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 \ x & x < n} = {x. 0 < x & x<= n}"; + also have "(%x. x + 1) ` {x. 0 \ x & x < n} = {x. 0 < x & x<= n}" apply (auto simp add: image_def) apply (rule_tac x = "x - 1" in exI) by arith - finally; show "card {x. 0 < x & x \ n} = nat n";.; -qed; + finally show "card {x. 0 < x & x \ n} = nat n". +qed lemma card_bdd_int_set_l_l: "0 < (n::int) ==> - card {x. 0 < x & x < n} = nat n - 1"; + card {x. 0 < x & x < n} = nat n - 1" apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \ n - 1}") apply (insert card_bdd_int_set_l_le [of "n - 1"]) by (auto simp add: nat_diff_distrib) lemma 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 \ 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 \ n ==> - int(card {x. 0 < x & x \ n}) = n"; + int(card {x. 0 < x & x \ 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) \ (A <*> B)"; + (insert x A) <*> B = ({ x } <*> B) \ (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 \ 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 \ f) B"; - apply (rule finite_induct, assumption, force) - apply (rule impI) - apply (auto simp add: inj_on_def) - apply (subgoal_tac "f x \ 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; \X \ A. finite X |] ==> - finite (Union A)"; + finite (Union A)" apply (induct set: Finites) by auto lemma finite_index_UNION_finite_sets: "finite A ==> - (\x \ A. finite (f x)) --> finite (UNION A f)"; + (\x \ A. finite (f x)) --> finite (UNION A f)" by (induct_tac rule: finite_induct, auto) lemma card_union_disjoint_sets: "finite A ==> ((\X \ A. finite X) & (\X \ A. \Y \ A. X \ Y --> X \ 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 ==> - ((\x \ A. finite (g x)) & - (\x \ A. \y \ A. x \ y --> (g x) \ (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 \ (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 ==> ((\x \ A. finite (g x)) & (\x \ A. \y \ A. x \ y --> (g x) \ (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 "(\x \ UNION A g. 1) = (\x \ A. \x \ g x. 1)"); + setsum_UN_disjoint) +apply assumption+ +apply (subgoal_tac "finite (UNION A g)") +apply (subgoal_tac "(\x \ UNION A g. 1) = (\x \ A. \x \ 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 ==> ((\x \ A. finite (g x)) & (\x \ A. \y \ A. x \ y --> (g x) \ (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 "(\x \ UNION A g. 1) = (\x \ A. \x \ g x. 1)"); + setsum_UN_disjoint) +apply assumption+ +apply (subgoal_tac "finite (UNION A g)") +apply (subgoal_tac "(\x \ UNION A g. 1) = (\x \ A. \x \ 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 \ B; inj_on f A; - g ` B \ A; inj_on g B |] ==> setsum g B = setsum (g \ f) A"; -apply (frule_tac h = g and f = f in sum_prop, auto) -apply (subgoal_tac "setsum g B = setsum g (f ` A)"); + g ` B \ A; inj_on g B |] ==> setsum g B = setsum (g \ f) A" +apply (frule_tac h = g and f = f in setsum_reindex) +apply (subgoal_tac "setsum g B = setsum g (f ` A)") 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 \ B; inj_on f A; - g ` B \ A; inj_on g B |] ==> gsetprod g B = gsetprod (g \ 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 \ B; inj_on f A; + g ` B \ A; inj_on g B |] ==> setprod g B = setprod (g \ f) A" + apply (frule_tac h = g and f = f in setprod_reindex) + apply (subgoal_tac "setprod g B = setprod g (f ` A)") apply (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 ==> - ((\X \ A. finite X) & (\X \ A. \Y \ A. X \ Y --> X \ 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 \ (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); - (\X \ A. finite (X :: int set)); - (\X \ A. (\Y \ A. (X :: int set) \ (Y :: int set) --> - (X \ 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 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; - \X \ A. finite X; - \X \ A. \Y \ A. (X \ Y --> X \ 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); - \X \ A. finite X; - \X \ A. \Y \ A. (X \ Y --> X \ 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 diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Gauss.thy --- 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 \ D) \ 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: "\x \ E. [p - x = 0 - x] (mod p)"; + moreover have a: "\x \ E. [p - x = 0 - x] (mod p)" apply clarify apply (insert zcong_id [of p]) by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto) - moreover have b: "\x \ E. [StandardRes p (p - x) = p - x](mod p)"; + moreover have b: "\x \ E. [StandardRes p (p - x) = p - x](mod p)" apply clarify by (simp add: StandardRes_prop1 zcong_sym) - moreover have "\x \ E. [StandardRes p (p - x) = - x](mod p)"; + moreover have "\x \ 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 diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Int2.thy --- 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; \x \ 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) (*****************************************************************) diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/IntFact.thy --- 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 ((\n. nat n) :: int => nat)" "zfact n = (if n \ 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 ((\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 \ 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: "\(d22set a) = zfact a" apply (induct a rule: d22set.induct) apply safe apply (simp add: d22set.simps zfact.simps) diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Quadratic_Reciprocity.thy --- 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 \ E)"; + also from C_eq have "... = setsum id (D \ 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 \ F)"; + setsum id D" +proof - + from F_Un_D_eq_A have "setsum id A = setsum id (D \ 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 * (\x \ A. x * a div p) + setsum id D + + also note QRLemma1 + also from QRLemma2 have "p * (\x \ A. x * a div p) + setsum id D + setsum id E - setsum id A = p * (\x \ 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 * (\x \ A. x * a div p) - - p * int (card E) + 2 * setsum id E"; + also have "... = p * (\x \ 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 \ zOdd ==> - (setsum (%x. ((x * a) div p)) A \ zEven) = (int(card E): zEven)"; -proof -; - assume a_odd: "a \ zOdd"; + (setsum (%x. ((x * a) div p)) A \ zEven) = (int(card E): zEven)" +proof - + assume a_odd: "a \ 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 \ zEven" by (rule odd_minus_one_even) - hence "(a - 1) * setsum id A \ zEven"; + hence "(a - 1) * setsum id A \ zEven" by (rule even_times_either) - moreover have "2 * setsum id E \ zEven"; + moreover have "2 * setsum id E \ zEven" by (auto simp add: zEven_def) ultimately have "(a - 1) * setsum id A - 2 * setsum id E \ 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 \ zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"; + hence "p \ 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 \ zOdd ==> - (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"; -proof -; - assume "a \ zOdd"; + (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))" +proof - + assume "a \ zOdd" from QRLemma4 have - "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \ zEven)";..; - moreover have "0 \ int(card E)"; + "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \ zEven)".. + moreover have "0 \ int(card E)" by auto - moreover have "0 \ setsum (%x. ((x * a) div p)) A"; - proof (intro setsum_non_neg); - from finite_A show "finite A";.; - next show "\x \ A. 0 \ x * a div p"; - proof; - fix x; - assume "x \ A"; - then have "0 \ x"; + moreover have "0 \ setsum (%x. ((x * a) div p)) A" + proof (intro setsum_nonneg) + from finite_A show "finite A". + next show "\x \ A. 0 \ x * a div p" + proof + fix x + assume "x \ A" + then have "0 \ x" by (auto simp add: A_def) - with a_nonzero have "0 \ x * a"; + with a_nonzero have "0 \ x * a" by (auto simp add: zero_le_mult_iff) - with p_g_2 show "0 \ x * a div p"; + with p_g_2 show "0 \ 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(((\x \ A. x * a div p)))"; + (-1)^nat(((\x \ 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 \ zOdd; 0 < a; ~([a = 0] (mod p));p \ zprime; 2 < p; A = {x. 0 < x & x \ (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 \ (q * j) div p) }" defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j & - (x \ (p * j) div q) }"; + (x \ (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 \ p - 1" by arith then have "2 div 2 \ (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 \ q - 1" by arith then have "2 div 2 \ (q - 1) div 2" by (rule zdiv_mono1, auto) then show ?thesis by auto -qed; +qed lemma (in QRTEMP) pb_neq_qa: "[|1 \ b; b \ (q - 1) div 2 |] ==> - (p * b \ q * a)"; -proof; - assume "p * b = q * a" and "1 \ b" and "b \ (q - 1) div 2"; + (p * b \ q * a)" +proof + assume "p * b = q * a" and "1 \ b" and "b \ (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 \ b"; - proof -; - assume "q dvd b"; + then have "q \ 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 \ (q - 1) div 2" by auto then have "2 * q \ 2 * ((q - 1) div 2)" by arith - then have "2 * q \ q - 1"; - proof -; - assume "2 * q \ 2 * ((q - 1) div 2)"; + then have "2 * q \ q - 1" + proof - + assume "2 * q \ 2 * ((q - 1) div 2)" with prems have "q \ 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 \ -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 \ 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 \ 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 \ S2 = {}"; +lemma (in QRTEMP) S1_Int_S2_prop: "S1 \ S2 = {}" by (auto simp add: S1_def S2_def) -lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \ S2"; +lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \ 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 \ (q - 1) div 2"; + proof - + fix a and b + assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \ (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 \ 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 \ (p - 1) div 2; 0 < b; b \ (q - 1) div 2 |] ==> - (p * b < q * a) = (b \ q * a div p)"; -proof -; - assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2"; - have "p * b < q * a ==> b \ q * a div p"; - proof -; - assume "p * b < q * a"; + (p * b < q * a) = (b \ q * a div p)" +proof - + assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2" + have "p * b < q * a ==> b \ q * a div p" + proof - + assume "p * b < q * a" then have "p * b \ q * a" by auto - then have "(p * b) div p \ (q * a) div p"; + then have "(p * b) div p \ (q * a) div p" by (rule zdiv_mono1, insert p_g_2, auto) - then show "b \ (q * a) div p"; + then show "b \ (q * a) div p" apply (subgoal_tac "p \ 0") apply (frule zdiv_zmult_self2, force) by (insert p_g_2, auto) - qed; - moreover have "b \ q * a div p ==> p * b < q * a"; - proof -; - assume "b \ q * a div p"; - then have "p * b \ p * ((q * a) div p)"; + qed + moreover have "b \ q * a div p ==> p * b < q * a" + proof - + assume "b \ q * a div p" + then have "p * b \ p * ((q * a) div p)" by (insert p_g_2, auto simp add: mult_le_cancel_left) - also have "... \ q * a"; + also have "... \ q * a" by (rule zdiv_leq_prop, insert p_g_2, auto) - finally have "p * b \ q * a" .; - then have "p * b < q * a | p * b = q * a"; + finally have "p * b \ 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 \ q * a"; + moreover have "p * b \ 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 \ (p - 1) div 2; 0 < b; b \ (q - 1) div 2 |] ==> - (q * a < p * b) = (a \ p * b div q)"; -proof -; - assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2"; - have "q * a < p * b ==> a \ p * b div q"; - proof -; - assume "q * a < p * b"; + (q * a < p * b) = (a \ p * b div q)" +proof - + assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2" + have "q * a < p * b ==> a \ p * b div q" + proof - + assume "q * a < p * b" then have "q * a \ p * b" by auto - then have "(q * a) div q \ (p * b) div q"; + then have "(q * a) div q \ (p * b) div q" by (rule zdiv_mono1, insert q_g_2, auto) - then show "a \ (p * b) div q"; + then show "a \ (p * b) div q" apply (subgoal_tac "q \ 0") apply (frule zdiv_zmult_self2, force) by (insert q_g_2, auto) - qed; - moreover have "a \ p * b div q ==> q * a < p * b"; - proof -; - assume "a \ p * b div q"; - then have "q * a \ q * ((p * b) div q)"; + qed + moreover have "a \ p * b div q ==> q * a < p * b" + proof - + assume "a \ p * b div q" + then have "q * a \ q * ((p * b) div q)" by (insert q_g_2, auto simp add: mult_le_cancel_left) - also have "... \ p * b"; + also have "... \ p * b" by (rule zdiv_leq_prop, insert q_g_2, auto) - finally have "q * a \ p * b" .; - then have "q * a < p * b | q * a = p * b"; + finally have "q * a \ 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 \ q * a"; + moreover have "p * b \ 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 \ zprime; q \ zprime; 2 < p; 2 < q |] ==> - (q * ((p - 1) div 2)) div p \ (q - 1) div 2"; -proof-; - assume "p \ zprime" and "q \ zprime" and "2 < p" and "2 < q"; + (q * ((p - 1) div 2)) div p \ (q - 1) div 2" +proof- + assume "p \ zprime" and "q \ zprime" and "2 < p" and "2 < q" (* Set up what's even and odd *) - then have "p \ zOdd & q \ zOdd"; + then have "p \ zOdd & q \ 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: "\j \ P_set. int (card (f1 j)) = (q * j) div p"; -proof; - fix j; - assume j_fact: "j \ P_set"; - have "int (card (f1 j)) = int (card {y. y \ Q_set & y \ (q * j) div p})"; - proof -; - have "finite (f1 j)"; - proof -; +lemma (in QRTEMP) aux3a: "\j \ P_set. int (card (f1 j)) = (q * j) div p" +proof + fix j + assume j_fact: "j \ P_set" + have "int (card (f1 j)) = int (card {y. y \ Q_set & y \ (q * j) div p})" + proof - + have "finite (f1 j)" + proof - have "(f1 j) \ 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 \ Q_set & y \ (q * j) div p}"; + moreover have "((%(x,y). y) ` (f1 j)) = {y. y \ Q_set & y \ (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 \ (q * j) div p})"; - proof -; + qed + also have "... = int (card {y. 0 < y & y \ (q * j) div p})" + proof - have "{y. y \ Q_set & y \ (q * j) div p} = - {y. 0 < y & y \ (q * j) div p}"; + {y. 0 < y & y \ (q * j) div p}" apply (auto simp add: Q_set_def) - proof -; - fix x; - assume "0 < x" and "x \ q * j div p"; - with j_fact P_set_def have "j \ (p - 1) div 2"; by auto - with q_g_2; have "q * j \ q * ((p - 1) div 2)"; + proof - + fix x + assume "0 < x" and "x \ q * j div p" + with j_fact P_set_def have "j \ (p - 1) div 2" by auto + with q_g_2 have "q * j \ q * ((p - 1) div 2)" by (auto simp add: mult_le_cancel_left) - with p_g_2 have "q * j div p \ q * ((p - 1) div 2) div p"; + with p_g_2 have "q * j div p \ q * ((p - 1) div 2) div p" by (auto simp add: zdiv_mono1) - also from prems have "... \ (q - 1) div 2"; + also from prems have "... \ (q - 1) div 2" apply simp apply (insert aux2) by (simp add: QRTEMP_def) finally show "x \ (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 \ j" by auto with q_g_2 have "q * 0 \ q * j" by (auto simp only: mult_left_mono) then have "0 \ q * j" by auto - then have "0 div p \ (q * j) div p"; + then have "0 div p \ (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: "\j \ Q_set. int (card (f2 j)) = (p * j) div q"; -proof; - fix j; - assume j_fact: "j \ Q_set"; - have "int (card (f2 j)) = int (card {y. y \ P_set & y \ (p * j) div q})"; - proof -; - have "finite (f2 j)"; - proof -; +lemma (in QRTEMP) aux3b: "\j \ Q_set. int (card (f2 j)) = (p * j) div q" +proof + fix j + assume j_fact: "j \ Q_set" + have "int (card (f2 j)) = int (card {y. y \ P_set & y \ (p * j) div q})" + proof - + have "finite (f2 j)" + proof - have "(f2 j) \ 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 \ P_set & y \ (p * j) div q}"; + moreover have "((%(x,y). x) ` (f2 j)) = {y. y \ P_set & y \ (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 \ (p * j) div q})"; - proof -; + qed + also have "... = int (card {y. 0 < y & y \ (p * j) div q})" + proof - have "{y. y \ P_set & y \ (p * j) div q} = - {y. 0 < y & y \ (p * j) div q}"; + {y. 0 < y & y \ (p * j) div q}" apply (auto simp add: P_set_def) - proof -; - fix x; - assume "0 < x" and "x \ p * j div q"; - with j_fact Q_set_def have "j \ (q - 1) div 2"; by auto - with p_g_2; have "p * j \ p * ((q - 1) div 2)"; + proof - + fix x + assume "0 < x" and "x \ p * j div q" + with j_fact Q_set_def have "j \ (q - 1) div 2" by auto + with p_g_2 have "p * j \ p * ((q - 1) div 2)" by (auto simp add: mult_le_cancel_left) - with q_g_2 have "p * j div q \ p * ((q - 1) div 2) div q"; + with q_g_2 have "p * j div q \ p * ((q - 1) div 2) div q" by (auto simp add: zdiv_mono1) - also from prems have "... \ (p - 1) div 2"; + also from prems have "... \ (p - 1) div 2" by (auto simp add: aux2 QRTEMP_def) finally show "x \ (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 \ j" by auto with p_g_2 have "p * 0 \ p * j" by (auto simp only: mult_left_mono) then have "0 \ p * j" by auto - then have "0 div q \ (p * j) div q"; + then have "0 div q \ (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 "\x \ 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 "\x \ P_set. finite (f1 x)" + proof + fix x have "f1 x \ S" by (auto simp add: f1_def) with S_finite show "finite (f1 x)" by (auto simp add: finite_subset) - qed; - moreover have "(\x \ P_set. \y \ P_set. x \ y --> (f1 x) \ (f1 y) = {})"; + qed + moreover have "(\x \ P_set. \y \ P_set. x \ y --> (f1 x) \ (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 "\x \ 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 "\x \ Q_set. finite (f2 x)" + proof + fix x have "f2 x \ S" by (auto simp add: f2_def) with S_finite show "finite (f2 x)" by (auto simp add: finite_subset) - qed; + qed moreover have "(\x \ Q_set. \y \ Q_set. x \ y --> - (f2 x) \ (f2 y) = {})"; + (f2 x) \ (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 \ zprime; q \ zprime; p \ q |] ==> (~[p = 0] (mod q))"; +lemma pq_prime_neq: "[| p \ zprime; q \ zprime; p \ q |] ==> (~[p = 0] (mod q))" apply (auto simp add: zcong_eq_zdvd_prop zprime_def) apply (drule_tac x = q in allE) apply (drule_tac x = p in allE) 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 \ zOdd; p \ zprime; q \ zOdd; q \ zprime; p \ 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) diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Residues.thy --- 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) diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/WilsonBij.thy --- 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 \ zprime ==> A \ bijER (reciR p) ==> [setprod A = 1] (mod p)" + "p \ zprime ==> A \ bijER (reciR p) ==> [\A = 1] (mod p)" apply (unfold reciR_def) apply (erule bijER.induct) apply (subgoal_tac [2] "a = 1 \ a = p - 1") @@ -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) * \A) (1 * 1) p") apply (simp add: zmult_assoc) apply (rule zcong_zmult) apply auto diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/WilsonRuss.thy --- 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 \ zprime --> - 5 \ p --> a < p - 1 --> [setprod (wset (a, p)) = 1] (mod p)" + 5 \ p --> a < p - 1 --> [(\x\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 * (\x\ wset(a - 1, p). x)) (1 * 1) p") prefer 5 apply (simp add: zmult_assoc) apply (rule_tac [5] zcong_zmult)