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