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