Theory First_Order_Clause.Natural_Functor_To_Multiset

theory Natural_Functor_To_Multiset
  imports
    Abstract_Substitution.Natural_Functor
    Multiset_Extra
begin

locale natural_functor_to_multiset = natural_functor where to_set = to_set
for
  to_mset :: "'b ⇒ 'a multiset" and
  to_set :: "'b ⇒ 'a set" +
assumes
    (* TODO: Separate inj! *)
  to_mset_to_set: "⋀b. set_mset (to_mset b) = to_set b" and
  to_mset_map: "⋀f b. to_mset (map f b) = image_mset f (to_mset b)" and
  inj_to_mset: "inj to_mset"

global_interpretation id_natural_functor_multiset: natural_functor_to_multiset where
  to_set = set_mset and map = image_mset and to_mset = "λx. x"
  by unfold_locales auto

end