# HG changeset patch
# User wenzelm
# Date 1506977281 -7200
# Node ID d44ea023ac09efb09ea6dacf3735f2076e44ed18
# Parent  918f15c9367a2a1ed20c80e5791643ee9b017d05
misc tuning and modernization;

diff -r 918f15c9367a -r d44ea023ac09 src/HOL/Algebra/More_Finite_Product.thy
--- a/src/HOL/Algebra/More_Finite_Product.thy	Mon Oct 02 19:58:29 2017 +0200
+++ b/src/HOL/Algebra/More_Finite_Product.thy	Mon Oct 02 22:48:01 2017 +0200
@@ -5,71 +5,69 @@
 section \<open>More on finite products\<close>
 
 theory More_Finite_Product
-imports
-  More_Group
+  imports More_Group
 begin
 
 lemma (in comm_monoid) finprod_UN_disjoint:
-  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
-     (A i) Int (A j) = {}) \<longrightarrow>
-      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
-        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
+  "finite I \<Longrightarrow> (\<forall>i\<in>I. finite (A i)) \<longrightarrow> (\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}) \<longrightarrow>
+    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
+    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
   apply (induct set: finite)
-  apply force
+   apply force
   apply clarsimp
   apply (subst finprod_Un_disjoint)
-  apply blast
-  apply (erule finite_UN_I)
-  apply blast
-  apply (fastforce)
-  apply (auto intro!: funcsetI finprod_closed)
+       apply blast
+      apply (erule finite_UN_I)
+      apply blast
+     apply (fastforce)
+    apply (auto intro!: funcsetI finprod_closed)
   done
 
 lemma (in comm_monoid) finprod_Union_disjoint:
-  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
-      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
-   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
+  "finite C \<Longrightarrow>
+    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
+    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
+    finprod G f (\<Union>C) = finprod G (finprod G f) C"
   apply (frule finprod_UN_disjoint [of C id f])
   apply auto
   done
 
-lemma (in comm_monoid) finprod_one:
-    "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
+lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
   by (induct set: finite) auto
 
 
 (* need better simplification rules for rings *)
 (* the next one holds more generally for abelian groups *)
 
-lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
+lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   by (metis minus_equality)
 
 lemma (in domain) square_eq_one:
   fixes x
-  assumes [simp]: "x : carrier R"
+  assumes [simp]: "x \<in> carrier R"
     and "x \<otimes> x = \<one>"
-  shows "x = \<one> | x = \<ominus>\<one>"
+  shows "x = \<one> \<or> x = \<ominus>\<one>"
 proof -
   have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
     by (simp add: ring_simprules)
   also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
     by (simp add: ring_simprules)
   finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
-  then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
-    by (intro integral, auto)
+  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
+    by (intro integral) auto
   then show ?thesis
     apply auto
-    apply (erule notE)
-    apply (rule sum_zero_eq_neg)
-    apply auto
+     apply (erule notE)
+     apply (rule sum_zero_eq_neg)
+       apply auto
     apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
-    apply (simp add: ring_simprules)
+     apply (simp add: ring_simprules)
     apply (rule sum_zero_eq_neg)
-    apply auto
+      apply auto
     done
 qed
 
-lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
+lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
   by (metis Units_closed Units_l_inv square_eq_one)
 
 
@@ -90,15 +88,15 @@
     monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
   done
 
-lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
-    \<Longrightarrow> a (^) card(Units R) = \<one>"
+lemma (in cring) units_power_order_eq_one:
+  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a (^) card(Units R) = \<one>"
   apply (subst units_of_carrier [symmetric])
   apply (subst units_of_one [symmetric])
   apply (subst units_of_pow [symmetric])
-  apply assumption
+   apply assumption
   apply (rule comm_group.power_order_eq_one)
-  apply (rule units_comm_group)
-  apply (unfold units_of_def, auto)
+    apply (rule units_comm_group)
+   apply (unfold units_of_def, auto)
   done
 
-end
\ No newline at end of file
+end
diff -r 918f15c9367a -r d44ea023ac09 src/HOL/Algebra/More_Group.thy
--- a/src/HOL/Algebra/More_Group.thy	Mon Oct 02 19:58:29 2017 +0200
+++ b/src/HOL/Algebra/More_Group.thy	Mon Oct 02 22:48:01 2017 +0200
@@ -5,8 +5,7 @@
 section \<open>More on groups\<close>
 
 theory More_Group
-imports
-  Ring
+  imports Ring
 begin
 
 text \<open>
@@ -16,63 +15,62 @@
   facts about the unit group within the ring locale.
 \<close>
 
-definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
-  "units_of G == (| carrier = Units G,
-     Group.monoid.mult = Group.monoid.mult G,
-     one  = one G |)"
+definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
+  where "units_of G =
+    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
 
-lemma (in monoid) units_group: "group(units_of G)"
+lemma (in monoid) units_group: "group (units_of G)"
   apply (unfold units_of_def)
   apply (rule groupI)
-  apply auto
-  apply (subst m_assoc)
-  apply auto
+      apply auto
+   apply (subst m_assoc)
+      apply auto
   apply (rule_tac x = "inv x" in bexI)
-  apply auto
+   apply auto
   done
 
-lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
+lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
   apply (rule group.group_comm_groupI)
-  apply (rule units_group)
+   apply (rule units_group)
   apply (insert comm_monoid_axioms)
   apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
   apply auto
   done
 
 lemma units_of_carrier: "carrier (units_of G) = Units G"
-  unfolding units_of_def by auto
+  by (auto simp: units_of_def)
 
