Theory Applicative_Set
subsection ‹Set with Cartesian product›
theory Applicative_Set imports
Applicative
"HOL-Library.Adhoc_Overloading"
begin
definition ap_set :: "('a ⇒ 'b) set ⇒ 'a set ⇒ 'b set"
where "ap_set F X = {f x | f x. f ∈ F ∧ x ∈ X}"
adhoc_overloading Applicative.ap ap_set
lemma ap_set_transfer[transfer_rule]:
"rel_fun (rel_set (rel_fun A B)) (rel_fun (rel_set A) (rel_set B)) ap_set ap_set"
unfolding ap_set_def[abs_def] rel_set_def
by (fastforce elim: rel_funE)
applicative set (C)
for
pure: "λx. {x}"
ap: ap_set
rel: rel_set
set: "λx. x"
proof -
fix R :: "'a ⇒ 'b ⇒ bool"
show "rel_fun R (rel_set R) (λx. {x}) (λx. {x})" by (auto intro: rel_setI)
next
fix R and f :: "('a ⇒ 'b) set" and g :: "('a ⇒ 'c) set" and x
assume [transfer_rule]: "rel_set (rel_fun (eq_on x) R) f g"
have [transfer_rule]: "rel_set (eq_on x) x x" by (auto intro: rel_setI)
show "rel_set R (ap_set f x) (ap_set g x)" by transfer_prover
qed (unfold ap_set_def, fast+)
end