Email Gateway (Aug 22 2022 at 13:41): Email Gateway (Aug 22 2022 at 13:41):From: Alexander Kogtenkov via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 13:41):From: Peter Lammich <lammich@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:42):From: Peter Gammie <peteg42@gmail.com>
Alexander, Peter:
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)
Email Gateway (Aug 22 2022 at 13:42):From: Alexander Kogtenkov via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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
Last updated: Apr 23 2024 at 12:29 UTC