(*

 A partial mechanisation of Gibbons/Hutton "Proof methods for co-recursive
 programs" 2005.

 I began with trying to understand how the Bird/Wadler-popularised "take
 lemma" works on infinite lists, and found this paper easy to follow. (In
 brief: there's no mystery, continuity does the job. The lemmata are cute as
 they reflect the information order of the data type into the term language
 of the logic. This would have been quite helpful in the LCF days.)

 Note that the HOLCF domain package generates an approx-style lemma for
 datatypes introduced that way.


 (C)opyright Peter Gammie, peteg42 at gmail.com, commenced December 2007.

 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are
 met:

   1. Redistributions of source code must retain the above copyright
      notice, this list of conditions and the following disclaimer.

   2. Redistributions in binary form must reproduce the above copyright
      notice, this list of conditions and the following disclaimer in the
      documentation and/or other materials provided with the distribution.

 THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
 OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN
 NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE FOR ANY
 DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
 OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
 DAMAGE.

 (This licence is intended to be in the spirit of the BSD licence.)

*)

theory approx_lemma

imports HOLCF

begin

(* The fully-lazy list type. *)

domain 'a llist =
    lnil
  | lcons (lazy lhead::"'a") (lazy ltail::"'a llist")

(* The "map/iterate property" example from Gibbons/Hutton. *)

consts inf_iterate :: "('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a llist"
fixrec "inf_iterate\<cdot>f\<cdot>x = lcons\<cdot>x\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))"

declare inf_iterate_simps[simp del]

consts lmap :: "('a \<rightarrow> 'b) \<rightarrow> 'a llist \<rightarrow> 'b llist"
fixrec
  "lmap\<cdot>f\<cdot>(lnil) = lnil"
  "lmap\<cdot>f\<cdot>(lcons\<cdot>x\<cdot>xs) = lcons\<cdot>(f\<cdot>x)\<cdot>(lmap\<cdot>f\<cdot>xs)"

fixpat lmap_strict[simp]: "lmap\<cdot>f\<cdot>\<bottom>"

declare lmap_simps(2)[simp del]
declare lmap_simps(2)[symmetric, simp add]

definition
  mapiterate :: "('a \<rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where
  mapiterate_def[simp]:
    "mapiterate f x \<equiv> lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>x) = inf_iterate\<cdot>f\<cdot>(f\<cdot>x)"

(* Fixpoint induction.

thm fix_ind: \<lbrakk>adm ?P; ?P \<bottom>; \<And>x. ?P x \<Longrightarrow> ?P (?F\<cdot>x)\<rbrakk> \<Longrightarrow> ?P (fix\<cdot>?F)

*)
lemma
  fixes f :: "'a \<rightarrow> 'a"
  fixes x :: "'a"
  shows "mapiterate f x"
proof -
  let ?F = "\<Lambda> inf_iterate (f :: 'a \<rightarrow> 'a) x . lcons\<cdot>x\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))"
  let ?P = "\<lambda>g . \<forall> (f :: 'a \<rightarrow> 'a)  (x :: 'a) . lmap\<cdot>f\<cdot>(g\<cdot>f\<cdot>x) = g\<cdot>f\<cdot>(f\<cdot>x)"
  let ?h = "\<Lambda> g (f :: 'a \<rightarrow> 'a) (x :: 'a) . lcons\<cdot>x\<cdot>(g\<cdot>f\<cdot>(f\<cdot>x))"
  have "adm ?P" by simp
  moreover have "?P \<bottom>" by simp
  moreover
  {
    fix g assume pg: "?P g"
    {
      fix f x
      from pg have "lmap\<cdot>f\<cdot>(g\<cdot>f\<cdot>(f\<cdot>x)) = g\<cdot>f\<cdot>(f\<cdot>(f\<cdot>x))" by simp
             hence "lcons\<cdot>(f\<cdot>x)\<cdot>(lmap\<cdot>f\<cdot>(g\<cdot>f\<cdot>(f\<cdot>x))) = lcons\<cdot>(f\<cdot>x)\<cdot>(g\<cdot>f\<cdot>(f\<cdot>(f\<cdot>x)))"
	       by simp
             hence "lmap\<cdot>f\<cdot>(lcons\<cdot>x\<cdot>(g\<cdot>f\<cdot>(f\<cdot>x))) = lcons\<cdot>(f\<cdot>x)\<cdot>(g\<cdot>f\<cdot>(f\<cdot>(f\<cdot>x)))"
	       by (simp only: lmap_simps(2))
             hence "lmap\<cdot>f\<cdot>(?h\<cdot>g\<cdot>f\<cdot>x) = ?h\<cdot>g\<cdot>f\<cdot>(f\<cdot>x)" by simp
    }
    hence "?P (?h\<cdot>g)" by blast
  }
  ultimately have "?P (fix\<cdot>?F)" by (rule fix_ind[where ?F="?F" and ?P="?P"])
  thus ?thesis by (simp add: inf_iterate_def)
