Theory Types_To_Sets_Extension.VS_Prerequisites
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