author paulson Sun, 08 Jul 2018 23:35:33 +0100 changeset 68605 440aa6b7d99a parent 68604 57721285d4ef child 68606 96a49db47c97
removal of smt
 src/HOL/Algebra/Cycles.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Generated_Groups.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Group.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Ideal_Product.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Polynomials.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Solvable_Groups.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Zassenhaus.thy file | annotate | diff | comparison | revisions
```--- 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
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 (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 @@
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 @@
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"
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
-        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
@@ -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)"
-  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)

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>) []"
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)]
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