Theory Applicative_Lifting.Applicative_Set

(* Author: Joshua Schneider, ETH Zurich *)

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