--- a/src/HOL/Algebra/Complete_Lattice.thy Sat Jun 23 17:05:59 2018 +0200
+++ b/src/HOL/Algebra/Complete_Lattice.thy Sun Jun 24 11:41:41 2018 +0100
@@ -43,11 +43,8 @@
proof -
interpret dual: weak_lattice "inv_gorder L"
by (metis dual_weak_lattice)
-
show ?thesis
- apply (unfold_locales)
- apply (simp_all add:inf_exists sup_exists)
- done
+ by (unfold_locales) (simp_all add:inf_exists sup_exists)
qed
lemma (in weak_complete_lattice) supI:
@@ -125,32 +122,21 @@
have B_L: "?B \<subseteq> carrier L" by simp
from inf_exists [OF B_L B_non_empty]
obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+ then have bcarr: "b \<in> carrier L"
+ by auto
have "least L b (Upper L A)"
-apply (rule least_UpperI)
- apply (rule greatest_le [where A = "Lower L ?B"])
- apply (rule b_inf_B)
- apply (rule Lower_memI)
- apply (erule Upper_memD [THEN conjunct1])
- apply assumption
- apply (rule L)
- apply (fast intro: L [THEN subsetD])
- apply (erule greatest_Lower_below [OF b_inf_B])
- apply simp
- apply (rule L)
-apply (rule greatest_closed [OF b_inf_B])
-done
+ proof (rule least_UpperI)
+ show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
+ by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)
+ show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
+ by (meson B_L b_inf_B greatest_Lower_below)
+ qed (use bcarr L in auto)
then show "\<exists>s. least L s (Upper L A)" ..
next
fix A
assume L: "A \<subseteq> carrier L"
show "\<exists>i. greatest L i (Lower L A)"
- proof (cases "A = {}")
- case True then show ?thesis
- by (simp add: top_exists)
- next
- case False with L show ?thesis
- by (rule inf_exists)
- qed
+ by (metis L Lower_empty inf_exists top_exists)
qed
@@ -205,12 +191,8 @@
proof -
obtain i where "greatest L i (Lower L A)"
by (metis assms inf_exists)
-
thus ?thesis
- apply (simp add: inf_def)
- apply (rule someI2[of _ "i"])
- apply (auto)
- done
+ by (metis inf_def someI_ex)
qed
lemma inf_lower:
@@ -231,17 +213,20 @@
by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
lemma weak_inf_insert [simp]:
- "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
- apply (rule weak_le_antisym)
- apply (force intro: meet_le inf_greatest inf_lower inf_closed)
- apply (rule inf_greatest)
- apply (force)
- apply (force intro: inf_closed)
- apply (auto)
- apply (metis inf_closed meet_left)
- apply (force intro: le_trans inf_closed meet_right meet_left inf_lower)
-done
-
+ assumes "a \<in> carrier L" "A \<subseteq> carrier L"
+ shows "\<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
+proof (rule weak_le_antisym)
+ show "\<Sqinter>insert a A \<sqsubseteq> a \<sqinter> \<Sqinter>A"
+ by (simp add: assms inf_lower local.inf_greatest meet_le)
+ show aA: "a \<sqinter> \<Sqinter>A \<in> carrier L"
+ using assms by simp
+ show "a \<sqinter> \<Sqinter>A \<sqsubseteq> \<Sqinter>insert a A"
+ apply (rule inf_greatest)
+ using assms apply (simp_all add: aA)
+ by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)
+ show "\<Sqinter>insert a A \<in> carrier L"
+ using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
+qed
subsection \<open>Supremum Laws\<close>
@@ -268,17 +253,20 @@
by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
lemma weak_sup_insert [simp]:
- "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Squnion>insert a A .= a \<squnion> \<Squnion>A"
- apply (rule weak_le_antisym)
- apply (rule sup_least)
- apply (auto)
- apply (metis join_left sup_closed)
- apply (rule le_trans) defer
- apply (rule join_right)
- apply (auto)
- apply (rule join_le)
- apply (auto intro: sup_upper sup_least sup_closed)
-done
+ assumes "a \<in> carrier L" "A \<subseteq> carrier L"
+ shows "\<Squnion>insert a A .= a \<squnion> \<Squnion>A"
+proof (rule weak_le_antisym)
+ show aA: "a \<squnion> \<Squnion>A \<in> carrier L"
+ using assms by simp
+ show "\<Squnion>insert a A \<sqsubseteq> a \<squnion> \<Squnion>A"
+ apply (rule sup_least)
+ using assms apply (simp_all add: aA)
+ by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)
+ show "a \<squnion> \<Squnion>A \<sqsubseteq> \<Squnion>insert a A"
+ by (simp add: assms join_le local.sup_least sup_upper)
+ show "\<Squnion>insert a A \<in> carrier L"
+ using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
+qed
end
@@ -303,30 +291,26 @@
proof -
from assms(2) have AL: "A \<subseteq> carrier L"
by (auto simp add: fps_def)
-
show ?thesis
proof (rule sup_cong, simp_all add: AL)
from assms(1) AL show "f ` A \<subseteq> carrier L"
- by (auto)
+ by auto
+ then have *: "\<And>b. \<lbrakk>A \<subseteq> {x \<in> carrier L. f x .= x}; b \<in> A\<rbrakk> \<Longrightarrow> \<exists>a\<in>f ` A. b .= a"
+ by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)
from assms(2) show "f ` A {.=} A"
- apply (auto simp add: fps_def)
- apply (rule set_eqI2)
- apply blast
- apply (rename_tac b)
- apply (rule_tac x="f b" in bexI)
- apply (metis (mono_tags, lifting) Ball_Collect assms(1) Pi_iff local.sym)
- apply (auto)
- done
+ by (auto simp add: fps_def intro: set_eqI2 [OF _ *])
qed
qed
lemma (in weak_complete_lattice) fps_idem:
- "\<lbrakk> f \<in> carrier L \<rightarrow> carrier L; Idem f \<rbrakk> \<Longrightarrow> fps L f {.=} f ` carrier L"
- apply (rule set_eqI2)
- apply (auto simp add: idempotent_def fps_def)
- apply (metis Pi_iff local.sym)
- apply force
-done
+ assumes "f \<in> carrier L \<rightarrow> carrier L" "Idem f"
+ shows "fps L f {.=} f ` carrier L"
+proof (rule set_eqI2)
+ show "\<And>a. a \<in> fps L f \<Longrightarrow> \<exists>b\<in>f ` carrier L. a .= b"
+ using assms by (force simp add: fps_def intro: local.sym)
+ show "\<And>b. b \<in> f ` carrier L \<Longrightarrow> \<exists>a\<in>fps L f. b .= a"
+ using assms by (force simp add: idempotent_def fps_def)
+qed
context weak_complete_lattice
begin
@@ -392,20 +376,19 @@
lemma LFP_lemma2:
assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
shows "f (LFP f) \<sqsubseteq> LFP f"
- using assms
- apply (auto simp add:Pi_def)
- apply (rule LFP_greatest)
- apply (metis LFP_closed)
- apply (metis LFP_closed LFP_lowerbound le_trans use_iso1)
-done
+proof (rule LFP_greatest)
+ have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
+ using assms by (auto simp add: Pi_def)
+ with assms show "f (LFP f) \<in> carrier L"
+ by blast
+ show "\<And>u. \<lbrakk>u \<in> carrier L; f u \<sqsubseteq> u\<rbrakk> \<Longrightarrow> f (LFP f) \<sqsubseteq> u"
+ by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)
+qed
lemma LFP_lemma3:
assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
shows "LFP f \<sqsubseteq> f (LFP f)"
- using assms
- apply (auto simp add:Pi_def)
- apply (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
-done
+ using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
lemma LFP_weak_unfold:
"\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f .= f (LFP f)"
@@ -477,12 +460,14 @@
lemma GFP_lemma2:
assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
shows "GFP f \<sqsubseteq> f (GFP f)"
- using assms
- apply (auto simp add:Pi_def)
- apply (rule GFP_least)
- apply (metis GFP_closed)
- apply (metis GFP_closed GFP_upperbound le_trans use_iso2)
-done
+proof (rule GFP_least)
+ have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
+ using assms by (auto simp add: Pi_def)
+ with assms show "f (GFP f) \<in> carrier L"
+ by blast
+ show "\<And>u. \<lbrakk>u \<in> carrier L; u \<sqsubseteq> f u\<rbrakk> \<Longrightarrow> u \<sqsubseteq> f (GFP f)"
+ by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)
+qed
lemma GFP_lemma3:
assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
@@ -599,20 +584,15 @@
have B_L: "?B \<subseteq> carrier L" by simp
from inf_exists [OF B_L B_non_empty]
obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+ then have bcarr: "b \<in> carrier L"
+ by blast
have "least L b (Upper L A)"
-apply (rule least_UpperI)
- apply (rule greatest_le [where A = "Lower L ?B"])
- apply (rule b_inf_B)
- apply (rule Lower_memI)
- apply (erule Upper_memD [THEN conjunct1])
- apply assumption
- apply (rule L)
- apply (fast intro: L [THEN subsetD])
- apply (erule greatest_Lower_below [OF b_inf_B])
- apply simp
- apply (rule L)
-apply (rule greatest_closed [OF b_inf_B])
-done
+ proof (rule least_UpperI)
+ show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
+ by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)
+ show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
+ by (auto elim: greatest_Lower_below [OF b_inf_B])
+ qed (use L bcarr in auto)
then show "\<exists>s. least L s (Upper L A)" ..
next
fix A
@@ -666,23 +646,11 @@
context weak_complete_lattice
begin
- lemma at_least_at_most_Sup:
- "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
- apply (rule weak_le_antisym)
- apply (rule sup_least)
- apply (auto simp add: at_least_at_most_closed)
- apply (rule sup_upper)
- apply (auto simp add: at_least_at_most_closed)
- done
+ lemma at_least_at_most_Sup: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
+ by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)
- lemma at_least_at_most_Inf:
- "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
- apply (rule weak_le_antisym)
- apply (rule inf_lower)
- apply (auto simp add: at_least_at_most_closed)
- apply (rule inf_greatest)
- apply (auto simp add: at_least_at_most_closed)
- done
+ lemma at_least_at_most_Inf: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
+ by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)
end
@@ -695,7 +663,7 @@
interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"
proof -
have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"
- by (auto, simp add: at_least_at_most_def)
+ by (auto simp add: at_least_at_most_def)
thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
qed
--- a/src/HOL/Algebra/Divisibility.thy Sat Jun 23 17:05:59 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sun Jun 24 11:41:41 2018 +0100
@@ -2382,10 +2382,8 @@
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
- apply (subst (2 3) somegcd_meet, (simp add: carr)+)
- apply (simp add: somegcd_meet carr)
- apply (rule weak_meet_assoc[simplified], fact+)
- done
+ unfolding associated_def
+ by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
qed
lemma (in gcd_condition_monoid) gcd_mult:
@@ -2645,10 +2643,7 @@
by blast
have a'fs: "wfactors G as a'"
apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
- apply (simp add: a)
- apply (insert ascarr a'carr)
- apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
- done
+ by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed)
from afs have ahirr: "irreducible G ah"
by (elim wfactorsE) simp
with ascarr have ahprime: "prime G ah"
@@ -2674,31 +2669,18 @@
from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
by blast
with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
- apply -
- apply (elim irreducible_prodE[of "ah" "x"], assumption+)
- apply (rule associatedI2[of x], assumption+)
- apply (rule irreducibleE[OF ahirr], simp)
- done
-
+ by (metis ahprime associatedI2 irreducible_prodE primeE)
note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
note carr = carr partscarr
have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
- apply (intro wfactors_prod_exists)
- using setparts afs'
- apply (fast elim: wfactorsE)
- apply simp
- done
+ by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
by auto
have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
- apply (intro wfactors_prod_exists)
- using setparts afs'
- apply (fast elim: wfactorsE)
- apply simp
- done
+ by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
by auto
@@ -2709,21 +2691,12 @@
have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
by (intro wfactors_mult, simp+)
then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
- apply (intro wfactors_mult_single)
- using setparts afs'
- apply (fast intro: nth_mem[OF len] elim: wfactorsE)
- apply simp_all
- done
-
+ using irrasi wfactors_mult_single by auto
from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
by (metis irrasi wfactors_mult_single)
with len carr aa1carr aa2carr aa1fs
have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
- apply (intro wfactors_mult)
- apply fast
- apply (simp, (fast intro: nth_mem[OF len])?)+
- done
-
+ using wfactors_mult by auto
from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
by (simp add: Cons_nth_drop_Suc)
with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
@@ -2763,14 +2736,8 @@
note ee1
also note ee2
also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
- (take i as' @ as' ! i # drop (Suc i) as')"
- apply (intro essentially_equalI)
- apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
- take i as' @ as' ! i # drop (Suc i) as'")
- apply simp
- apply (rule perm_append_Cons)
- apply simp
- done
+ (take i as' @ as' ! i # drop (Suc i) as')"
+ by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
by simp
then show "essentially_equal G (ah # as) as'"
@@ -2813,21 +2780,17 @@
lemma (in factorial_monoid) factorcount_unique:
assumes afs: "wfactors G as a"
- and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"
+ and acarr[simp]: "a \<in> carrier G" and ascarr: "set as \<subseteq> carrier G"
shows "factorcount G a = length as"
proof -
have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
by (rule factorcount_exists) simp
then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
by auto
- have ac: "ac = factorcount G a"
- apply (simp add: factorcount_def)
- apply (rule theI2)
- apply (rule alen)
- apply (metis afs alen ascarr)+
- done
+ then have ac: "ac = factorcount G a"
+ unfolding factorcount_def using ascarr by (blast intro: theI2 afs)
from ascarr afs have "ac = length as"
- by (iprover intro: alen[rule_format])
+ by (simp add: alen)
with ac show ?thesis
by simp
qed
@@ -2872,11 +2835,8 @@
and bcarr: "b \<in> carrier G"
and asc: "a \<sim> b"
shows "factorcount G a = factorcount G b"
- apply (rule associatedE[OF asc])
- apply (drule divides_fcount[OF _ acarr bcarr])
- apply (drule divides_fcount[OF _ bcarr acarr])
- apply simp
- done
+ using assms
+ by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)
lemma (in factorial_monoid) properfactor_fcount:
assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
--- a/src/HOL/Algebra/Sylow.thy Sat Jun 23 17:05:59 2018 +0200
+++ b/src/HOL/Algebra/Sylow.thy Sun Jun 24 11:41:41 2018 +0100
@@ -161,23 +161,17 @@
by (simp add: H_def coset_mult_assoc [symmetric])
lemma H_not_empty: "H \<noteq> {}"
- apply (simp add: H_def)
- apply (rule exI [of _ \<one>])
- apply simp
- done
+ by (force simp add: H_def intro: exI [of _ \<one>])
lemma H_is_subgroup: "subgroup H G"
- apply (rule subgroupI)
- apply (rule subsetI)
- apply (erule H_into_carrier_G)
- apply (rule H_not_empty)
- apply (simp add: H_def)
- apply clarify
- apply (erule_tac P = "\<lambda>z. lhs z = M1" for lhs in subst)
- apply (simp add: coset_mult_assoc )
- apply (blast intro: H_m_closed)
- done
-
+proof (rule subgroupI)
+ show "H \<subseteq> carrier G"
+ using H_into_carrier_G by blast
+ show "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
+ by (metis H_I H_into_carrier_G H_m_closed M1_subset_G Units_eq Units_inv_closed Units_inv_inv coset_mult_inv1 in_H_imp_eq)
+ show "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
+ by (blast intro: H_m_closed)
+qed (use H_not_empty in auto)
lemma rcosetGM1g_subset_G: "\<lbrakk>g \<in> carrier G; x \<in> M1 #> g\<rbrakk> \<Longrightarrow> x \<in> carrier G"
by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
@@ -191,13 +185,19 @@
lemma M1_cardeq_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> card (M1 #> g) = card M1"
by (metis M1_subset_G card_rcosets_equal rcosetsI)
-lemma M1_RelM_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> (M1, M1 #> g) \<in> RelM"
- apply (simp add: RelM_def calM_def card_M1)
- apply (rule conjI)
- apply (blast intro: rcosetGM1g_subset_G)
- apply (simp add: card_M1 M1_cardeq_rcosetGM1g)
- apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
- done
+lemma M1_RelM_rcosetGM1g:
+ assumes "g \<in> carrier G"
+ shows "(M1, M1 #> g) \<in> RelM"
+proof -
+ have "M1 #> g \<subseteq> carrier G"
+ by (simp add: assms r_coset_subset_G)
+ moreover have "card (M1 #> g) = p ^ a"
+ using assms by (simp add: card_M1 M1_cardeq_rcosetGM1g)
+ moreover have "\<exists>h\<in>carrier G. M1 = M1 #> g #> h"
+ by (metis assms M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
+ ultimately show ?thesis
+ by (simp add: RelM_def calM_def card_M1)
+qed
end
@@ -226,20 +226,26 @@
by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)
lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
- apply (rule bexI)
- apply (rule_tac [2] M_funcset_rcosets_H)
- apply (rule inj_onI, simp)
- apply (rule trans [OF _ M_elem_map_eq])
- prefer 2 apply assumption
- apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
- apply (rule coset_mult_inv1)
- apply (erule_tac [2] M_elem_map_carrier)+
- apply (rule_tac [2] M1_subset_G)
- apply (rule coset_join1 [THEN in_H_imp_eq])
- apply (rule_tac [3] H_is_subgroup)
- prefer 2 apply (blast intro: M_elem_map_carrier)
- apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
- done
+proof
+ let ?inv = "\<lambda>x. SOME g. g \<in> carrier G \<and> M1 #> g = x"
+ show "inj_on (\<lambda>x\<in>M. H #> ?inv x) M"
+ proof (rule inj_onI, simp)
+ fix x y
+ assume eq: "H #> ?inv x = H #> ?inv y" and xy: "x \<in> M" "y \<in> M"
+ have "x = M1 #> ?inv x"
+ by (simp add: M_elem_map_eq \<open>x \<in> M\<close>)
+ also have "... = M1 #> ?inv y"
+ proof (rule coset_mult_inv1 [OF in_H_imp_eq [OF coset_join1]])
+ show "H #> ?inv x \<otimes> inv (?inv y) = H"
+ by (simp add: H_into_carrier_G M_elem_map_carrier xy coset_mult_inv2 eq subsetI)
+ qed (simp_all add: H_is_subgroup M_elem_map_carrier xy)
+ also have "... = y"
+ using M_elem_map_eq \<open>y \<in> M\<close> by simp
+ finally show "x=y" .
+ qed
+ show "(\<lambda>x\<in>M. H #> ?inv x) \<in> M \<rightarrow> rcosets H"
+ by (rule M_funcset_rcosets_H)
+qed
end
@@ -258,28 +264,34 @@
lemma rcosets_H_funcset_M:
"(\<lambda>C \<in> rcosets H. M1 #> (SOME g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
- apply (simp add: RCOSETS_def)
- apply (fast intro: someI2
- intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
- done
+ using in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]
+ by (simp add: M1_in_M H_elem_map_carrier RCOSETS_def)
-text \<open>Close to a duplicate of \<open>inj_M_GmodH\<close>.\<close>
lemma inj_GmodH_M: "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
- apply (rule bexI)
- apply (rule_tac [2] rcosets_H_funcset_M)
- apply (rule inj_onI)
- apply (simp)
- apply (rule trans [OF _ H_elem_map_eq])
- prefer 2 apply assumption
- apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
- apply (rule coset_mult_inv1)
- apply (erule_tac [2] H_elem_map_carrier)+
- apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
- apply (rule coset_join2)
- apply (blast intro: H_elem_map_carrier)
- apply (rule H_is_subgroup)
- apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
- done
+proof
+ let ?inv = "\<lambda>x. SOME g. g \<in> carrier G \<and> H #> g = x"
+ show "inj_on (\<lambda>C\<in>rcosets H. M1 #> ?inv C) (rcosets H)"
+ proof (rule inj_onI, simp)
+ fix x y
+ assume eq: "M1 #> ?inv x = M1 #> ?inv y" and xy: "x \<in> rcosets H" "y \<in> rcosets H"
+ have "x = H #> ?inv x"
+ by (simp add: H_elem_map_eq \<open>x \<in> rcosets H\<close>)
+ also have "... = H #> ?inv y"
+ proof (rule coset_mult_inv1 [OF coset_join2])
+ show "?inv x \<otimes> inv (?inv y) \<in> carrier G"
+ by (simp add: H_elem_map_carrier \<open>x \<in> rcosets H\<close> \<open>y \<in> rcosets H\<close>)
+ then show "(?inv x) \<otimes> inv (?inv y) \<in> H"
+ by (simp add: H_I H_elem_map_carrier xy coset_mult_inv2 eq)
+ show "H \<subseteq> carrier G"
+ by (simp add: H_is_subgroup subgroup.subset)
+ qed (simp_all add: H_is_subgroup H_elem_map_carrier xy)
+ also have "... = y"
+ by (simp add: H_elem_map_eq \<open>y \<in> rcosets H\<close>)
+ finally show "x=y" .
+ qed
+ show "(\<lambda>C\<in>rcosets H. M1 #> ?inv C) \<in> rcosets H \<rightarrow> M"
+ using rcosets_H_funcset_M by blast
+qed
lemma calM_subset_PowG: "calM \<subseteq> Pow (carrier G)"
by (auto simp: calM_def)
@@ -289,41 +301,42 @@
by (metis M_subset_calM finite_calM rev_finite_subset)
lemma cardMeqIndexH: "card M = card (rcosets H)"
- apply (insert inj_M_GmodH inj_GmodH_M)
- apply (blast intro: card_bij finite_M H_is_subgroup
- rcosets_subset_PowG [THEN finite_subset]
- finite_Pow_iff [THEN iffD2])
- done
+ using inj_M_GmodH inj_GmodH_M
+ by (blast intro: card_bij finite_M H_is_subgroup rcosets_subset_PowG [THEN finite_subset])
lemma index_lem: "card M * card H = order G"
by (simp add: cardMeqIndexH lagrange H_is_subgroup)
-lemma lemma_leq1: "p^a \<le> card H"
- apply (rule dvd_imp_le)
- apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
- prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
- apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd zero_less_m)
- done
-
-lemma lemma_leq2: "card H \<le> p^a"
- apply (subst card_M1 [symmetric])
- apply (cut_tac M1_inj_H)
- apply (blast intro!: M1_subset_G intro: card_inj H_into_carrier_G finite_subset [OF _ finite_G])
- done
-
lemma card_H_eq: "card H = p^a"
- by (blast intro: le_antisym lemma_leq1 lemma_leq2)
+proof (rule antisym)
+ show "p^a \<le> card H"
+ proof (rule dvd_imp_le)
+ show "p ^ a dvd card H"
+ apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
+ by (simp add: index_lem multiplicity_dvd order_G power_add)
+ show "0 < card H"
+ by (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
+ qed
+next
+ show "card H \<le> p^a"
+ using M1_inj_H card_M1 card_inj finite_M1 by fastforce
+qed
end
lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G \<and> card H = p^a"
- using lemma_A1
- apply clarify
- apply (frule existsM1inM, clarify)
- apply (subgoal_tac "sylow_central G p a m M1 M")
- apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
- apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
- done
+proof -
+ obtain M where M: "M \<in> calM // RelM" "\<not> (p ^ Suc (multiplicity p m) dvd card M)"
+ using lemma_A1 by blast
+ then obtain M1 where "M1 \<in> M"
+ by (metis existsM1inM)
+ define H where "H \<equiv> {g. g \<in> carrier G \<and> M1 #> g = M1}"
+ with M \<open>M1 \<in> M\<close>
+ interpret sylow_central G p a m calM RelM H M1 M
+ by unfold_locales (auto simp add: H_def calM_def RelM_def)
+ show ?thesis
+ using H_is_subgroup card_H_eq by blast
+qed
text \<open>Needed because the locale's automatic definition refers to
@{term "semigroup G"} and @{term "group_axioms G"} rather than