(* Title: ETTS/ETTS_Auxiliary.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins Auxiliary functionality for the ETTS. *) section‹Auxiliary functionality and helpful lemmas for Types-To-Sets› theory ETTS_Auxiliary imports ETTS begin subsection‹Further transfer rules› lemma Domainp_eq[transfer_domain_rule, transfer_rule]: "Domainp (=) = (λx. x ∈ UNIV)" by auto lemma Domainp_rel_prod[transfer_domain_rule, transfer_rule]: assumes "Domainp cr⇩_{1}= (λx. x ∈ 𝔘⇩_{1})" and "Domainp cr⇩_{2}= (λx. x ∈ 𝔘⇩_{2})" shows "Domainp (rel_prod cr⇩_{1}cr⇩_{2}) = (λx. x ∈ 𝔘⇩_{1}× 𝔘⇩_{2})" using assms by (simp add: ctr_simps_pred_prod_eq_cart prod.Domainp_rel) subsection‹Constant function› definition const_fun :: "['b, 'a] ⇒ 'b" where "const_fun c = (λx. c)" lemma const_fun_transfer[transfer_rule]: includes lifting_syntax assumes "Domainp A = (λx. x ∈ 𝔘A)" and "∀x ∈ 𝔘A. f x = c" and "B c c'" shows "(A ===> B) f (const_fun c')" proof(intro rel_funI) fix x y assume "A x y" then have "x ∈ 𝔘A" by (meson Domainp.DomainI assms(1)) then have "f x = c" by (rule assms(2)[rule_format]) show "B (f x) (const_fun c' y)" unfolding ‹f x = c› const_fun_def by (rule assms(3)) qed subsection‹Transfer rules suitable for instantiation› lemma Domainp_eq_Collect: "Domainp A = (λx. x ∈ 𝔘) = (𝔘 = Collect (Domainp A))" by (metis mem_Collect_eq pred_equals_eq) context includes lifting_syntax begin lemma tts_rel_set_transfer: fixes A :: "'al ⇒ 'ar ⇒ bool" and B :: "'bl ⇒ 'br ⇒ bool" assumes "S ⊆ Collect (Domainp A)" shows "∃S'. rel_set A S S'" by (metis assms(1)[folded Ball_Collect] DomainpE Domainp_set) lemma tts_AB_transfer: fixes f :: "'al ⇒ 'bl" and A :: "'al ⇒ 'ar ⇒ bool" and B :: "'bl ⇒ 'br ⇒ bool" assumes closed: "f ` 𝔘A ⊆ 𝔘B" assumes "Domainp A = (λx. x ∈ 𝔘A)" "bi_unique A" "right_total A" "Domainp B = (λx. x ∈ 𝔘B)" "bi_unique B" "right_total B" shows "∃rcdt. (A ===> B) f rcdt" proof- from closed have closed': "x ∈ 𝔘A ⟹ f x ∈ 𝔘B" for x by auto from assms(3,4) obtain Rep_a :: "'ar ⇒ 'al" and Abs_a :: "'al ⇒ 'ar" where td_a: "type_definition Rep_a Abs_a (Collect (Domainp A))" and A_Rep: "A b b' = (b = Rep_a b')" for b b' by (blast dest: ex_type_definition) from assms(6,7) obtain Rep_b :: "'br ⇒ 'bl" and Abs_b :: "'bl ⇒ 'br" where td_b: "type_definition Rep_b Abs_b (Collect (Domainp B))" and B_Rep: "B b b' = (b = Rep_b b')" for b b' by (blast dest: ex_type_definition) define f' where f': "f' = (Rep_a ---> Abs_b) f" have f_closed: "f (Rep_a a) ∈ 𝔘B" for a using td_a td_b by (intro closed') (simp add: assms(2,5))+ have rep_abs_b: "y ∈ 𝔘B ⟹ y = Rep_b (Abs_b y)" for y using td_b unfolding type_definition_def by (simp add: assms(5)) have "(A ===> B) f f'" unfolding f' map_fun_apply by ( intro rel_funI, unfold A_Rep B_Rep, elim ssubst, intro rep_abs_b f_closed ) then show ?thesis by auto qed lemma tts_AB_transfer': fixes f' :: "'ar ⇒ 'br" and A :: "'al ⇒ 'ar ⇒ bool" and B :: "'bl ⇒ 'br ⇒ bool" assumes "Domainp A = (λx. x ∈ 𝔘A)" "bi_unique A" "right_total A" "Domainp B = (λx. x ∈ 𝔘B)" "bi_unique B" "right_total B" shows "∃f. (A ===> B) f f'" proof- from assms(2,3) obtain Rep_a :: "'ar ⇒ 'al" and Abs_a :: "'al ⇒ 'ar" where td_a: "type_definition Rep_a Abs_a (Collect (Domainp A))" and A_Rep: "A b b' = (b = Rep_a b')" for b b' by (blast dest: ex_type_definition) from assms(5,6) obtain Rep_b :: "'br ⇒ 'bl" and Abs_b :: "'bl ⇒ 'br" where td_b: "type_definition Rep_b Abs_b (Collect (Domainp B))" and B_Rep: "B b b' = (b = Rep_b b')" for b b' by (blast dest: ex_type_definition) define f where f: "f = (Abs_a ---> Rep_b) f'" have abs_rep_a: "y = Abs_a (Rep_a y)" for y using td_a unfolding type_definition_def by simp have "(A ===> B) f f'" unfolding f map_fun_apply by ( intro rel_funI, unfold A_Rep B_Rep, elim ssubst, fold abs_rep_a, intro refl ) then show ?thesis by auto qed lemma tts_AB_C_transfer: fixes f :: "'al ⇒ 'bl ⇒ 'cl" and A :: "'al ⇒ 'ar ⇒ bool" and B :: "'bl ⇒ 'br ⇒ bool" and C :: "'cl ⇒ 'cr ⇒ bool" assumes closed: "⋀a b. ⟦ a ∈ 𝔘A; b ∈ 𝔘B ⟧ ⟹ f a b ∈ 𝔘C" assumes "Domainp A = (λx. x ∈ 𝔘A)" "bi_unique A" "right_total A" "Domainp B = (λx. x ∈ 𝔘B)" "bi_unique B" "right_total B" "Domainp C = (λx. x ∈ 𝔘C)" "bi_unique C" "right_total C" shows "∃rcdt. (A ===> B ===> C) f rcdt" proof- from assms(3,4) obtain Rep_a :: "'ar ⇒ 'al" and Abs_a :: "'al ⇒ 'ar" where td_a: "type_definition Rep_a Abs_a (Collect (Domainp A))" and A_Rep: "A b b' = (b = Rep_a b')" for b b' by (blast dest: ex_type_definition) from assms(6,7) obtain Rep_b :: "'br ⇒ 'bl" and Abs_b :: "'bl ⇒ 'br" where td_b: "type_definition Rep_b Abs_b (Collect (Domainp B))" and B_Rep: "B b b' = (b = Rep_b b')" for b b' by (blast dest: ex_type_definition) from assms(9,10) obtain Rep_c :: "'cr ⇒ 'cl" and Abs_c :: "'cl ⇒ 'cr" where td_c: "type_definition Rep_c Abs_c (Collect (Domainp C))" and C_Rep: "C b b' = (b = Rep_c b')" for b b' by (blast dest: ex_type_definition) define f' where f': "f' = (Rep_a ---> Rep_b ---> Abs_c) f" from td_a td_b td_c have f_closed: "f (Rep_a a) (Rep_b b) ∈ 𝔘C" for a b by (intro closed; simp_all add: assms(2,5,8))+ have rep_abs_c: "y ∈ 𝔘C ⟹ y = Rep_c (Abs_c y)" for y using td_c unfolding type_definition_def by (simp add: assms(8)) have "(A ===> B ===> C) f f'" unfolding f' map_fun_apply by ( intro rel_funI, unfold A_Rep B_Rep C_Rep, elim ssubst, intro rep_abs_c f_closed ) then show ?thesis by auto qed lemma tts_AA_A_transfer: fixes A :: "'a ⇒ 'b ⇒ bool" and f :: "'a ⇒ 'a ⇒ 'a" assumes closed: "⋀a b. ⟦ a ∈ 𝔘; b ∈ 𝔘 ⟧ ⟹ f a b ∈ 𝔘" assumes "Domainp A = (λx. x ∈ 𝔘)" "bi_unique A" "right_total A" shows "∃rcdt. (A ===> A ===> A) f rcdt" using closed by (rule tts_AB_C_transfer[OF _ assms(2-4) assms(2-4) assms(2-4)]) lemma tts_AA_eq_transfer: fixes A :: "'a ⇒ 'b ⇒ bool" and f :: "'a ⇒ 'a ⇒ bool" assumes "Domainp A = (λx. x ∈ 𝔘)" "bi_unique A" "right_total A" shows "∃rcdt. (A ===> A ===> (=)) f rcdt" proof- have closed: "f x y ∈ UNIV" for x y by auto have dom_eq: "Domainp (=) = (λx. x ∈ UNIV)" by auto from tts_AB_C_transfer[ OF _ assms(1-3) assms(1-3) dom_eq bi_unique_eq right_total_eq ] show ?thesis by auto qed lemma Dom_fun_eq_set: assumes "Domainp A = (λx. x ∈ 𝔘A)" "bi_unique A" "right_total A" "Domainp B = (λx. x ∈ 𝔘B)" "bi_unique B" "right_total B" shows "{f. f ` 𝔘A ⊆ 𝔘B} = Collect (Domainp (A ===> B))" proof(standard; (standard, intro CollectI, elim CollectE DomainpE)) fix x assume "x ` 𝔘A ⊆ 𝔘B" from tts_AB_transfer[OF this assms] obtain x' where xx': "(A ===> B) x x'" by clarsimp show "Domainp (A ===> B) x" by standard (rule xx') next fix x b assume "(A ===> B) x b" then show "x ` 𝔘A ⊆ 𝔘B" unfolding rel_fun_def Domainp_eq_Collect[THEN iffD1, OF assms(1)] Domainp_eq_Collect[THEN iffD1, OF assms(4)] by auto qed lemma Dom_AB_eq_pred: assumes "Domainp A = (λx. x ∈ 𝔘A)" "bi_unique A" "right_total A" "Domainp B = (λx. x ∈ 𝔘B)" "bi_unique B" "right_total B" shows "(Domainp (A ===> B) f) = (f ` 𝔘A ⊆ 𝔘B)" using Dom_fun_eq_set[OF assms] by blast end end