From: "Dr A. Koutsoukou-Argyraki" <firstname.lastname@example.org>
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
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!
From: Tobias Nipkow <email@example.com>
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".
From: Manuel Eberl <firstname.lastname@example.org>
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)"
Last updated: Jan 25 2022 at 02:35 UTC