# Theory Lifting_Set_Ext

```(* Title: Examples/SML_Relativization/Foundations/Lifting_Set_Ext.thy
Author: Mihails Milehins
*)
section‹Extension of the theory \<^text>‹Lifting_Set››
theory Lifting_Set_Ext
imports Main
begin

context
includes lifting_syntax
begin

lemma set_pred_eq_transfer[transfer_rule]:
assumes "right_total A"
shows
"((rel_set A ===> (=)) ===> (rel_set A ===> (=)) ===> (=))
(λX Y. ∀s⊆Collect (Domainp A). X s = Y s)
((=)::['b set ⇒ bool, 'b set ⇒ bool] ⇒ bool)"
proof(intro rel_funI)
let ?sA = "Collect (Domainp A)"
fix X Y :: "'a set ⇒ bool"
fix X' Y' :: "'b set ⇒ bool"
assume rs: "(rel_set A ===> (=)) X X'" "(rel_set A ===> (=)) Y Y'"
show "(∀s⊆?sA. X s = Y s) = (X' = Y')"
proof
assume X_eq_Y: "∀s⊆?sA. X s = Y s"
{
fix s' assume "X' s'"
then obtain s where "rel_set A s s'"
by (meson assms right_total_def right_total_rel_set)
then have "X s" using rs(1) unfolding rel_fun_def by (simp add: ‹X' s'›)
moreover from ‹rel_set A s s'› have "s ⊆ ?sA"
unfolding Ball_Collect[symmetric] by (auto dest: rel_setD1)
ultimately have "Y' s'"
using rs(2)[unfolded rel_fun_def] ‹rel_set A s s'› by (simp add: X_eq_Y)
}
note XY = this
{
fix s' assume "Y' s'"
then obtain s where "rel_set A s s'"
by (meson assms right_total_def right_total_rel_set)
then have "Y s" using rs(2)[unfolded rel_fun_def] by (simp add: ‹Y' s'›)
moreover from ‹rel_set A s s'› have "s ⊆ ?sA"
unfolding Ball_Collect[symmetric] by (auto dest: rel_setD1)
ultimately have "X' s'"
using X_eq_Y rs(1)[unfolded rel_fun_def] ‹rel_set A s s'› by auto
}
with XY show "X' = Y'" by auto
next
assume "X' = Y'" show "∀s⊆?sA. X s = Y s"
unfolding Ball_Collect[symmetric]
using rs[unfolded rel_fun_def] ‹X' = Y'› by (metis DomainpE Domainp_set)+
qed
qed

private lemma vimage_fst_transfer_h:
"
pred_prod (Domainp A) (Domainp B) x =
(x ∈ Collect (Domainp A) × Collect (Domainp B))
"
unfolding pred_prod_beta mem_Times_iff by simp

lemma vimage_fst_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A" "right_total B"
shows
"((rel_prod A B ===> A) ===> rel_set A ===> rel_set (rel_prod A B))
(λf S. (f -` S) ∩ ((Collect (Domainp A)) × (Collect (Domainp B))))
vimage"
unfolding vimage_def
apply transfer_prover_start
apply transfer_step+
unfolding vimage_fst_transfer_h
by auto

lemma vimage_snd_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total A" "bi_unique B" "right_total B"
shows
"((rel_prod A B ===> B) ===> rel_set B ===> rel_set (rel_prod A B))
(λf S. (f -` S) ∩ ((Collect (Domainp A)) × (Collect (Domainp B))))
vimage"
unfolding vimage_def
apply transfer_prover_start
apply transfer_step+
unfolding vimage_fst_transfer_h by auto

lemma vimage_transfer[transfer_rule]:
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 pairwise_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> A ===> (=)) ===> rel_set A  ===> (=)) pairwise pairwise"
unfolding pairwise_def by transfer_prover

lemma disjnt_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "(rel_set A ===> rel_set A  ===> (=)) disjnt disjnt"
unfolding disjnt_def by transfer_prover

lemma bij_betw_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "bi_unique B"
shows "((A ===> B) ===> rel_set A ===> rel_set B ===> (=)) bij_betw bij_betw"
unfolding bij_betw_def
apply transfer_prover_start
apply transfer_step+
by simp

end

text‹\newpage›

end```