src/HOL/Algebra/More_Finite_Product.thy
 changeset 66760 d44ea023ac09 parent 65416 f707dbcf11e3 child 67341 df79ef3b3a41
```     1.1 --- a/src/HOL/Algebra/More_Finite_Product.thy	Mon Oct 02 19:58:29 2017 +0200
1.2 +++ b/src/HOL/Algebra/More_Finite_Product.thy	Mon Oct 02 22:48:01 2017 +0200
1.3 @@ -5,71 +5,69 @@
1.4  section \<open>More on finite products\<close>
1.5
1.6  theory More_Finite_Product
1.7 -imports
1.8 -  More_Group
1.9 +  imports More_Group
1.10  begin
1.11
1.12  lemma (in comm_monoid) finprod_UN_disjoint:
1.13 -  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
1.14 -     (A i) Int (A j) = {}) \<longrightarrow>
1.15 -      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
1.16 -        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
1.17 +  "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.18 +    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
1.19 +    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
1.20    apply (induct set: finite)
1.21 -  apply force
1.22 +   apply force
1.23    apply clarsimp
1.24    apply (subst finprod_Un_disjoint)
1.25 -  apply blast
1.26 -  apply (erule finite_UN_I)
1.27 -  apply blast
1.28 -  apply (fastforce)
1.29 -  apply (auto intro!: funcsetI finprod_closed)
1.30 +       apply blast
1.31 +      apply (erule finite_UN_I)
1.32 +      apply blast
1.33 +     apply (fastforce)
1.34 +    apply (auto intro!: funcsetI finprod_closed)
1.35    done
1.36
1.37  lemma (in comm_monoid) finprod_Union_disjoint:
1.38 -  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
1.39 -      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
1.40 -   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
1.41 +  "finite C \<Longrightarrow>
1.42 +    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
1.43 +    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
1.44 +    finprod G f (\<Union>C) = finprod G (finprod G f) C"
1.45    apply (frule finprod_UN_disjoint [of C id f])
1.46    apply auto
1.47    done
1.48
1.49 -lemma (in comm_monoid) finprod_one:
1.50 -    "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
1.51 +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.52    by (induct set: finite) auto
1.53
1.54
1.55  (* need better simplification rules for rings *)
1.56  (* the next one holds more generally for abelian groups *)
1.57
1.58 -lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
1.59 +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.60    by (metis minus_equality)
1.61
1.62  lemma (in domain) square_eq_one:
1.63    fixes x
1.64 -  assumes [simp]: "x : carrier R"
1.65 +  assumes [simp]: "x \<in> carrier R"
1.66      and "x \<otimes> x = \<one>"
1.67 -  shows "x = \<one> | x = \<ominus>\<one>"
1.68 +  shows "x = \<one> \<or> x = \<ominus>\<one>"
1.69  proof -
1.70    have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
1.72    also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
1.74    finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
1.75 -  then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
1.76 -    by (intro integral, auto)
1.77 +  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
1.78 +    by (intro integral) auto
1.79    then show ?thesis
1.80      apply auto
1.81 -    apply (erule notE)
1.82 -    apply (rule sum_zero_eq_neg)
1.83 -    apply auto
1.84 +     apply (erule notE)
1.85 +     apply (rule sum_zero_eq_neg)
1.86 +       apply auto
1.87      apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
1.88 -    apply (simp add: ring_simprules)
1.89 +     apply (simp add: ring_simprules)
1.90      apply (rule sum_zero_eq_neg)
1.91 -    apply auto
1.92 +      apply auto
1.93      done
1.94  qed
1.95
1.96 -lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
1.97 +lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
1.98    by (metis Units_closed Units_l_inv square_eq_one)
1.99
1.100
1.101 @@ -90,15 +88,15 @@
1.102      monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
1.103    done
1.104
1.105 -lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
1.106 -    \<Longrightarrow> a (^) card(Units R) = \<one>"
1.107 +lemma (in cring) units_power_order_eq_one:
1.108 +  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a (^) card(Units R) = \<one>"
1.109    apply (subst units_of_carrier [symmetric])
1.110    apply (subst units_of_one [symmetric])
1.111    apply (subst units_of_pow [symmetric])
1.112 -  apply assumption
1.113 +   apply assumption
1.114    apply (rule comm_group.power_order_eq_one)
1.115 -  apply (rule units_comm_group)
1.116 -  apply (unfold units_of_def, auto)
1.117 +    apply (rule units_comm_group)
1.118 +   apply (unfold units_of_def, auto)
1.119    done
1.120
1.121 -end
1.122 \ No newline at end of file
1.123 +end
```