src/HOL/Algebra/More_Finite_Product.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66760 d44ea023ac09 child 67341 df79ef3b3a41 permissions -rw-r--r--
tuned: each session has at most one defining entry;
```     1 (*  Title:      HOL/Algebra/More_Finite_Product.thy
```
```     2     Author:     Jeremy Avigad
```
```     3 *)
```
```     4
```
```     5 section \<open>More on finite products\<close>
```
```     6
```
```     7 theory More_Finite_Product
```
```     8   imports More_Group
```
```     9 begin
```
```    10
```
```    11 lemma (in comm_monoid) finprod_UN_disjoint:
```
```    12   "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>
```
```    13     (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
```
```    14     finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
```
```    15   apply (induct set: finite)
```
```    16    apply force
```
```    17   apply clarsimp
```
```    18   apply (subst finprod_Un_disjoint)
```
```    19        apply blast
```
```    20       apply (erule finite_UN_I)
```
```    21       apply blast
```
```    22      apply (fastforce)
```
```    23     apply (auto intro!: funcsetI finprod_closed)
```
```    24   done
```
```    25
```
```    26 lemma (in comm_monoid) finprod_Union_disjoint:
```
```    27   "finite C \<Longrightarrow>
```
```    28     \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
```
```    29     \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
```
```    30     finprod G f (\<Union>C) = finprod G (finprod G f) C"
```
```    31   apply (frule finprod_UN_disjoint [of C id f])
```
```    32   apply auto
```
```    33   done
```
```    34
```
```    35 lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
```
```    36   by (induct set: finite) auto
```
```    37
```
```    38
```
```    39 (* need better simplification rules for rings *)
```
```    40 (* the next one holds more generally for abelian groups *)
```
```    41
```
```    42 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"
```
```    43   by (metis minus_equality)
```
```    44
```
```    45 lemma (in domain) square_eq_one:
```
```    46   fixes x
```
```    47   assumes [simp]: "x \<in> carrier R"
```
```    48     and "x \<otimes> x = \<one>"
```
```    49   shows "x = \<one> \<or> x = \<ominus>\<one>"
```
```    50 proof -
```
```    51   have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
```
```    52     by (simp add: ring_simprules)
```
```    53   also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
```
```    54     by (simp add: ring_simprules)
```
```    55   finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
```
```    56   then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
```
```    57     by (intro integral) auto
```
```    58   then show ?thesis
```
```    59     apply auto
```
```    60      apply (erule notE)
```
```    61      apply (rule sum_zero_eq_neg)
```
```    62        apply auto
```
```    63     apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
```
```    64      apply (simp add: ring_simprules)
```
```    65     apply (rule sum_zero_eq_neg)
```
```    66       apply auto
```
```    67     done
```
```    68 qed
```
```    69
```
```    70 lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
```
```    71   by (metis Units_closed Units_l_inv square_eq_one)
```
```    72
```
```    73
```
```    74 text \<open>
```
```    75   The following translates theorems about groups to the facts about
```
```    76   the units of a ring. (The list should be expanded as more things are
```
```    77   needed.)
```
```    78 \<close>
```
```    79
```
```    80 lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
```
```    81   by (rule finite_subset) auto
```
```    82
```
```    83 lemma (in monoid) units_of_pow:
```
```    84   fixes n :: nat
```
```    85   shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
```
```    86   apply (induct n)
```
```    87   apply (auto simp add: units_group group.is_monoid
```
```    88     monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
```
```    89   done
```
```    90
```
```    91 lemma (in cring) units_power_order_eq_one:
```
```    92   "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a (^) card(Units R) = \<one>"
```
```    93   apply (subst units_of_carrier [symmetric])
```
```    94   apply (subst units_of_one [symmetric])
```
```    95   apply (subst units_of_pow [symmetric])
```
```    96    apply assumption
```
```    97   apply (rule comm_group.power_order_eq_one)
```
```    98     apply (rule units_comm_group)
```
```    99    apply (unfold units_of_def, auto)
```
```   100   done
```
```   101
```
```   102 end
```