Theory ETTS_Auxiliary
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