# Theory More_Finite_Product

theory More_Finite_Product
imports More_Group
```(*  Title:      HOL/Algebra/More_Finite_Product.thy
*)

section ‹More on finite products›

theory More_Finite_Product
imports
More_Group
begin

lemma (in comm_monoid) finprod_UN_disjoint:
"finite I ⟹ (ALL i:I. finite (A i)) ⟶ (ALL i:I. ALL j:I. i ~= j ⟶
(A i) Int (A j) = {}) ⟶
(ALL i:I. ALL x: (A i). g x : carrier G) ⟶
finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
apply (induct set: finite)
apply force
apply clarsimp
apply (subst finprod_Un_disjoint)
apply blast
apply (erule finite_UN_I)
apply blast
apply (fastforce)
apply (auto intro!: funcsetI finprod_closed)
done

lemma (in comm_monoid) finprod_Union_disjoint:
"[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
(ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
==> finprod G f (⋃C) = finprod G (finprod G f) C"
apply (frule finprod_UN_disjoint [of C id f])
apply auto
done

lemma (in comm_monoid) finprod_one:
"finite A ⟹ (⋀x. x:A ⟹ f x = 𝟭) ⟹ finprod G f A = 𝟭"
by (induct set: finite) auto

(* need better simplification rules for rings *)
(* the next one holds more generally for abelian groups *)

lemma (in cring) sum_zero_eq_neg: "x : carrier R ⟹ y : carrier R ⟹ x ⊕ y = 𝟬 ⟹ x = ⊖ y"
by (metis minus_equality)

lemma (in domain) square_eq_one:
fixes x
assumes [simp]: "x : carrier R"
and "x ⊗ x = 𝟭"
shows "x = 𝟭 | x = ⊖𝟭"
proof -
have "(x ⊕ 𝟭) ⊗ (x ⊕ ⊖ 𝟭) = x ⊗ x ⊕ ⊖ 𝟭"
also from ‹x ⊗ x = 𝟭› have "… = 𝟬"
finally have "(x ⊕ 𝟭) ⊗ (x ⊕ ⊖ 𝟭) = 𝟬" .
then have "(x ⊕ 𝟭) = 𝟬 | (x ⊕ ⊖ 𝟭) = 𝟬"
by (intro integral, auto)
then show ?thesis
apply auto
apply (erule notE)
apply (rule sum_zero_eq_neg)
apply auto
apply (subgoal_tac "x = ⊖ (⊖ 𝟭)")
apply (rule sum_zero_eq_neg)
apply auto
done
qed

lemma (in Ring.domain) inv_eq_self: "x : Units R ⟹ x = inv x ⟹ x = 𝟭 ∨ x = ⊖𝟭"
by (metis Units_closed Units_l_inv square_eq_one)

text ‹
the units of a ring. (The list should be expanded as more things are
needed.)
›

lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) ⟹ finite (Units R)"
by (rule finite_subset) auto

lemma (in monoid) units_of_pow:
fixes n :: nat
shows "x ∈ Units G ⟹ x (^)⇘units_of G⇙ n = x (^)⇘G⇙ n"
apply (induct n)
apply (auto simp add: units_group group.is_monoid
monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
done

lemma (in cring) units_power_order_eq_one: "finite (Units R) ⟹ a : Units R
⟹ a (^) card(Units R) = 𝟭"
apply (subst units_of_carrier [symmetric])
apply (subst units_of_one [symmetric])
apply (subst units_of_pow [symmetric])
apply assumption
apply (rule comm_group.power_order_eq_one)
apply (rule units_comm_group)
apply (unfold units_of_def, auto)
done

end```