Discussion:
[isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
(too old to reply)
Alexander Kogtenkov via Cl-isabelle-users
2016-07-28 09:04:29 UTC
Permalink
Raw Message
Dear Isabelle users,

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?

Regards,
Alexander Kogtenkov
Peter Lammich
2016-07-28 09:20:15 UTC
Permalink
Raw Message
Reminds me of kleene fp iteration.

This one might help in proving the lemma you have in mind:
Nat.lfp_Kleene_iter:
⟦mono ?f; (?f ^^ Suc ?k) bot = (?f ^^ ?k) bot⟧
⟹ lfp ?f = (?f ^^ ?k) bot

--
Peter

On Mi, 2016-07-27 at 20:06 +0300, Alexander Kogtenkov via
Post by Alexander Kogtenkov via Cl-isabelle-users
Dear Isabelle users,
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?
Regards,
Alexander Kogtenkov
Peter Gammie
2016-07-28 09:39:38 UTC
Permalink
Raw Message
Post by Alexander Kogtenkov via Cl-isabelle-users
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/
Alexander Kogtenkov via Cl-isabelle-users
2016-07-28 10:24:11 UTC
Permalink
Raw Message
Hi Peter,

Looks promising indeed. And I'm both hands for including these in the repository so that other people who need something like that can benefit from your work.

I'll come back to you if I encounter any issues/questions when using the lemmas in my context.

Best regards,
Alexander Kogtenkov
Post by Peter Gammie
Post by Alexander Kogtenkov via Cl-isabelle-users
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
text\<open>
"while"} in \<open>While_Combinator\<close> to an arbitrary finite
could be generalized from finite types to chain-finite lattices.
\<close>
(* Nat, Kleene iteration for gfp. *)
subsection \<open>Kleene iteration\<close>
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 *)
  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)
  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)
  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])
  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
  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 *)
  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])
  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
  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/
Loading...