Theory Transfer_Ext
section‹Extension of the theory \<^text>‹Transfer››
theory Transfer_Ext
imports Main
begin
lemma bi_unique_intersect_r:
assumes "bi_unique T"
and "rel_set T a a'"
and "rel_set T b b'"
and "rel_set T (a ∩ b) xr"
shows "a' ∩ b' = xr"
proof -
{
fix x assume "x ∈ a ∩ b"
then have "x ∈ a" and "x ∈ b" by simp+
from assms(2) ‹x ∈ a› have "∃y ∈ a'. T x y" by (rule rel_setD1)
moreover from assms(3) ‹x ∈ b› have "∃y ∈ b'. T x y" by (rule rel_setD1)
ultimately have "∃y ∈ a' ∩ b'. T x y"
using assms(1) by (auto dest: bi_uniqueDr)
}
note unique_r = this
{
fix x assume "x ∈ a' ∩ b'"
then have "x ∈ a'" and "x ∈ b'" by simp+
from assms(2) ‹x ∈ a'› have "∃y ∈ a. T y x" by (rule rel_setD2)
moreover from assms(3) ‹x ∈ b'› have "∃y ∈ b. T y x" by (rule rel_setD2)
ultimately have "∃y ∈ a ∩ b. T y x"
using assms(1) by (auto dest: bi_uniqueDl)
}
with unique_r have "rel_set T (a ∩ b) (a' ∩ b')" using rel_setI by blast
with assms(1,4) show ?thesis by (auto dest: bi_uniqueDr bi_unique_rel_set)
qed
lemma bi_unique_intersect_l:
assumes "bi_unique T"
and "rel_set T a a'"
and "rel_set T b b'"
and "rel_set T xl (a' ∩ b')"
shows "a ∩ b = xl"
proof -
let ?T' = "λ y x. T x y"
from assms(1) have "bi_unique ?T'" unfolding bi_unique_def by simp
moreover from assms(2) have "rel_set ?T' a' a" unfolding rel_set_def by simp
moreover from assms(3) have "rel_set ?T' b' b" unfolding rel_set_def by simp
moreover from assms(4) have "rel_set ?T' (a' ∩ b') xl"
unfolding rel_set_def by simp
ultimately show ?thesis by (rule bi_unique_intersect_r)
qed
lemma bi_unique_intersect:
assumes "bi_unique T" and "rel_set T a a'" and "rel_set T b b'"
shows "rel_set T (a ∩ b) (a' ∩ b')"
proof -
{
fix xl assume "xl ∈ a ∩ b"
then have "xl ∈ a" and "xl ∈ b" by simp+
with assms(3) obtain xr where "T xl xr" unfolding rel_set_def by auto
with assms(1,2) ‹xl ∈ a› have "xr ∈ a'"
by (auto dest: bi_uniqueDr rel_setD1)
moreover with assms(1,3) ‹xl ∈ b› ‹T xl xr› have "xr ∈ b'"
by (auto dest: bi_uniqueDr rel_setD1)
ultimately have "xr ∈ a' ∩ b'" by simp
with ‹T xl xr› have "∃xr. xr ∈ a' ∩ b' ∧ T xl xr" by auto
}
then have prem_lhs: "∀xl ∈ a ∩ b. ∃xr. xr ∈ a' ∩ b' ∧ T xl xr" by simp
{
fix xr
assume "xr ∈ a' ∩ b'"
then have "xr ∈ a'" and "xr ∈ b'" by simp+
with assms(3) obtain xl where "T xl xr" unfolding rel_set_def by auto
with assms(1,2) ‹xr ∈ a'› have "xl ∈ a"
by (auto dest: bi_uniqueDl rel_setD2)
moreover with assms(1,3) ‹xr ∈ b'› ‹T xl xr› have "xl ∈ b"
by (auto dest: bi_uniqueDl rel_setD2)
ultimately have "xl ∈ a ∩ b" by simp
with ‹T xl xr› have "∃xl. xl ∈ a ∩ b ∧ T xl xr" by auto
}
then have prem_rhs: "∀xr ∈ a' ∩ b'. ∃xl. xl ∈ a ∩ b ∧ T xl xr" by simp
from prem_lhs prem_rhs show ?thesis unfolding rel_set_def by auto
qed
lemma bi_unique_union_r:
assumes "bi_unique T"
and "rel_set T a a'"
and "rel_set T b b'"
and "rel_set T (a ∪ b) xr"
shows "a' ∪ b' = xr"
proof -
{
fix x assume "x ∈ a ∪ b"
then have "x ∈ a ∨ x ∈ b" by simp
from assms(2) have "∃y ∈ a'. T x y" if "x ∈ a"
using that by (rule rel_setD1)
moreover from assms(3) have "∃y ∈ b'. T x y" if "x ∈ b"
using that by (rule rel_setD1)
ultimately have "∃y ∈ a' ∪ b'. T x y" using ‹x ∈ a ∨ x ∈ b› by auto
}
note unique_r = this
{
fix x assume "x ∈ a' ∪ b'"
then have "x ∈ a' ∨ x ∈ b'" by simp
from assms(2) have "∃y ∈ a. T y x" if "x ∈ a'"
using that by (rule rel_setD2)
moreover from assms(3) have "∃y ∈ b. T y x" if "x ∈ b'"
using that by (rule rel_setD2)
ultimately have "∃y ∈ a ∪ b. T y x" using ‹x ∈ a' ∨ x ∈ b'› by auto
}
with unique_r have "rel_set T (a ∪ b) (a' ∪ b')" by (auto intro: rel_setI)
with assms(1,4) show ?thesis by (auto dest: bi_uniqueDr bi_unique_rel_set)
qed
lemma bi_unique_union_l:
assumes "bi_unique T"
and "rel_set T a a'"
and "rel_set T b b'"
and "rel_set T xl (a' ∪ b')"
shows "a ∪ b = xl"
proof -
let ?T' = "λy x. T x y"
from assms(1) have "bi_unique ?T'" unfolding bi_unique_def by simp
moreover from assms(2) have "rel_set ?T' a' a" unfolding rel_set_def by simp
moreover from assms(3) have "rel_set ?T' b' b" unfolding rel_set_def by simp
moreover from assms(4) have "rel_set ?T' (a' ∪ b') xl"
unfolding rel_set_def by simp
ultimately show ?thesis by (rule bi_unique_union_r)
qed
lemma bi_unique_union:
assumes "bi_unique T" and "rel_set T a a'" and "rel_set T b b'"
shows "rel_set T (a ∪ b) (a' ∪ b')"
proof -
{
fix xl assume "xl ∈ a ∪ b"
with assms(2,3) obtain xr where "T xl xr" unfolding rel_set_def by auto
with assms ‹xl ∈ a ∪ b› have "xr ∈ a' ∪ b'"
unfolding bi_unique_def using Un_iff by (metis Un_iff rel_setD1)
with ‹T xl xr› have "∃xr. xr ∈ a' ∪ b' ∧ T xl xr" by auto
}
then have prem_lhs: "∀xl ∈ a ∪ b. ∃xr. xr ∈ a' ∪ b' ∧ T xl xr" by simp
{
fix xr assume "xr ∈ a' ∪ b'"
with assms(2,3) obtain xl where "T xl xr" unfolding rel_set_def by auto
with assms ‹xr ∈ a' ∪ b'› have "xl ∈ a ∪ b"
unfolding bi_unique_def by (metis Un_iff rel_setD2)
with ‹T xl xr› have "∃xl. xl ∈ a ∪ b ∧ T xl xr" by auto
}
then have prem_rhs: "∀xr ∈ a' ∪ b'. ∃xl. xl ∈ a ∪ b ∧ T xl xr" by simp
from prem_lhs prem_rhs show ?thesis unfolding rel_set_def by auto
qed
lemma bi_unique_Union_r:
fixes T :: "['a, 'b] ⇒ bool" and K
defines K': "K' ≡ {(x, y). rel_set T x y} `` K"
assumes "bi_unique T"
and "⋃K ⊆ Collect (Domainp T)"
and "rel_set T (⋃K) xr"
shows "⋃K' = xr"
proof -
{
fix x assume "x ∈ ⋃K"
then obtain k where "x ∈ k" and "k ∈ K" by clarsimp
from assms have ex_k'_prem: "∀k ∈ K. ∀x ∈ k. ∃x'. T x x'" by auto
define k' where k': "k' = {x'. ∃x ∈ k. T x x'}"
have "rel_set T k k'"
unfolding rel_set_def Bex_def k'
using ‹k ∈ K› by (blast dest: ex_k'_prem[rule_format])
with ‹k ∈ K› have "k' ∈ K'" unfolding K' by auto
from ‹rel_set T k k'› ‹x ∈ k› obtain y where "y ∈ k' ∧ T x y"
by (auto dest: rel_setD1)
then have "∃y ∈ ⋃K'. T x y" using ‹k' ∈ K'› by auto
}
note unique_r = this
{
fix x' assume "x' ∈ ⋃K'"
then obtain k' where "x' ∈ k'" and "k' ∈ K'" by clarsimp
then have ex_k_prem: "∀k' ∈ K'. ∀x ∈ k'. ∃x. T x x'"
unfolding K' by (auto dest: rel_setD2)
define k where k: "k = {x. ∃x' ∈ k'. T x x'}"
have "rel_set T k k'"
unfolding rel_set_def Bex_def k
using ‹k' ∈ K'› K' by (blast dest: rel_setD2)
from assms(2) have "bi_unique (rel_set T)" by (rule bi_unique_rel_set)
with ‹rel_set T k k'› have "∃!k. rel_set T k k'" by (auto dest: bi_uniqueDl)
with ‹rel_set T k k'› K' ‹k' ∈ K'› have "k ∈ K" by auto
from ‹rel_set T k k'› ‹x' ∈ k'› obtain y where "y ∈ k ∧ T y x'"
by (auto dest: rel_setD2)
then have "∃y ∈ ⋃K. T y x'" using ‹k ∈ K› by auto
}
with unique_r have "rel_set T (⋃K) (⋃K')" by (intro rel_setI)
with assms(2,4) show ?thesis by (auto dest: bi_uniqueDr bi_unique_rel_set)
qed
lemma bi_unique_Union_l:
fixes T :: "['a, 'b] ⇒ bool" and K'
defines K: "K ≡ {(x, y). rel_set (λ y x. T x y) x y} `` K'"
assumes "bi_unique T"
and "⋃K' ⊆ Collect (Rangep T)"
and "rel_set T xl (⋃K')"
shows "⋃K = xl"
proof -
let ?T' = "λ y x. T x y"
from assms(2) have "bi_unique ?T'" unfolding bi_unique_def by simp
moreover from assms(3) have "⋃K' ⊆ Collect (Domainp ?T')" by blast
moreover from assms(4) have "rel_set ?T' (⋃K') xl"
unfolding rel_set_def by simp
ultimately have "⋃({(x, y). rel_set ?T' x y} `` K') = xl"
by (rule bi_unique_Union_r)
thus ?thesis using K by simp
qed
context
includes lifting_syntax
begin
text‹
The lemma \<^text>‹Domainp_applyI› was adopted from the lemma with the
identical name in the theory \<^text>‹Types_To_Sets/Group_on_With.thy›.
›
lemma Domainp_applyI:
includes lifting_syntax
shows "(A ===> B) f g ⟹ A x y ⟹ Domainp B (f x)"
by (auto simp: rel_fun_def)
lemma Domainp_fun:
assumes "left_unique A"
shows
"Domainp (rel_fun A B) =
(λf. f ` (Collect (Domainp A)) ⊆ (Collect (Domainp B)))"
proof-
have
"pred_fun (Domainp A) (Domainp B) =
(λf. f ` (Collect (Domainp A)) ⊆ (Collect (Domainp B)))"
by (simp add: image_subset_iff)
from Domainp_pred_fun_eq[OF ‹left_unique A›, of B, unfolded this]
show ?thesis .
qed
lemma Bex_fun_transfer[transfer_rule]:
assumes "bi_unique A" "right_total B"
shows
"(((A ===> B) ===> (=)) ===> (=))
(Bex (Collect (λf. f ` (Collect (Domainp A)) ⊆ (Collect (Domainp B)))))
Ex"
proof-
from assms(1) have "left_unique A" by (simp add: bi_unique_alt_def)
note right_total_BA[transfer_rule] =
right_total_fun[
OF conjunct2[OF bi_unique_alt_def[THEN iffD1, OF assms(1)]] assms(2)
]
show ?thesis
unfolding Domainp_fun[OF ‹left_unique A›, symmetric]
by transfer_prover
qed
end
text‹\newpage›
end