[isabelle] well-founded strict partial ordering

Christian Sternagel

2018-09-20 08:02:37 UTC

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

Post by Sophie Tourret
Hello,
I would like to know if there exist a generic well-founded strict
partial ordering available somewhere in Isabelle/HOL.
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