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  llastyys)"

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

fixrec llast_body :: "('a llist  'a)  'a llist  'a"
where
  "llast_bodyf(x :@ yys) = (case yys of lnil  x | y :@ ys  fyys)"

lemma llast_llast_body: "llast = fixllast_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). fxxs"

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  ryys"

definition llast' :: "'a llist  'a" where
  "llast'  wrap(fixllast_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 = fixllast_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