Re: [isabelle] Trouble selecting maximum element of locally linear relation



I don't think there is anything readymade anywhere. All I can suggest is to take the development of Max in FiniteSet and generalize and adapt it to your situation. The structure of the development should stay the same, but of course many details will change.

Regards
Tobias

Denis Bueno schrieb:
Hi all,

In a proof I am working on, I need to formalise the statement "let x
be the largest member of X".  There is the Max operator in Finite_Set
which provides this, but it requires the elements in the set X to be
ordered by a linear order.  My elements are *linearly ordered* but
they are not ordered by a linear order.  That is, my order is locally
linear in the context I care about, but it is not linear in general.
Is there a way to express this fact to Isabelle so I can use the Max
function?

Second, since I couldn't figure out how to express this to Isabelle
(if it is indeed possible), I tried to prove that there is always a
max for my set.  Mathematically, this is achieved via a simple
induction on the cardinality of the set X, and indeed in the
Finite_Set library there is the induction rule
"Finite_Set.finite_ne_induct" for an induction whose base case is a
non-empty set, which is exactly what I want.  However, Isabelle
rejects my attempt to perform this induction ("empty result
sequence").

Concretely, I am using a sequence-prefix ordering from the library
LList2 [0]: x <= y if the sequence x is a prefix of y.  In my proof,
every element of the set X is a prefix of a fixed sequence, t.  Thus,
the elements in X are linearly ordered, since any two elements x and y
are prefixes of t, and thus x <= y or y <= x.

If you can help me, please try out the proof script, which I've
attached: the relevant induction is for the theorem on line 152.
Thank you.

[0] http://afp.sourceforge.net/browser_info/current/HOL/Lazy-Lists-II/LList2.html






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.