src/HOL/Algebra/More_Finite_Product.thy
changeset 68448 3d1517f3ba49
parent 68442 477b3f7067c9
parent 68447 0beb927eed89
child 68449 6d0f1a5a16ea
     1.1 --- a/src/HOL/Algebra/More_Finite_Product.thy	Thu Jun 14 15:45:53 2018 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,102 +0,0 @@
     1.4 -(*  Title:      HOL/Algebra/More_Finite_Product.thy
     1.5 -    Author:     Jeremy Avigad
     1.6 -*)
     1.7 -
     1.8 -section \<open>More on finite products\<close>
     1.9 -
    1.10 -theory More_Finite_Product
    1.11 -  imports More_Group
    1.12 -begin
    1.13 -
    1.14 -lemma (in comm_monoid) finprod_UN_disjoint:
    1.15 -  "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>
    1.16 -    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
    1.17 -    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
    1.18 -  apply (induct set: finite)
    1.19 -   apply force
    1.20 -  apply clarsimp
    1.21 -  apply (subst finprod_Un_disjoint)
    1.22 -       apply blast
    1.23 -      apply (erule finite_UN_I)
    1.24 -      apply blast
    1.25 -     apply (fastforce)
    1.26 -    apply (auto intro!: funcsetI finprod_closed)
    1.27 -  done
    1.28 -
    1.29 -lemma (in comm_monoid) finprod_Union_disjoint:
    1.30 -  "finite C \<Longrightarrow>
    1.31 -    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
    1.32 -    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
    1.33 -    finprod G f (\<Union>C) = finprod G (finprod G f) C"
    1.34 -  apply (frule finprod_UN_disjoint [of C id f])
    1.35 -  apply auto
    1.36 -  done
    1.37 -
    1.38 -lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
    1.39 -  by (induct set: finite) auto
    1.40 -
    1.41 -
    1.42 -(* need better simplification rules for rings *)
    1.43 -(* the next one holds more generally for abelian groups *)
    1.44 -
    1.45 -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"
    1.46 -  by (metis minus_equality)
    1.47 -
    1.48 -lemma (in domain) square_eq_one:
    1.49 -  fixes x
    1.50 -  assumes [simp]: "x \<in> carrier R"
    1.51 -    and "x \<otimes> x = \<one>"
    1.52 -  shows "x = \<one> \<or> x = \<ominus>\<one>"
    1.53 -proof -
    1.54 -  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
    1.55 -    by (simp add: ring_simprules)
    1.56 -  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
    1.57 -    by (simp add: ring_simprules)
    1.58 -  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
    1.59 -  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
    1.60 -    by (intro integral) auto
    1.61 -  then show ?thesis
    1.62 -    apply auto
    1.63 -     apply (erule notE)
    1.64 -     apply (rule sum_zero_eq_neg)
    1.65 -       apply auto
    1.66 -    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
    1.67 -     apply (simp add: ring_simprules)
    1.68 -    apply (rule sum_zero_eq_neg)
    1.69 -      apply auto
    1.70 -    done
    1.71 -qed
    1.72 -
    1.73 -lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
    1.74 -  by (metis Units_closed Units_l_inv square_eq_one)
    1.75 -
    1.76 -
    1.77 -text \<open>
    1.78 -  The following translates theorems about groups to the facts about
    1.79 -  the units of a ring. (The list should be expanded as more things are
    1.80 -  needed.)
    1.81 -\<close>
    1.82 -
    1.83 -lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
    1.84 -  by (rule finite_subset) auto
    1.85 -
    1.86 -lemma (in monoid) units_of_pow:
    1.87 -  fixes n :: nat
    1.88 -  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
    1.89 -  apply (induct n)
    1.90 -  apply (auto simp add: units_group group.is_monoid
    1.91 -    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
    1.92 -  done
    1.93 -
    1.94 -lemma (in cring) units_power_order_eq_one:
    1.95 -  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
    1.96 -  apply (subst units_of_carrier [symmetric])
    1.97 -  apply (subst units_of_one [symmetric])
    1.98 -  apply (subst units_of_pow [symmetric])
    1.99 -   apply assumption
   1.100 -  apply (rule comm_group.power_order_eq_one)
   1.101 -    apply (rule units_comm_group)
   1.102 -   apply (unfold units_of_def, auto)
   1.103 -  done
   1.104 -
   1.105 -end