qed

(* Using the take lemma HOLCF derived for llist. *)

(*   take_def: "llist_take \<equiv> \<lambda>n. iterate n llist_copy \<bottom>" *)
(*   take_lemmas: "(\<And>n. llist_take n\<cdot>?x = llist_take n\<cdot>?x') \<Longrightarrow> ?x = ?x'" *)
(*   take_rews: *)
(*     "llist_take ?n\<cdot>\<bottom> = \<bottom>" *)
(*     "llist_take 0\<cdot>?x = \<bottom>" *)
(*     "llist_take (Suc ?n)\<cdot>lnil = lnil" *)
(*     "llist_take (Suc ?n)\<cdot>(lcons\<cdot>?a\<cdot>?l) = lcons\<cdot>?a\<cdot>(llist_take ?n\<cdot>?l)" *)

lemma
  fixes f :: "'a \<rightarrow> 'a"
  fixes x :: "'a"
  shows "mapiterate f x"
proof -
  {
    fix n
    have "\<And>x. llist_take n\<cdot>(lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>x)) = llist_take n\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))"
    proof(induct n)
      case 0 show ?case by (simp add: take_rews)
    next
      case (Suc i)
      have "llist_take (Suc i)\<cdot>(lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>x))
	  = llist_take (Suc i)\<cdot>(lcons\<cdot>(f\<cdot>x)\<cdot>(lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))))"
	by (simp add: inf_iterate_simps[symmetric])
      also have "\<dots> = lcons\<cdot>(f\<cdot>x)\<cdot>(llist_take i\<cdot>(lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))))"
	by (simp only: llist.rews)
      also have "\<dots> = lcons\<cdot>(f\<cdot>x)\<cdot>(llist_take i\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>(f\<cdot>x))))"
	using Suc by simp
      also have "\<dots> = llist_take (Suc i)\<cdot>(lcons\<cdot>(f\<cdot>x)\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>(f\<cdot>x))))"
	by (simp add: llist.rews)
      also have "\<dots> = llist_take (Suc i)\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))"
	by (simp add: inf_iterate_simps[symmetric])
      finally show ?case .
    qed
  }
  thus ?thesis by - (unfold mapiterate_def, rule take_lemmas)
qed

