Theory Applicative_DNEList
section ‹Distinct, non-empty list›
theory Applicative_DNEList imports
Applicative_List
"HOL-Library.Dlist"
begin
lemma bind_eq_Nil_iff [simp]: "List.bind xs f = [] ⟷ (∀x∈set xs. f x = [])"
by(simp add: List.bind_def)
lemma zip_eq_Nil_iff [simp]: "zip xs ys = [] ⟷ xs = [] ∨ ys = []"
by(cases xs ys rule: list.exhaust[case_product list.exhaust]) simp_all
lemma remdups_append1: "remdups (remdups xs @ ys) = remdups (xs @ ys)"
by(induction xs) simp_all
lemma remdups_append2: "remdups (xs @ remdups ys) = remdups (xs @ ys)"
by(induction xs) simp_all
lemma remdups_append1_drop: "set xs ⊆ set ys ⟹ remdups (xs @ ys) = remdups ys"
by(induction xs) auto
lemma remdups_concat_map: "remdups (concat (map remdups xss)) = remdups (concat xss)"
by(induction xss)(simp_all add: remdups_append1, metis remdups_append2)
lemma remdups_concat_remdups: "remdups (concat (remdups xss)) = remdups (concat xss)"
apply(induction xss)
apply(auto simp add: remdups_append1_drop)
apply(subst remdups_append1_drop; auto)
apply(metis remdups_append2)
done
lemma remdups_replicate: "remdups (replicate n x) = (if n = 0 then [] else [x])"
by(induction n) simp_all
typedef 'a dnelist = "{xs::'a list. distinct xs ∧ xs ≠ []}"
morphisms list_of_dnelist Abs_dnelist
proof
show "[x] ∈ ?dnelist" for x by simp
qed
setup_lifting type_definition_dnelist
lemma dnelist_subtype_dlist:
"type_definition (λx. Dlist (list_of_dnelist x)) (λx. Abs_dnelist (list_of_dlist x)) {xs. xs ≠ Dlist.empty}"
apply unfold_locales
subgoal by(transfer; auto simp add: dlist_eq_iff)
subgoal by(simp add: distinct_remdups_id dnelist.list_of_dnelist[simplified] list_of_dnelist_inverse)
subgoal by(simp add: dlist_eq_iff Abs_dnelist_inverse)
done
lift_bnf (no_warn_transfer, no_warn_wits) 'a dnelist via dnelist_subtype_dlist for map: map
by(auto simp: dlist_eq_iff)
hide_const (open) map
context begin
qualified lemma map_def: "Applicative_DNEList.map = map_fun id (map_fun list_of_dnelist Abs_dnelist) (λf xs. remdups (list.map f xs))"
unfolding map_def by(simp add: fun_eq_iff distinct_remdups_id list_of_dnelist[simplified])
qualified lemma map_transfer [transfer_rule]:
"rel_fun (=) (rel_fun (pcr_dnelist (=)) (pcr_dnelist (=))) (λf xs. remdups (map f xs)) Applicative_DNEList.map"
by(simp add: map_def rel_fun_def dnelist.pcr_cr_eq cr_dnelist_def list_of_dnelist[simplified] Abs_dnelist_inverse)
qualified lift_definition single :: "'a ⇒ 'a dnelist" is "λx. [x]" by simp
qualified lift_definition insert :: "'a ⇒ 'a dnelist ⇒ 'a dnelist" is "λx xs. if x ∈ set xs then xs else x # xs" by auto
qualified lift_definition append :: "'a dnelist ⇒ 'a dnelist ⇒ 'a dnelist" is "λxs ys. remdups (xs @ ys)" by auto
qualified lift_definition bind :: "'a dnelist ⇒ ('a ⇒ 'b dnelist) ⇒ 'b dnelist" is "λxs f. remdups (List.bind xs f)" by auto
abbreviation (input) pure_dnelist :: "'a ⇒ 'a dnelist"
where "pure_dnelist ≡ single"
end
lift_definition ap_dnelist :: "('a ⇒ 'b) dnelist ⇒ 'a dnelist ⇒ 'b dnelist"
is "λf x. remdups (ap_list f x)"
by(auto simp add: ap_list_def)
adhoc_overloading Applicative.ap ap_dnelist
lemma ap_pure_list [simp]: "ap_list [f] xs = map f xs"
by(simp add: ap_list_def List.bind_def)
context includes applicative_syntax
begin
lemma ap_pure_dlist: "pure_dnelist f ⋄ x = Applicative_DNEList.map f x"
by transfer simp
applicative dnelist (K)
for pure: pure_dnelist
ap: ap_dnelist
proof -
show "pure_dnelist (λx. x) ⋄ x = x" for x :: "'a dnelist"
by transfer simp
have *: "remdups (remdups (remdups ([λg f x. g (f x)] ⋄ g) ⋄ f) ⋄ x) = remdups (g ⋄ remdups (f ⋄ x))"
(is "?lhs = ?rhs") for g :: "('b ⇒ 'c) list" and f :: "('a ⇒ 'b) list" and x
proof -
have "?lhs = remdups (concat (map (λf. map f x) (remdups (concat (map (λx. map (λf y. x (f y)) f) g)))))"
unfolding ap_list_def List.bind_def
by(subst (2) remdups_concat_remdups[symmetric])(simp add: o_def remdups_map_remdups remdups_concat_remdups)
also have "… = remdups (concat (map (λf. map f x) (concat (map (λx. map (λf y. x (f y)) f) g))))"
by(subst (1) remdups_concat_remdups[symmetric])(simp add: remdups_map_remdups remdups_concat_remdups)
also have "… = remdups (concat (map remdups (map (λg. map g (concat (map (λf. map f x) f))) g)))"
using list.pure_B_conv[of g f x] unfolding remdups_concat_map
by(simp add: ap_list_def List.bind_def o_def)
also have "… = ?rhs" unfolding ap_list_def List.bind_def
by(subst (2) remdups_concat_map[symmetric])(simp add: o_def remdups_map_remdups)
finally show ?thesis .
qed
show "pure_dnelist (λg f x. g (f x)) ⋄ g ⋄ f ⋄ x = g ⋄ (f ⋄ x)"
for g :: "('b ⇒ 'c) dnelist" and f :: "('a ⇒ 'b) dnelist" and x
by transfer(rule *)
show "pure_dnelist f ⋄ pure_dnelist x = pure_dnelist (f x)" for f :: "'a ⇒ 'b" and x
by transfer simp
show "f ⋄ pure_dnelist x = pure_dnelist (λf. f x) ⋄ f" for f :: "('a ⇒ 'b) dnelist" and x
by transfer(simp add: list.interchange)
have *: "remdups (remdups ([λx y. x] ⋄ x) ⋄ y) = x" if x: "distinct x" and y: "distinct y" "y ≠ []"
for x :: "'b list" and y :: "'a list"
proof -
have "remdups (map (λ(x :: 'b) (y :: 'a). x) x) = map (λ(x :: 'b) (y :: 'a). x) x"
using that by(simp add: distinct_map inj_on_def fun_eq_iff)
hence "remdups (remdups ([λx y. x] ⋄ x) ⋄ y) = remdups (concat (map (λf. map f y) (map (λx y. x) x)))"
by(simp add: ap_list_def List.bind_def del: remdups_id_iff_distinct)
also have "… = x" using that
by(simp add: o_def map_replicate_const)(subst remdups_concat_map[symmetric], simp add: o_def remdups_replicate)
finally show ?thesis .
qed
show "pure_dnelist (λx y. x) ⋄ x ⋄ y = x"
for x :: "'b dnelist" and y :: "'a dnelist"
by transfer(rule *; simp)
qed
text ‹@{typ "_ dnelist"} does not have combinator C, so it cannot have W either.›
context begin
private lift_definition x :: "int dnelist" is "[2,3]" by simp
private lift_definition y :: "int dnelist" is "[5,7]" by simp
private lemma "pure_dnelist (λf x y. f y x) ⋄ pure_dnelist ((*)) ⋄ x ⋄ y ≠ pure_dnelist ((*)) ⋄ y ⋄ x"
by transfer(simp add: ap_list_def fun_eq_iff)
end
end
end