Theory FixedPointTheorems

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

theory FixedPointTheorems
imports
  HOLCF
begin

setup ‹
  Document_Output.antiquotation_raw \<^binding>‹haskell› (Scan.lift Args.name)
    (fn _ => fn s => Latex.string ("\\" ^ "<" ^ s ^ "\\>"))
›

(* LaTeXsugar fights with HOLCF syntax: at least cdot *)

(* THEOREMS *)
notation (Rule output)
  Pure.imp  ("\<^latex>‹\\mbox{}\\inferrule{\\mbox{›_\<^latex>‹}}›\<^latex>‹{\\mbox{›_\<^latex>‹}}›")

syntax (Rule output)
  "_bigimpl" :: "asms ⇒ prop ⇒ prop"
  ("\<^latex>‹\\mbox{}\\inferrule{›_\<^latex>‹}›\<^latex>‹{\\mbox{›_\<^latex>‹}}›")

  "_asms" :: "prop ⇒ asms ⇒ asms"
  ("\<^latex>‹\\mbox{›_\<^latex>‹}\\\\›/ _")

  "_asm" :: "prop ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}›")

(*>*)
section‹Fixed-point theorems for program transformation›

text‹

We begin by recounting some standard theorems from the early days of
denotational semantics. The origins of these results are lost to
history; the interested reader can find some of it in
\<^citet>‹"Bekic:1969" and "Manna:1974" and "Greibach:1975" and "Stoy:1977" and "DBLP:books/daglib/0002432" and "Harel:1980" and "Plotkin:1983" and "Winskel:1993" and "DBLP:journals/toplas/Sangiorgi09"›.

›

subsection‹The rolling rule›

text‹

The \emph{rolling rule} captures what intuitively happens when we
re-order a recursive computation consisting of two parts. This theorem
dates from the 1970s at the latest -- see \<^citet>‹‹p210› in "Stoy:1977"› and
\<^citet>‹"Plotkin:1983"›. The following proofs were provided by
\<^citet>‹"GillHutton:2009"›.

›

lemma rolling_rule_ltr: "fix⋅(g oo f) ⊑ g⋅(fix⋅(f oo g))"
proof -
  have "g⋅(fix⋅(f oo g)) ⊑ g⋅(fix⋅(f oo g))"
    by (rule below_refl) ― ‹reflexivity›
  hence "g⋅((f oo g)⋅(fix⋅(f oo g))) ⊑ g⋅(fix⋅(f oo g))"
    using fix_eq[where F="f oo g"] by simp ― ‹computation›
  hence "(g oo f)⋅(g⋅(fix⋅(f oo g))) ⊑ g⋅(fix⋅(f oo g))"
    by simp ― ‹re-associate @{term "(oo)"}›
  thus "fix⋅(g oo f) ⊑ g⋅(fix⋅(f oo g))"
    using fix_least_below by blast ― ‹induction›
qed

lemma rolling_rule_rtl: "g⋅(fix⋅(f oo g)) ⊑ fix⋅(g oo f)"
proof -
  have "fix⋅(f oo g) ⊑ f⋅(fix⋅(g oo f))" by (rule rolling_rule_ltr)
  hence "g⋅(fix⋅(f oo g)) ⊑ g⋅(f⋅(fix⋅(g oo f)))"
    by (rule monofun_cfun_arg) ― ‹g is monotonic›
  thus "g⋅(fix⋅(f oo g)) ⊑ fix⋅(g oo f)"
    using fix_eq[where F="g oo f"] by simp ― ‹computation›
qed

lemma rolling_rule: "fix⋅(g oo f) = g⋅(fix⋅(f oo g))"
  by (rule below_antisym[OF rolling_rule_ltr rolling_rule_rtl])
(*

This property of a fixed-point operator is termed \emph{dinaturality}
by \citet{DBLP:conf/lics/SimpsonP00}.

*)

subsection‹Least-fixed-point fusion›

text‹

\label{sec:lfp-fusion}

