# Theory FNDS_Lifting_Set_Ext

(* Title: Examples/TTS_Foundations/Foundations/FNDS_Lifting_Set_Ext.thy
Author: Mihails Milehins
*)
section‹Extension of the theory text‹Lifting_Set›
theory FNDS_Lifting_Set_Ext
imports Main
begin

context
includes lifting_syntax
begin

lemma set_pred_eq_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total A"
shows
"((rel_set A ===> (=)) ===> (rel_set A ===> (=)) ===> (=))
(λX Y. sCollect (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
unfolding pairwise_def by transfer_prover

lemma disjnt_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows
unfolding disjnt_def by transfer_prover

lemma bij_betw_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "bi_unique B"
shows
unfolding bij_betw_def
apply transfer_prover_start
apply transfer_step+
by simp

end

text‹\newpage›

end