## 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: Dec 05 2021 at 22:18 UTC