--- a/src/HOL/Algebra/Coset.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Coset.thy Sun Jul 08 16:07:26 2018 +0100
@@ -77,7 +77,15 @@
using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
also have " ... = (h1 \<otimes> (g \<otimes> inv g) \<otimes> inv h2)"
using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
- monoid_axioms subgroup.mem_carrier by smt
+ monoid_axioms subgroup.mem_carrier
+ proof -
+ have "h1 \<in> carrier G"
+ by (meson subgroup.mem_carrier assms(1) h1(1))
+ moreover have "h2 \<in> carrier G"
+ by (meson subgroup.mem_carrier assms(1) h2(1))
+ ultimately show ?thesis
+ using g(1) inv_closed m_assoc m_closed by presburger
+ qed
finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2"
using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
@@ -210,7 +218,8 @@
thus "x <# H \<subseteq> H" unfolding l_coset_def by blast
next
have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> ((inv x) \<otimes> h) = h"
- by (smt assms inv_closed l_one m_assoc r_inv subgroup.mem_carrier)
+ by (metis (no_types, lifting) assms group.inv_closed group.inv_solve_left is_group
+ monoid.m_closed monoid_axioms subgroup.mem_carrier)
moreover have "\<And>h. h \<in> H \<Longrightarrow> (inv x) \<otimes> h \<in> H"
by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)
ultimately show "H \<subseteq> x <# H" unfolding l_coset_def by blast
@@ -293,7 +302,7 @@
text \<open>Multiplication of general subsets\<close>
lemma (in comm_group) mult_subgroups:
- assumes "subgroup H G" and "subgroup K G"
+ assumes HG: "subgroup H G" and KG: "subgroup K G"
shows "subgroup (H <#> K) G"
proof (rule subgroup.intro)
show "H <#> K \<subseteq> carrier G"
@@ -323,13 +332,16 @@
then obtain h1 k1 h2 k2 where h1k1: "h1 \<in> H" "k1 \<in> K" "x = h1 \<otimes> k1"
and h2k2: "h2 \<in> H" "k2 \<in> K" "y = h2 \<otimes> k2"
unfolding set_mult_def by blast
- hence "x \<otimes> y = (h1 \<otimes> k1) \<otimes> (h2 \<otimes> k2)" by simp
+ with KG HG have carr: "k1 \<in> carrier G" "h1 \<in> carrier G" "k2 \<in> carrier G" "h2 \<in> carrier G"
+ by (meson subgroup.mem_carrier)+
+ have "x \<otimes> y = (h1 \<otimes> k1) \<otimes> (h2 \<otimes> k2)"
+ using h1k1 h2k2 by simp
also have " ... = h1 \<otimes> (k1 \<otimes> h2) \<otimes> k2"
- by (smt h1k1 h2k2 m_assoc m_closed assms subgroup.mem_carrier)
+ by (simp add: carr comm_groupE(3) comm_group_axioms)
also have " ... = h1 \<otimes> (h2 \<otimes> k1) \<otimes> k2"
- by (metis (no_types, hide_lams) assms m_comm h1k1(2) h2k2(1) subgroup.mem_carrier)
+ by (simp add: carr m_comm)
finally have "x \<otimes> y = (h1 \<otimes> h2) \<otimes> (k1 \<otimes> k2)"
- by (smt assms h1k1 h2k2 m_assoc monoid.m_closed monoid_axioms subgroup.mem_carrier)
+ by (simp add: carr comm_groupE(3) comm_group_axioms)
thus "x \<otimes> y \<in> H <#> K" unfolding set_mult_def
using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)]
subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast
@@ -452,8 +464,15 @@
proof -
obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
using assms(1) unfolding l_coset_def by blast
- hence "\<And> h. h \<in> H \<Longrightarrow> x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)"
- by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier)
+ hence "x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)" if "h \<in> H" for h
+ proof -
+ have f3: "h' \<in> carrier G"
+ by (meson assms(3) h'(1) subgroup.mem_carrier)
+ have f4: "h \<in> carrier G"
+ by (meson assms(3) subgroup.mem_carrier that)
+ then show ?thesis
+ by (metis assms(2) f3 h'(2) inv_closed inv_solve_right m_assoc m_closed)
+ qed
hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
@@ -494,7 +513,7 @@
proof
fix x assume x: "x \<in> H" thus "x \<in> H <#> H" unfolding set_mult_def
using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms]
- by (smt UN_iff assms coset_join3 l_coset_def subgroup.mem_carrier)
+ using assms subgroup.mem_carrier by force
qed
qed
--- a/src/HOL/Algebra/Divisibility.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Sun Jul 08 16:07:26 2018 +0100
@@ -1654,8 +1654,10 @@
by (clarsimp simp add: map_eq_Cons_conv) blast
next
case (trans xs ys zs)
+ then obtain as' where " as <~~> as' \<and> map (assocs G) as' = ys"
+ by (metis (no_types, lifting) ex_map_conv mset_eq_perm set_mset_mset)
then show ?case
- by (smt ex_map_conv perm.trans perm_setP)
+ using trans.IH(2) trans.prems(2) by blast
qed auto
lemma (in comm_monoid_cancel) fmset_ee:
--- a/src/HOL/Algebra/Embedded_Algebras.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Embedded_Algebras.thy Sun Jul 08 16:07:26 2018 +0100
@@ -235,7 +235,8 @@
hence "inv k \<otimes> (k \<otimes> a) \<in> Span K Us"
using Span_smult_closed[OF assms _ ka] by simp
thus ?thesis
- using inv_k subring_props(1)a k by (smt DiffD1 l_one m_assoc set_rev_mp)
+ using inv_k subring_props(1)a k
+ by (metis (no_types, lifting) DiffE l_one m_assoc subset_iff)
qed
--- a/src/HOL/Algebra/Ideal.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Ideal.thy Sun Jul 08 16:07:26 2018 +0100
@@ -348,7 +348,10 @@
text \<open>Generation of Principal Ideals in Commutative Rings\<close>
definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
- where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
+ where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
+
+lemma cginideal_def': "cgenideal R a = (\<lambda>x. x \<otimes>\<^bsub>R\<^esub> a) ` carrier R"
+ by (auto simp add: cgenideal_def)
text \<open>genhideal (?) really generates an ideal\<close>
lemma (in cring) cgenideal_ideal:
--- a/src/HOL/Algebra/QuotRing.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Sun Jul 08 16:07:26 2018 +0100
@@ -854,14 +854,13 @@
using ring_iso_set_trans unfolding is_ring_iso_def by blast
lemma ring_iso_set_sym:
- assumes "ring R"
- shows "h \<in> ring_iso R S \<Longrightarrow> (inv_into (carrier R) h) \<in> ring_iso S R"
+ assumes "ring R" and h: "h \<in> ring_iso R S"
+ shows "(inv_into (carrier R) h) \<in> ring_iso S R"
proof -
- assume h: "h \<in> ring_iso R S"
- hence h_hom: "h \<in> ring_hom R S"
+ have h_hom: "h \<in> ring_hom R S"
and h_surj: "h ` (carrier R) = (carrier S)"
and h_inj: "\<And> x1 x2. \<lbrakk> x1 \<in> carrier R; x2 \<in> carrier R \<rbrakk> \<Longrightarrow> h x1 = h x2 \<Longrightarrow> x1 = x2"
- unfolding ring_iso_def bij_betw_def inj_on_def by auto
+ using h unfolding ring_iso_def bij_betw_def inj_on_def by auto
have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
using bij_betw_inv_into h ring_iso_def by fastforce
@@ -869,13 +868,12 @@
show "inv_into (carrier R) h \<in> ring_iso S R"
apply (rule ring_iso_memI)
apply (simp add: h_surj inv_into_into)
- apply (auto simp add: h_inv_bij)
- apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into
- ring.ring_simprules(5) ring_hom_closed ring_hom_mult)
- apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into
- ring.ring_simprules(1) ring_hom_add ring_hom_closed)
- by (metis (no_types, hide_lams) assms f_inv_into_f h_hom h_inj
- imageI inv_into_into ring.ring_simprules(6) ring_hom_one)
+ apply (auto simp add: h_inv_bij)
+ using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij]
+ apply (simp_all add: \<open>ring R\<close> bij_betw_def bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules(5))
+ using ring_iso_memE [OF h] bij_betw_inv_into_right [of h "carrier R" "carrier S"]
+ apply (simp add: \<open>ring R\<close> inv_into_f_eq ring.ring_simprules(1))
+ by (simp add: \<open>ring R\<close> inv_into_f_eq ring.ring_simprules(6))
qed
corollary ring_iso_sym:
--- a/src/HOL/Algebra/Ring_Divisibility.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Sun Jul 08 16:07:26 2018 +0100
@@ -216,7 +216,7 @@
proof (rule ccontr)
assume "\<not> carrier R \<noteq> PIdl p" hence "carrier R = PIdl p" by simp
then obtain c where "c \<in> carrier R" "c \<otimes> p = \<one>"
- unfolding cgenideal_def using one_closed by (smt mem_Collect_eq)
+ unfolding cginideal_def' by (metis (no_types, lifting) image_iff one_closed)
hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto
thus False using A unfolding prime_def by simp
qed
--- a/src/HOL/Algebra/Sym_Groups.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Sym_Groups.thy Sun Jul 08 16:07:26 2018 +0100
@@ -328,7 +328,7 @@
-abbreviation three_cycles :: "nat \<Rightarrow> (nat \<Rightarrow> nat) set"
+definition three_cycles :: "nat \<Rightarrow> (nat \<Rightarrow> nat) set"
where "three_cycles n \<equiv>
{ cycle_of_list cs | cs. cycle cs \<and> length cs = 3 \<and> set cs \<subseteq> {1..n} }"
@@ -354,7 +354,8 @@
proof -
from \<open>p \<in> three_cycles n\<close>
obtain cs where p: "p = cycle_of_list cs"
- and cs: "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}" by blast
+ and cs: "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
+ using three_cycles_def by blast
hence "p = (Fun.swap (cs ! 0) (cs ! 1) id) \<circ> (Fun.swap (cs ! 1) (cs ! 2) id)"
using stupid_lemma[OF cs(2)] p
by (metis comp_id cycle_of_list.simps(1) cycle_of_list.simps(3))
@@ -395,12 +396,16 @@
thus "q \<in> generate (alt_group n) (three_cycles n)"
using generate.one[of "alt_group n"] by (simp add: alt_group_def sym_group_def)
next
- assume "c \<noteq> a" hence "q \<in> (three_cycles n)"
- by (smt A distinct.simps(2) distinct_singleton empty_set length_Cons
- list.simps(15) list.size(3) mem_Collect_eq numeral_3_eq_3 set_ConsD)
+ assume "c \<noteq> a"
+ have "q \<in> (three_cycles n)"
+ unfolding three_cycles_def mem_Collect_eq
+ proof (intro exI conjI)
+ show "cycle [a,b,c]"
+ using A \<open>c \<noteq> a\<close> by auto
+ qed (use A in auto)
thus "q \<in> generate (alt_group n) (three_cycles n)"
by (simp add: generate.incl)
- qed } note aux_lemma1 = this
+ qed } note gen3 = this
{ fix S :: "nat set" and q :: "nat \<Rightarrow> nat" assume A: "swapidseq_ext S 2 q" "S \<subseteq> {1..n}"
have "q \<in> generate (alt_group n) (three_cycles n)"
@@ -416,20 +421,20 @@
thus ?thesis
proof (cases)
assume Eq: "b = c" hence "q = cycle_of_list [a, b, d]" by (simp add: q)
- thus ?thesis using aux_lemma1 ab cd Eq incl by simp
+ thus ?thesis using gen3 ab cd Eq incl by simp
next
assume In: "b \<noteq> c"
have "q = (cycle_of_list [a, b, c]) \<circ> (cycle_of_list [b, c, d])"
by (metis (no_types, lifting) comp_id cycle_of_list.simps(1)
cycle_of_list.simps(3) fun.map_comp q swap_id_idempotent)
- thus ?thesis
- using aux_lemma1[of a b c] aux_lemma1[of b c d]
- generate.eng[where ?h1.0 = "cycle_of_list [a, b, c]"
- and ?h2.0 = "cycle_of_list [b, c, d]"]
- using In ab alt_group_def cd sym_group_def incl
- by (smt insert_subset monoid.select_convs(1) partial_object.simps(3))
+ moreover have "... = cycle_of_list [a, b, c] \<otimes>\<^bsub>alt_group n\<^esub> cycle_of_list [b, c, d]"
+ by (simp add: alt_group_def sym_group_def)
+ ultimately show ?thesis
+ by (metis (no_types) In generate.eng[where ?h1.0 = "cycle_of_list [a, b, c]"
+ and ?h2.0 = "cycle_of_list [b, c, d]"]
+ gen3[of a b c] gen3[of b c d] \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> insert_subset incl)
qed
- qed } note aux_lemma2 = this
+ qed } note gen3swap = this
have "p permutes {1..n}"
using p permutation_permutes unfolding alt_group_def by auto
@@ -452,19 +457,17 @@
case (Suc k)
then obtain S1 S2 q r
where split: "swapidseq_ext S1 2 q" "swapidseq_ext S2 (2 * k) r" "p = q \<circ> r" "S1 \<union> S2 = {1..n}"
- using split_swapidseq_ext[of 2 "2 * Suc k" "{1..n}" p]
- by (smt One_nat_def Suc_1 Suc_leI Suc_le_mono add_diff_cancel_left' le_Suc_eq
- mult_Suc_right nat_mult_eq_1_iff one_le_mult_iff zero_less_Suc)
+ using split_swapidseq_ext[of 2 "2 * Suc k" "{1..n}" p] by auto
hence "r \<in> generate (alt_group n) (three_cycles n)"
using Suc.hyps swapidseq_ext_finite_expansion[of "{1..n}" S2 "2 * k" r]
by (metis (no_types, lifting) Suc.prems Un_commute sup.right_idem swapidseq_ext_finite)
moreover have "q \<in> generate (alt_group n) (three_cycles n)"
- using aux_lemma2[OF split(1)] \<open>S1 \<union> S2 = {1..n}\<close> by auto
+ using gen3swap[OF split(1)] \<open>S1 \<union> S2 = {1..n}\<close> by auto
ultimately show ?case
using split generate.eng[of q "alt_group n" "three_cycles n" r]
- by (smt alt_group_def monoid.select_convs(1) partial_object.simps(3) sym_group_def)
+ by (metis (full_types) alt_group_def monoid.simps(1) partial_object.simps(3) sym_group_def)
qed
qed
qed
@@ -530,7 +533,8 @@
proof
fix p :: "nat \<Rightarrow> nat" assume "p \<in> three_cycles n"
then obtain cs
- where cs: "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}" and p: "p = cycle_of_list cs" by blast
+ where cs: "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}" and p: "p = cycle_of_list cs"
+ unfolding three_cycles_def by blast
then obtain i j k where i: "i = cs ! 0" and j: "j = cs ! 1" and k: "k = cs ! 2"
and ijk: "cs = [i, j, k]" using stupid_lemma[OF cs(2)] by blast
@@ -559,10 +563,10 @@
ultimately show ?thesis using \<open>l \<in> {i, j, k}\<close> by auto
qed
qed
- hence "p ^^ 2 = (Fun.swap j k id) \<circ> (cycle_of_list [i, j, k]) \<circ> (inv' (Fun.swap j k id))"
+ hence p2: "p ^^ 2 = (Fun.swap j k id) \<circ> (cycle_of_list [i, j, k]) \<circ> (inv' (Fun.swap j k id))"
using conjugation_of_cycle[of "[i, j, k]" "Fun.swap j k id"] cs(1) ijk by auto
- moreover have "card ({1..n} - {i, j, k}) \<ge> card {1..n} - card {i, j, k}"
+ have "card ({1..n} - {i, j, k}) \<ge> card {1..n} - card {i, j, k}"
by (meson diff_card_le_card_Diff finite.emptyI finite.insertI)
hence card_ge_two: "card ({1..n} - {i, j, k}) \<ge> 2"
using assms cs ijk by simp
@@ -570,21 +574,35 @@
using elts_from_card[OF card_ge_two] by blast
then obtain g h where gh: "g = f 1" "h = f 2" "g \<noteq> h"
by (metis Suc_1 atLeastAtMost_iff diff_Suc_1 diff_Suc_Suc inj_onD nat.simps(3) one_le_numeral order_refl)
- hence g: "g \<in> {1..n} - {i, j, k}" using f(2) gh(2) by force
- hence h: "h \<in> {1..n} - {i, j, k}" using f(2) gh(2) by force
+ hence g: "g \<in> {1..n} - {i, j, k}" and h: "h \<in> {1..n} - {i, j, k}" using f(2) gh(2) by force+
hence gh_simps: "g \<noteq> h \<and> g \<in> {1..n} \<and> h \<in> {1..n} \<and> g \<notin> {i, j, k} \<and> h \<notin> {i, j, k}"
using g gh(3) by blast
-
- ultimately have final_step:
+ moreover have ijjk: "Fun.swap i j id = Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id)"
+ and jkij: "Fun.swap j k id \<circ> (Fun.swap i j id \<circ> Fun.swap j k id) \<circ> inv' (Fun.swap j k id) = Fun.swap g h (Fun.swap g h (Fun.swap i j (Fun.swap j k id)))"
+ by (simp_all add: comp_swap inv_swap_id)
+ moreover have "Fun.swap g h (Fun.swap i j id) = Fun.swap i j (Fun.swap g h id)"
+ by (metis (no_types) comp_id comp_swap gh_simps insert_iff swap_id_independent)
+ moreover have "Fun.swap i j (Fun.swap g h (Fun.swap j k id \<circ> id)) = Fun.swap g h (Fun.swap i j (Fun.swap j k id))"
+ by (metis (no_types) calculation(4) comp_id comp_swap)
+ moreover have "inj (Fun.swap j k id)" "bij (Fun.swap g h id)" "bij (Fun.swap j k id)"
+ by auto
+ moreover have "Fun.swap j k id \<circ> inv' (Fun.swap j k id \<circ> Fun.swap g h id) = Fun.swap g h id"
+ by (metis (no_types) bij_betw_id bij_swap_iff comp_id comp_swap gh_simps insert_iff inv_swap_id o_inv_distrib swap_id_independent swap_nilpotent)
+ moreover have "Fun.swap j k id \<circ> (Fun.swap j k id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id)) \<circ> inv' (Fun.swap j k id) = Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id)"
+ by (simp add: comp_swap inv_swap_id)
+ moreover have "Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id = Fun.swap j k id \<circ> (Fun.swap j k id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id))"
+ by (simp add: comp_swap inv_swap_id)
+ moreover have "Fun.swap g h id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id) \<circ> inv' (Fun.swap j k id \<circ> Fun.swap g h id) = Fun.swap j k id \<circ> (Fun.swap j k id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id)) \<circ> inv' (Fun.swap j k id)"
+ by (metis calculation(10) calculation(4) calculation(9) comp_assoc comp_id comp_swap swap_nilpotent)
+ ultimately have "Fun.swap i j (Fun.swap j k id) = Fun.swap j k id \<circ> Fun.swap g h id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id) \<circ> inv' (Fun.swap j k id \<circ> Fun.swap g h id)"
+ by (simp add: comp_assoc)
+ then have final_step:
"p ^^ 2 = ((Fun.swap j k id) \<circ> (Fun.swap g h id)) \<circ>
(cycle_of_list [i, j, k]) \<circ>
(inv' ((Fun.swap j k id) \<circ> (Fun.swap g h id)))"
- by (smt bij_id bij_swap_iff comp_id cycle_of_list.simps(1) cycle_of_list.simps(3)
- fun.map_comp insertCI inv_swap_id o_inv_distrib o_inv_o_cancel surj_id
- surj_imp_inj_inv surj_imp_surj_swap swap_id_independent)
-
- define q where "q = (Fun.swap j k id) \<circ> (Fun.swap g h id)"
+ using ijjk jkij by (auto simp: p2)
+ define q where "q \<equiv> (Fun.swap j k id) \<circ> (Fun.swap g h id)"
hence "(p \<circ> p) = q \<circ> p \<circ> (inv' q)"
by (metis final_step One_nat_def Suc_1 comp_id funpow.simps(2) funpow_simps_right(1) ijk p)
hence "(p \<circ> p) \<circ> (inv' p) = q \<circ> p \<circ> (inv' q) \<circ> (inv' p)" by simp
@@ -632,7 +650,8 @@
have "set [1 :: nat, 2, 3] \<subseteq> {1..n}" using assms by auto
moreover have "cycle [1 :: nat, 2, 3]" by simp
moreover have "length [1 :: nat, 2, 3] = 3" by simp
- ultimately have "cycle_of_list [1 :: nat, 2, 3] \<in> three_cycles n" by blast
+ ultimately have "cycle_of_list [1 :: nat, 2, 3] \<in> three_cycles n"
+ unfolding three_cycles_def by blast
hence "cycle_of_list [1 :: nat, 2, 3] \<in> carrier (alt_group n)"
using alt_group_as_three_cycles by (simp add: generate.incl)
--- a/src/HOL/Algebra/Zassenhaus.thy Sun Jul 08 11:00:20 2018 +0100
+++ b/src/HOL/Algebra/Zassenhaus.thy Sun Jul 08 16:07:26 2018 +0100
@@ -68,7 +68,7 @@
proof-
have N_carrierG : "N \<subseteq> carrier(G)"
using assms normal_imp_subgroup subgroup.subset
- by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
+ using incl_subgroup by blast
{have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
proof
fix x assume xH : "x \<in> H"
@@ -113,8 +113,10 @@
using B2 B3 assms l_coset_def by fastforce
from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2"
using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
- have " x\<otimes>y = n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3
- by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier)
+ have "\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G" "\<And>a. a \<in> H \<Longrightarrow> a \<in> carrier G"
+ by (meson assms normal_def subgroup.mem_carrier)+
+ then have "x\<otimes>y = n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3
+ by (metis (no_types) B2 B3 \<open>\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G\<close> m_assoc m_closed y2_def y2_prop)
moreover have B4 :"n1 \<otimes> y2 \<in>N"
using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def)
moreover have "h1 \<otimes> h2 \<in>H" using B2 B3 assms by (simp add: subgroup.m_closed)