Email Gateway (Aug 22 2022 at 18:17): Email Gateway (Aug 22 2022 at 18:17):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Sophie,
I required both well-founded partial orders and the possibility to
obtain minimal elements in the past.
Which is why there are at least two further places you could consult:
(1) Well-founded Partial Orders
===============================
I formalized predicates "po_on" (for partial orders) and "wfp_on" (for
well-founded relations) in
https://www.isa-afp.org/browser_info/current/AFP/Open_Induction/Restricted_Predicates.html
where the "p" in "wfp_on" refers to the fact that I am using the
"predicate" version of relations, namely:
'a => 'a => bool
instead of
('a * 'a) set
and "_on" refers to the fact that there is a specific carrier set.
(2) Minimal Elements
=====================
There is the locale "minimal_element" in
https://www.isa-afp.org/browser_info/current/AFP/Well_Quasi_Orders/Minimal_Elements.html
which captures well-founded partial orders and provides a constant
"min_elt B" that yields some minimal element from a given set "B"
together with some facts about it.
cheers
chris
Email Gateway (Aug 22 2022 at 18:33):From: Sophie Tourret <stourret@mpi-inf.mpg.de>
Hello,
I would like to know if there exist a generic well-founded strict
partial ordering available somewhere in Isabelle/HOL.
In more details:
I need to use a well-founded strict partial ordering in some
isabelle/HOL proof I am currently working on. I found the wellorder
class and could use it to some extend but it is build on a total
ordering and I really need the ordering to be partial (and strict and
well-founded). In particular, I need to be able to obtain minimal
elements verifying some properties and reason on them.
I have taken a look around and my current plan is to extend the preorder
class with well-foundedness (and prove the existence of minimal elements
and needed properties by myself).
This looks like a lot of work (at least for someone relatively new to
Isabelle like me), thus before I start I would like to know if I have
missed something that does what I need (and suggestions of better plans
are also welcome). Here is where I looked and why I think it is not
exactly what I need.
Anything about lattices is out because I want no supremum at all and no
unique infimum.
[Main] HOL.Orderings.thy - where the classes wellorder and preorder are,
I didn't find a partial strict well-founded order there.
[Main] HOL.Wellfounded.thy - deals with binary relations, not with
orderings. Maybe I could use it but is looks trickier than my plan.
[IsaFOR] Quasi_Order.thy - maybe the class wf_order does what I want but
I am not sure and I don't see how I can use it to get a minimal element.
Again, it doesn't look better than my plan to me.
Best,
Sophie
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC