Theory Applicative_DNEList

(* Author: Andreas Lochbihler, ETH Zurich *)

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