Re: [isabelle] Non terminating function proven terminating
I did not find Isabelle's bug tracker so I hope that this is the place where
I'm supposed to report this.
In principle, yes, although this concrete one is a misunderstanding. (We
currently have no formal tracking of bugs or misunderstandings)
Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle.
As in Agda, we do not lose SN but we do accept a function that is not
Some further remarks:
You seem to be using a specific notion of "well-defined", probably
coming from constructive type theory.
In HOL, there is no formal notion of well-definedness other than a very
primitive one. Leaving pattern matching aside for now, we should rather
say that a function (given by a recursive equation) is "definable", iff
there is a HOL term that satisfies the equation (here that term is
"\<lambda> _. ()"). Finding that term basically amounts to "solving" the
equation, and this is what the definition command does for you for a
certain subclass of definable functions.
Note also that Isabelle has no notion of SN other than the trivial
beta/eta reduction of simply-typed lambda calculus. In particular,
definitions are not unfolded (aka reduced) automatically, unlike in Coq,
Agda etc. This means that "f is terminating" is merely an informal way
of saying "f can be defined using well-founded induction".
This archive was generated by a fusion of
Pipermail (Mailman edition) and