--- 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
--- 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)"
--- 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