Theory Abstract_Substitution.Natural_Functor

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

(* TODO: Integration with built-in functor command possible? *)

locale natural_functor =
  fixes
    map :: "('a ⇒ 'a) ⇒ 'b ⇒ 'b" and
    to_set :: "'b ⇒ 'a set"
  assumes
    map_comp [simp]: "⋀b f g. map f (map g b) = map (λx. f (g x)) b" and
    map_ident [simp]: "⋀b. map (λx. x) b = b" and
    map_cong0 [cong]: "⋀b f g. (⋀a. a ∈ to_set b ⟹ f a = g a) ⟹ map f b = map g b" and
    to_set_map [simp]: "⋀b f. to_set (map f b) = f ` to_set b" and
    exists_functor [intro]: "⋀a. ∃b. a ∈ to_set b"
begin

lemma map_id [simp]: "map id b = b"
  unfolding id_def
  by(rule map_ident)

lemma map_cong [cong]: 
  assumes "b = b'" "⋀a. a ∈ to_set b' ⟹ f a = g a" 
  shows "map f b = map g b'"
  using map_cong0 assms
  by blast
  

end

locale finite_natural_functor = natural_functor +
  assumes finite_to_set [intro]: "⋀b. finite (to_set b)"

locale natural_functor_conversion =
  natural_functor +
  functor': natural_functor where map = map' and to_set = to_set'
  for map' :: "('b ⇒ 'b) ⇒ 'd ⇒ 'd" and to_set' :: "'d ⇒ 'b set" +
  fixes
    map_to :: "('a ⇒ 'b) ⇒ 'c ⇒ 'd" and
    map_from :: "('b ⇒ 'a) ⇒ 'd ⇒ 'c"
  assumes
    to_set_map_from [simp]: "⋀f d. to_set (map_from f d) = f ` to_set' d" and
    to_set_map_to [simp]: "⋀f c. to_set' (map_to f c) = f ` to_set c" and
    conversion_map_comp [simp]: "⋀c f g. map_from f (map_to g c) = map (λx. f (g x)) c" and
    conversion_map_comp' [simp]: "⋀d f g. map_to f (map_from g d) = map' (λx. f (g x)) d"

end