Theory Applicative
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
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