Theory MiscAlgebra

theory MiscAlgebra
imports Ring
(*  Title:      HOL/Number_Theory/MiscAlgebra.thy
Author: Jeremy Avigad

These are things that can be added to the Algebra library.
*)


theory MiscAlgebra
imports
"~~/src/HOL/Algebra/Ring"
"~~/src/HOL/Algebra/FiniteProduct"
begin

(* finiteness stuff *)

lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
apply (erule finite_subset)
apply auto
done


(* The rest is for the algebra libraries *)

(* These go in Group.thy. *)

(*
Show that the units in any monoid give rise to a group.

The file Residues.thy provides some infrastructure to use
facts about the unit group within the ring locale.
*)



definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
"units_of G == (| carrier = Units G,
Group.monoid.mult = Group.monoid.mult G,
one = one G |)"


(*

lemma (in monoid) Units_mult_closed [intro]:
"x : Units G ==> y : Units G ==> x ⊗ y : Units G"
apply (unfold Units_def)
apply (clarsimp)
apply (rule_tac x = "xaa ⊗ xa" in bexI)
apply auto
apply (subst m_assoc)
apply auto
apply (subst (2) m_assoc [symmetric])
apply auto
apply (subst m_assoc)
apply auto
apply (subst (2) m_assoc [symmetric])
apply auto
done

*)


lemma (in monoid) units_group: "group(units_of G)"
apply (unfold units_of_def)
apply (rule groupI)
apply auto
apply (subst m_assoc)
apply auto
apply (rule_tac x = "inv x" in bexI)
apply auto
done

lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
apply (rule group.group_comm_groupI)
apply (rule units_group)
apply (insert comm_monoid_axioms)
apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
apply auto
done

lemma units_of_carrier: "carrier (units_of G) = Units G"
unfolding units_of_def by auto

lemma units_of_mult: "mult(units_of G) = mult G"
unfolding units_of_def by auto

lemma units_of_one: "one(units_of G) = one G"
unfolding units_of_def by auto

lemma (in monoid) units_of_inv: "x : Units G ==>
m_inv (units_of G) x = m_inv G x"

apply (rule sym)
apply (subst m_inv_def)
apply (rule the1_equality)
apply (rule ex_ex1I)
apply (subst (asm) Units_def)
apply auto
apply (erule inv_unique)
apply auto
apply (rule Units_closed)
apply (simp_all only: units_of_carrier [symmetric])
apply (insert units_group)
apply auto
apply (subst units_of_mult [symmetric])
apply (subst units_of_one [symmetric])
apply (erule group.r_inv, assumption)
apply (subst units_of_mult [symmetric])
apply (subst units_of_one [symmetric])
apply (erule group.l_inv, assumption)
done

lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
inj_on (%x. a ⊗ x) (carrier G)"

unfolding inj_on_def by auto

