Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?



Alexander, Peter:

> On 28 Jul 2016, at 03:06, Alexander Kogtenkov via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk> wrote:
> 

> Theory While_Combinator proves lemmas for least fixed point (e.g. lfp_while) using finite sets (BTW, the dual versions for gfp are missing for some reason). Are there more general versions of the lemmas that use finite lattices instead?

I recently had a similar need and bashed out the lemmas below.

Iâm hoping Andreas L. will commit these and others to the Isabelle repository when he gets some time.

If youâre going to go down the chain-finite route, give me a shout and Iâll send you some boilerplate.

cheers,
peter


subsection\<open> Relate @{const "gfp"} and @{const "while"} \<close>

text\<open>

We adapt and generalise the lemmas relating @{const "lfp"} to @{const
"while"} in \<open>While_Combinator\<close> to an arbitrary finite
complete lattice and play the same game for @{const "gfp"}. This story
could be generalized from finite types to chain-finite lattices.

\<close>

(* Nat, Kleene iteration for gfp. *)
subsection \<open>Kleene iteration\<close>

lemma Kleene_iter_gpfp:
assumes "mono f" and "p \<le> f p" shows "p \<le> (f^^k) (top::'a::order_top)"
proof(induction k)
  case 0 show ?case by simp
next
  case Suc
  from monoD[OF assms(1) Suc] assms(2)
  show ?case by simp
qed

lemma gfp_Kleene_iter: assumes "mono f" and "(f^^Suc k) top = (f^^k) top"
shows "gfp f = (f^^k) top"
proof(rule antisym)
  show "(f^^k) top \<le> gfp f"
  proof(rule gfp_upperbound)
    show "(f^^k) top \<le> f ((f^^k) top)" using assms(2) by simp
  qed
next
  show "gfp f \<le> (f^^k) top"
    using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp
qed

(* While_Combinator *)

lemma wf_finite_less:
  assumes "finite (C :: 'a::order set)"
  shows "wf {(x, y). {x, y} \<subseteq> C \<and> x < y}"
by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> a < b}", THEN wf_subset])
   (fastforce simp: less_eq assms intro: psubset_card_mono)

lemma wf_finite_greater:
  assumes "finite (C :: 'a::order set)"
  shows "wf {(x, y). {x, y} \<subseteq> C \<and> y < x}"
by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> b < a}", THEN wf_subset])
   (fastforce simp: less_eq assms intro: psubset_card_mono)

lemma while_option_finite_increasing_Some:
  fixes f :: "'a::order \<Rightarrow> 'a"
  assumes "mono f" and "finite (UNIV :: 'a set)" and "s \<le> f s"
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\<lambda>A. A \<le> f A" and s="s"])
   (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified])

lemma lfp_the_while_option:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  assumes "mono f" and "finite (UNIV :: 'a set)"
  shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f bot)"
proof -
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f bot = Some P"
    using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
  show ?thesis by auto
qed

lemma lfp_while:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  assumes "mono f" and "finite (UNIV :: 'a set)"
  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f bot"
unfolding while_def using assms by (rule lfp_the_while_option)

(* gfp *)

lemma while_option_finite_decreasing_Some:
  fixes f :: "'a::order \<Rightarrow> 'a"
  assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \<le> s"
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\<lambda>A. f A \<le> A" and s="s"])
   (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified])

lemma gfp_the_while_option:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  assumes "mono f" and "finite (UNIV :: 'a set)"
  shows "gfp f = the(while_option (\<lambda>A. f A \<noteq> A) f top)"
proof -
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f top = Some P"
    using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
  with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
  show ?thesis by auto
qed

lemma gfp_while:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  assumes "mono f" and "finite (UNIV :: 'a set)"
  shows "gfp f = while (\<lambda>A. f A \<noteq> A) f top"
unfolding while_def using assms by (rule gfp_the_while_option)



-- 
http://peteg.org/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.