Theory Abstract_Representations_2

subsection "Abstract Representations 2"

theory Abstract_Representations_2
  imports Main
begin

text "Idea: a subset @{term represented_set} of some type @{text 'a} is represented non-uniquely by
some type @{text 'b}."

locale abstract_representation_2 =
  fixes from_type :: "'a ⇒ 'b"
  fixes to_type :: "'b ⇒ 'a"
  fixes represented_set :: "'a set"
  assumes to_from: "⋀x. x ∈ represented_set ⟹ to_type (from_type x) = x"
  assumes to_type_in_represented_set: "⋀y. to_type y ∈ represented_set"
begin

definition reduce where
"reduce x ≡ from_type (to_type x)"

abbreviation reduced where
"reduced x ≡ reduce x = x"

lemma reduce_reduce[simp]: "reduced (reduce x)"
  unfolding reduce_def
  by (simp add: to_from to_type_in_represented_set)

definition representations where
"representations ≡ from_type ` represented_set"

lemma range_reduce: "representations = range reduce"
  unfolding representations_def reduce_def
  image_def 
  apply (intro equalityI subsetI)
  subgoal for x
  proof -
    assume "x ∈ {y. ∃x∈represented_set. y = from_type x}"
    then have "∃y∈represented_set. x = from_type y" by simp
    then obtain y where "x = from_type y" "y ∈ represented_set" by blast
    then have "to_type x = y" using to_from by simp
    then have "x = from_type (to_type x)" using ‹x = from_type y› by simp
    then show ?thesis by blast
  qed
  subgoal for x
    using to_type_in_represented_set by blast
  done

corollary reduced_from_type[simp]: "x ∈ represented_set ⟹ reduced (from_type x)"
  using range_reduce representations_def reduce_reduce by force

lemma to_type_reduce: "to_type (reduce x) = to_type x"
  unfolding reduce_def
  by (simp add: to_from to_type_in_represented_set)

lemma reduced_iff: "reduced x ⟷ (∃y∈represented_set. x = from_type y)"
  apply standard
  subgoal
    using reduce_def to_type_in_represented_set by metis
  subgoal
    by fastforce
  done

lemma to_eq_iff_f_eq: "to_type x = to_type y ⟷ reduce x = reduce y"
proof
  show "to_type x = to_type y ⟹ reduce x = reduce y" unfolding reduce_def by simp
next
  show "reduce x = reduce y ⟹ to_type x = to_type y" using to_type_reduce by metis
qed

lemma from_inj: "inj_on from_type represented_set"
  unfolding inj_on_def
  apply standard+
  subgoal for x y
    using to_from[of x, symmetric] to_from[of y] by simp
  done

corollary from_bij_betw: "bij_betw from_type represented_set representations"
  unfolding representations_def
  using from_inj
  by (simp add: inj_on_imp_bij_betw)

lemma correctness_to_from:
  fixes h :: "'a ⇒ 'a ⇒ 'a"
  fixes g :: "'b ⇒ 'b ⇒ 'b"
  assumes "⋀x y. to_type (g x y) = h (to_type x) (to_type y)"
  shows "⋀x y. x ∈ represented_set ⟹ y ∈ represented_set ⟹ reduce (g (from_type x) (from_type y)) = from_type (h x y)"
proof -
  fix x y
  assume "x ∈ represented_set" "y ∈ represented_set"
  have "reduce (g (from_type x) (from_type y)) = from_type (to_type (g (from_type x) (from_type y)))"
    unfolding reduce_def by simp
  also have "... = from_type (h (to_type (from_type x)) (to_type (from_type y)))"
    using assms by simp
  also have "... = from_type (h x y)"
    using to_from ‹x ∈ represented_set› ‹y ∈ represented_set› by simp
  finally show "reduce (g (from_type x) (from_type y)) = from_type (h x y)" .
qed

end

lemma from_to_f_criterion:
  assumes "⋀x. x ∈ represented_set ⟹ to_type (from_type x) = x"
  assumes "⋀x. x ∈ represented_set ⟹ f (from_type x) = from_type x"
  assumes "⋀x y. to_type x = to_type y ⟹ f x = f y"
  assumes "⋀y. to_type y ∈ represented_set"
  shows "⋀x. from_type (to_type x) = f x"
proof -
  fix x
  have "to_type (from_type (to_type x)) = to_type x"
    using assms(1) assms(4) by simp
  hence "f (from_type (to_type x)) = f x"
    using assms(3) by metis
  thus "from_type (to_type x) = f x"
    using assms(2) assms(4) by simp
qed

end