Theory Nub

(*<*)
(*
 * The worker/wrapper transformation, following Gill and Hutton.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Nub
imports
  HOLCF
  LList
  Maybe
  Nats
  WorkerWrapperNew
begin
(*>*)

section‹Transforming $O(n^2)$ \emph{nub} into an $O(n\lg n)$ one›

text‹Andy Gill's solution, mechanised.›

subsection‹The @{term "nub"} function.›

fixrec nub :: "Nat llist  Nat llist"
where
  "nublnil = lnil"
| "nub(x :@ xs) = x :@ nub(lfilter(neg oo (Λ y. x =B y))xs)"

lemma nub_strict[simp]: "nub = "
by fixrec_simp

fixrec nub_body :: "(Nat llist  Nat llist)  Nat llist  Nat llist"
where
  "nub_bodyflnil = lnil"
| "nub_bodyf(x :@ xs) = x :@ f(lfilter(neg oo (Λ y. x =B y))xs)"

lemma nub_nub_body_eq: "nub = fixnub_body"
  by (rule cfun_eqI, subst nub_def, subst nub_body.unfold, simp)

(* **************************************** *)

subsection‹Optimised data type.›

text ‹Implement sets using lazy lists for now. Lifting up HOL's @{typ "'a
set"} type causes continuity grief.›

type_synonym NatSet = "Nat llist"

definition
  SetEmpty :: "NatSet" where
  "SetEmpty  lnil"

definition
  SetInsert :: "Nat  NatSet  NatSet" where
  "SetInsert  lcons"

definition
  SetMem :: "Nat  NatSet  tr" where
  "SetMem  lmember(bpred (=))"

lemma SetMem_strict[simp]: "SetMemx = " by (simp add: SetMem_def)
lemma SetMem_SetEmpty[simp]: "SetMemxSetEmpty = FF"
  by (simp add: SetMem_def SetEmpty_def)
lemma SetMem_SetInsert: "SetMemv(SetInsertxs) = (SetMemvs orelse x =B v)"
  by (simp add: SetMem_def SetInsert_def)

text ‹AndyG's new type.›

domain R = R (lazy resultR :: "Nat llist") (lazy exceptR :: "NatSet")

definition
  nextR :: "R  (Nat * R) Maybe" where
  "nextR = (Λ r. case ldropWhile(Λ x. SetMemx(exceptRr))(resultRr) of
                     lnil  Nothing
                   | x :@ xs  Just(x, Rxs(exceptRr)))"

lemma nextR_strict1[simp]: "nextR = " by (simp add: nextR_def)
lemma nextR_strict2[simp]: "nextR(RS) = " by (simp add: nextR_def)

lemma nextR_lnil[simp]: "nextR(RlnilS) = Nothing" by (simp add: nextR_def)

definition
  filterR :: "Nat  R  R" where
  "filterR  (Λ v r. R(resultRr)(SetInsertv(exceptRr)))"

definition
  c2a :: "Nat llist  R" where
  "c2a  Λ xs. RxsSetEmpty"

definition
  a2c :: "R  Nat llist" where
  "a2c  Λ r. lfilter(Λ v. neg(SetMemv(exceptRr)))(resultRr)"

lemma a2c_strict[simp]: "a2c = " unfolding a2c_def by simp

lemma a2c_c2a_id: "a2c oo c2a = ID"
  by (rule cfun_eqI, simp add: a2c_def c2a_def lfilter_const_true)

definition
  wrap :: "(R  Nat llist)  Nat llist  Nat llist" where
  "wrap  Λ f xs. f(c2axs)"

definition
  unwrap :: "(Nat llist  Nat llist)  R  Nat llist" where
  "unwrap  Λ f r. f(a2cr)"

lemma unwrap_strict[simp]: "unwrap = "
  unfolding unwrap_def by (rule cfun_eqI, simp)

lemma wrap_unwrap_id: "wrap oo unwrap = ID"
  using cfun_fun_cong[OF a2c_c2a_id]
  by - ((rule cfun_eqI)+, simp add: wrap_def unwrap_def)

text ‹Equivalences needed for later.›

lemma TR_deMorgan: "neg(x orelse y) = (negx andalso negy)"
  by (rule trE[where p=x], simp_all)

lemma case_maybe_case:
  "(case (case L of lnil  Nothing | x :@ xs  Just(hxxs)) of
     Nothing  f | Just(a, b)  gab)
   =
   (case L of lnil  f | x :@ xs  g(fst (hxxs))(snd (hxxs)))"
  apply (cases L, simp_all)
  apply (case_tac "hallist")
  apply simp
  done

