Theory Abstract_Substitution.Natural_Magma

theory Natural_Magma ✐‹contributor ‹Balazs Toth››
  imports Main
begin

locale natural_magma =
  fixes
    to_set :: "'b ⇒ 'a set" and
    plus :: "'b ⇒ 'b ⇒ 'b" and
    wrap :: "'a ⇒ 'b" and
    add
  defines "⋀a b. add a b ≡ plus (wrap a) b"
  assumes
    to_set_plus [simp]: "⋀b b'. to_set (plus b b') = (to_set b) ∪ (to_set b')" and
    to_set_wrap [simp]: "⋀a. to_set (wrap a) = {a}"
begin

lemma to_set_add [simp]: "to_set (add a b) = insert a (to_set b)"
  using to_set_plus to_set_wrap add_def
  by simp

end

locale natural_magma_with_empty = natural_magma +
  fixes empty
  assumes to_set_empty [simp]: "to_set empty = {}"

end