section ‹The Unit Group›

theory "UnitGroup"
imports
   "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 ∈ iso G unit_group"
proof-
  from assms obtain x where "carrier G = {x}" by (auto dest: card_eq_SucD)
  hence "(λ x. ()) ∈ iso 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