Theory Applicative_Lifting.Applicative

(* Author: Joshua Schneider, ETH Zurich *)

section ‹Lifting with applicative functors›

theory Applicative
imports Main
keywords "applicative" :: thy_goal and "print_applicative" :: diag
begin

subsection ‹Equality restricted to a set›

definition eq_on :: "'a set  'a  'a  bool"
where [simp]: "eq_on A = (λx y. x  A  x = y)"

lemma rel_fun_eq_onI: "(x. x  A  R (f x) (g x))  rel_fun (eq_on A) R f g"
by auto

lemma rel_fun_map_fun2: "rel_fun (eq_on (range h)) A f g  rel_fun (BNF_Def.Grp UNIV h)¯¯ A f (map_fun h id g)"
  by(auto simp add: rel_fun_def Grp_def eq_onp_def)

lemma rel_fun_refl_eq_onp:
  "(z. z  f ` X  A z z)  rel_fun (eq_on X) A f f"
  by(auto simp add: rel_fun_def eq_onp_def)

lemma eq_onE: " eq_on X a b;  b  X; a = b   thesis   thesis" by auto

lemma Domainp_eq_on [simp]: "Domainp (eq_on X) = (λx. x  X)"
  by auto

subsection ‹Proof automation›

lemma arg1_cong: "x = y  f x z = f y z"
by (rule arg_cong)

lemma UNIV_E: "x  UNIV  P  P" .

context begin

private named_theorems combinator_unfold
private named_theorems combinator_repr

private definition "B g f x  g (f x)"
private definition "C f x y  f y x"
private definition "I x  x"
private definition "K x y  x"
private definition "S f g x  (f x) (g x)"
private definition "T x f  f x"
private definition "W f x  f x x"

lemmas [abs_def, combinator_unfold] = B_def C_def I_def K_def S_def T_def W_def
lemmas [combinator_repr] = combinator_unfold

private definition "cpair  Pair"
private definition "cuncurry  case_prod"

private lemma uncurry_pair: "cuncurry f (cpair x y) = f x y"
unfolding cpair_def cuncurry_def by simp

ML_file "applicative.ML"

local_setup Applicative.setup_combinators
 [("B", @{thm B_def}),
  ("C", @{thm C_def}),
  ("I", @{thm I_def}),
  ("K", @{thm K_def}),
  ("S", @{thm S_def}),
  ("T", @{thm T_def}),
  ("W", @{thm W_def})]

private attribute_setup combinator_eq =
  Scan.lift (Scan.option (Args.$$$ "weak" |--
    Scan.optional (Args.colon |-- Scan.repeat1 Args.name) []) >>
    Applicative.combinator_rule_attrib)

lemma [combinator_eq]: "B  S (K S) K" unfolding combinator_unfold .
lemma [combinator_eq]: "C  S (S (K (S (K S) K)) S) (K K)" unfolding combinator_unfold .
lemma [combinator_eq]: "I  W K" unfolding combinator_unfold .
lemma [combinator_eq]: "I  C K ()" unfolding combinator_unfold .
lemma [combinator_eq]: "S  B (B W) (B B C)" unfolding combinator_unfold .
lemma [combinator_eq]: "T  C I" unfolding combinator_unfold .
lemma [combinator_eq]: "W  S S (S K)" unfolding combinator_unfold .

lemma [combinator_eq weak: C]:
  "C  C (B B (B B (B W (C (B C (B (B B) (C B (cuncurry (K I))))) (cuncurry K))))) cpair"
unfolding combinator_unfold uncurry_pair .

end (* context *)


method_setup applicative_unfold =
  Applicative.parse_opt_afun >> (fn opt_af => fn ctxt =>
    SIMPLE_METHOD' (Applicative.unfold_wrapper_tac ctxt opt_af))
  "unfold into an applicative expression"

method_setup applicative_fold =
  Applicative.parse_opt_afun >> (fn opt_af => fn ctxt =>
    SIMPLE_METHOD' (Applicative.fold_wrapper_tac ctxt opt_af))
  "fold an applicative expression"

method_setup applicative_nf =
  Applicative.parse_opt_afun >> (fn opt_af => fn ctxt =>
    SIMPLE_METHOD' (Applicative.normalize_wrapper_tac ctxt opt_af))
  "prove an equation that has been lifted to an applicative functor, using normal forms"

method_setup applicative_lifting =
  Applicative.parse_opt_afun >> (fn opt_af => fn ctxt =>
    SIMPLE_METHOD' (Applicative.lifting_wrapper_tac ctxt opt_af))
  "prove an equation that has been lifted to an applicative functor"

ML Outer_Syntax.local_theory_to_proof @{command_keyword "applicative"}
  "register applicative functors"
  (Parse.binding --
    Scan.optional (@{keyword "("} |-- Parse.list Parse.short_ident --| @{keyword ")"}) [] --
    (@{keyword "for"} |-- Parse.reserved "pure" |-- @{keyword ":"} |-- Parse.term) --
    (Parse.reserved "ap" |-- @{keyword ":"} |-- Parse.term) --
    Scan.option (Parse.reserved "rel" |-- @{keyword ":"} |-- Parse.term) --
    Scan.option (Parse.reserved "set" |-- @{keyword ":"} |-- Parse.term) >>
    Applicative.applicative_cmd)

ML Outer_Syntax.command @{command_keyword "print_applicative"}
  "print registered applicative functors"
  (Scan.succeed (Toplevel.keep (Applicative.print_afuns o Toplevel.context_of)))

attribute_setup applicative_unfold =
  Scan.lift (Scan.option Parse.name >> Applicative.add_unfold_attrib)
  "register rules for unfolding into applicative expressions"

attribute_setup applicative_lifted =
  Scan.lift (Parse.name >> Applicative.forward_lift_attrib)
  "lift an equation to an applicative functor"


subsection ‹Overloaded applicative operators›

consts
  pure :: "'a  'b"
  ap :: "'a  'b  'c"

bundle applicative_syntax
begin
  notation ap (infixl "" 70)
end

hide_const (open) ap

end