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