Theory VS_Prerequisites

(* Title: Examples/Vector_Spaces/VS_Prerequisites.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
chapter‹TTS Vector Spaces›
theory VS_Prerequisites
  imports Types_To_Sets_Extension.ETTS_Auxiliary
begin




section‹Introduction›



subsection‹Background›


text‹
The content of this chapter is an adoption of the applied relativization
study presented in \<^cite>‹"immler_smooth_2019"› to the ETTS. 
The content of this chapter incorporates 
many elements of the content of the aforementioned relativization study without 
an explicit reference. Nonetheless, no attempt was made to ensure that
the theorems obtained as a result of this work are identical to the theorems 
obtained in \<^cite>‹"immler_smooth_2019"›. 
›



subsection‹Prerequisites›

ctr parametricity
  in bij_betw_ow: bij_betw_def

lemma bij_betw_parametric'[transfer_rule]:
  includes lifting_syntax
  assumes "bi_unique A"
  shows "((A ===> A) ===> rel_set A ===> rel_set A ===> (=)) 
    bij_betw bij_betw"
  by (rule bij_betw_ow.transfer[OF assms assms])

lemma vimage_transfer[transfer_rule]: 
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique B" "right_total A" 
  shows 
    "((A ===> B) ===> (rel_set B) ===> rel_set A) 
      (λf s. (vimage f s) ∩ (Collect (Domainp A))) (-`)"
  by transfer_prover

lemma Eps_unique_transfer_lemma:
  includes lifting_syntax
  assumes [transfer_rule]: 
    "right_total A" "(A ===> (=)) f g" "(A ===> (=)) f' g'"
    and holds: "∃x. Domainp A x ∧ f x"
    and unique_g: "⋀x y. ⟦ g x; g y ⟧ ⟹ g' x = g' y"
  shows "f' (Eps (λx. Domainp A x ∧ f x)) = g' (Eps g)"
proof -
  define Epsg where "Epsg = Eps g"
  have "∃x. g x" by transfer (simp add: holds)
  then have "g Epsg" unfolding Epsg_def by (rule someI_ex)
  obtain x where x[transfer_rule]: "A x Epsg" 
    by (meson ‹right_total A› right_totalE)
  then have "Domainp A x" by auto
  from ‹g Epsg›[untransferred] have "f x" .
  from unique_g have unique:
    "⋀x y. ⟦ Domainp A x; Domainp A y; f x; f y ⟧ ⟹ f' x = f' y"
    by transfer
  have "f' (Eps (λx. Domainp A x ∧ f x)) = f' x"
    by (rule unique[OF _ ‹Domainp A x› _ ‹f x›]) 
      (metis (mono_tags, lifting) local.holds someI_ex)+
  show "f' (SOME x. Domainp A x ∧ f x) = g' (Eps g)"
    using x ‹f' (Eps _) = f' x› Epsg_def rel_funE assms(3) by fastforce
qed

text‹\newpage›

end