lemma (in group) surj_const_mult: "a : (carrier G) ==>
(%x. a ⊗ x) ` (carrier G) = (carrier G)"

apply (auto simp add: image_def)
apply (rule_tac x = "(m_inv G a) ⊗ x" in bexI)
apply auto
(* auto should get this. I suppose we need "comm_monoid_simprules"
for mult_ac rewriting. *)

apply (subst m_assoc [symmetric])
apply auto
done

lemma (in group) l_cancel_one [simp]: "x : carrier G ==> a : carrier G ==>
(x ⊗ a = x) = (a = one G)"

apply auto
apply (subst l_cancel [symmetric])
prefer 4
apply (erule ssubst)
apply auto
done

lemma (in group) r_cancel_one [simp]: "x : carrier G ==> a : carrier G ==>
(a ⊗ x = x) = (a = one G)"

apply auto
apply (subst r_cancel [symmetric])
prefer 4
apply (erule ssubst)
apply auto
done

(* Is there a better way to do this? *)

lemma (in group) l_cancel_one' [simp]: "x : carrier G ==> a : carrier G ==>
(x = x ⊗ a) = (a = one G)"

apply (subst eq_commute)
apply simp
done

lemma (in group) r_cancel_one' [simp]: "x : carrier G ==> a : carrier G ==>
(x = a ⊗ x) = (a = one G)"

apply (subst eq_commute)
apply simp
done

(* This should be generalized to arbitrary groups, not just commutative
ones, using Lagrange's theorem. *)


lemma (in comm_group) power_order_eq_one:
assumes fin [simp]: "finite (carrier G)"
and a [simp]: "a : carrier G"
shows "a (^) card(carrier G) = one G"
proof -
have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a ⊗ x)"
by (subst (2) finprod_reindex [symmetric],
auto simp add: Pi_def inj_on_const_mult surj_const_mult)
also have "… = (\<Otimes>x:carrier G. a) ⊗ (\<Otimes>x:carrier G. x)"
by (auto simp add: finprod_multf Pi_def)
also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
by (auto simp add: finprod_const)
finally show ?thesis
(* uses the preceeding lemma *)
by auto
qed


(* Miscellaneous *)

lemma (in cring) field_intro2: "\<zero>R ~= \<one>R ==> ALL x : carrier R - {\<zero>R}.
x : Units R ==> field R"

apply (unfold_locales)
apply (insert cring_axioms, auto)
apply (rule trans)
apply (subgoal_tac "a = (a ⊗ b) ⊗ inv b")
apply assumption
apply (subst m_assoc)
apply auto
apply (unfold Units_def)
apply auto
done

lemma (in monoid) inv_char: "x : carrier G ==> y : carrier G ==>
x ⊗ y = \<one> ==> y ⊗ x = \<one> ==> inv x = y"

apply (subgoal_tac "x : Units G")
apply (subgoal_tac "y = inv x ⊗ \<one>")
apply simp
apply (erule subst)
apply (subst m_assoc [symmetric])
apply auto
apply (unfold Units_def)
apply auto
done

lemma (in comm_monoid) comm_inv_char: "x : carrier G ==> y : carrier G ==>
x ⊗ y = \<one> ==> inv x = y"

apply (rule inv_char)
apply auto
apply (subst m_comm, auto)
done

lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
apply (rule inv_char)
apply (auto simp add: l_minus r_minus)
done

lemma (in monoid) inv_eq_imp_eq: "x : Units G ==> y : Units G ==>
inv x = inv y ==> x = y"

apply (subgoal_tac "inv(inv x) = inv(inv y)")
apply (subst (asm) Units_inv_inv)+
apply auto
done

lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
apply (unfold Units_def)
apply auto
apply (rule_tac x = "\<ominus> \<one>" in bexI)
apply auto
apply (simp add: l_minus r_minus)
done

lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
apply (rule inv_char)
apply auto
done

lemma (in ring) inv_eq_neg_one_eq: "x : Units R ==> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
apply auto
apply (subst Units_inv_inv [symmetric])
apply auto
done

lemma (in monoid) inv_eq_one_eq: "x : Units G ==> (inv x = \<one>) = (x = \<one>)"
apply auto
apply (subst Units_inv_inv [symmetric])
apply auto
done


(* This goes in FiniteProduct *)

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 (Union C) = finprod G (finprod G f) C"

apply (frule finprod_UN_disjoint [of C id f])
apply (auto simp add: SUP_def)
done

lemma (in comm_monoid) finprod_one:
"finite A ==> (!!x. x:A ==> f x = \<one>) ==> finprod G f A = \<one>"
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 = \<zero> ==> x = \<ominus> y"
apply (subgoal_tac "\<ominus> y = \<zero> ⊕ \<ominus> y")
apply (erule ssubst)back
apply (erule subst)
apply (simp_all add: ring_simprules)
done

(* there's a name conflict -- maybe "domain" should be
"integral_domain" *)


lemma (in Ring.domain) square_eq_one:
fixes x
assumes [simp]: "x : carrier R" and
"x ⊗ x = \<one>"
shows "x = \<one> | x = \<ominus>\<one>"
proof -
have "(x ⊕ \<one>) ⊗ (x ⊕ \<ominus> \<one>) = x ⊗ x ⊕ \<ominus> \<one>"
by (simp add: ring_simprules)
also from `x ⊗ x = \<one>` have "… = \<zero>"
by (simp add: ring_simprules)
finally have "(x ⊕ \<one>) ⊗ (x ⊕ \<ominus> \<one>) = \<zero>" .
then have "(x ⊕ \<one>) = \<zero> | (x ⊕ \<ominus> \<one>) = \<zero>"
by (intro integral, auto)
then show ?thesis
apply auto
apply (erule notE)
apply (rule sum_zero_eq_neg)
apply auto
apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
apply (simp add: ring_simprules)
apply (rule sum_zero_eq_neg)
apply auto
done
qed

lemma (in Ring.domain) inv_eq_self: "x : Units R ==>
x = inv x ==> x = \<one> | x = \<ominus> \<one>"

apply (rule square_eq_one)
apply auto
apply (erule ssubst)back
apply (erule Units_r_inv)
done


(*
The following translates theorems about groups to the facts about
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

(* this belongs with MiscAlgebra.thy *)
lemma (in monoid) units_of_pow:
"x : Units G ==> x (^)units_of G (n::nat) = 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) = \<one>"

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