Theory C2

Up to index of Isabelle/HOL/Free-Groups

theory C2
imports Group
theory C2
imports "~~/src/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 = op =, one = True |)),"

lemma [simp]: "op ⊗C2 = op ="
unfolding C2_def by simp

lemma [simp]: "\<one>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