# HG changeset patch # User paulson # Date 1531062446 -3600 # Node ID 57721285d4ef8c8480b64691d6597656b38f0551 # Parent 73eeb3f3140648911eec98044e8a6a95d8035a29 elimination of some "smt" diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Coset.thy --- 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 \ (g \ inv g) \ 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 \ carrier G" + by (meson subgroup.mem_carrier assms(1) h1(1)) + moreover have "h2 \ 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 \ inv r2 = h1 \ inv h2" using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce thus "r1 \ inv r2 \ H" by (metis assms(1) h1(1) h2(1) subgroup_def) @@ -210,7 +218,8 @@ thus "x <# H \ H" unfolding l_coset_def by blast next have "\h. h \ H \ x \ ((inv x) \ 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 "\h. h \ H \ (inv x) \ h \ H" by (simp add: assms subgroup.m_closed subgroup.m_inv_closed) ultimately show "H \ x <# H" unfolding l_coset_def by blast @@ -293,7 +302,7 @@ text \Multiplication of general subsets\ 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 \ carrier G" @@ -323,13 +332,16 @@ then obtain h1 k1 h2 k2 where h1k1: "h1 \ H" "k1 \ K" "x = h1 \ k1" and h2k2: "h2 \ H" "k2 \ K" "y = h2 \ k2" unfolding set_mult_def by blast - hence "x \ y = (h1 \ k1) \ (h2 \ k2)" by simp + with KG HG have carr: "k1 \ carrier G" "h1 \ carrier G" "k2 \ carrier G" "h2 \ carrier G" + by (meson subgroup.mem_carrier)+ + have "x \ y = (h1 \ k1) \ (h2 \ k2)" + using h1k1 h2k2 by simp also have " ... = h1 \ (k1 \ h2) \ 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 \ (h2 \ k1) \ 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 \ y = (h1 \ h2) \ (k1 \ 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 \ y \ 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' \ H" "y = x \ h'" using assms(1) unfolding l_coset_def by blast - hence "\ h. h \ H \ x \ h = y \ ((inv h') \ h)" - by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier) + hence "x \ h = y \ ((inv h') \ h)" if "h \ H" for h + proof - + have f3: "h' \ carrier G" + by (meson assms(3) h'(1) subgroup.mem_carrier) + have f4: "h \ 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 "\ xh. xh \ x <# H \ xh \ y <# H" unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def) moreover have "\ h. h \ H \ y \ h = x \ (h' \ h)" @@ -494,7 +513,7 @@ proof fix x assume x: "x \ H" thus "x \ 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 diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Divisibility.thy --- 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' \ 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: diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Embedded_Algebras.thy --- 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 \ (k \ a) \ 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 diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Ideal.thy --- 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 \Generation of Principal Ideals in Commutative Rings\ definition cgenideal :: "_ \ 'a \ 'a set" ("PIdl\ _" [80] 79) - where "cgenideal R a = {x \\<^bsub>R\<^esub> a | x. x \ carrier R}" + where "cgenideal R a \ {x \\<^bsub>R\<^esub> a | x. x \ carrier R}" + +lemma cginideal_def': "cgenideal R a = (\x. x \\<^bsub>R\<^esub> a) ` carrier R" + by (auto simp add: cgenideal_def) text \genhideal (?) really generates an ideal\ lemma (in cring) cgenideal_ideal: diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/QuotRing.thy --- 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 \ ring_iso R S \ (inv_into (carrier R) h) \ ring_iso S R" + assumes "ring R" and h: "h \ ring_iso R S" + shows "(inv_into (carrier R) h) \ ring_iso S R" proof - - assume h: "h \ ring_iso R S" - hence h_hom: "h \ ring_hom R S" + have h_hom: "h \ ring_hom R S" and h_surj: "h ` (carrier R) = (carrier S)" and h_inj: "\ x1 x2. \ x1 \ carrier R; x2 \ carrier R \ \ h x1 = h x2 \ 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 \ 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: \ring R\ 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: \ring R\ inv_into_f_eq ring.ring_simprules(1)) + by (simp add: \ring R\ inv_into_f_eq ring.ring_simprules(6)) qed corollary ring_iso_sym: diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Ring_Divisibility.thy --- 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 "\ carrier R \ PIdl p" hence "carrier R = PIdl p" by simp then obtain c where "c \ carrier R" "c \ p = \" - 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 \ Units R" unfolding Units_def using m_comm assms by auto thus False using A unfolding prime_def by simp qed diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Sym_Groups.thy --- 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 \ (nat \ nat) set" +definition three_cycles :: "nat \ (nat \ nat) set" where "three_cycles n \ { cycle_of_list cs | cs. cycle cs \ length cs = 3 \ set cs \ {1..n} }" @@ -354,7 +354,8 @@ proof - from \p \ three_cycles n\ obtain cs where p: "p = cycle_of_list cs" - and cs: "cycle cs" "length cs = 3" "set cs \ {1..n}" by blast + and cs: "cycle cs" "length cs = 3" "set cs \ {1..n}" + using three_cycles_def by blast hence "p = (Fun.swap (cs ! 0) (cs ! 1) id) \ (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 \ 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 \ a" hence "q \ (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 \ a" + have "q \ (three_cycles n)" + unfolding three_cycles_def mem_Collect_eq + proof (intro exI conjI) + show "cycle [a,b,c]" + using A \c \ a\ by auto + qed (use A in auto) thus "q \ 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 \ nat" assume A: "swapidseq_ext S 2 q" "S \ {1..n}" have "q \ 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 \ c" have "q = (cycle_of_list [a, b, c]) \ (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] \\<^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] \a \ b\ \c \ d\ 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 \ r" "S1 \ 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 \ 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 \ generate (alt_group n) (three_cycles n)" - using aux_lemma2[OF split(1)] \S1 \ S2 = {1..n}\ by auto + using gen3swap[OF split(1)] \S1 \ S2 = {1..n}\ 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 \ nat" assume "p \ three_cycles n" then obtain cs - where cs: "cycle cs" "length cs = 3" "set cs \ {1..n}" and p: "p = cycle_of_list cs" by blast + where cs: "cycle cs" "length cs = 3" "set cs \ {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 \l \ {i, j, k}\ by auto qed qed - hence "p ^^ 2 = (Fun.swap j k id) \ (cycle_of_list [i, j, k]) \ (inv' (Fun.swap j k id))" + hence p2: "p ^^ 2 = (Fun.swap j k id) \ (cycle_of_list [i, j, k]) \ (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}) \ card {1..n} - card {i, j, k}" + have "card ({1..n} - {i, j, k}) \ 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}) \ 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 \ 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 \ {1..n} - {i, j, k}" using f(2) gh(2) by force - hence h: "h \ {1..n} - {i, j, k}" using f(2) gh(2) by force + hence g: "g \ {1..n} - {i, j, k}" and h: "h \ {1..n} - {i, j, k}" using f(2) gh(2) by force+ hence gh_simps: "g \ h \ g \ {1..n} \ h \ {1..n} \ g \ {i, j, k} \ h \ {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 \ Fun.swap i j (Fun.swap j k id)" + and jkij: "Fun.swap j k id \ (Fun.swap i j id \ Fun.swap j k id) \ 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 \ 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 \ inv' (Fun.swap j k id \ 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 \ (Fun.swap j k id \ (Fun.swap j k id \ Fun.swap i j (Fun.swap j k id) \ Fun.swap j k id)) \ inv' (Fun.swap j k id) = Fun.swap j k id \ Fun.swap i j (Fun.swap j k id)" + by (simp add: comp_swap inv_swap_id) + moreover have "Fun.swap j k id \ Fun.swap i j (Fun.swap j k id) \ Fun.swap j k id = Fun.swap j k id \ (Fun.swap j k id \ (Fun.swap j k id \ Fun.swap i j (Fun.swap j k id) \ Fun.swap j k id))" + by (simp add: comp_swap inv_swap_id) + moreover have "Fun.swap g h id \ (Fun.swap j k id \ Fun.swap i j (Fun.swap j k id) \ Fun.swap j k id) \ inv' (Fun.swap j k id \ Fun.swap g h id) = Fun.swap j k id \ (Fun.swap j k id \ (Fun.swap j k id \ Fun.swap i j (Fun.swap j k id) \ Fun.swap j k id)) \ 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 \ Fun.swap g h id \ (Fun.swap j k id \ Fun.swap i j (Fun.swap j k id) \ Fun.swap j k id) \ inv' (Fun.swap j k id \ Fun.swap g h id)" + by (simp add: comp_assoc) + then have final_step: "p ^^ 2 = ((Fun.swap j k id) \ (Fun.swap g h id)) \ (cycle_of_list [i, j, k]) \ (inv' ((Fun.swap j k id) \ (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) \ (Fun.swap g h id)" + using ijjk jkij by (auto simp: p2) + define q where "q \ (Fun.swap j k id) \ (Fun.swap g h id)" hence "(p \ p) = q \ p \ (inv' q)" by (metis final_step One_nat_def Suc_1 comp_id funpow.simps(2) funpow_simps_right(1) ijk p) hence "(p \ p) \ (inv' p) = q \ p \ (inv' q) \ (inv' p)" by simp @@ -632,7 +650,8 @@ have "set [1 :: nat, 2, 3] \ {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] \ three_cycles n" by blast + ultimately have "cycle_of_list [1 :: nat, 2, 3] \ three_cycles n" + unfolding three_cycles_def by blast hence "cycle_of_list [1 :: nat, 2, 3] \ carrier (alt_group n)" using alt_group_as_three_cycles by (simp add: generate.incl) diff -r 73eeb3f31406 -r 57721285d4ef src/HOL/Algebra/Zassenhaus.thy --- 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 \ 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 \ normalizer G N" unfolding normalizer_def stabilizer_def proof fix x assume xH : "x \ H" @@ -113,8 +113,10 @@ using B2 B3 assms l_coset_def by fastforce from this obtain y2 where y2_def:"y2 \ N" and y2_prop:"y2\h1 = h1\n2" using singletonD by (metis (no_types, lifting) UN_E r_coset_def) - have " x\y = n1 \ y2 \ h1 \ h2" using y2_def B2 B3 - by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier) + have "\a. a \ N \ a \ carrier G" "\a. a \ H \ a \ carrier G" + by (meson assms normal_def subgroup.mem_carrier)+ + then have "x\y = n1 \ y2 \ h1 \ h2" using y2_def B2 B3 + by (metis (no_types) B2 B3 \\a. a \ N \ a \ carrier G\ m_assoc m_closed y2_def y2_prop) moreover have B4 :"n1 \ y2 \N" using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def) moreover have "h1 \ h2 \H" using B2 B3 assms by (simp add: subgroup.m_closed)