# HG changeset patch # User paulson # Date 1531089333 -3600 # Node ID 440aa6b7d99a6c4d99a4e69ab00dfaca458b6b6c # Parent 57721285d4ef8c8480b64691d6597656b38f0551 removal of smt diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Cycles.thy --- 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 "\y. y \ ?S' \ ?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 \ 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' \x \ S\ card_seteq leI less.prems(2) subsetI) @@ -710,7 +709,6 @@ assume y: "y \ set (support p x)" hence "y \ 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 \ set (support p x)" thus ?thesis diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Generated_Groups.thy --- 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 \ carrier G" - shows "generate G { a } = { a [^] k | k. k \ (UNIV :: int set) }" + shows "generate G { a } = range (\k::int. a [^] k)" (is "?lhs = ?rhs") proof - show "generate G { a } \ { a [^] k | k. k \ (UNIV :: int set) }" + show "?lhs \ ?rhs" proof - fix h show "h \ generate G { a } \ h \ { a [^] k | k. k \ (UNIV :: int set) }" + fix h show "h \ generate G { a } \ h \ range (\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 \h = a\ 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 \ (UNIV :: int set) } \ generate G { a }" + show "?rhs \ ?lhs" proof { fix k :: "nat" have "a [^] k \ 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 \ { a [^] k | k. k \ (UNIV :: int set) }" + fix h assume "h \ ?rhs" then obtain k :: "nat" where "h = a [^] k \ h = inv (a [^] k)" - by (smt group.int_pow_def2 is_group mem_Collect_eq) + by (auto simp: int_pow_def2) thus "h \ generate G { a }" using aux_lemma using assms generate_m_inv_closed by auto qed qed +(* { a [^] k | k. k \ (UNIV :: int set) } *) + corollary (in group) generate_one: "generate G { \ } = { \ }" - using generate_pow[of "\", OF one_closed] by simp + using generate_pow[of "\", OF one_closed] by auto corollary (in group) generate_empty: "generate G {} = { \ }" using mono_generate[of "{}" "{ \ }"] generate_one generate.one one_closed by blast @@ -425,9 +428,12 @@ proof - obtain h1 h2 where h1: "h1 \ H" and h2: "h2 \ H" and h: "h = h1 \ h2 \ inv h1 \ inv h2" using A by blast - hence "h = (h1 \ inv h1) \ (h2 \ 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 \ carrier G" "h2 \ carrier G" + using assms by auto + then have "\ = h" + by (metis \h1 \ carrier G\ \h2 \ carrier G\ h inv_closed inv_mult m_assoc m_closed r_inv) + then show ?thesis + using \h1 \ carrier G\ \h2 \ carrier G\ 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) \ G" + assume a2: "x \ derived G ((derived G ^^ n) I)" + assume "\Ja Ia. \Ja \ carrier G; Ia \ Ja\ \ derived G Ia \ derived G Ja" + then show "x \ carrier G" + using a2 a1 by (meson Suc.IH normal_def order_refl subgroup.subset subsetCE) + qed qed } note aux_lemma2 = this show ?thesis diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Group.thy --- 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: "\ m \ 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: "\ m \ 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: "\ n \ 0" thus ?thesis proof (cases) - assume m_ge: "m \ 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 \ 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: "\ m \ 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 \ inv\<^bsub>G\carrier := H\\<^esub> a= \" using aH assms group.inv_closed[OF assms(2)] ab_eq by simp ultimately have "inv\<^bsub>G\carrier := H\\<^esub> a = inv a" - by (smt aH assms(1) contra_subsetD group.inv_inv is_group local.inv_equality) - moreover have "inv\<^bsub>G\carrier := H\\<^esub> a \ 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\carrier := H\\<^esub> a \ H" + using aH group.inv_closed[OF assms(2)] by auto ultimately show "inv a \ 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" diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Ideal_Product.thy --- 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 \ I \ J" and s2: "s2 \ I \ J" + have IJcarr: "\a. a \ I \ J \ a \ carrier R" + by (meson assms subsetD ideal_prod_in_carrier) show "s1 \ carrier R" using ideal_prod_in_carrier[OF assms] s1 by blast show "s1 \ s2 \ I \ J" by (simp add: ideal_prod.sum[OF s1 s2]) show "inv\<^bsub>add_monoid R\<^esub> s1 \ I \ 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 \ J \ carrier R" + by (metis (no_types) assms(1) assms(2) ideal.axioms(2) ring.ideal_prod_in_carrier) + then have "s2 \ carrier R" + using sum.hyps(3) by blast + moreover have "s1 \ 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 \ x \ I \ J" using s proof (induct s rule: ideal_prod.induct) case (prod i j) thus ?case using ideal_prod.prod[of i I "j \ 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 \ carrier R" "s2 \ 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 \ carrier R" "s2 \ carrier R" + by (meson assms subsetD ideal.axioms(2) ring.ideal_prod_in_carrier sum.hyps)+ + moreover have "k \ 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 "\a A B. \a \ B \ A; ideal A R; ideal B R\ \ a \ carrier R" + by (meson subsetD ideal_prod_in_carrier) + moreover have "i \ 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 \ ideal (I 0) R" using Suc.prems(1) by auto have fprod_cl2: "ideal (\\<^bsub>(ideals_set R)\<^esub> k \ {..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)) <+> diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Polynomials.thy --- 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) \) @ p2" have p1: "p1 \ []" and p2: "?p2 \ []" using A(3) by auto + then have "zip p1 (replicate (length p1 - length p2) \ @ p2) = zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) \ @ p2) # tl (replicate (length p1 - length p2) \ @ p2))" + by auto hence "lead_coeff (map2 (\) p1 ?p2) = lead_coeff p1 \ 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 \ carrier R" using p1 A(1) unfolding polynomial_def by auto ultimately have "lead_coeff (map2 (\) p1 ?p2) = lead_coeff p1" @@ -465,7 +467,7 @@ assumes "polynomial R p1" "polynomial R p2" and "degree p1 \ 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 \ length p2" @@ -1032,7 +1034,12 @@ also have " ... = poly_add ((map (\a. \ \ a) p) @ (replicate n \)) []" using Suc by (simp add: degree_def) also have " ... = poly_add ((map (\a. \) p) @ (replicate n \)) []" - using Suc(2) by (smt map_eq_conv ring_simprules(24) subset_code(1)) + proof - + have "map ((\) \) p = map (\a. \) p" + using Suc.prems by auto + then show ?thesis + by presburger + qed also have " ... = poly_add (replicate (length p + n) \) []" 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 \ b" using poly_mult_lead_coeff_aux[OF assms] p1 p2 by simp - hence "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) \ \" + hence neq0: "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) \ \" using assms p1 p2 integral[of a b] unfolding polynomial_def by auto - moreover have "\i. i > (degree p1) + (degree p2) \ (coeff (poly_mult p1 p2)) i = \" + moreover have eq0: "\i. i > (degree p1) + (degree p2) \ (coeff (poly_mult p1 p2)) i = \" proof - have aux_lemma: "degree (poly_mult p1 p2) \ (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 diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Solvable_Groups.thy --- 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 \ carrier := H \) Mod K)" have "derived G H \ K" proof - + have Hcarr: "\a. a \ H \ a \ carrier G" + by (meson A(4) subgroup.mem_carrier) have "derived_set G H \ K" proof fix h assume "h \ derived_set G H" @@ -91,15 +93,19 @@ finally have "K #>\<^bsub>G\carrier := H\\<^esub> (h1 \ h2) = K #>\<^bsub>G\carrier := H\\<^esub> (h2 \ h1)" using normal.rcos_sum[OF A(2),of h2 h1] h12(1-2) by simp - moreover have "h1 \ h2 \ H" and "h2 \ h1 \ H" + moreover have h12H: "h1 \ h2 \ H" and "h2 \ h1 \ H" using h12 subgroupE(4)[OF A(4)] by auto ultimately have "K #> (h1 \ h2) = K #> (h2 \ h1)" by auto then obtain k where k: "k \ K" "\ \ (h1 \ h2) = k \ (h2 \ h1)" using subgroup.one_closed[OF A(3)] unfolding r_coset_def by blast hence "(h1 \ h2) \ (inv h1 \ 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 \ 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) \h1 \ h2 \ H\ inv_closed m_assoc subgroup.mem_carrier) thus "h \ K" using k(1) by simp @@ -237,6 +243,8 @@ { fix K assume A: "K \ carrier G" have "derived H (h ` K) = h ` (derived G K)" proof - + have Kcarr: "\a. a \ K \ a \ 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) \ h ` derived_set G K" @@ -244,9 +252,14 @@ fix x assume "x \ derived_set H (h ` K)" then obtain k1 k2 where k12: "k1 \ K" "k2 \ K" - and "x = (h k1) \\<^bsub>H\<^esub> (h k2) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h k2)" by blast + and xeq: "x = (h k1) \\<^bsub>H\<^esub> (h k2) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h k2)" by blast hence "x = h (k1 \ k2 \ inv k1 \ inv k2)" - by (smt G.inv_closed G.m_closed A hom_inv hom_mult subsetCE) + proof - + have "k1 \ carrier G" "k2 \ carrier G" + using A \k1 \ K\ \k2 \ K\ by blast+ + then show ?thesis + using G.inv_closed G.m_closed xeq hom_inv hom_mult by presburger + qed thus "x \ h ` (derived_set G K)" using k12 by blast qed next @@ -256,7 +269,7 @@ then obtain k1 k2 where k12: "k1 \ K" "k2 \ K" and "x = h (k1 \ k2 \ inv k1 \ inv k2)" by blast hence "x = (h k1) \\<^bsub>H\<^esub> (h k2) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \\<^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 \ derived_set H (h ` K)" using k12 by blast qed qed diff -r 57721285d4ef -r 440aa6b7d99a src/HOL/Algebra/Zassenhaus.thy --- 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 \ carrier G" "K \ carrier G" "H1 \ carrier G" "K1 \ carrier G" using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ . + have HK1: "H \ K1 \ carrier G" + by (simp add: allG(1) le_infI1) have HK1_normal: "H\K1 \ (G\carrier := H \ K\)" using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add : inf_commute) have "H \ K \ normalizer G (H \ K1)" @@ -400,7 +402,7 @@ also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \ K1 <#> {inv x})" by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult) also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H \ 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 <#> {\}) <#> (H \ 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 \ K1 <#> {inv x})" @@ -490,6 +492,8 @@ hence x_def : "x \ H1 <#> H \ K" by simp from this obtain h1 hk where h1hk_def :"h1 \ H1" "hk \ H \ K" "h1 \ hk = x" unfolding set_mult_def by blast + have HK1: "H \ K1 \ carrier G" + by (simp add: all_inclG(1) le_infI1) have xH : "x \ H" using subgroup.subset[OF subH1] using x_def by auto hence allG : "h1 \ carrier G" "hk \ carrier G" "x \ 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 #> \ <#> H\K1 #> \)" 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\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\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = - h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\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\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) + = h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\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 \ normalizer G H1" using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp hence "\g. g \ H \ g \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) H1 = H1}"