instantiation list :: (type) monoid_mult
begin

  definition times_list:
    "xs * ys ≡ xs @ ys"

  definition one_list:
    "1 ≡ []"

  instance proof
    fix xs ys zs :: "'a list"
    show "xs * ys * zs = xs * (ys * zs)"
      by (simp add: times_list)
    show "1 * xs = xs"
      by (simp add: one_list times_list)
    show "xs * 1 = xs"
      by (simp add: one_list times_list)
  qed

end  (* instantiation *)


instantiation set :: (monoid_mult) power
begin

  definition one_set:
    "1 = {1}"

  definition times_set :
    "A * B = {u * v | u v. u ∈ A ∧ v ∈ B}"

  instance ..
end

instantiation set :: (monoid_mult) plus
begin

  definition plus_set:
      "A + B = A ∪ B"

  instance ..
end


instantiation set :: (monoid_mult)  zero
begin

  definition zero_set:
    "0 = {}"

  instance ..
end

instantiation set :: (monoid_mult)  monoid_mult
begin
instance proof
  fix a b c ::"'a set"
  show "a * b * c = a * (b * c)"
    apply(simp add:times_set)
    by (metis (no_types, opaque_lifting) mult.assoc)
  show "1 * a = a"
    apply(simp add:one_set times_set) done
  show "a * 1 = a"
    apply(simp add:one_set times_set) done
qed
end

instantiation set :: (monoid_mult) star_op
begin
  definition star_set: "X⇧⋆ = (⋃n. X ^ n)"
  instance ..
end

lemma "x⇧⋆ = ((1::'a list set) + x)⇧⋆"