Theory Abstract_Representations

section "Representations"

subsection "Abstract Representations"

theory Abstract_Representations
  imports Main
begin

text "Idea: some type @{text 'a} is represented non-uniquely by some type @{text 'b}.
The function @{term f} produces a unique representant."

locale abstract_representation =
  fixes from_type :: "'a ⇒ 'b"
  fixes to_type :: "'b ⇒ 'a"
  fixes f :: "'b ⇒ 'b"
  assumes to_from: "to_type ∘ from_type = id"
  assumes from_to: "from_type ∘ to_type = f"
begin

lemma to_from_elem[simp]: "to_type (from_type x) = x"
  using to_from by (metis comp_apply id_apply)
lemma from_to_elem: "from_type (to_type x) = f x"
  using from_to by (metis comp_apply)

lemma f_idem: "f ∘ f = f"
proof -
  have "f ∘ f = from_type ∘ to_type ∘ from_type ∘ to_type"
    using from_to by fastforce
  also have "... = from_type ∘ to_type"
    using to_from by (simp add: rewriteR_comp_comp)
  finally show ?thesis using from_to by simp
qed

corollary f_idem_elem[simp]: "f (f x) = f x"
  using f_idem by (metis comp_apply)

lemma f_from: "f ∘ from_type = from_type"
proof -
  have "f ∘ from_type = from_type ∘ to_type ∘ from_type"
    using from_to by simp
  also have "... = from_type"
    using to_from by (simp add: rewriteR_comp_comp)
  finally show ?thesis .
qed

corollary f_from_elem[simp]: "f (from_type x) = from_type x"
  using f_from by (metis comp_apply)

lemma to_f: "to_type ∘ f = to_type"
proof -
  have "to_type ∘ f = to_type ∘ from_type ∘ to_type"
    using from_to by fastforce
  also have "... = to_type" using to_from by simp
  finally show ?thesis .
qed

corollary to_f_elem[simp]: "to_type (f x) = to_type x"
  using to_f by (metis comp_apply)

lemma f_fixed_point_iff: "f x = x ⟷ (∃y. x = from_type y)"
proof
  assume "f x = x"
  then show "∃y. x = from_type y" using from_to_elem by metis
next
  assume "∃y. x = from_type y"
  then obtain y where "x = from_type y" by blast
  then show "f x = x" by simp
qed

lemma f_fixed_point_iff': "f x = x ⟷ x = from_type (to_type x)"
  using from_to by auto

lemma range_f_range_from: "range f = range from_type"
proof (standard; standard)
  fix x
  assume "x ∈ range f"
  then obtain x' where "x = f x'" by blast
  then have "f x = x" by simp
  then show "x ∈ range from_type" using f_fixed_point_iff by blast
next
  fix x
  assume "x ∈ range from_type"
  then obtain y where "x = from_type y" by blast
  then have "f x = x" using f_fixed_point_iff by simp
  then show "x ∈ range f" by (metis rangeI)
qed

lemma to_eq_iff_f_eq: "to_type x = to_type y ⟷ f x = f y"
proof
  show "to_type x = to_type y ⟹ f x = f y" using from_to_elem[symmetric] by simp
next
  show "f x = f y ⟹ to_type x = to_type y" using to_f_elem by metis
qed

lemma from_inj: "inj from_type"
  using to_from by (metis inj_on_id inj_on_imageI2)

end

lemma from_to_f_criterion:
  assumes "to_type ∘ from_type = id"
  assumes "f ∘ from_type = from_type"
  assumes "⋀x y. to_type x = to_type y ⟹ f x = f y"
  shows "from_type ∘ to_type = f"
proof
  fix x
  have "to_type (from_type (to_type x)) = to_type x"
    using assms(1) by (metis comp_apply id_apply)
  hence "f (from_type (to_type x)) = f x"
    using assms(3) by metis
  hence "from_type (to_type x) = f x"
    using assms(2) by (metis comp_apply)
  thus "(from_type ∘ to_type) x = f x"
    by (metis comp_apply)
qed

end