(* Title: Examples/SML_Relativization/Foundations/Transfer_Ext.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) 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