--- a/src/HOL/Algebra/Generated_Groups.thy Mon Jul 02 18:58:50 2018 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy Mon Jul 02 21:45:10 2018 +0100
@@ -51,7 +51,7 @@
show "\<And>h. h \<in> generate G H \<Longrightarrow> inv h \<in> generate G H"
using generate_m_inv_closed[OF assms] by blast
show "\<And>h1 h2. \<lbrakk> h1 \<in> generate G H; h2 \<in> generate G H \<rbrakk> \<Longrightarrow> h1 \<otimes> h2 \<in> generate G H"
- by (simp add: generate.eng)
+ by (simp add: generate.eng)
qed
@@ -64,11 +64,11 @@
proof
fix h show "h \<in> generate G H \<Longrightarrow> h \<in> E"
proof (induct rule: generate.induct)
- case one thus ?case using subgroup.one_closed[OF assms(2)] by simp
+ case one thus ?case using subgroup.one_closed[OF assms(2)] by simp
case incl thus ?case using assms(3) by blast
case inv thus ?case using subgroup.m_inv_closed[OF assms(2)] assms(3) by blast
next
- case eng thus ?case using subgroup.m_closed[OF assms(2)] by simp
+ case eng thus ?case using subgroup.m_closed[OF assms(2)] by simp
qed
qed
@@ -119,14 +119,14 @@
where
"norm G (One) = \<one>\<^bsub>G\<^esub>"
| "norm G (Inv h) = (inv\<^bsub>G\<^esub> h)"
- | "norm G (Leaf h) = h"
+ | "norm G (Leaf h) = h"
| "norm G (Mult h1 h2) = (norm G h1) \<otimes>\<^bsub>G\<^esub> (norm G h2)"
fun elts :: "'a repr \<Rightarrow> 'a set"
where
"elts (One) = {}"
| "elts (Inv h) = { h }"
- | "elts (Leaf h) = { h }"
+ | "elts (Leaf h) = { h }"
| "elts (Mult h1 h2) = (elts h1) \<union> (elts h2)"
lemma (in group) generate_repr_iff:
@@ -136,7 +136,7 @@
show "h \<in> generate G H \<Longrightarrow> \<exists>r. (elts r) \<subseteq> H \<and> norm G r = h"
proof (induction rule: generate.induct)
case one thus ?case
- using elts.simps(1) norm.simps(1)[of G] by fastforce
+ using elts.simps(1) norm.simps(1)[of G] by fastforce
next
case (incl h)
hence "elts (Leaf h) \<subseteq> H \<and> norm G (Leaf h) = h" by simp
@@ -150,7 +150,7 @@
then obtain r1 r2 where r1: "elts r1 \<subseteq> H" "norm G r1 = h1"
and r2: "elts r2 \<subseteq> H" "norm G r2 = h2" by blast
hence "elts (Mult r1 r2) \<subseteq> H \<and> norm G (Mult r1 r2) = h1 \<otimes> h2" by simp
- thus ?case by blast
+ thus ?case by blast
qed
show "\<exists>r. elts r \<subseteq> H \<and> norm G r = h \<Longrightarrow> h \<in> generate G H"
@@ -161,7 +161,7 @@
proof (induction arbitrary: h rule: repr.induct)
case One thus ?case using generate.one by auto
next
- case Inv thus ?case using generate.simps by force
+ case Inv thus ?case using generate.simps by force
next
case Leaf thus ?case using generate.simps by force
next
@@ -207,10 +207,10 @@
proof (induction r rule: repr.induct)
case One thus ?case by simp
next
- case (Inv k) hence "k \<in> K" using A by simp
+ case (Inv k) hence "k \<in> K" using A by simp
thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto
next
- case (Leaf k) hence "k \<in> K" using A by simp
+ case (Leaf k) hence "k \<in> K" using A by simp
thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto
next
case (Mult k1 k2) thus ?case using mult_eq by auto
@@ -259,7 +259,7 @@
thus "(g \<otimes> (norm G r) \<otimes> (inv g)) \<in> (generate G H)"
proof (induction r rule: repr.induct)
case One thus ?case
- by (simp add: generate.one)
+ by (simp add: generate.one)
next
case (Inv h)
hence "g \<otimes> h \<otimes> (inv g) \<in> H" using assms(2) by simp
@@ -267,7 +267,7 @@
using Inv.prems(1) Inv.prems(2) assms(1) inv_mult_group m_assoc by auto
ultimately have "\<exists>r. elts r \<subseteq> H \<and> norm G r = g \<otimes> (inv h) \<otimes> (inv g)"
by (metis elts.simps(2) empty_subsetI insert_subset)
- thus ?case by (simp add: assms(1) generate_repr_iff)
+ thus ?case by (simp add: assms(1) generate_repr_iff)
next
case (Leaf h)
thus ?case using assms(2)[of h g] generate.incl[of "g \<otimes> h \<otimes> inv g" H] by simp
@@ -305,16 +305,16 @@
proof
fix h show "h \<in> generate G { a } \<Longrightarrow> h \<in> { a [^] k | k. k \<in> (UNIV :: int set) }"
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 (mono_tags, lifting) UNIV_I int_pow_0 mem_Collect_eq)
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 (mono_tags, lifting) CollectI UNIV_I assms group.int_pow_1 is_group)
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)
next
case (eng h1 h2) thus ?case
- by (smt assms group.int_pow_mult is_group iso_tuple_UNIV_I mem_Collect_eq)
+ by (smt assms group.int_pow_mult is_group iso_tuple_UNIV_I mem_Collect_eq)
qed
qed
@@ -444,7 +444,7 @@
qed
thus ?thesis by simp
qed
- thus ?thesis unfolding derived_def using generate_empty generate_one by presburger
+ thus ?thesis unfolding derived_def using generate_empty generate_one by presburger
qed
lemma (in group) derived_set_in_carrier:
@@ -569,7 +569,7 @@
have "group (G \<lparr> carrier := H \<rparr>)"
using assms subgroup_imp_group by auto
thus ?thesis
- using group.derived_quot_is_comm_group subgroup_derived_equality[OF assms] by fastforce
+ using group.derived_quot_is_comm_group subgroup_derived_equality[OF assms] by fastforce
qed
lemma (in group) mono_derived:
@@ -610,8 +610,8 @@
also have " ... \<subseteq> (derived G) (carrier G)"
using mono_derived[of "carrier G" "(derived G ^^ n) H" 1] Suc by simp
also have " ... \<subseteq> carrier G" unfolding derived_def
- by (simp add: derived_set_incl generate_min_subgroup1 subgroup_self)
- finally show ?case .
+ by (simp add: derived_set_incl generate_min_subgroup1 subgroup_self)
+ finally show ?case .
qed
lemma (in group) exp_of_derived_is_subgroup:
@@ -624,8 +624,10 @@
have "(derived G ^^ n) H \<subseteq> carrier G"
by (simp add: Suc.IH assms subgroup.subset)
hence "subgroup ((derived G) ((derived G ^^ n) H)) G"
- unfolding derived_def using derived_set_in_carrier generate_is_subgroup by auto
+ unfolding derived_def using derived_set_in_carrier generate_is_subgroup by auto
thus ?case by simp
qed
-end
\ No newline at end of file
+hide_const (open) norm
+
+end
--- a/src/HOL/Algebra/Solvable_Groups.thy Mon Jul 02 18:58:50 2018 +0100
+++ b/src/HOL/Algebra/Solvable_Groups.thy Mon Jul 02 21:45:10 2018 +0100
@@ -174,9 +174,9 @@
show "generate H (h ` K) \<subseteq> h ` generate G K"
proof
fix x assume "x \<in> generate H (h ` K)"
- then obtain r where r: "elts r \<subseteq> (h ` K)" "norm H r = x"
+ then obtain r where r: "elts r \<subseteq> (h ` K)" "Generated_Groups.norm H r = x"
using H.generate_repr_iff img_in_carrier by auto
- from \<open>elts r \<subseteq> (h ` K)\<close> have "norm H r \<in> h ` generate G K"
+ from \<open>elts r \<subseteq> (h ` K)\<close> have "Generated_Groups.norm H r \<in> h ` generate G K"
proof (induct r rule: repr.induct)
case One
have "\<one>\<^bsub>G\<^esub> \<in> generate G K" using generate.one[of G] by simp
@@ -193,11 +193,11 @@
thus ?case by (simp add: generate.incl)
next
case (Mult x1 x2) hence A: "elts x1 \<union> elts x2 \<subseteq> h ` K" by simp
- have "norm H x1 \<in> h ` (generate G K)" using A Mult by simp
- moreover have "norm H x2 \<in> h ` (generate G K)" using A Mult by simp
- ultimately obtain k1 k2 where k1: "k1 \<in> generate G K" "norm H x1 = h k1"
- and k2: "k2 \<in> generate G K" "norm H x2 = h k2" by blast
- hence "norm H (Mult x1 x2) = h (k1 \<otimes> k2)"
+ have "Generated_Groups.norm H x1 \<in> h ` (generate G K)" using A Mult by simp
+ moreover have "Generated_Groups.norm H x2 \<in> h ` (generate G K)" using A Mult by simp
+ ultimately obtain k1 k2 where k1: "k1 \<in> generate G K" "Generated_Groups.norm H x1 = h k1"
+ and k2: "k2 \<in> generate G K" "Generated_Groups.norm H x2 = h k2" by blast
+ hence "Generated_Groups.norm H (Mult x1 x2) = h (k1 \<otimes> k2)"
using G.generate_in_carrier assms by auto
thus ?case using k1 k2 by (simp add: generate.eng)
qed
@@ -208,24 +208,24 @@
show "h ` generate G K \<subseteq> generate H (h ` K)"
proof
fix x assume "x \<in> h ` generate G K"
- then obtain r where r: "elts r \<subseteq> K" "x = h (norm G r)" using G.generate_repr_iff assms by auto
- from \<open>elts r \<subseteq> K\<close> have "h (norm G r) \<in> generate H (h ` K)"
+ then obtain r where r: "elts r \<subseteq> K" "x = h (Generated_Groups.norm G r)" using G.generate_repr_iff assms by auto
+ from \<open>elts r \<subseteq> K\<close> have "h (Generated_Groups.norm G r) \<in> generate H (h ` K)"
proof (induct r rule: repr.induct)
case One thus ?case by (simp add: generate.one)
next
case (Inv x) hence A: "x \<in> K" by simp
- hence "h (norm G (Inv x)) = inv\<^bsub>H\<^esub> (h x)" using assms by auto
+ hence "h (Generated_Groups.norm G (Inv x)) = inv\<^bsub>H\<^esub> (h x)" using assms by auto
moreover have "h x \<in> generate H (h ` K)" using A by (simp add: generate.incl)
ultimately show ?case by (simp add: A generate.inv)
next
case (Leaf x) thus ?case by (simp add: generate.incl)
next
case (Mult x1 x2) hence A: "elts x1 \<union> elts x2 \<subseteq> K" by simp
- have "norm G x1 \<in> carrier G"
+ have "Generated_Groups.norm G x1 \<in> carrier G"
by (meson A G.generateE(1) G.generate_repr_iff Un_subset_iff assms subgroup.mem_carrier)
- moreover have "norm G x2 \<in> carrier G"
+ moreover have "Generated_Groups.norm G x2 \<in> carrier G"
by (meson A G.generateE(1) G.generate_repr_iff Un_subset_iff assms subgroup.mem_carrier)
- ultimately have "h (norm G (Mult x1 x2)) = h (norm G x1) \<otimes>\<^bsub>H\<^esub> h (norm G x2)" by simp
+ ultimately have "h (Generated_Groups.norm G (Mult x1 x2)) = h (Generated_Groups.norm G x1) \<otimes>\<^bsub>H\<^esub> h (Generated_Groups.norm G x2)" by simp
thus ?case using Mult A by (simp add: generate.eng)
qed
thus "x \<in> generate H (h ` K)" using r by simp