Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] syntax for algorithm definition? Email Gateway (Aug 19 2021 at 03:12):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Hi,

I'm looking for the appropriate syntax to define an algorithm using
cases that does the following job:

My goal is to prove that I can always obtain some object with property
a.

Starting with object A: if it has property a the proof is finished.

If A doesn't have property a, Lemma X applies that produces some object
A' with certain properties.

If A' has property a, the proof is finished.

If A' doesn't have property a, Lemma X applies that produces some
object A'' with certain properties.

If A'' has property a, the proof is finished.

If A'' doesn't have property a, Lemma X applies that produces some
object A''' with certain properties...

and so on.

But it can be shown that Lemma X can only be applied N many times:

Because after N many applications of Lemma X, the conclusion of Lemma X
cannot hold anymore because the object that would be produced cannot
have one of the properties guaranteed by the lemma.

By contrapositive, the assumption of Lemma X (i.e. the assumption that
the object from the previous step does not have property a) cannot hold
after N many steps.

Therefore, some object produced after at most N many applications of
Lemma X must have property a.

Any hints about some syntax pattern that would work for something like
this would be much appreciated.

Best wishes,
Angeliki Email Gateway (Aug 19 2021 at 06:11):

From: Tobias Nipkow <nipkow@in.tum.de>
Isn't it just:

g A = (if a A then A else g(f A))

where f is the function corresponding to lemma X? In order to define g in HOL
you need to prove its totality. Using "fun", you need to provide a well founded
relation "<" such that "~ a A ==> f A < A".

Tobias
smime.p7s Email Gateway (Aug 19 2021 at 09:52):

From: Manuel Eberl <eberlm@in.tum.de>
Note that that well-founded relation can just be "measure foo", where

"foo A = (some natural number that upper-bounds the number of
recursion steps you will take on input A)"
smime.p7s

Last updated: Jan 25 2022 at 02:35 UTC