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.

Many thanks in advance!

Best wishes,

Angeliki

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

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