-lemma units_of_mult: "mult(units_of G) = mult G"
-  unfolding units_of_def by auto
+lemma units_of_mult: "mult (units_of G) = mult G"
+  by (auto simp: units_of_def)
 
-lemma units_of_one: "one(units_of G) = one G"
-  unfolding units_of_def by auto
+lemma units_of_one: "one (units_of G) = one G"
+  by (auto simp: units_of_def)
 
-lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
+lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
   apply (rule sym)
   apply (subst m_inv_def)
   apply (rule the1_equality)
-  apply (rule ex_ex1I)
-  apply (subst (asm) Units_def)
-  apply auto
-  apply (erule inv_unique)
-  apply auto
-  apply (rule Units_closed)
-  apply (simp_all only: units_of_carrier [symmetric])
-  apply (insert units_group)
-  apply auto
-  apply (subst units_of_mult [symmetric])
-  apply (subst units_of_one [symmetric])
-  apply (erule group.r_inv, assumption)
+   apply (rule ex_ex1I)
+    apply (subst (asm) Units_def)
+    apply auto
+     apply (erule inv_unique)
+        apply auto
+    apply (rule Units_closed)
+    apply (simp_all only: units_of_carrier [symmetric])
+    apply (insert units_group)
+    apply auto
+   apply (subst units_of_mult [symmetric])
+   apply (subst units_of_one [symmetric])
+   apply (erule group.r_inv, assumption)
   apply (subst units_of_mult [symmetric])
   apply (subst units_of_one [symmetric])
   apply (erule group.l_inv, assumption)
   done
 
-lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
+lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
   unfolding inj_on_def by auto
 
-lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
+lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
   apply (auto simp add: image_def)
   apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   apply auto
@@ -82,33 +80,29 @@
   apply auto
   done
 
-lemma (in group) l_cancel_one [simp]:
-    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
+lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
   apply auto
   apply (subst l_cancel [symmetric])
-  prefer 4
-  apply (erule ssubst)
-  apply auto
+     prefer 4
+     apply (erule ssubst)
+     apply auto
   done
 
-lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
-    (a \<otimes> x = x) = (a = one G)"
+lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
   apply auto
   apply (subst r_cancel [symmetric])
-  prefer 4
-  apply (erule ssubst)
-  apply auto
+     prefer 4
+     apply (erule ssubst)
+     apply auto
   done
 
 (* Is there a better way to do this? *)
-lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
-    (x = x \<otimes> a) = (a = one G)"
+lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
   apply (subst eq_commute)
   apply simp
   done
 
-lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
-    (x = a \<otimes> x) = (a = one G)"
+lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
   apply (subst eq_commute)
   apply simp
   done
@@ -118,7 +112,7 @@
 
 lemma (in comm_group) power_order_eq_one:
   assumes fin [simp]: "finite (carrier G)"
-    and a [simp]: "a : carrier G"
+    and a [simp]: "a \<in> carrier G"
   shows "a (^) card(carrier G) = one G"
 proof -
   have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
diff -r 918f15c9367a -r d44ea023ac09 src/HOL/Algebra/More_Ring.thy
--- a/src/HOL/Algebra/More_Ring.thy	Mon Oct 02 19:58:29 2017 +0200
+++ b/src/HOL/Algebra/More_Ring.thy	Mon Oct 02 22:48:01 2017 +0200
@@ -5,73 +5,70 @@
 section \<open>More on rings etc.\<close>
 
 theory More_Ring
-imports
-  Ring
+  imports Ring
 begin
 
-lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
+lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
   apply (unfold_locales)
-  apply (insert cring_axioms, auto)
-  apply (rule trans)
-  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
-  apply assumption
-  apply (subst m_assoc)
-  apply auto
+    apply (use cring_axioms in auto)
+   apply (rule trans)
+    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
+     apply assumption
+    apply (subst m_assoc)
+       apply auto
   apply (unfold Units_def)
   apply auto
   done
 
-lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
-    x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
-  apply (subgoal_tac "x : Units G")
-  apply (subgoal_tac "y = inv x \<otimes> \<one>")
-  apply simp
-  apply (erule subst)
-  apply (subst m_assoc [symmetric])
-  apply auto
+lemma (in monoid) inv_char:
+  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
+  apply (subgoal_tac "x \<in> Units G")
+   apply (subgoal_tac "y = inv x \<otimes> \<one>")
+    apply simp
+   apply (erule subst)
+   apply (subst m_assoc [symmetric])
+      apply auto
   apply (unfold Units_def)
   apply auto
   done
 
-lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
-  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
+lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
   apply (rule inv_char)
-  apply auto
+     apply auto
   apply (subst m_comm, auto)
   done
 
 lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
   apply (rule inv_char)
-  apply (auto simp add: l_minus r_minus)
+     apply (auto simp add: l_minus r_minus)
   done
 
-lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
-    inv x = inv y \<Longrightarrow> x = y"
-  apply (subgoal_tac "inv(inv x) = inv(inv y)")
-  apply (subst (asm) Units_inv_inv)+
-  apply auto
+lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
+  apply (subgoal_tac "inv (inv x) = inv (inv y)")
+   apply (subst (asm) Units_inv_inv)+
+    apply auto
   done
 
-lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
+lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
   apply (unfold Units_def)
   apply auto
   apply (rule_tac x = "\<ominus> \<one>" in bexI)
-  apply auto
+   apply auto
   apply (simp add: l_minus r_minus)
   done
 
 lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
   apply (rule inv_char)
-  apply auto
+     apply auto
   done
 
-lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
+lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
   apply auto
   apply (subst Units_inv_inv [symmetric])
-  apply auto
+   apply auto
   done
 
-lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
+lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
   by (metis Units_inv_inv inv_one)
 
 end