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.71      by (simp add: ring_simprules)
    1.72    also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
    1.73      by (simp add: ring_simprules)
    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