*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Thu, 28 Jul 2016 19:37:24 +1000*In-reply-to*: <1469697349.9851.8.camel@lapnipkow10>*References*: <1469639166.428286860@f306.i.mail.ru> <1469697349.9851.8.camel@lapnipkow10>

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/

**Follow-Ups**:**Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?***From:*Alexander Kogtenkov via Cl-isabelle-users

**References**:**[isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?***From:*Alexander Kogtenkov via Cl-isabelle-users

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

- Previous by Date: Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
- Next by Date: Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
- Previous by Thread: Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
- Next by Thread: Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list