lemma case_a2c_case_caseR:
    "(case a2cw of lnil  f | x :@ xs  gxxs)
   = (case nextRw of Nothing  f | Just(x, r)  gx(a2cr))" (is "?lhs = ?rhs")
proof -
  have "?rhs = (case (case ldropWhile(Λ x. SetMemx(exceptRw))(resultRw) of
                     lnil  Nothing
                   | x :@ xs  Just(x, Rxs(exceptRw))) of Nothing  f | Just(x, r)  gx(a2cr))"
    by (simp add: nextR_def)
  also have " = (case ldropWhile(Λ x. SetMemx(exceptRw))(resultRw) of
                     lnil  f | x :@ xs  gx(a2c(Rxs(exceptRw))))"
    using case_maybe_case[where L="ldropWhile(Λ x. SetMemx(exceptRw))(resultRw)"
                            and f=f and g="Λ x r. gx(a2cr)" and h="Λ x xs. (x, Rxs(exceptRw))"]
    by simp
  also have " = ?lhs"
    apply (simp add: a2c_def)
    apply (cases "resultRw")
      apply simp_all
    apply (rule_tac p="SetMema(exceptRw)" in trE)
      apply simp_all
    apply (induct_tac llist)
       apply simp_all
    apply (rule_tac p="SetMemaa(exceptRw)" in trE)
      apply simp_all
    done
  finally show "?lhs = ?rhs" by simp
qed

lemma filter_filterR: "lfilter(neg oo (Λ y. x =B y))(a2cr) = a2c(filterRxr)"
  using filter_filter[where p="Tr.neg oo (Λ y. x =B y)" and q="Λ v. Tr.neg(SetMemv(exceptRr))"]
  unfolding a2c_def filterR_def
  by (cases r, simp_all add: SetMem_SetInsert TR_deMorgan)

text‹Apply worker/wrapper. Unlike Gill/Hutton, we manipulate the body of
the worker into the right form then apply the lemma.›

definition
  nub_body' :: "(R  Nat llist)  R  Nat llist" where
  "nub_body'  Λ f r. case a2cr of lnil  lnil
                                   | x :@ xs  x :@ f(c2a(lfilter(neg oo (Λ y. x =B y))xs))"

lemma nub_body_nub_body'_eq: "unwrap oo nub_body oo wrap = nub_body'"
  unfolding nub_body_def nub_body'_def unwrap_def wrap_def a2c_def c2a_def
  by ((rule cfun_eqI)+
     , case_tac "lfilter(Λ v. Tr.neg(SetMemv(exceptRxa)))(resultRxa)"
     , simp_all add: fix_const)

definition
  nub_body'' :: "(R  Nat llist)  R  Nat llist" where
  "nub_body''  Λ f r. case nextRr of Nothing  lnil
                                      | Just(x, xs)  x :@ f(c2a(lfilter(neg oo (Λ y. x =B y))(a2cxs)))"

lemma nub_body'_nub_body''_eq: "nub_body' = nub_body''"
proof(rule cfun_eqI)+
  fix f r show "nub_body'fr = nub_body''fr"
    unfolding nub_body'_def nub_body''_def
    using case_a2c_case_caseR[where f="lnil" and g="Λ x xs. x :@ f(c2a(lfilter(Tr.neg oo (Λ y. x =B y))xs))" and w="r"]
    by simp
qed

definition
  nub_body''' :: "(R  Nat llist)  R  Nat llist" where
  "nub_body'''  (Λ f r. case nextRr of Nothing  lnil
                                      | Just(x, xs)  x :@ f(filterRxxs))"

lemma nub_body''_nub_body'''_eq: "nub_body'' = nub_body''' oo (unwrap oo wrap)"
  unfolding nub_body''_def nub_body'''_def wrap_def unwrap_def
  by ((rule cfun_eqI)+, simp add: filter_filterR)

text‹Finally glue it all together.›

lemma nub_wrap_nub_body''': "nub = wrap(fixnub_body''')"
  using worker_wrapper_fusion_new[OF wrap_unwrap_id unwrap_strict, where body=nub_body]
        nub_nub_body_eq
        nub_body_nub_body'_eq
        nub_body'_nub_body''_eq
        nub_body''_nub_body'''_eq
  by simp

end