Theory MiscAlgebra

(*  Title:      HOL/Number_Theory/MiscAlgebra.thy
    Author:     Jeremy Avigad
*)

section ‹Things that can be added to the Algebra library›

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

subsection ‹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


subsection ‹The rest is for the algebra libraries›

subsubsection ‹These go in Group.thy›

text ‹
  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 ac_simps 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 "(⨂x∈carrier G. x) = (⨂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 "… = (⨂x∈carrier G. a) ⊗ (⨂x∈carrier G. x)"
    by (auto simp add: finprod_multf Pi_def)
  also have "(⨂x∈carrier G. a) = a (^) card(carrier G)"
    by (auto simp add: finprod_const)
  finally show ?thesis
(* uses the preceeding lemma *)
    by auto
qed


subsubsection ‹Miscellaneous›

lemma (in cring) field_intro2: "𝟬⇘R⇙ ~= 𝟭⇘R⇙ ⟹ ∀x ∈ carrier R - {𝟬⇘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 = 𝟭 ⟹ y ⊗ x = 𝟭 ⟹ inv x = y"
  apply (subgoal_tac "x : Units G")
  apply (subgoal_tac "y = inv x ⊗ 𝟭")
  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 = 𝟭 ⟹ inv x = y"
  apply (rule inv_char)
  apply auto
  apply (subst m_comm, auto)
  done

lemma (in ring) inv_neg_one [simp]: "inv (⊖ 𝟭) = ⊖ 𝟭"
  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]: "⊖ 𝟭 : Units R"
  apply (unfold Units_def)
  apply auto
  apply (rule_tac x = "⊖ 𝟭" in bexI)
  apply auto
  apply (simp add: l_minus r_minus)
  done

lemma (in monoid) inv_one [simp]: "inv 𝟭 = 𝟭"
  apply (rule inv_char)
  apply auto
  done

lemma (in ring) inv_eq_neg_one_eq: "x : Units R ⟹ (inv x = ⊖ 𝟭) = (x = ⊖ 𝟭)"
  apply auto
  apply (subst Units_inv_inv [symmetric])
  apply auto
  done

lemma (in monoid) inv_eq_one_eq: "x : Units G ⟹ (inv x = 𝟭) = (x = 𝟭)"
  by (metis Units_inv_inv inv_one)


subsubsection ‹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 (⋃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 ⊕ ⊖ 𝟭"
    by (simp add: ring_simprules)
  also from ‹x ⊗ x = 𝟭› have "… = 𝟬"
    by (simp add: ring_simprules)
  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 (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 = 𝟭 ∨ x = ⊖𝟭"
  by (metis Units_closed Units_l_inv square_eq_one)


text ‹
  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

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