Theory Applicative_List

(* Author: Joshua Schneider, ETH Zurich *)

subsection ‹Lists›

theory Applicative_List imports
  Applicative
  "HOL-Library.Adhoc_Overloading"
begin

definition "ap_list fs xs = List.bind fs (λf. List.bind xs (λx. [f x]))"

adhoc_overloading Applicative.ap ap_list

lemma Nil_ap[simp]: "ap_list [] xs = []"
unfolding ap_list_def by simp

lemma ap_Nil[simp]: "ap_list fs [] = []"
unfolding ap_list_def by (induction fs) simp_all

lemma ap_list_transfer[transfer_rule]:
  "rel_fun (list_all2 (rel_fun A B)) (rel_fun (list_all2 A) (list_all2 B)) ap_list ap_list"
unfolding ap_list_def[abs_def] List.bind_def
by transfer_prover

context includes applicative_syntax
begin

lemma cons_ap_list: "(f # fs) ⋄ xs = map f xs @ fs ⋄ xs"
unfolding ap_list_def by (induction xs) simp_all

lemma append_ap_distrib: "(fs @ gs) ⋄ xs = fs ⋄ xs @ gs ⋄ xs"
unfolding ap_list_def by (induction fs) simp_all

applicative list
for
  pure: "λx. [x]"
  ap: ap_list
  rel: list_all2
  set: set
proof -
  fix x :: "'a list"
  show "[λx. x] ⋄ x = x" unfolding ap_list_def by (induction x) simp_all
next
  fix g :: "('b ⇒ 'c) list" and f :: "('a ⇒ 'b) list" and x
  let ?B = "λg f x. g (f x)"
  show "[?B] ⋄ g ⋄ f ⋄ x = g ⋄ (f ⋄ x)"
  proof (induction g)
    case Nil show ?case by simp
  next
    case (Cons g gs)
    have g_comp: "[?B g] ⋄ f ⋄ x = [g] ⋄ (f ⋄ x)"
    proof (induction f)
      case Nil show ?case by simp
    next
      case (Cons f fs)
      have "[?B g] ⋄ (f # fs) ⋄ x = [g] ⋄ ([f] ⋄ x) @ [?B g] ⋄ fs ⋄ x"
        by (simp add: cons_ap_list)
      also have "... = [g] ⋄ ([f] ⋄ x) @ [g] ⋄ (fs ⋄ x)" using Cons.IH ..
      also have "... = [g] ⋄ ((f # fs) ⋄ x)" by (simp add: cons_ap_list)
      finally show ?case .
    qed
    have "[?B] ⋄ (g # gs) ⋄ f ⋄ x = [?B g] ⋄ f ⋄ x @ [?B] ⋄ gs ⋄ f ⋄ x"
      by (simp add: cons_ap_list append_ap_distrib)
    also have "... = [g] ⋄ (f ⋄ x) @ gs ⋄ (f ⋄ x)" using g_comp Cons.IH by simp
    also have "... = (g # gs) ⋄ (f ⋄ x)" by (simp add: cons_ap_list)
    finally show ?case .
  qed
next
  fix f :: "('a ⇒ 'b) list" and x
  show "f ⋄ [x] = [λf. f x] ⋄ f" unfolding ap_list_def by simp
next
  fix R :: "'a ⇒ 'b ⇒ bool"
  show "rel_fun R (list_all2 R) (λx. [x]) (λx. [x])" by transfer_prover
next
  fix R and f :: "('a ⇒ 'b) list" and g :: "('a ⇒ 'c) list" and x
  assume [transfer_rule]: "list_all2 (rel_fun (eq_on (set x)) R) f g"
  have [transfer_rule]: "list_all2 (eq_on (set x)) x x" by (simp add: list_all2_same)
  show "list_all2 R (f ⋄ x) (g ⋄ x)" by transfer_prover
qed (simp add: cons_ap_list)

lemma map_ap_conv[applicative_unfold]: "map f x = [f] ⋄ x"
unfolding ap_list_def List.bind_def
by simp

end

end