Scratch.thy

theory Scratch imports Main begin

locale Magma =
  fixes m :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

locale SemiGroup = Magma +
  assumes assoc: "\<And>x y z. m (m x y) z = m x (m y z)"

locale Commutative = Magma +
  assumes comm: "\<And>x y. m x y = m y x"

locale Monoid = SemiGroup +
  fixes e :: "'a"
  assumes lunit: "\<And>x. m e x = x"
  assumes runit: "\<And>x. m x e = x"

locale Group = Monoid +
  fixes i :: "'a \<Rightarrow> 'a"
  assumes linv: "\<And>x. m (i x) x = e"
  assumes rinv: "\<And>x. m x (i x) = e"

locale AbelianGroup = Commutative + Group

locale BooleanGroup = Monoid +
  assumes selfi: "\<And>x. m x x = e"

context BooleanGroup begin

sublocale Commutative
  proof
    fix x y
    have "m (m y x) (m y x) = e"
      by (rule selfi)
    hence "m y (m (m (m y x) (m y x)) x) = m y x"
      by (simp add: lunit)
    hence "m (m y y) (m (m x y) (m x x)) = m y x"
      by (simp add: assoc)
    thus "m x y = m y x"
      by (simp add: selfi lunit runit)
  qed

sublocale AbelianGroup _ _ id
  unfolding id_def by unfold_locales (rule selfi)+

end

end