Theory Last

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

theory Last
imports
  HOLCF
  LList
  WorkerWrapper
begin

(*>*)
section‹Optimise ``last''.›

text‹Andy Gill's solution, mechanised. No fusion, works fine using their rule.›

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

fixrec llast :: "'a llist → 'a"
where
  "llast⋅(x :@ yys) = (case yys of lnil ⇒ x | y :@ ys ⇒ llast⋅yys)"

lemma llast_strict[simp]: "llast⋅⊥ = ⊥"
by fixrec_simp

fixrec llast_body :: "('a llist → 'a) → 'a llist → 'a"
where
  "llast_body⋅f⋅(x :@ yys) = (case yys of lnil ⇒ x | y :@ ys ⇒ f⋅yys)"

lemma llast_llast_body: "llast = fix⋅llast_body"
  by (rule cfun_eqI, subst llast_def, subst llast_body.unfold, simp)

definition wrap :: "('a → 'a llist → 'a) → ('a llist → 'a)" where
  "wrap ≡ Λ f (x :@ xs). f⋅x⋅xs"

definition unwrap :: "('a llist → 'a) → ('a → 'a llist → 'a)" where
  "unwrap ≡ Λ f x xs. f⋅(x :@ xs)"

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

lemma wrap_unwrap_ID: "wrap oo unwrap oo llast_body = llast_body"
  unfolding llast_body_def wrap_def unwrap_def
  apply (rule cfun_eqI)+
  apply (case_tac xa)
  apply (simp_all add: fix_const)
  done

definition llast_worker :: "('a → 'a llist → 'a) → 'a → 'a llist → 'a" where
  "llast_worker ≡ Λ r x yys. case yys of lnil ⇒ x | y :@ ys ⇒ r⋅y⋅ys"

definition llast' :: "'a llist → 'a" where
  "llast' ≡ wrap⋅(fix⋅llast_worker)"

lemma llast_worker_llast_body: "llast_worker = unwrap oo llast_body oo wrap"
  unfolding llast_worker_def llast_body_def wrap_def unwrap_def
  apply (rule cfun_eqI)+
  apply (case_tac xb)
  apply (simp_all add: fix_const)
  done

lemma llast'_llast: "llast' = llast" (is "?lhs = ?rhs")
proof -
  have "?rhs = fix⋅llast_body" by (simp only: llast_llast_body)
  also have "… = wrap⋅(fix⋅(unwrap oo llast_body oo wrap))"
    by (simp only: worker_wrapper_body[OF wrap_unwrap_ID])
  also have "… = wrap⋅(fix⋅(llast_worker))"
    by (simp only: llast_worker_llast_body)
  also have "... = ?lhs" unfolding llast'_def by simp
  finally show ?thesis by simp
qed

end