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



 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


>Peter Gammie <peteg42 at gmail.com>:
>
>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.