\emph{Least-fixed-point fusion} provides a kind of induction that has
proven to be very useful in calculational settings. Intuitively it
lifts the step-by-step correspondence between @{term "f"} and @{term
"h"} witnessed by the strict function @{term "g"} to the fixed points
of @{term "f"} and @{term "g"}:
\[
  \begin{diagram}
    \node{\bullet} \arrow{e,t}{h} \node{\bullet}\\
    \node{\bullet} \arrow{n,l}{g} \arrow{e,b}{f} \node{\bullet} \arrow{n,r}{g}
  \end{diagram}
  \qquad \Longrightarrow \qquad
  \begin{diagram}
    \node{\mathsf{fix}\ h}\\
    \node{\mathsf{fix}\ f} \arrow{n,r}{g}
  \end{diagram}
\]
\citet*{FokkingaMeijer:1991}, and also their later
\citet*{barbed-wire:1991}, made extensive use of this rule, as did
\<^citet>‹"Tullsen:PhDThesis"› in his program transformation tool PATH.
This diagram is strongly reminiscent of the simulations used to
establish refinement relations between imperative programs and their
specifications \citep*{EdR:cup98}.

The following proof is close to the third variant of
\<^citet>‹‹p215› in "Stoy:1977"›. We relate the two fixpoints using the rule
\texttt{parallel\_fix\_ind}:
\begin{center}
  @{thm[mode=Rule] parallel_fix_ind}
\end{center}
in a very straightforward way:

›

lemma lfp_fusion:
  assumes "g⋅⊥ = ⊥"
  assumes "g oo f = h oo g"
  shows "g⋅(fix⋅f) = fix⋅h"
proof(induct rule: parallel_fix_ind)
  case 2 show "g⋅⊥ = ⊥" by fact
  case (3 x y)
  from ‹g⋅x = y› ‹g oo f = h oo g› show "g⋅(f⋅x) = h⋅y"
    by (simp add: cfun_eq_iff)
qed simp

text‹

