Email Gateway (Aug 19 2021 at 03:12): 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.
Many thanks in advance!
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 04 2025 at 20:18 UTC