(*<*)
(*
 * 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
  "nub⋅lnil = 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_body⋅f⋅lnil = lnil"
| "nub_body⋅f⋅(x :@ xs) = x :@ f⋅(lfilter⋅(neg oo (Λ y. x =_B y))⋅xs)"

lemma nub_nub_body_eq: "nub = fix⋅nub_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
 "} 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]: "SetMem⋅x⋅⊥ = ⊥" by (simp add: SetMem_def)
lemma SetMem_SetEmpty[simp]: "SetMem⋅x⋅SetEmpty = FF"
  by (simp add: SetMem_def SetEmpty_def)
lemma SetMem_SetInsert: "SetMem⋅v⋅(SetInsert⋅x⋅s) = (SetMem⋅v⋅s 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. SetMem⋅x⋅(exceptR⋅r))⋅(resultR⋅r) of
                     lnil → Nothing
                   | x :@ xs → Just⋅(x, R⋅xs⋅(exceptR⋅r)))"

lemma nextR_strict1[simp]: "nextR⋅⊥ = ⊥" by (simp add: nextR_def)
lemma nextR_strict2[simp]: "nextR⋅(R⋅⊥⋅S) = ⊥" by (simp add: nextR_def)

lemma nextR_lnil[simp]: "nextR⋅(R⋅lnil⋅S) = Nothing" by (simp add: nextR_def)

definition
  filterR :: "Nat → R → R" where
  "filterR ≡ (Λ v r. R⋅(resultR⋅r)⋅(SetInsert⋅v⋅(exceptR⋅r)))"

definition
  c2a :: "Nat llist → R" where
  "c2a ≡ Λ xs. R⋅xs⋅SetEmpty"

definition
  a2c :: "R → Nat llist" where
  "a2c ≡ Λ r. lfilter⋅(Λ v. neg⋅(SetMem⋅v⋅(exceptR⋅r)))⋅(resultR⋅r)"

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⋅(c2a⋅xs)"

definition
  unwrap :: "(Nat llist → Nat llist) → R → Nat llist" where
  "unwrap ≡ Λ f r. f⋅(a2c⋅r)"

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) = (neg⋅x andalso neg⋅y)"
  by (rule trE[where p=x], simp_all)

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

lemma case_a2c_case_caseR:
    "(case a2c⋅w of lnil → f | x :@ xs → g⋅x⋅xs)
   = (case nextR⋅w of Nothing → f | Just⋅(x, r) → g⋅x⋅(a2c⋅r))" (is "?lhs = ?rhs")
proof -
  have "?rhs = (case (case ldropWhile⋅(Λ x. SetMem⋅x⋅(exceptR⋅w))⋅(resultR⋅w) of
                     lnil → Nothing
                   | x :@ xs → Just⋅(x, R⋅xs⋅(exceptR⋅w))) of Nothing → f | Just⋅(x, r) → g⋅x⋅(a2c⋅r))"
    by (simp add: nextR_def)
  also have "… = (case ldropWhile⋅(Λ x. SetMem⋅x⋅(exceptR⋅w))⋅(resultR⋅w) of
                     lnil → f | x :@ xs → g⋅x⋅(a2c⋅(R⋅xs⋅(exceptR⋅w))))"
    using case_maybe_case[where L="ldropWhile⋅(Λ x. SetMem⋅x⋅(exceptR⋅w))⋅(resultR⋅w)"
                            and f=f and g="Λ x r. g⋅x⋅(a2c⋅r)" and h="Λ x xs. (x, R⋅xs⋅(exceptR⋅w))"]
    by simp
  also have "… = ?lhs"
    apply (simp add: a2c_def)
    apply (cases "resultR⋅w")
      apply simp_all
    apply (rule_tac p="SetMem⋅a⋅(exceptR⋅w)" in trE)
      apply simp_all
    apply (induct_tac llist)
       apply simp_all
    apply (rule_tac p="SetMem⋅aa⋅(exceptR⋅w)" in trE)
      apply simp_all
    done
  finally show "?lhs = ?rhs" by simp
qed

lemma filter_filterR: "lfilter⋅(neg oo (Λ y. x =_B y))⋅(a2c⋅r) = a2c⋅(filterR⋅x⋅r)"
  using filter_filter[where p="Tr.neg oo (Λ y. x =_B y)" and q="Λ v. Tr.neg⋅(SetMem⋅v⋅(exceptR⋅r))"]
  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
  worker into the right form then apply the lemma.›

definition
  nub_body' :: "(R → Nat llist) → R → Nat llist" where
  "nub_body' ≡ Λ f r. case a2c⋅r 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⋅(SetMem⋅v⋅(exceptR⋅xa)))⋅(resultR⋅xa)"
     , simp_all add: fix_const)

definition
  nub_body'' :: "(R → Nat llist) → R → Nat llist" where
  "nub_body'' ≡ Λ f r. case nextR⋅r of Nothing → lnil
                                      | Just⋅(x, xs) → x :@ f⋅(c2a⋅(lfilter⋅(neg oo (Λ y. x =_B y))⋅(a2c⋅xs)))"

lemma nub_body'_nub_body''_eq: "nub_body' = nub_body''"
proof(rule cfun_eqI)+
  fix f r show "nub_body'⋅f⋅r = nub_body''⋅f⋅r"
    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 nextR⋅r of Nothing → lnil
                                      | Just⋅(x, xs) → x :@ f⋅(filterR⋅x⋅xs))"

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⋅(fix⋅nub_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