Theory UnitGroup

header {* The Unit Group *}

theory "UnitGroup"
imports
   "~~/src/HOL/Algebra/Group"
   "Generators"
begin

text {* There is, up to isomorphisms, only one group with one element. *}

definition unit_group :: "unit monoid"
where 
  "unit_group ≡ (|
     carrier = UNIV,
     mult = λ x y. (),
     one = ()
  |)),"

theorem unit_group_is_group: "group unit_group"
  by (rule groupI, auto simp add:unit_group_def)

theorem (in group) unit_group_unique:
  assumes "card (carrier G) = 1"
  shows "∃ h. h ∈ G ≅ unit_group"
proof-
  from assms obtain x where "carrier G = {x}" by (auto dest: card_eq_SucD)
  hence "(λ x. ()) ∈ G ≅ unit_group"  
    by -(rule group_isoI, auto simp add:unit_group_is_group is_group, simp add:unit_group_def)
  thus ?thesis by auto
qed

end