Email Gateway (Aug 18 2022 at 10:30): Email Gateway (Aug 18 2022 at 10:30):From: Christian Urban <urbanc@in.tum.de>
Hi,
A question about wf/accessible part/strong normalisation:
I have restricted a reduction relation to its accessible
part. (In other words I have a reduction relation consisting
of only strongly normalising terms.)
Now, I have to prove that this relation is well-founded.
Does anybody know how one can prove such things?
The lemmas in Accessible_Part and WellFounded_Recursion
do not seem to be of much help for this.
Any hints are greatly appreciated.
Thanks a lot,
Christian
Email Gateway (Aug 18 2022 at 10:30):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Christian Urban wrote:
I have proved a number of results in this area, which are available in
http://users.rsise.anu.edu.au/~jeremy/isabelle/gen05/Wfss.{ML,thy}
They don't use the Accessible_Part theory, rather they have equivalent
definitions (wfp = "well-founded part"). This was because when I
looked quickly at the Accessible_Part theory, I misunderstood what the
definition of the set acc meant.
This has turned out to be a fortunate mistake, since the Accessible_Part
theory has changed in the latest version of Isabelle, so if I had used
it, my theories would now not work.
Jeremy
Email Gateway (Aug 18 2022 at 10:30):From: Christian Urban <urbanc@in.tum.de>
Jeremy Dawson kindly helped me. He found a clever
proof for what I needed.
Christian
Christian Urban writes:
Hi,
A question about wf/accessible part/strong normalisation:
I have restricted a reduction relation to its accessible
part. (In other words I have a reduction relation consisting
of only strongly normalising terms.)Now, I have to prove that this relation is well-founded.
Does anybody know how one can prove such things?
The lemmas in Accessible_Part and WellFounded_Recursion
do not seem to be of much help for this.Any hints are greatly appreciated.
Thanks a lot,
Christian
Last updated: May 03 2024 at 04:19 UTC