(* Using the coinduction rule HOLCF derived for llist.

(*   bisim_def: *)
(*     "llist_bisim \<equiv> *)
(*      \<lambda>R. \<forall>x x'. *)
(*             R x x' \<longrightarrow> *)
(*             x = \<bottom> \<and> x' = \<bottom> \<or> *)
(*             x = lnil \<and> x' = lnil \<or> *)
(*             (\<exists>a l l'. R l l' \<and> x = lcons\<cdot>a\<cdot>l \<and> x' = lcons\<cdot>a\<cdot>l')" *)
(*   casedist: *)
(*     "\<lbrakk>?x = \<bottom> \<Longrightarrow> ?P; ?x = lnil \<Longrightarrow> ?P; \<And>a l. ?x = lcons\<cdot>a\<cdot>l \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P" *)
(*   coind: "\<lbrakk>llist_bisim ?R; ?R ?x ?x'\<rbrakk> \<Longrightarrow> ?x = ?x'" *)

*)
lemma
  fixes f :: "'a \<rightarrow> 'a"
  fixes x :: "'a"
  shows "mapiterate f x"
proof -
  let ?R =
    "\<lambda> xs ys. \<exists> (f :: 'a \<rightarrow> 'a) (x :: 'a).
      xs = lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>x) \<and> ys = inf_iterate\<cdot>f\<cdot>(f\<cdot>x)"
  have "llist_bisim ?R"
  proof -
    {
      fix as bs
      assume rasbs: "?R as bs"
      then obtain f :: "'a \<rightarrow> 'a" and x :: "'a"
	where lhs: "as = lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>x)"
	  and rhs: "bs = inf_iterate\<cdot>f\<cdot>(f\<cdot>x)" by blast
      from lhs have "as = lmap\<cdot>f\<cdot>(lcons\<cdot>x\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x)))" by (simp add: inf_iterate_simps[symmetric])
          also have "\<dots> = lcons\<cdot>(f\<cdot>x)\<cdot>(lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x)))" by simp
       finally have as': "as = lcons\<cdot>(f\<cdot>x)\<cdot>(lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x)))" .
      from rhs have bs': "bs = lcons\<cdot>(f\<cdot>x)\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>(f\<cdot> x)))" by (simp add: inf_iterate_simps[symmetric])
      have rtails: "?R (lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>(f\<cdot>x))) (inf_iterate\<cdot>f\<cdot>(f\<cdot>(f\<cdot>x)))"
	by blast
      from rtails as' bs' have "\<exists>a l l'. ?R l l' \<and> as = lcons\<cdot>a\<cdot>l \<and> bs = lcons\<cdot>a\<cdot>l'"
	by blast
    }
    thus ?thesis by (unfold bisim_def, blast)
  qed
  moreover have "?R (lmap\<cdot>f\<cdot>(inf_iterate\<cdot>f\<cdot>x)) (inf_iterate\<cdot>f\<cdot>(f\<cdot>x))" by blast
  ultimately show ?thesis by (unfold mapiterate_def, blast dest: llist.coind)
qed

(* Meta-theory *)

(* "approx" is strict and total in it's first argument, and we need to do
induction over it. Let's use HOL's @{typ "nat"}. *)

consts
  approx :: "nat \<Rightarrow> 'a llist \<rightarrow> 'a llist"

primrec
  "approx 0 = \<bottom>"
  "approx (Suc n) =
     (\<Lambda> xxs. case xxs of lnil \<Rightarrow> lnil | lcons\<cdot>x\<cdot>xs \<Rightarrow> lcons\<cdot>x\<cdot>(approx n\<cdot>xs))"

lemma approx_strict[simp]: "approx x\<cdot>\<bottom> = \<bottom>" by (cases x, simp_all add: llist.rews)
lemma approx_lnil[simp]: "approx (Suc x)\<cdot>lnil = lnil" by (simp add: llist.rews)
lemma approx_lnil_le[simp]: "approx x\<cdot>lnil \<sqsubseteq> lnil" by (cases x, simp_all add: llist.rews)

(* Left-to-right. *)

lemma approx_chain: "chain approx"
proof(rule chainI)
  fix n
  show "(approx n :: 'a llist \<rightarrow> 'a llist) \<sqsubseteq> approx (Suc n)"
  proof(induct n)
    case (Suc n)
    {
      fix xs :: "'a llist"
      have "approx (Suc n)\<cdot>xs \<sqsubseteq> approx (Suc (Suc n))\<cdot>xs"
      proof(cases xs rule: llist.casedist)
	case (3 y ys)
	from Suc have "approx n\<cdot>ys \<sqsubseteq> approx (Suc n)\<cdot>ys"
	  by - (rule monofun_cfun_fun)
	hence "lcons\<cdot>y\<cdot>(approx n\<cdot>ys) \<sqsubseteq> lcons\<cdot>y\<cdot>(approx (Suc n)\<cdot>ys)"
	  by (simp add: monofun_cfun)
	hence "approx (Suc n)\<cdot>(lcons\<cdot>y\<cdot>ys) \<sqsubseteq> approx (Suc (Suc n))\<cdot>(lcons\<cdot>y\<cdot>ys)"
	  by (simp add: llist.rews)
	with 3 show ?thesis by simp
      qed (simp_all add: llist.rews)
    }
    thus ?case by (rule less_cfun_ext)
  qed simp
qed

lemma lub_shift:
  assumes chainF: "chain (F :: nat \<Rightarrow> 'a::cpo)"
  shows "(\<Squnion> i. F i) = (\<Squnion> i. F (i + j))" (is "?lhs = ?rhs")
proof -
  have "range F <<| ?lhs"
    using thelubE[OF chainF] by simp
  hence "range (\<lambda>i. F (i + j)) <<| ?lhs"
    using is_lub_range_shift[OF chainF, where j=j] by simp
  thus "?lhs = ?rhs"
    using thelubI[where l="?lhs" and M="range (\<lambda>i. F (i + j))"]
    by simp
qed

lemma approx_limit: "(\<Squnion>i. approx i) = ID"
proof(rule ext_cfun)
  fix xs show "(\<Squnion>i. approx i)\<cdot>xs = ID\<cdot>xs"
  proof(induct xs rule: llist.ind)
    case 2 show ?case
      using contlub_cfun_fun[OF approx_chain, where x="\<bottom>"] by simp
  next
    case 3
    have "(\<Squnion> i\<Colon>nat. approx i)\<cdot>lnil = (\<Squnion> i\<Colon>nat. approx i\<cdot>lnil)"
      using contlub_cfun_fun[OF approx_chain, where x="lnil"] by simp
    also have "\<dots> = lnil"
      by (rule lub_chain_maxelem[where i=1], simp_all add: llist.rews)
    finally show ?case by simp
  next
    case (4 y ys)
    have "(\<Squnion> i\<Colon>nat. approx i)\<cdot>(lcons\<cdot>y\<cdot>ys) = (\<Squnion> i\<Colon>nat. approx i\<cdot>(lcons\<cdot>y\<cdot>ys))"
      using contlub_cfun_fun[OF approx_chain, where x="lcons\<cdot>y\<cdot>ys"] by simp
    also have "\<dots> = (\<Squnion> i. approx (Suc i)\<cdot>(lcons\<cdot>y\<cdot>ys))"
      using lub_shift[OF ch2ch_Rep_CFunL[OF approx_chain], where j=1] by simp
    also have "\<dots> = (\<Squnion> i. lcons\<cdot>y\<cdot>(approx i\<cdot>ys))" by (simp add: llist.rews)
    also have "\<dots> = lcons\<cdot>y\<cdot>(\<Squnion> i. approx i\<cdot>ys)"
      using contlub_cfun_arg[where f="lcons\<cdot>y", OF ch2ch_Rep_CFunL[OF approx_chain]]
      by simp
    also have "\<dots> = lcons\<cdot>y\<cdot>((\<Squnion> i. approx i)\<cdot>ys)"
      using contlub_cfun_fun[OF approx_chain, where x="ys"] by simp
    also from 4 have "\<dots> = lcons\<cdot>y\<cdot>ys" by simp
    finally show ?case by simp
  qed simp
qed

lemma approx_lemma: "(\<forall>n. approx n\<cdot>xs = approx n\<cdot>ys) = (xs = ys)" (is "?lhs = ?rhs")
proof
  assume lhs: "?lhs"
  hence "(\<Squnion>i. approx i\<cdot>xs) = (\<Squnion>i. approx i\<cdot>ys)" by simp
  hence "((\<Squnion>i. approx i)\<cdot>xs) = ((\<Squnion>i. approx i)\<cdot>ys)"
    by (simp add: contlub_cfun_fun [OF approx_chain])
  hence "ID\<cdot>xs = ID\<cdot>ys" by (simp add: approx_limit)
  thus "xs = ys" by simp
qed simp

end