# HG changeset patch # User paulson # Date 1529269243 -3600 # Node ID 023b353911c5007e02d42f4395dfadfdd237eec6 # Parent ba2a92af88b428458fe1ac766cc6360549a695ed Algebra tidy-up diff -r ba2a92af88b4 -r 023b353911c5 src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Sat Jun 16 22:09:24 2018 +0200 +++ b/src/HOL/Algebra/FiniteProduct.thy Sun Jun 17 22:00:43 2018 +0100 @@ -13,42 +13,40 @@ subsubsection \Inductive Definition of a Relation for Products over Sets\ text \Instantiation of locale \LC\ of theory \Finite_Set\ is not - possible, because here we have explicit typing rules like + possible, because here we have explicit typing rules like \x \ carrier G\. We introduce an explicit argument for the domain \D\.\ inductive_set - foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" - for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a + foldSetD :: "['a set, 'b \ 'a \ 'a, 'a] \ ('b set * 'a) set" + for D :: "'a set" and f :: "'b \ 'a \ 'a" and e :: 'a where - emptyI [intro]: "e \ D ==> ({}, e) \ foldSetD D f e" - | insertI [intro]: "[| x \ A; f x y \ D; (A, y) \ foldSetD D f e |] ==> + emptyI [intro]: "e \ D \ ({}, e) \ foldSetD D f e" + | insertI [intro]: "\x \ A; f x y \ D; (A, y) \ foldSetD D f e\ \ (insert x A, f x y) \ foldSetD D f e" inductive_cases empty_foldSetDE [elim!]: "({}, x) \ foldSetD D f e" definition - foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" + foldD :: "['a set, 'b \ 'a \ 'a, 'a, 'b set] \ 'a" where "foldD D f e A = (THE x. (A, x) \ foldSetD D f e)" lemma foldSetD_closed: - "[| (A, z) \ foldSetD D f e ; e \ D; !!x y. [| x \ A; y \ D |] ==> f x y \ D - |] ==> z \ D" + "\(A, z) \ foldSetD D f e; e \ D; \x y. \x \ A; y \ D\ \ f x y \ D\ + \ z \ D" by (erule foldSetD.cases) auto lemma Diff1_foldSetD: - "[| (A - {x}, y) \ foldSetD D f e; x \ A; f x y \ D |] ==> + "\(A - {x}, y) \ foldSetD D f e; x \ A; f x y \ D\ \ (A, f x y) \ foldSetD D f e" - apply (erule insert_Diff [THEN subst], rule foldSetD.intros) - apply auto - done + by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert) -lemma foldSetD_imp_finite [simp]: "(A, x) \ foldSetD D f e ==> finite A" +lemma foldSetD_imp_finite [simp]: "(A, x) \ foldSetD D f e \ finite A" by (induct set: foldSetD) auto lemma finite_imp_foldSetD: - "[| finite A; e \ D; !!x y. [| x \ A; y \ D |] ==> f x y \ D |] ==> - \x. (A, x) \ foldSetD D f e" + "\finite A; e \ D; \x y. \x \ A; y \ D\ \ f x y \ D\ + \ \x. (A, x) \ foldSetD D f e" proof (induct set: finite) case empty then show ?case by auto next @@ -66,30 +64,21 @@ locale LCD = fixes B :: "'b set" and D :: "'a set" - and f :: "'b => 'a => 'a" (infixl "\" 70) + and f :: "'b \ 'a \ 'a" (infixl "\" 70) assumes left_commute: - "[| x \ B; y \ B; z \ D |] ==> x \ (y \ z) = y \ (x \ z)" - and f_closed [simp, intro!]: "!!x y. [| x \ B; y \ D |] ==> f x y \ D" + "\x \ B; y \ B; z \ D\ \ x \ (y \ z) = y \ (x \ z)" + and f_closed [simp, intro!]: "!!x y. \x \ B; y \ D\ \ f x y \ D" -lemma (in LCD) foldSetD_closed [dest]: - "(A, z) \ foldSetD D f e ==> z \ D" +lemma (in LCD) foldSetD_closed [dest]: "(A, z) \ foldSetD D f e \ z \ D" by (erule foldSetD.cases) auto lemma (in LCD) Diff1_foldSetD: - "[| (A - {x}, y) \ foldSetD D f e; x \ A; A \ B |] ==> + "\(A - {x}, y) \ foldSetD D f e; x \ A; A \ B\ \ (A, f x y) \ foldSetD D f e" - apply (subgoal_tac "x \ B") - prefer 2 apply fast - apply (erule insert_Diff [THEN subst], rule foldSetD.intros) - apply auto - done - -lemma (in LCD) foldSetD_imp_finite [simp]: - "(A, x) \ foldSetD D f e ==> finite A" - by (induct set: foldSetD) auto + by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE) lemma (in LCD) finite_imp_foldSetD: - "[| finite A; A \ B; e \ D |] ==> \x. (A, x) \ foldSetD D f e" + "\finite A; A \ B; e \ D\ \ \x. (A, x) \ foldSetD D f e" proof (induct set: finite) case empty then show ?case by auto next @@ -101,94 +90,113 @@ then show ?case .. qed + lemma (in LCD) foldSetD_determ_aux: - "e \ D \ \A x. A \ B \ card A < n \ (A, x) \ foldSetD D f e \ - (\y. (A, y) \ foldSetD D f e \ y = x)" - apply (induct n) - apply (auto simp add: less_Suc_eq) (* slow *) - apply (erule foldSetD.cases) - apply blast - apply (erule foldSetD.cases) - apply blast - apply clarify - txt \force simplification of \card A < card (insert ...)\.\ - apply (erule rev_mp) - apply (simp add: less_Suc_eq_le) - apply (rule impI) - apply (rename_tac xa Aa ya xb Ab yb, case_tac "xa = xb") - apply (subgoal_tac "Aa = Ab") - prefer 2 apply (blast elim!: equalityE) - apply blast - txt \case @{prop "xa \ xb"}.\ - apply (subgoal_tac "Aa - {xb} = Ab - {xa} \ xb \ Aa \ xa \ Ab") - prefer 2 apply (blast elim!: equalityE) - apply 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}" in finite_imp_foldSetD [THEN exE]) - apply (blast intro: foldSetD_imp_finite) - apply best - apply assumption - apply (frule (1) Diff1_foldSetD) - apply best - apply (subgoal_tac "ya = f xb x") - prefer 2 - apply (subgoal_tac "Aa \ B") - prefer 2 apply best (* slow *) - apply (blast del: equalityCE) - apply (subgoal_tac "(Ab - {xa}, x) \ foldSetD D f e") - prefer 2 apply simp - apply (subgoal_tac "yb = f xa x") - prefer 2 - apply (blast del: equalityCE dest: Diff1_foldSetD) - apply (simp (no_asm_simp)) - apply (rule left_commute) - apply assumption - apply best (* slow *) - apply best - done + assumes "e \ D" and A: "card A < n" "A \ B" "(A, x) \ foldSetD D f e" "(A, y) \ foldSetD D f e" + shows "y = x" + using A +proof (induction n arbitrary: A x y) + case 0 + then show ?case + by auto +next + case (Suc n) + then consider "card A = n" | "card A < n" + by linarith + then show ?case + proof cases + case 1 + show ?thesis + using foldSetD.cases [OF \(A,x) \ foldSetD D (\) e\] + proof cases + case 1 + then show ?thesis + using \(A,y) \ foldSetD D (\) e\ by auto + next + case (2 x' A' y') + note A' = this + show ?thesis + using foldSetD.cases [OF \(A,y) \ foldSetD D (\) e\] + proof cases + case 1 + then show ?thesis + using \(A,x) \ foldSetD D (\) e\ by auto + next + case (2 x'' A'' y'') + note A'' = this + show ?thesis + proof (cases "x' = x''") + case True + show ?thesis + proof (cases "y' = y''") + case True + then show ?thesis + using A' A'' \x' = x''\ by (blast elim!: equalityE) + next + case False + then show ?thesis + using A' A'' \x' = x''\ + by (metis \card A = n\ Suc.IH Suc.prems(2) card_insert_disjoint foldSetD_imp_finite insert_eq_iff insert_subset lessI) + qed + next + case False + then have *: "A' - {x''} = A'' - {x'}" "x'' \ A'" "x' \ A''" + using A' A'' by fastforce+ + then have "A' = insert x'' A'' - {x'}" + using \x' \ A'\ by blast + then have card: "card A' \ card A''" + using A' A'' * by (metis card_Suc_Diff1 eq_refl foldSetD_imp_finite) + obtain u where u: "(A' - {x''}, u) \ foldSetD D (\) e" + using finite_imp_foldSetD [of "A' - {x''}"] A' Diff_insert \A \ B\ \e \ D\ by fastforce + have "y' = f x'' u" + using Diff1_foldSetD [OF u] \x'' \ A'\ \card A = n\ A' Suc.IH \A \ B\ by auto + then have "(A'' - {x'}, u) \ foldSetD D f e" + using "*"(1) u by auto + then have "y'' = f x' u" + using A'' by (metis * \card A = n\ A'(1) Diff1_foldSetD Suc.IH \A \ B\ + card card_Suc_Diff1 card_insert_disjoint foldSetD_imp_finite insert_subset le_imp_less_Suc) + then show ?thesis + using A' A'' + by (metis \A \ B\ \y' = x'' \ u\ insert_subset left_commute local.foldSetD_closed u) + qed + qed + qed + next + case 2 with Suc show ?thesis by blast + qed +qed lemma (in LCD) foldSetD_determ: - "[| (A, x) \ foldSetD D f e; (A, y) \ foldSetD D f e; e \ D; A \ B |] - ==> y = x" + "\(A, x) \ foldSetD D f e; (A, y) \ foldSetD D f e; e \ D; A \ B\ + \ y = x" by (blast intro: foldSetD_determ_aux [rule_format]) lemma (in LCD) foldD_equality: - "[| (A, y) \ foldSetD D f e; e \ D; A \ B |] ==> foldD D f e A = y" + "\(A, y) \ foldSetD D f e; e \ D; A \ B\ \ foldD D f e A = y" by (unfold foldD_def) (blast intro: foldSetD_determ) lemma foldD_empty [simp]: - "e \ D ==> foldD D f e {} = e" + "e \ D \ foldD D f e {} = e" by (unfold foldD_def) blast lemma (in LCD) foldD_insert_aux: - "[| x \ A; x \ B; e \ D; A \ B |] ==> - ((insert x A, v) \ foldSetD D f e) = - (\y. (A, y) \ foldSetD D f e \ v = f x y)" + "\x \ A; x \ B; e \ D; A \ B\ + \ ((insert x A, v) \ foldSetD D f e) \ (\y. (A, y) \ foldSetD D f e \ v = f x y)" apply auto - apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE]) - apply (fastforce dest: foldSetD_imp_finite) - apply assumption - apply assumption - apply (blast intro: foldSetD_determ) - done + by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed) lemma (in LCD) foldD_insert: - "[| finite A; x \ A; x \ B; e \ D; A \ B |] ==> - foldD D f e (insert x A) = f x (foldD D f e A)" - apply (unfold foldD_def) - apply (simp add: foldD_insert_aux) - apply (rule the_equality) - apply (auto intro: finite_imp_foldSetD - cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality) - done + assumes "finite A" "x \ A" "x \ B" "e \ D" "A \ B" + shows "foldD D f e (insert x A) = f x (foldD D f e A)" +proof - + have "(THE v. \y. (A, y) \ foldSetD D (\) e \ v = x \ y) = x \ (THE y. (A, y) \ foldSetD D (\) e)" + by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in \metis+\) + then show ?thesis + unfolding foldD_def using assms by (simp add: foldD_insert_aux) +qed lemma (in LCD) foldD_closed [simp]: - "[| finite A; e \ D; A \ B |] ==> foldD D f e A \ D" + "\finite A; e \ D; A \ B\ \ foldD D f e A \ D" proof (induct set: finite) case empty then show ?case by simp next @@ -196,29 +204,26 @@ qed lemma (in LCD) foldD_commute: - "[| finite A; x \ B; e \ D; A \ B |] ==> + "\finite A; x \ B; e \ D; A \ B\ \ f x (foldD D f e A) = foldD D f (f x e) A" - apply (induct set: finite) - apply simp - apply (auto simp add: left_commute foldD_insert) - done + by (induct set: finite) (auto simp add: left_commute foldD_insert) lemma Int_mono2: - "[| A \ C; B \ C |] ==> A Int B \ C" + "\A \ C; B \ C\ \ A Int B \ C" by blast lemma (in LCD) foldD_nest_Un_Int: - "[| finite A; finite C; e \ D; A \ B; C \ B |] ==> + "\finite A; finite C; e \ D; A \ B; C \ B\ \ foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)" - apply (induct set: finite) - apply simp - apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb - Int_mono2) - done +proof (induction set: finite) + case (insert x F) + then show ?case + by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2) +qed simp lemma (in LCD) foldD_nest_Un_disjoint: - "[| finite A; finite B; A Int B = {}; e \ D; A \ B; C \ B |] - ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A" + "\finite A; finite B; A Int B = {}; e \ D; A \ B; C \ B\ + \ foldD D f e (A Un B) = foldD D f (foldD D f e B) A" by (simp add: foldD_nest_Un_Int) \ \Delete rules to do with \foldSetD\ relation.\ @@ -233,22 +238,22 @@ text \Commutative Monoids\ text \ - We enter a more restrictive context, with \f :: 'a => 'a => 'a\ - instead of \'b => 'a => 'a\. + We enter a more restrictive context, with \f :: 'a \ 'a \ 'a\ + instead of \'b \ 'a \ 'a\. \ locale ACeD = fixes D :: "'a set" - and f :: "'a => 'a => 'a" (infixl "\" 70) + and f :: "'a \ 'a \ 'a" (infixl "\" 70) and e :: 'a - assumes ident [simp]: "x \ D ==> x \ e = x" - and commute: "[| x \ D; y \ D |] ==> x \ y = y \ x" - and assoc: "[| x \ D; y \ D; z \ D |] ==> (x \ y) \ z = x \ (y \ z)" + assumes ident [simp]: "x \ D \ x \ e = x" + and commute: "\x \ D; y \ D\ \ x \ y = y \ x" + and assoc: "\x \ D; y \ D; z \ D\ \ (x \ y) \ z = x \ (y \ z)" and e_closed [simp]: "e \ D" - and f_closed [simp]: "[| x \ D; y \ D |] ==> x \ y \ D" + and f_closed [simp]: "\x \ D; y \ D\ \ x \ y \ D" lemma (in ACeD) left_commute: - "[| x \ D; y \ D; z \ D |] ==> x \ (y \ z) = y \ (x \ z)" + "\x \ D; y \ D; z \ D\ \ x \ (y \ z) = y \ (x \ z)" proof - assume D: "x \ D" "y \ D" "z \ D" then have "x \ (y \ z) = (y \ z) \ x" by (simp add: commute) @@ -259,7 +264,7 @@ lemmas (in ACeD) AC = assoc commute left_commute -lemma (in ACeD) left_ident [simp]: "x \ D ==> e \ x = x" +lemma (in ACeD) left_ident [simp]: "x \ D \ e \ x = x" proof - assume "x \ D" then have "x \ e = x" by (rule ident) @@ -267,19 +272,23 @@ qed lemma (in ACeD) foldD_Un_Int: - "[| finite A; finite B; A \ D; B \ D |] ==> + "\finite A; finite B; A \ D; B \ D\ \ foldD D f e A \ foldD D f e B = foldD D f e (A Un B) \ foldD D f e (A Int B)" - apply (induct set: finite) - apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]]) - apply (simp add: AC insert_absorb Int_insert_left - LCD.foldD_insert [OF LCD.intro [of D]] - LCD.foldD_closed [OF LCD.intro [of D]] - Int_mono2) - done +proof (induction set: finite) + case empty + then show ?case + by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]]) +next + case (insert x F) + then show ?case + by(simp add: AC insert_absorb Int_insert_left Int_mono2 + LCD.foldD_insert [OF LCD.intro [of D]] + LCD.foldD_closed [OF LCD.intro [of D]]) +qed lemma (in ACeD) foldD_Un_disjoint: - "[| finite A; finite B; A Int B = {}; A \ D; B \ D |] ==> + "\finite A; finite B; A Int B = {}; A \ D; B \ D\ \ foldD D f e (A Un B) = foldD D f e A \ foldD D f e B" by (simp add: foldD_Un_Int left_commute LCD.foldD_closed [OF LCD.intro [of D]]) @@ -288,25 +297,25 @@ subsubsection \Products over Finite Sets\ definition - finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" + finprod :: "[('b, 'm) monoid_scheme, 'a \ 'b, 'a set] \ 'b" where "finprod G f A = (if finite A then foldD (carrier G) (mult G \ f) \\<^bsub>G\<^esub> A else \\<^bsub>G\<^esub>)" syntax - "_finprod" :: "index => idt => 'a set => 'b => 'b" + "_finprod" :: "index \ idt \ 'a set \ 'b \ 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations "\\<^bsub>G\<^esub>i\A. b" \ "CONST finprod G (%i. b) A" \ \Beware of argument permutation!\ -lemma (in comm_monoid) finprod_empty [simp]: +lemma (in comm_monoid) finprod_empty [simp]: "finprod G f {} = \" by (simp add: finprod_def) lemma (in comm_monoid) finprod_infinite[simp]: - "\ finite A \ finprod G f A = \" + "\ finite A \ finprod G f A = \" by (simp add: finprod_def) declare funcsetI [intro] @@ -315,22 +324,18 @@ context comm_monoid begin lemma finprod_insert [simp]: - "[| finite F; a \ F; f \ F \ carrier G; f a \ carrier G |] ==> - finprod G f (insert a F) = f a \ finprod G f F" - apply (rule trans) - apply (simp add: finprod_def) - apply (rule trans) - apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) - apply simp - apply (rule m_lcomm) - apply fast - apply fast - apply assumption - apply fastforce - apply simp+ - apply fast - apply (auto simp add: finprod_def) - done + assumes "finite F" "a \ F" "f \ F \ carrier G" "f a \ carrier G" + shows "finprod G f (insert a F) = f a \ finprod G f F" +proof - + have "finprod G f (insert a F) = foldD (carrier G) ((\) \ f) \ (insert a F)" + by (simp add: finprod_def assms) + also have "... = ((\) \ f) a (foldD (carrier G) ((\) \ f) \ F)" + by (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) + (use assms in \auto simp: m_lcomm Pi_iff\) + also have "... = f a \ finprod G f F" + using \finite F\ by (auto simp add: finprod_def) + finally show ?thesis . +qed lemma finprod_one_eqI: "(\x. x \ A \ f x = \) \ finprod G f A = \" proof (induct A rule: infinite_finite_induct) @@ -346,7 +351,7 @@ lemma finprod_closed [simp]: fixes A - assumes f: "f \ A \ carrier G" + assumes f: "f \ A \ carrier G" shows "finprod G f A \ carrier G" using f proof (induct A rule: infinite_finite_induct) @@ -359,7 +364,7 @@ qed simp lemma funcset_Int_left [simp, intro]: - "[| f \ A \ C; f \ B \ C |] ==> f \ A Int B \ C" + "\f \ A \ C; f \ B \ C\ \ f \ A Int B \ C" by fast lemma funcset_Un_left [iff]: @@ -367,7 +372,7 @@ by fast lemma finprod_Un_Int: - "[| finite A; finite B; g \ A \ carrier G; g \ B \ carrier G |] ==> + "\finite A; finite B; g \ A \ carrier G; g \ B \ carrier G\ \ finprod G g (A Un B) \ finprod G g (A Int B) = finprod G g A \ finprod G g B" \ \The reversed orientation looks more natural, but LOOPS as a simprule!\ @@ -378,19 +383,17 @@ then have a: "g a \ carrier G" by fast from insert have A: "g \ A \ carrier G" by fast from insert A a show ?case - by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) + by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) qed lemma finprod_Un_disjoint: - "[| finite A; finite B; A Int B = {}; - g \ A \ carrier G; g \ B \ carrier G |] - ==> finprod G g (A Un B) = finprod G g A \ finprod G g B" - apply (subst finprod_Un_Int [symmetric]) - apply auto - done + "\finite A; finite B; A Int B = {}; + g \ A \ carrier G; g \ B \ carrier G\ + \ finprod G g (A Un B) = finprod G g A \ finprod G g B" + by (metis Pi_split_domain finprod_Un_Int finprod_closed finprod_empty r_one) lemma finprod_multf: - "[| f \ A \ carrier G; g \ A \ carrier G |] ==> + "\f \ A \ carrier G; g \ A \ carrier G\ \ finprod G (%x. f x \ g x) A = (finprod G f A \ finprod G g A)" proof (induct A rule: infinite_finite_induct) case empty show ?case by simp @@ -407,16 +410,16 @@ qed simp lemma finprod_cong': - "[| A = B; g \ B \ carrier G; - !!i. i \ B ==> f i = g i |] ==> finprod G f A = finprod G g B" + "\A = B; g \ B \ carrier G; + !!i. i \ B \ f i = g i\ \ finprod G f A = finprod G g B" proof - assume prems: "A = B" "g \ B \ carrier G" - "!!i. i \ B ==> f i = g i" + "!!i. i \ B \ f i = g i" show ?thesis proof (cases "finite B") case True - then have "!!A. [| A = B; g \ B \ carrier G; - !!i. i \ B ==> f i = g i |] ==> finprod G f A = finprod G g B" + then have "!!A. \A = B; g \ B \ carrier G; + !!i. i \ B \ f i = g i\ \ finprod G f A = finprod G g B" proof induct case empty thus ?case by simp next @@ -448,8 +451,8 @@ qed lemma finprod_cong: - "[| A = B; f \ B \ carrier G = True; - !!i. i \ B =simp=> f i = g i |] ==> finprod G f A = finprod G g B" + "\A = B; f \ B \ carrier G = True; + \i. i \ B =simp=> f i = g i\ \ finprod G f A = finprod G g B" (* This order of prems is slightly faster (3%) than the last two swapped. *) by (rule finprod_cong') (auto simp add: simp_implies_def) @@ -468,16 +471,16 @@ context comm_monoid begin lemma finprod_0 [simp]: - "f \ {0::nat} \ carrier G ==> finprod G f {..0} = f 0" + "f \ {0::nat} \ carrier G \ finprod G f {..0} = f 0" by (simp add: Pi_def) lemma finprod_Suc [simp]: - "f \ {..Suc n} \ carrier G ==> + "f \ {..Suc n} \ carrier G \ finprod G f {..Suc n} = (f (Suc n) \ finprod G f {..n})" by (simp add: Pi_def atMost_Suc) lemma finprod_Suc2: - "f \ {..Suc n} \ carrier G ==> + "f \ {..Suc n} \ carrier G \ finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \ f 0)" proof (induct n) case 0 thus ?case by (simp add: Pi_def) @@ -486,7 +489,7 @@ qed lemma finprod_mult [simp]: - "[| f \ {..n} \ carrier G; g \ {..n} \ carrier G |] ==> + "\f \ {..n} \ carrier G; g \ {..n} \ carrier G\ \ finprod G (%i. f i \ g i) {..n::nat} = finprod G f {..n} \ finprod G g {..n}" by (induct n) (simp_all add: m_ac Pi_def) @@ -494,7 +497,7 @@ (* The following two were contributed by Jeremy Avigad. *) lemma finprod_reindex: - "f \ (h ` A) \ carrier G \ + "f \ (h ` A) \ carrier G \ inj_on h A \ finprod G f (h ` A) = finprod G (\x. f (h x)) A" proof (induct A rule: infinite_finite_induct) case (infinite A) @@ -508,7 +511,7 @@ shows "finprod G (\x. a) A = a [^] card A" proof (induct A rule: infinite_finite_induct) case (insert b A) - show ?case + show ?case proof (subst finprod_insert[OF insert(1-2)]) show "a \ (\x\A. a) = a [^] card (insert b A)" by (insert insert, auto, subst m_comm, auto) @@ -522,7 +525,7 @@ shows "(\j\A. if i = j then f j else \) = f i" using i_in_A finprod_insert [of "A - {i}" i "(\j. if i = j then f j else \)"] fin_A f_Pi finprod_one [of "A - {i}"] - finprod_cong [of "A - {i}" "A - {i}" "(\j. if i = j then f j else \)" "(\i. \)"] + finprod_cong [of "A - {i}" "A - {i}" "(\j. if i = j then f j else \)" "(\i. \)"] unfolding Pi_def simp_implies_def by (force simp add: insert_absorb) end @@ -537,7 +540,7 @@ proof - have "(\x\carrier G. x) = (\x\carrier G. a \ x)" by (subst (2) finprod_reindex [symmetric], - auto simp add: Pi_def inj_on_const_mult surj_const_mult) + auto simp add: Pi_def inj_on_cmult surj_const_mult) also have "\ = (\x\carrier G. a) \ (\x\carrier G. x)" by (auto simp add: finprod_multf Pi_def) also have "(\x\carrier G. a) = a [^] card(carrier G)" @@ -547,26 +550,28 @@ by auto qed - lemma (in comm_monoid) finprod_UN_disjoint: - "finite I \ (\i\I. finite (A i)) \ (\i\I. \j\I. i \ j \ A i \ A j = {}) \ - (\i\I. \x \ A i. g x \ carrier G) \ - finprod G g (UNION I A) = finprod G (\i. finprod G g (A i)) I" - apply (induct set: finite) - apply force - apply clarsimp - apply (subst finprod_Un_disjoint) - apply blast - apply (erule finite_UN_I) - apply blast - apply (fastforce) - apply (auto intro!: funcsetI finprod_closed) - done + assumes + "finite I" "\i. i \ I \ finite (A i)" "pairwise (\i j. disjnt (A i) (A j)) I" + "\i x. i \ I \ x \ A i \ g x \ carrier G" +shows "finprod G g (UNION I A) = finprod G (\i. finprod G g (A i)) I" + using assms +proof (induction set: finite) + case empty + then show ?case + by force +next + case (insert i I) + then show ?case + unfolding pairwise_def disjnt_def + apply clarsimp + apply (subst finprod_Un_disjoint) + apply (fastforce intro!: funcsetI finprod_closed)+ + done +qed lemma (in comm_monoid) finprod_Union_disjoint: - "finite C \ - \A\C. finite A \ (\x\A. f x \ carrier G) \ - \A\C. \B\C. A \ B \ A \ B = {} \ + "\finite C; \A. A \ C \ finite A \ (\x\A. f x \ carrier G); pairwise disjnt C\ \ finprod G f (\C) = finprod G (finprod G f) C" apply (frule finprod_UN_disjoint [of C id f]) apply auto diff -r ba2a92af88b4 -r 023b353911c5 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Sat Jun 16 22:09:24 2018 +0200 +++ b/src/HOL/Algebra/Group.thy Sun Jun 17 22:00:43 2018 +0100 @@ -136,10 +136,7 @@ lemma (in monoid) Units_r_inv [simp]: "x \ Units G ==> x \ inv x = \" - apply (unfold Units_def m_inv_def, auto) - apply (rule theI2, fast) - apply (fast intro: inv_unique, fast) - done + by (metis (full_types) Units_closed Units_inv_closed Units_l_inv Units_r_inv_ex inv_unique) lemma (in monoid) inv_one [simp]: "inv \ = \" @@ -503,10 +500,6 @@ "x \ H \ x \ carrier G" using subset by blast -lemma submonoid_imp_subset: - "submonoid H G \ H \ carrier G" - by (rule submonoid.subset) - lemma (in submonoid) submonoid_is_monoid [intro]: assumes "monoid G" shows "monoid (G\carrier := H\)" @@ -516,15 +509,6 @@ by (simp add: monoid_def m_assoc) qed -lemma (in monoid) submonoidE: - assumes "submonoid H G" - shows "H \ carrier G" - and "H \ {}" - and "\a b. \a \ H; b \ H\ \ a \ b \ H" - using assms submonoid_imp_subset apply blast - using assms submonoid_def apply auto[1] - by (simp add: assms submonoid.m_closed)+ - lemma submonoid_nonempty: "~ submonoid {} G" by (blast dest: submonoid.one_closed) @@ -569,21 +553,15 @@ "x \ H \ x \ carrier G" using subset by blast -(*DELETE*) -lemma subgroup_imp_subset: - "subgroup H G \ H \ carrier G" - by (rule subgroup.subset) - lemma (in subgroup) subgroup_is_group [intro]: assumes "group G" shows "group (G\carrier := H\)" proof - interpret group G by fact - show ?thesis - apply (rule monoid.group_l_invI) - apply (unfold_locales) [1] - apply (auto intro: m_assoc l_inv mem_carrier) - done + have "Group.monoid (G\carrier := H\)" + by (simp add: monoid_axioms submonoid.intro submonoid.submonoid_is_monoid subset) + then show ?thesis + by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier) qed lemma (in group) subgroup_inv_equality: @@ -808,23 +786,42 @@ using iso_set_refl unfolding is_iso_def by auto lemma (in group) iso_set_sym: - "h \ iso G H \ inv_into (carrier G) h \ (iso H G)" -apply (simp add: iso_def bij_betw_inv_into) -apply (subgoal_tac "inv_into (carrier G) h \ carrier H \ carrier G") - prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) -apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def) -done + assumes "h \ iso G H" + shows "inv_into (carrier G) h \ iso H G" +proof - + have h: "h \ hom G H" "bij_betw h (carrier G) (carrier H)" + using assms by (auto simp add: iso_def bij_betw_inv_into) + then have HG: "bij_betw (inv_into (carrier G) h) (carrier H) (carrier G)" + by (simp add: bij_betw_inv_into) + have "inv_into (carrier G) h \ hom H G" + unfolding hom_def + proof safe + show *: "\x. x \ carrier H \ inv_into (carrier G) h x \ carrier G" + by (meson HG bij_betwE) + show "inv_into (carrier G) h (x \\<^bsub>H\<^esub> y) = inv_into (carrier G) h x \ inv_into (carrier G) h y" + if "x \ carrier H" "y \ carrier H" for x y + proof (rule inv_into_f_eq) + show "inj_on h (carrier G)" + using bij_betw_def h(2) by blast + show "inv_into (carrier G) h x \ inv_into (carrier G) h y \ carrier G" + by (simp add: * that) + show "h (inv_into (carrier G) h x \ inv_into (carrier G) h y) = x \\<^bsub>H\<^esub> y" + using h bij_betw_inv_into_right [of h] unfolding hom_def by (simp add: "*" that) + qed + qed + then show ?thesis + by (simp add: Group.iso_def bij_betw_inv_into h) +qed -corollary (in group) iso_sym : -"G \ H \ H \ G" + +corollary (in group) iso_sym: "G \ H \ H \ G" using iso_set_sym unfolding is_iso_def by auto lemma (in group) iso_set_trans: "[|h \ iso G H; i \ iso H I|] ==> (compose (carrier G) i h) \ iso G I" by (auto simp add: iso_def hom_compose bij_betw_compose) -corollary (in group) iso_trans : -"\G \ H ; H \ I\ \ G \ I" +corollary (in group) iso_trans: "\G \ H ; H \ I\ \ G \ I" using iso_set_trans unfolding is_iso_def by blast (* Next four lemmas contributed by Paulo. *) @@ -1143,15 +1140,6 @@ shows "comm_monoid G" by (rule comm_monoidI) (auto intro: m_assoc m_comm) -(*lemma (in comm_monoid) r_one [simp]: - "x \ carrier G ==> x \ \ = x" -proof - - assume G: "x \ carrier G" - then have "x \ \ = \ \ x" by (simp add: m_comm) - also from G have "... = x" by simp - finally show ?thesis . -qed*) - lemma (in comm_monoid) nat_pow_distr: "[| x \ carrier G; y \ carrier G |] ==> (x \ y) [^] (n::nat) = x [^] n \ y [^] n" @@ -1397,22 +1385,24 @@ \carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one = one G\" lemma (in monoid) units_group: "group (units_of G)" - apply (unfold units_of_def) - apply (rule groupI) - apply auto - apply (subst m_assoc) - apply auto - apply (rule_tac x = "inv x" in bexI) - apply auto - done +proof - + have "\x y z. \x \ Units G; y \ Units G; z \ Units G\ \ x \ y \ z = x \ (y \ z)" + by (simp add: Units_closed m_assoc) + moreover have "\x. x \ Units G \ \y\Units G. y \ x = \" + using Units_l_inv by blast + ultimately show ?thesis + unfolding units_of_def + by (force intro!: groupI) +qed lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)" - apply (rule group.group_comm_groupI) - apply (rule units_group) - apply (insert comm_monoid_axioms) - apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) - apply auto - done +proof - + have "\x y. \x \ carrier (units_of G); y \ carrier (units_of G)\ + \ x \\<^bsub>units_of G\<^esub> y = y \\<^bsub>units_of G\<^esub> x" + by (simp add: Units_closed m_comm units_of_def) + then show ?thesis + by (rule group.group_comm_groupI [OF units_group]) auto +qed lemma units_of_carrier: "carrier (units_of G) = Units G" by (auto simp: units_of_def) @@ -1423,39 +1413,14 @@ lemma units_of_one: "one (units_of G) = one G" by (auto simp: units_of_def) -lemma (in monoid) units_of_inv: "x \ Units G \ m_inv (units_of G) x = m_inv G x" - apply (rule sym) - apply (subst m_inv_def) - apply (rule the1_equality) - apply (rule ex_ex1I) - apply (subst (asm) Units_def) - apply auto - apply (erule inv_unique) - apply auto - apply (rule Units_closed) - apply (simp_all only: units_of_carrier [symmetric]) - apply (insert units_group) - apply auto - apply (subst units_of_mult [symmetric]) - apply (subst units_of_one [symmetric]) - apply (erule group.r_inv, assumption) - apply (subst units_of_mult [symmetric]) - apply (subst units_of_one [symmetric]) - apply (erule group.l_inv, assumption) - done - -lemma (in group) inj_on_const_mult: "a \ carrier G \ inj_on (\x. a \ x) (carrier G)" - unfolding inj_on_def by auto +lemma (in monoid) units_of_inv: + assumes "x \ Units G" + shows "m_inv (units_of G) x = m_inv G x" + by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one) lemma (in group) surj_const_mult: "a \ carrier G \ (\x. a \ x) ` carrier G = carrier G" apply (auto simp add: image_def) - apply (rule_tac x = "(m_inv G a) \ x" in bexI) - apply auto -(* auto should get this. I suppose we need "comm_monoid_simprules" - for ac_simps rewriting. *) - apply (subst m_assoc [symmetric]) - apply auto - done + by (metis inv_closed inv_solve_left m_closed) lemma (in group) l_cancel_one [simp]: "x \ carrier G \ a \ carrier G \ x \ a = x \ a = one G" by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed) diff -r ba2a92af88b4 -r 023b353911c5 src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Sat Jun 16 22:09:24 2018 +0200 +++ b/src/HOL/Algebra/Ideal.thy Sun Jun 17 22:00:43 2018 +0100 @@ -17,11 +17,14 @@ and I_r_closed: "\a \ I; x \ carrier R\ \ a \ x \ I" sublocale ideal \ abelian_subgroup I R - apply (intro abelian_subgroupI3 abelian_group.intro) - apply (rule ideal.axioms, rule ideal_axioms) - apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms) - apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms) - done +proof (intro abelian_subgroupI3 abelian_group.intro) + show "additive_subgroup I R" + by (simp add: is_additive_subgroup) + show "abelian_monoid R" + by (simp add: abelian_monoid_axioms) + show "abelian_group_axioms R" + using abelian_group_def is_abelian_group by blast +qed lemma (in ideal) is_ideal: "ideal I R" by (rule ideal_axioms) diff -r ba2a92af88b4 -r 023b353911c5 src/HOL/Number_Theory/Residues.thy --- a/src/HOL/Number_Theory/Residues.thy Sat Jun 16 22:09:24 2018 +0200 +++ b/src/HOL/Number_Theory/Residues.thy Sun Jun 17 22:00:43 2018 +0100 @@ -348,7 +348,7 @@ done also have "(\i\(\?Inverse_Pairs). i) = (\A\?Inverse_Pairs. (\y\A. y))" apply (subst finprod_Union_disjoint) - apply auto + apply (auto simp: pairwise_def disjnt_def) apply (metis Units_inv_inv)+ done also have "\ = \"