# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530564310 -3600
# Node ID b6cc5c265b045411bd5a544dc43bda5121e85344
# Parent  d40d03487f648d9aeb7e3c055d835ebc4a20dab0
Hiding the constant "norm", lest it clash with the norm of a vector space

diff -r d40d03487f64 -r b6cc5c265b04 src/HOL/Algebra/Generated_Groups.thy
--- 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
diff -r d40d03487f64 -r b6cc5c265b04 src/HOL/Algebra/Solvable_Groups.thy
--- 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