author wenzelm Wed, 10 Oct 2012 15:27:10 +0200 changeset 49755 b286e8f47560 parent 49754 acafcac41690 child 49756 28e37eab4e6f
avoid duplicate facts;
 src/ZF/ex/Group.thy file | annotate | diff | comparison | revisions
--- a/src/ZF/ex/Group.thy	Wed Oct 10 15:21:26 2012 +0200
+++ b/src/ZF/ex/Group.thy	Wed Oct 10 15:27:10 2012 +0200
@@ -203,11 +203,11 @@
qed

lemma (in group) inv_comm:
-  assumes inv: "x \<cdot> y = \<one>"
+  assumes "x \<cdot> y = \<one>"
and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
shows "y \<cdot> x = \<one>"
proof -
-  from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
+  from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: assms)
with G show ?thesis by (simp del: r_one add: m_assoc)
qed

@@ -490,11 +490,12 @@

lemma (in group) subgroupI:
assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
-    and inv: "!!a. a \<in> H ==> inv a \<in> H"
-    and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
+    and "!!a. a \<in> H ==> inv a \<in> H"
+    and "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
shows "subgroup(H,G)"
-  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
+  show "\<one> \<in> H"
+    by (rule one_in_subset) (auto simp only: assms)
qed

@@ -595,7 +596,7 @@
"set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"

-locale normal = subgroup + group +
+locale normal = subgroup: subgroup + group +
assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"

notation