src/HOL/Algebra/Group.thy

   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
   one     :: 'a ("\<one>\<index>")
 
 definition
   m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
-  where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
+  where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
 
 definition
   Units :: "_ => 'a set"
   \<comment>\<open>The set of invertible elements\<close>
-  where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
+  where "Units G = {y. y \<in> carrier G \<and> (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
 
 consts
   pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "'(^')\<index>" 75)
 
 overloading nat_pow == "pow :: [_, 'a, nat] => 'a"

     from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x"
       by (simp add: m_assoc [symmetric] l_inv)
     with x xG show "x \<otimes> \<one> = x" by simp
   qed
   have inv_ex:
-    "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
+    "\<And>x. x \<in> carrier G \<Longrightarrow> \<exists>y \<in> carrier G. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>"
   proof -
     fix x
     assume x: "x \<in> carrier G"
     with l_inv_ex obtain y where y: "y \<in> carrier G"
       and l_inv: "y \<otimes> x = \<one>" by fast
     from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>"
       by (simp add: m_assoc [symmetric] l_inv r_one)
     with x y have r_inv: "x \<otimes> y = \<one>"
       by simp
-    from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
+    from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>"
       by (fast intro: l_inv r_inv)
   qed
-  then have carrier_subset_Units: "carrier G <= Units G"
+  then have carrier_subset_Units: "carrier G \<subseteq> Units G"
     by (unfold Units_def) fast
   show ?thesis
     by standard (auto simp: r_one m_assoc carrier_subset_Units)
 qed
 

   by (rule groupI) (auto intro: m_assoc l_inv_ex)
 
 lemma (in group) Units_eq [simp]:
   "Units G = carrier G"
 proof
-  show "Units G <= carrier G" by fast
+  show "Units G \<subseteq> carrier G" by fast
 next
-  show "carrier G <= Units G" by (rule Units)
+  show "carrier G \<subseteq> Units G" by (rule Units)
 qed
 
 lemma (in group) inv_closed [intro, simp]:
   "x \<in> carrier G ==> inv x \<in> carrier G"
   using Units_inv_closed by simp

 
 declare monoid.one_closed [iff] group.inv_closed [simp]
   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
 
 lemma subgroup_nonempty:
-  "~ subgroup {} G"
+  "\<not> subgroup {} G"
   by (blast dest: subgroup.one_closed)
 
 lemma (in subgroup) finite_imp_card_positive:
   "finite (carrier G) ==> 0 < card H"
 proof (rule classical)
-  assume "finite (carrier G)" and a: "~ 0 < card H"
+  assume "finite (carrier G)" and a: "\<not> 0 < card H"
   then have "finite H" by (blast intro: finite_subset [OF subset])
   with is_subgroup a have "subgroup {} G" by simp
   with subgroup_nonempty show ?thesis by contradiction
 qed
 

 subsection \<open>Homomorphisms and Isomorphisms\<close>
 
 definition
   hom :: "_ => _ => ('a => 'b) set" where
   "hom G H =
-    {h. h \<in> carrier G \<rightarrow> carrier H &
+    {h. h \<in> carrier G \<rightarrow> carrier H \<and>
       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
 
 lemma (in group) hom_compose:
   "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
 by (fastforce simp add: hom_def compose_def)
 
 definition
   iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
-  where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
-
-lemma iso_refl: "(%x. x) \<in> G \<cong> G"
+  where "G \<cong> H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
+
+lemma iso_refl: "(\<lambda>x. x) \<in> G \<cong> G"
 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
 
 lemma (in group) iso_sym:
      "h \<in> G \<cong> H \<Longrightarrow> inv_into (carrier G) h \<in> H \<cong> G"
 apply (simp add: iso_def bij_betw_inv_into) 

 apply (rule subsetD [OF subgroup.subset], assumption)
 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
 done
 
 theorem (in group) subgroups_Inter:
-  assumes subgr: "(!!H. H \<in> A ==> subgroup H G)"
-    and not_empty: "A ~= {}"
+  assumes subgr: "(\<And>H. H \<in> A \<Longrightarrow> subgroup H G)"
+    and not_empty: "A \<noteq> {}"
   shows "subgroup (\<Inter>A) G"
 proof (rule subgroupI)
   from subgr [THEN subgroup.subset] and not_empty
   show "\<Inter>A \<subseteq> carrier G" by blast
 next
   from subgr [THEN subgroup.one_closed]
-  show "\<Inter>A ~= {}" by blast
+  show "\<Inter>A \<noteq> {}" by blast
 next
   fix x assume "x \<in> \<Inter>A"
   with subgr [THEN subgroup.m_inv_closed]
   show "inv x \<in> \<Inter>A" by blast
 next

   have "greatest ?L (carrier G) (carrier ?L)"
     by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
   then show "\<exists>G. greatest ?L G (carrier ?L)" ..
 next
   fix A
-  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
+  assume L: "A \<subseteq> carrier ?L" and non_empty: "A \<noteq> {}"
   then have Int_subgroup: "subgroup (\<Inter>A) G"
     by (fastforce intro: subgroups_Inter)
   have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
   proof (rule greatest_LowerI)
     fix H