--- a/src/HOL/Algebra/Cycles.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Cycles.thy Sun Jul 08 23:35:33 2018 +0100
@@ -319,7 +319,7 @@
moreover obtain n where "n * k > m"
by (metis calculation(1) dividend_less_times_div mult.commute mult_Suc_right)
ultimately show ?thesis
- using funpow_mult[of n k p] id_funpow[of n] mult.commute[of k n] by smt
+ by (metis (full_types) funpow_mult id_funpow mult.commute)
qed
@@ -595,9 +595,8 @@
finally show "p ((support p x) ! i) = (support p x) ! (i + 1)" .
qed
hence 1: "map p (butlast (support p x)) = tl (support p x)"
- using nth_equalityI[of "map p (butlast (support p x))" "tl (support p x)"]
- by (smt Suc_eq_plus1 le0 length_butlast length_map length_tl nth_butlast nth_map nth_tl)
-
+ using nth_butlast [where 'a='a] nth_tl [where 'a='a]
+ nth_equalityI[of "map p (butlast (support p x))" "tl (support p x)"] by force
have "p ((support p x) ! (length (support p x) - 1)) = p ((p ^^ (length (support p x) - 1)) x)"
using assms(2) by auto
also have " ... = (p ^^ (length (support p x))) x"
@@ -672,7 +671,8 @@
qed
hence "bij_betw p ?S' ?S'"
by (metis DiffD1 assms(1) bij_betw_subset permutes_imp_bij subsetI)
- hence "bij_betw ?q ?S' ?S'" by (smt bij_betw_cong)
+ hence "bij_betw ?q ?S' ?S'"
+ by (rule rev_iffD1 [OF _ bij_betw_cong]) auto
moreover have "\<And>y. y \<notin> ?S' \<Longrightarrow> ?q y = y" by auto
ultimately show ?thesis
using bij_imp_permutes by blast
@@ -686,7 +686,6 @@
case (less x) thus ?case
proof (cases "S = {}")
case True thus ?thesis
- (* using less empty by auto *)
by (metis empty less.prems(1) permutes_empty)
next
case False
@@ -696,7 +695,7 @@
hence q_permutes: "q permutes S'"
using semidecomposition[OF less.prems(1-2), of x] S' q by blast
moreover have "x \<in> set (support p x)"
- by (smt add.left_neutral diff_zero funpow_0 in_set_conv_nth least_power_gt_zero
+ by (metis (no_types, lifting) add.left_neutral diff_zero funpow_0 in_set_conv_nth least_power_gt_zero
length_map length_upt less.prems(1) less.prems(2) nth_map_upt permutation_permutes)
hence "card S' < card S"
by (metis Diff_iff S' \<open>x \<in> S\<close> card_seteq leI less.prems(2) subsetI)
@@ -710,7 +709,6 @@
assume y: "y \<in> set (support p x)" hence "y \<notin> S'" using S' by simp
hence "q y = y" using q by simp
thus ?thesis
- (* using cycle_restrict less.prems(1) less.prems(2) permutation_permutes y by fastforce *)
using comp_apply cycle_restrict less.prems permutation_permutes y by fastforce
next
assume y: "y \<notin> set (support p x)" thus ?thesis
--- a/src/HOL/Algebra/Generated_Groups.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy Sun Jul 08 23:35:33 2018 +0100
@@ -297,26 +297,27 @@
lemma (in group) generate_pow:
assumes "a \<in> carrier G"
- shows "generate G { a } = { a [^] k | k. k \<in> (UNIV :: int set) }"
+ shows "generate G { a } = range (\<lambda>k::int. a [^] k)" (is "?lhs = ?rhs")
proof
- show "generate G { a } \<subseteq> { a [^] k | k. k \<in> (UNIV :: int set) }"
+ show "?lhs \<subseteq> ?rhs"
proof
- fix h show "h \<in> generate G { a } \<Longrightarrow> h \<in> { a [^] k | k. k \<in> (UNIV :: int set) }"
+ fix h show "h \<in> generate G { a } \<Longrightarrow> h \<in> range (\<lambda>k::int. a [^] k)"
proof (induction rule: generate.induct)
- case one thus ?case by (metis (mono_tags, lifting) UNIV_I int_pow_0 mem_Collect_eq)
+ case one thus ?case
+ by (metis (full_types) int_pow_0 rangeI)
next
case (incl h) hence "h = a" by auto thus ?case
- by (metis (mono_tags, lifting) CollectI UNIV_I assms group.int_pow_1 is_group)
+ by (metis \<open>h = a\<close> assms group.int_pow_1 is_group rangeI)
next
case (inv h) hence "h = a" by auto thus ?case
- by (metis (mono_tags, lifting) mem_Collect_eq UNIV_I assms group.int_pow_1 int_pow_neg is_group)
+ by (metis (mono_tags) rangeI assms group.int_pow_1 int_pow_neg is_group)
next
case (eng h1 h2) thus ?case
- by (smt assms group.int_pow_mult is_group iso_tuple_UNIV_I mem_Collect_eq)
+ using assms is_group by (auto simp: image_iff simp flip: int_pow_mult)
qed
qed
- show "{ a [^] k | k. k \<in> (UNIV :: int set) } \<subseteq> generate G { a }"
+ show "?rhs \<subseteq> ?lhs"
proof
{ fix k :: "nat" have "a [^] k \<in> generate G { a }"
proof (induction k)
@@ -325,16 +326,18 @@
case (Suc k) thus ?case by (simp add: generate.eng generate.incl)
qed } note aux_lemma = this
- fix h assume "h \<in> { a [^] k | k. k \<in> (UNIV :: int set) }"
+ fix h assume "h \<in> ?rhs"
then obtain k :: "nat" where "h = a [^] k \<or> h = inv (a [^] k)"
- by (smt group.int_pow_def2 is_group mem_Collect_eq)
+ by (auto simp: int_pow_def2)
thus "h \<in> generate G { a }" using aux_lemma
using assms generate_m_inv_closed by auto
qed
qed
+(* { a [^] k | k. k \<in> (UNIV :: int set) } *)
+
corollary (in group) generate_one: "generate G { \<one> } = { \<one> }"
- using generate_pow[of "\<one>", OF one_closed] by simp
+ using generate_pow[of "\<one>", OF one_closed] by auto
corollary (in group) generate_empty: "generate G {} = { \<one> }"
using mono_generate[of "{}" "{ \<one> }"] generate_one generate.one one_closed by blast
@@ -425,9 +428,12 @@
proof -
obtain h1 h2 where h1: "h1 \<in> H" and h2: "h2 \<in> H" and h: "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
using A by blast
- hence "h = (h1 \<otimes> inv h1) \<otimes> (h2 \<otimes> inv h2)" using assms
- by (smt inv_closed inv_mult m_assoc m_closed r_inv set_rev_mp)
- thus ?thesis using h1 h2 assms by (metis contra_subsetD one_closed r_inv r_one)
+ then have "h1 \<in> carrier G" "h2 \<in> carrier G"
+ using assms by auto
+ then have "\<one> = h"
+ by (metis \<open>h1 \<in> carrier G\<close> \<open>h2 \<in> carrier G\<close> h inv_closed inv_mult m_assoc m_closed r_inv)
+ then show ?thesis
+ using \<open>h1 \<in> carrier G\<close> \<open>h2 \<in> carrier G\<close> by force
qed } note aux_lemma = this
show ?thesis
proof
@@ -585,8 +591,15 @@
case 0 thus ?case using A by simp
next
case (Suc n) thus ?case
- using aux_lemma1 derived_self_is_normal funpow_simps_right(2) funpow_swap1
- normal_def o_apply order.trans order_refl subgroup.subset by smt
+ using aux_lemma1 derived_self_is_normal normal_def o_apply
+ proof auto (*FIXME a mess*)
+ fix x :: 'a
+ assume a1: "derived G (carrier G) \<lhd> G"
+ assume a2: "x \<in> derived G ((derived G ^^ n) I)"
+ assume "\<And>Ja Ia. \<lbrakk>Ja \<subseteq> carrier G; Ia \<subseteq> Ja\<rbrakk> \<Longrightarrow> derived G Ia \<subseteq> derived G Ja"
+ then show "x \<in> carrier G"
+ using a2 a1 by (meson Suc.IH normal_def order_refl subgroup.subset subsetCE)
+ qed
qed } note aux_lemma2 = this
show ?thesis
--- a/src/HOL/Algebra/Group.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Group.thy Sun Jul 08 23:35:33 2018 +0100
@@ -454,23 +454,22 @@
using n_ge nat_pow_pow[OF assms, of "nat n" "nat m"] int_pow_def2
by (simp add: mult_less_0_iff nat_mult_distrib)
next
- assume m_lt: "\<not> m \<ge> 0" thus ?thesis
- using n_ge int_pow_def2 nat_pow_pow[OF assms, of "nat n" "nat (- m)"]
- by (smt assms group.int_pow_neg is_group mult_minus_right nat_mult_distrib split_mult_neg_le)
+ assume m_lt: "\<not> m \<ge> 0"
+ with n_ge show ?thesis
+ apply (simp add: int_pow_def2 mult_less_0_iff)
+ by (metis assms mult_minus_right n_ge nat_mult_distrib nat_pow_pow)
qed
next
assume n_lt: "\<not> n \<ge> 0" thus ?thesis
proof (cases)
- assume m_ge: "m \<ge> 0" thus ?thesis
- using n_lt nat_pow_pow[OF assms, of "nat (- n)" "nat m"]
- nat_pow_inv[of "x [^] nat (- n)" "nat m"] int_pow_def2
- by (smt assms group.int_pow_closed group.int_pow_neg is_group mult_minus_right
- mult_nonpos_nonpos nat_mult_distrib_neg)
+ assume m_ge: "m \<ge> 0"
+ have "inv x [^] (nat m * nat (- n)) = inv x [^] nat (- (m * n))"
+ by (metis (full_types) m_ge mult_minus_right nat_mult_distrib)
+ with m_ge n_lt show ?thesis
+ by (simp add: int_pow_def2 mult_less_0_iff assms mult.commute nat_pow_inv nat_pow_pow)
next
assume m_lt: "\<not> m \<ge> 0" thus ?thesis
- using n_lt nat_pow_pow[OF assms, of "nat (- n)" "nat (- m)"]
- nat_pow_inv[of "x [^] nat (- n)" "nat (- m)"] int_pow_def2
- by (smt assms inv_inv mult_nonpos_nonpos nat_mult_distrib_neg nat_pow_closed)
+ using n_lt by (auto simp: int_pow_def2 mult_less_0_iff assms nat_mult_distrib_neg nat_pow_inv nat_pow_pow)
qed
qed
@@ -698,8 +697,9 @@
hence "a \<otimes> inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a= \<one>"
using aH assms group.inv_closed[OF assms(2)] ab_eq by simp
ultimately have "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a = inv a"
- by (smt aH assms(1) contra_subsetD group.inv_inv is_group local.inv_equality)
- moreover have "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a \<in> H" using aH group.inv_closed[OF assms(2)] by auto
+ by (metis aH assms(1) contra_subsetD group.inv_inv is_group local.inv_equality)
+ moreover have "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a \<in> H"
+ using aH group.inv_closed[OF assms(2)] by auto
ultimately show "inv a \<in> H" by auto
qed
@@ -1072,8 +1072,7 @@
apply (rule subgroupI)
apply (auto simp add: image_subsetI)
apply (metis (no_types, hide_lams) G.inv_closed hom_inv image_iff)
- apply (smt G.monoid_axioms hom_mult image_iff monoid.m_closed)
- done
+ by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)
lemma (in group_hom) subgroup_img_is_subgroup:
assumes "subgroup I G"
--- a/src/HOL/Algebra/Ideal_Product.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Ideal_Product.thy Sun Jul 08 23:35:33 2018 +0100
@@ -58,6 +58,8 @@
by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
next
fix s1 s2 assume s1: "s1 \<in> I \<cdot> J" and s2: "s2 \<in> I \<cdot> J"
+ have IJcarr: "\<And>a. a \<in> I \<cdot> J \<Longrightarrow> a \<in> carrier R"
+ by (meson assms subsetD ideal_prod_in_carrier)
show "s1 \<in> carrier R" using ideal_prod_in_carrier[OF assms] s1 by blast
show "s1 \<oplus> s2 \<in> I \<cdot> J" by (simp add: ideal_prod.sum[OF s1 s2])
show "inv\<^bsub>add_monoid R\<^esub> s1 \<in> I \<cdot> J" using s1
@@ -69,8 +71,7 @@
by (simp add: additive_subgroup.a_subgroup ideal.axioms(1) prod.hyps subgroup.m_inv_closed)
next
case (sum s1 s2) thus ?case
- by (smt a_inv_def add.inv_mult_group contra_subsetD
- assms ideal_prod.sum ideal_prod_in_carrier)
+ by (metis (no_types) IJcarr a_inv_def add.inv_mult_group ideal_prod.sum sum.hyps)
qed
qed
next
@@ -81,16 +82,29 @@
by (simp add: x ideal.I_l_closed ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
- by (smt assms contra_subsetD ideal_prod.sum ideal_prod_in_carrier r_distr x)
+ proof -
+ have IJ: "I \<cdot> J \<subseteq> carrier R"
+ by (metis (no_types) assms(1) assms(2) ideal.axioms(2) ring.ideal_prod_in_carrier)
+ then have "s2 \<in> carrier R"
+ using sum.hyps(3) by blast
+ moreover have "s1 \<in> carrier R"
+ using IJ sum.hyps(1) by blast
+ ultimately show ?thesis
+ by (simp add: ideal_prod.sum r_distr sum.hyps x)
+ qed
qed
-
show "s \<otimes> x \<in> I \<cdot> J" using s
proof (induct s rule: ideal_prod.induct)
case (prod i j) thus ?case using ideal_prod.prod[of i I "j \<otimes> x" J R] assms x
by (simp add: x ideal.I_r_closed ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
- by (smt assms contra_subsetD ideal_prod.sum ideal_prod_in_carrier l_distr x)
+ proof -
+ have "s1 \<in> carrier R" "s2 \<in> carrier R"
+ by (meson assms subsetD ideal_prod_in_carrier sum.hyps)+
+ then show ?thesis
+ by (metis ideal_prod.sum l_distr sum.hyps(2) sum.hyps(4) x)
+ qed
qed
qed
@@ -198,8 +212,14 @@
by (metis assms ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
- by (smt additive_subgroup.a_Hcarr contra_subsetD ideal.axioms(1)
- assms ideal_prod.sum ideal_prod_in_carrier l_distr)
+ proof -
+ have "s1 \<in> carrier R" "s2 \<in> carrier R"
+ by (meson assms subsetD ideal.axioms(2) ring.ideal_prod_in_carrier sum.hyps)+
+ moreover have "k \<in> carrier R"
+ by (meson additive_subgroup.a_Hcarr assms(3) ideal.axioms(1) sum.prems)
+ ultimately show ?thesis
+ by (metis ideal_prod.sum l_distr sum.hyps(2) sum.hyps(4) sum.prems)
+ qed
qed
qed
qed
@@ -217,8 +237,14 @@
by (metis assms ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
- by (smt additive_subgroup.a_Hcarr contra_subsetD ideal.axioms(1)
- assms ideal_prod.sum ideal_prod_in_carrier r_distr)
+ proof -
+ have "\<And>a A B. \<lbrakk>a \<in> B \<cdot> A; ideal A R; ideal B R\<rbrakk> \<Longrightarrow> a \<in> carrier R"
+ by (meson subsetD ideal_prod_in_carrier)
+ moreover have "i \<in> carrier R"
+ by (meson additive_subgroup.a_Hcarr assms(1) ideal.axioms(1) sum.prems)
+ ultimately show ?thesis
+ by (metis (no_types) assms(2) assms(3) ideal_prod.sum r_distr sum)
+ qed
qed
qed
qed
@@ -428,8 +454,7 @@
have I_SucSuc_I0: "ideal (I (Suc (Suc n))) R \<and> ideal (I 0) R"
using Suc.prems(1) by auto
have fprod_cl2: "ideal (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) R"
- by (smt ISet.finprod_closed I_carr Pi_split_insert_domain atMost_Suc ideals_set_def mem_Collect_eq partial_object.select_convs(1))
-
+ by (metis (no_types) ISet.finprod_closed I_carr Pi_split_insert_domain atMost_Suc ideals_set_def mem_Collect_eq partial_object.select_convs(1))
have "carrier R = I (Suc (Suc n)) <+> I 0"
by (simp add: Suc.prems(2))
also have " ... = I (Suc (Suc n)) <+>
--- a/src/HOL/Algebra/Polynomials.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Polynomials.thy Sun Jul 08 23:35:33 2018 +0100
@@ -440,8 +440,10 @@
let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
have p1: "p1 \<noteq> []" and p2: "?p2 \<noteq> []"
using A(3) by auto
+ then have "zip p1 (replicate (length p1 - length p2) \<zero> @ p2) = zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) \<zero> @ p2) # tl (replicate (length p1 - length p2) \<zero> @ p2))"
+ by auto
hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
- by (smt case_prod_conv list.exhaust_sel list.map(2) list.sel(1) zip_Cons_Cons)
+ by simp
moreover have "lead_coeff p1 \<in> carrier R"
using p1 A(1) unfolding polynomial_def by auto
ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
@@ -465,7 +467,7 @@
assumes "polynomial R p1" "polynomial R p2" and "degree p1 \<noteq> degree p2"
shows "degree (poly_add p1 p2) = max (degree p1) (degree p2)"
using poly_add_length_eq[of p1 p2] assms
- by (smt degree_def diff_le_mono le_cases max.absorb1 max_def)
+ by (metis (no_types, lifting) degree_def diff_le_mono max.absorb_iff1 max_def)
lemma poly_add_coeff_aux:
assumes "length p1 \<ge> length p2"
@@ -1032,7 +1034,12 @@
also have " ... = poly_add ((map (\<lambda>a. \<zero> \<otimes> a) p) @ (replicate n \<zero>)) []"
using Suc by (simp add: degree_def)
also have " ... = poly_add ((map (\<lambda>a. \<zero>) p) @ (replicate n \<zero>)) []"
- using Suc(2) by (smt map_eq_conv ring_simprules(24) subset_code(1))
+ proof -
+ have "map ((\<otimes>) \<zero>) p = map (\<lambda>a. \<zero>) p"
+ using Suc.prems by auto
+ then show ?thesis
+ by presburger
+ qed
also have " ... = poly_add (replicate (length p + n) \<zero>) []"
by (simp add: map_replicate_const replicate_add)
also have " ... = poly_add [] []"
@@ -1158,9 +1165,9 @@
using p1 p2 polynomial_in_carrier[OF assms(1)] polynomial_in_carrier[OF assms(2)] by auto
have "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) = a \<otimes> b"
using poly_mult_lead_coeff_aux[OF assms] p1 p2 by simp
- hence "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) \<noteq> \<zero>"
+ hence neq0: "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) \<noteq> \<zero>"
using assms p1 p2 integral[of a b] unfolding polynomial_def by auto
- moreover have "\<And>i. i > (degree p1) + (degree p2) \<Longrightarrow> (coeff (poly_mult p1 p2)) i = \<zero>"
+ moreover have eq0: "\<And>i. i > (degree p1) + (degree p2) \<Longrightarrow> (coeff (poly_mult p1 p2)) i = \<zero>"
proof -
have aux_lemma: "degree (poly_mult p1 p2) \<le> (degree p1) + (degree p2)"
proof (induct p1)
@@ -1184,8 +1191,8 @@
using coeff_degree aux_lemma by simp
qed
ultimately have "degree (poly_mult p1 p2) = degree p1 + degree p2"
- using degree_def'[OF poly_mult_closed[OF assms]]
- by (smt coeff_degree linorder_cases not_less_Least)
+ by (metis eq0 neq0 assms coeff.simps(1) coeff_degree lead_coeff_simp length_greater_0_conv
+ normalize_idem normalize_length_lt not_less_iff_gr_or_eq poly_mult_closed)
thus ?thesis
using p1 p2 by auto
qed
--- a/src/HOL/Algebra/Solvable_Groups.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Solvable_Groups.thy Sun Jul 08 23:35:33 2018 +0100
@@ -70,6 +70,8 @@
"comm_group ((G \<lparr> carrier := H \<rparr>) Mod K)"
have "derived G H \<subseteq> K"
proof -
+ have Hcarr: "\<And>a. a \<in> H \<Longrightarrow> a \<in> carrier G"
+ by (meson A(4) subgroup.mem_carrier)
have "derived_set G H \<subseteq> K"
proof
fix h assume "h \<in> derived_set G H"
@@ -91,15 +93,19 @@
finally have "K #>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> (h1 \<otimes> h2) = K #>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> (h2 \<otimes> h1)"
using normal.rcos_sum[OF A(2),of h2 h1] h12(1-2) by simp
- moreover have "h1 \<otimes> h2 \<in> H" and "h2 \<otimes> h1 \<in> H"
+ moreover have h12H: "h1 \<otimes> h2 \<in> H" and "h2 \<otimes> h1 \<in> H"
using h12 subgroupE(4)[OF A(4)] by auto
ultimately have "K #> (h1 \<otimes> h2) = K #> (h2 \<otimes> h1)" by auto
then obtain k where k: "k \<in> K" "\<one> \<otimes> (h1 \<otimes> h2) = k \<otimes> (h2 \<otimes> h1)"
using subgroup.one_closed[OF A(3)] unfolding r_coset_def by blast
hence "(h1 \<otimes> h2) \<otimes> (inv h1 \<otimes> inv h2) = k"
- by (smt A(1) A(4) h12(1-2) inv_mult_group inv_solve_right
- l_one m_closed subgroup.mem_carrier subsetCE)
+ proof -
+ have "k \<in> carrier G"
+ by (meson A(3) k(1) subgroup.mem_carrier)
+ with Hcarr h12 show ?thesis
+ by (metis h12H inv_mult_group inv_solve_right k(2) r_cancel_one' subgroup_def subgroup_self)
+ qed
hence "h = k" using h12
by (meson A(4) \<open>h1 \<otimes> h2 \<in> H\<close> inv_closed m_assoc subgroup.mem_carrier)
thus "h \<in> K" using k(1) by simp
@@ -237,6 +243,8 @@
{ fix K assume A: "K \<subseteq> carrier G"
have "derived H (h ` K) = h ` (derived G K)"
proof -
+ have Kcarr: "\<And>a. a \<in> K \<Longrightarrow> a \<in> carrier G"
+ by (metis (no_types) A subsetCE)
have "derived_set H (h ` K) = h ` (derived_set G K)"
proof
show "derived_set H (h ` K) \<subseteq> h ` derived_set G K"
@@ -244,9 +252,14 @@
fix x assume "x \<in> derived_set H (h ` K)"
then obtain k1 k2
where k12: "k1 \<in> K" "k2 \<in> K"
- and "x = (h k1) \<otimes>\<^bsub>H\<^esub> (h k2) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h k2)" by blast
+ and xeq: "x = (h k1) \<otimes>\<^bsub>H\<^esub> (h k2) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h k2)" by blast
hence "x = h (k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2)"
- by (smt G.inv_closed G.m_closed A hom_inv hom_mult subsetCE)
+ proof -
+ have "k1 \<in> carrier G" "k2 \<in> carrier G"
+ using A \<open>k1 \<in> K\<close> \<open>k2 \<in> K\<close> by blast+
+ then show ?thesis
+ using G.inv_closed G.m_closed xeq hom_inv hom_mult by presburger
+ qed
thus "x \<in> h ` (derived_set G K)" using k12 by blast
qed
next
@@ -256,7 +269,7 @@
then obtain k1 k2 where k12: "k1 \<in> K" "k2 \<in> K"
and "x = h (k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2)" by blast
hence "x = (h k1) \<otimes>\<^bsub>H\<^esub> (h k2) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h k2)"
- by (smt G.inv_closed G.m_closed A hom_inv hom_mult subsetCE)
+ by (metis (no_types) Kcarr G.inv_closed G.m_closed hom_inv hom_mult)
thus "x \<in> derived_set H (h ` K)" using k12 by blast
qed
qed
--- a/src/HOL/Algebra/Zassenhaus.thy Sun Jul 08 16:07:26 2018 +0100
+++ b/src/HOL/Algebra/Zassenhaus.thy Sun Jul 08 23:35:33 2018 +0100
@@ -382,6 +382,8 @@
using subgroup.subset assms inv_closed xHK by auto
have allG : "H \<subseteq> carrier G" "K \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K1 \<subseteq> carrier G"
using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
+ have HK1: "H \<inter> K1 \<subseteq> carrier G"
+ by (simp add: allG(1) le_infI1)
have HK1_normal: "H\<inter>K1 \<lhd> (G\<lparr>carrier := H \<inter> K\<rparr>)" using normal_inter[OF assms(3)assms(1)assms(4)]
by (simp add : inf_commute)
have "H \<inter> K \<subseteq> normalizer G (H \<inter> K1)"
@@ -400,7 +402,7 @@
also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \<inter> K1 <#> {inv x})"
by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult)
also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H \<inter> K1 <#> {inv x})"
- by (smt Int_lower1 allG xG set_mult_assoc subset_trans setmult_subset_G)
+ using HK1 allG(3) set_mult_assoc setmult_subset_G xG(1) by auto
also have "... = ({x} <#> H1 <#> {\<one>}) <#> (H \<inter> K1 <#> {inv x})"
using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G)
also have "... =({x} <#> H1) <#> (H \<inter> K1 <#> {inv x})"
@@ -490,6 +492,8 @@
hence x_def : "x \<in> H1 <#> H \<inter> K" by simp
from this obtain h1 hk where h1hk_def :"h1 \<in> H1" "hk \<in> H \<inter> K" "h1 \<otimes> hk = x"
unfolding set_mult_def by blast
+ have HK1: "H \<inter> K1 \<subseteq> carrier G"
+ by (simp add: all_inclG(1) le_infI1)
have xH : "x \<in> H" using subgroup.subset[OF subH1] using x_def by auto
hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
@@ -502,14 +506,14 @@
using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
also have "... = h1 <# (hk <# H1 #> \<one> <#> H\<inter>K1 #> \<one>)"
using coset_mult_one allG all_inclG l_coset_subset_G
- by (smt inf_le2 setmult_subset_G subset_trans)
+ by (simp add: inf.coboundedI2 setmult_subset_G)
also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\<inter>K1 #> inv hk #> hk)"
using all_inclG allG coset_mult_assoc l_coset_subset_G
by (simp add: inf.coboundedI1 setmult_subset_G)
- finally have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) =
- h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\<inter>K1 #> inv hk) #> hk)"
- using rcos_assoc_lcos allG all_inclG
- by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans)
+ finally have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)
+ = h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\<inter>K1 #> inv hk) #> hk)"
+ using rcos_assoc_lcos allG all_inclG HK1
+ by (simp add: l_coset_subset_G r_coset_subset_G setmult_rcos_assoc)
moreover have "H \<subseteq> normalizer G H1"
using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
hence "\<And>g. g \<in> H \<Longrightarrow> g \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H1 = H1}"