Theory Natural_Functor

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

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_non_empty: "∃b. to_set b ≠ {}"
begin

lemma map_id [simp]: "map id b = b"
  unfolding id_def
  using 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

lemma map_id_cong [simp]:
  assumes "⋀a. a ∈ to_set b ⟹ f a = a"
  shows "map f b = b"
  using assms
  by simp

lemma to_set_map_not_ident:
  assumes "a ∈ to_set b" "f a ∉ to_set b"
  shows "map f b ≠ b"
  using assms
  by (metis rev_image_eqI to_set_map)

lemma exists_functor [intro]: "∃b. a ∈ to_set b"
proof -

  obtain a' b where "a' ∈ to_set b"
    using exists_non_empty
    by blast

  then have "a ∈ to_set (map (λ_. a) b)"
    by auto
  
  then show ?thesis
    by blast
qed

lemma to_set_const [simp]: "to_set b ≠ {} ⟹ to_set (map (λ_. a) b) = {a}"
  by auto

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"

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

ML ‹fun all_bnfs ctxt =
  ctxt |>
  Proof_Context.theory_of |>
  Theory.defs_of |> 
  Defs.all_specifications_of |>
  map_filter (fn ((kind, name), _) => if kind = Defs.Type then BNF_Def.bnf_of ctxt name else NONE)›

declare [[ML_print_depth=100]]
ML ‹all_bnfs @{context} |> map BNF_Def.T_of_bnf›
 *)

end