Theory C2

theory C2
imports "HOL-Algebra.Group"
begin

section ‹The group C2›

text ‹
The two-element group is defined over the set of boolean values. This allows to 
use the equality of boolean values as the group operation.
›

definition "C2"
  where "C2 = ⦇ carrier = UNIV, mult = (=), one = True ⦈"

lemma [simp]: "(⊗⇘C2⇙) = (=)"
  unfolding C2_def by simp

lemma [simp]: "𝟭⇘C2⇙ = True"
  unfolding C2_def by simp

lemma [simp]: "carrier C2 = UNIV"
  unfolding C2_def by simp

lemma C2_is_group: "group C2"
  unfolding C2_def
  by (rule groupI, auto simp add:Units_def)

end