# Theory Applicative_List

theory Applicative_List
```(* Author: Joshua Schneider, ETH Zurich *)

subsection ‹Lists›

theory Applicative_List imports
Applicative
begin

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

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