This lemma also goes by the name of \emph{Plotkin's axiom}
\<^citep>‹"PittsAM:relpod"› or \emph{uniformity}
\<^citep>‹"DBLP:conf/lics/SimpsonP00"›.

›
(*<*)

(* The rest of this theory is only of historical interest. *)

text ‹Some may find the pointed version easier to read.›

lemma lfp_fusion_pointed:
  assumes Cfg: "⋀f. C⋅(F⋅f) = G⋅(C⋅f)"
      and strictC: "C⋅⊥ = ⊥"
  shows "C⋅(fix⋅F) = fix⋅G"
  using lfp_fusion[where f=F and g=C and h=G] assms
  by (simp add: cfcomp1)

subsubsection‹More about ‹lfp-fusion››

text‹

Alternative proofs. This is the ``intuitive'' one
\<^citet>‹‹p125› in "Gunter:1992"› and \<^citet>‹‹p46› in "Tullsen:PhDThesis"›, where we
can shuffle @{term "g"} to the end of the the iteration of @{term "f"}
using @{term "fgh"}.

›

lemma lfp_fusion2_aux:
  assumes fgh: "g oo f = h oo g"
  shows "g⋅(iterate i⋅f⋅⊥) = iterate i⋅h⋅(g⋅⊥)"
proof(induct i)
  case (Suc i)
  have "g⋅(iterate (Suc i)⋅f⋅⊥) = (g oo f)⋅(iterate i⋅f⋅⊥)" by simp
  also have "... = h⋅(g⋅(iterate i⋅f⋅⊥))" using fgh by (simp add: cfcomp1)
  also have "... = h⋅(iterate i⋅h⋅(g⋅⊥))" using Suc by simp
  also have "... = iterate (Suc i)⋅h⋅(g⋅⊥)" by simp
  finally show ?case .
qed simp

lemma lfp_fusion2:
  assumes fgh: "g oo f = h oo g"
      and strictg: "g⋅⊥ = ⊥"
  shows "g⋅(fix⋅f) = fix⋅h"
proof -
  have "g⋅(fix⋅f) = g⋅(⨆i. iterate i⋅f⋅⊥)" by (simp only: fix_def2)
  also have "... = (⨆i. g⋅(iterate i⋅f⋅⊥))" by (simp add: contlub_cfun_arg)
  also have "... = (⨆i. (iterate i⋅h⋅(g⋅⊥)))" by (simp only: lfp_fusion2_aux[OF fgh])
  also have "... = fix⋅h" using strictg by (simp only: fix_def2)
  finally show ?thesis .
qed

text‹This is the first one by \<^citet>‹‹p213› in "Stoy:1977"›, almost
identical to the above.›

lemma lfp_fusion3_aux:
  assumes fgh: "g oo f = h oo g"
      and strictg: "g⋅⊥ = ⊥"
  shows "g⋅(iterate i⋅f⋅⊥) = iterate i⋅h⋅⊥"
proof(induct i)
  case 0 from strictg show ?case by simp
next
  case (Suc i)
  have "g⋅(iterate (Suc i)⋅f⋅⊥) = (g oo f)⋅(iterate i⋅f⋅⊥)" by simp
  also have "... = h⋅(g⋅(iterate i⋅f⋅⊥))" using fgh by (simp add: cfcomp1)
  also have "... = h⋅(iterate i⋅h⋅⊥)" using Suc by simp
  also have "... = iterate (Suc i)⋅h⋅⊥" by simp
  finally show ?case .
qed

lemma lfp_fusion3:
  assumes fgh: "g oo f = h oo g"
      and strictg: "g⋅⊥ = ⊥"
  shows "g⋅(fix⋅f) = fix⋅h"
proof -
  have "g⋅(fix⋅f) = g⋅(⨆i. iterate i⋅f⋅⊥)" by (simp only: fix_def2)
  also have "... = (⨆i. g⋅(iterate i⋅f⋅⊥))" by (simp add: contlub_cfun_arg)
  also have "... = (⨆i. (iterate i⋅h⋅⊥))" by (simp only: lfp_fusion3_aux[OF fgh strictg])
  also have "... = fix⋅h" by (simp only: fix_def2)
  finally show ?thesis .
qed

text‹Stoy's second proof \<^citep>‹‹p214› in "Stoy:1977"› is similar to the
original proof using fixed-point induction.›

lemma lfp_fusion4:
  assumes fgh: "g oo f = h oo g"
      and strictg: "g⋅⊥ = ⊥"
  shows "g⋅(fix⋅f) = fix⋅h"
proof(rule below_antisym)
  show "fix⋅h ⊑ g⋅(fix⋅f)"
  proof -
    have "h⋅(g⋅(fix⋅f)) = (g oo f)⋅(fix⋅f)" using fgh by simp
    also have "... = g⋅(fix⋅f)" by (subst fix_eq, simp)
    finally show ?thesis by (rule fix_least)
  qed
  let ?P = "λx. g⋅x ⊑ fix⋅h"
  show "?P (fix⋅f)"
  proof(induct rule: fix_ind[where P="?P"])
    case 2 with strictg show ?case by simp
  next
    case (3 x) hence indhyp: "g⋅x ⊑ fix⋅h" .
    have "g⋅(f⋅x) = (h oo g)⋅x" using fgh[symmetric] by simp
    with indhyp show "g⋅(f⋅x) ⊑ fix⋅h"
      by (subst fix_eq, simp add: monofun_cfun)
  qed simp
qed

text‹A wrinkly variant from \<^citet>‹‹p11› in "barbed-wire:1991"›.›

lemma lfp_fusion_barbed_variant:
  assumes ff': "f⋅⊥ = f'⋅⊥"
      and fgh: "f oo g = h oo f"
      and f'g'h: "f' oo g' = h oo f'"
  shows "f⋅(fix⋅g) = f'⋅(fix⋅g')"
proof(induct rule: parallel_fix_ind)
  case 2 show "f⋅⊥ = f'⋅⊥" by (rule ff')
  case (3 x y)
  from ‹f⋅x = f'⋅y› have "h⋅(f⋅x) = h⋅(f'⋅y)" by simp
  with fgh f'g'h have "f⋅(g⋅x) = f'⋅(g'⋅y)"
    using cfcomp2[where f="f" and g="g", symmetric]
          cfcomp2[where f="f'" and g="g'", symmetric]
    by simp
  thus ?case by simp
qed simp
(*>*)

(*<*)
end
(*>*)