Email Gateway (Aug 18 2022 at 11:34): Email Gateway (Aug 18 2022 at 11:34):From: Denis Bueno <dbueno@gmail.com>
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
Hyper.thy
Email Gateway (Aug 18 2022 at 11:34):From: Tobias Nipkow <nipkow@in.tum.de>
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:
Email Gateway (Aug 18 2022 at 11:34):From: Stefan Friedrich <stefan.friedrich@methodpark.de>
Hi Denis,
concerning your second question, the proof in the enclosed theory file
should do the trick.
Cheers,
Stefan
Denis Bueno schrieb:
Hyper.thy
Email Gateway (Aug 18 2022 at 11:36):From: Denis Bueno <dbueno@gmail.com>
Thank you all for your help. In the end I used the proof developed by
Stefan which I believe is essentially what Tobias suggested.
Stefan, reading your proof was insightful and helpful. Thanks again!
Last updated: Nov 21 2024 at 12:39 UTC