[isabelle] Trouble selecting maximum element of locally linear relation



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

-- 
 Denis

Attachment: Hyper.thy
Description: Binary data



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