# Theory Applicative

theory Applicative
imports Main
```(* 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

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 =
"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"

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

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

hide_const (open) ap

end
```