(* 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