Email Gateway (Aug 18 2022 at 11:19): Email Gateway (Aug 18 2022 at 11:19):From: Peter Lammich <peter.lammich@uni-muenster.de>
Just a remark on the lemma "lfp_ordinal_induct" (transfinite kleene
induction), defined in "Inductive.thy".
This lemma is formulated only for sets in Inductive.thy, of course it
holds, more generically, for complete lattices. Even the proof does not
really change when moving to complete lattices (This one was done in 5
minutes by copy-pasting from Inductive.thy):
text {* More general version of @{thm lfp_ordinal_induct} for complete
lattices *}
lemma lfp_ordinal_induct':
constrains f::"'l::complete_lattice \<Rightarrow> 'l"
assumes mono: "mono f"
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Sup M)"
shows "P(lfp f)"
proof -
let ?M = "{S. S \<le> lfp f & P S}"
have "P (Sup ?M)" using P_Union by simp
also have "Sup ?M = lfp f"
proof (rule antisym)
show "Sup ?M \<le> lfp f" by (blast intro: Sup_least)
hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD])
hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp
hence "f (Sup ?M) \<in> ?M" using P_f P_Union by simp
hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper)
thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound)
qed
finally show ?thesis .
qed
regards, Peter
p.s. Is there any reason why all the fancy syntax \<Squnion>,
\<sqsubseteq>, etc. is undefined at the end of Lattices.thy ?
Email Gateway (Aug 18 2022 at 11:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Peter,
This lemma is formulated only for sets in Inductive.thy, of course it
holds, more generically, for complete lattices. Even the proof does not
really change when moving to complete lattices (This one was done in 5
minutes by copy-pasting from Inductive.thy):
The reason for this is largely historical. Thanks for your contribution
which I will put into the distribution.
p.s. Is there any reason why all the fancy syntax \<Squnion>,
\<sqsubseteq>, etc. is undefined at the end of Lattices.thy ?
We are a bit cautious not to put too many things into HOL standard
syntax. You can re-establish this syntax by "notation". We are still
looking for a technically satisfying policy to deal which these syntax
issues.
Hope this helps,
Florian
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 12:27 UTC