Re: [isabelle] Non-terminating function domain qualifier

On Fri, May 15, 2009 at 02:49, Alexander Krauss <krauss at> wrote:
> You can prove termination for some subset by showing that some property of
> the input implies parse_len_dom. Note that f_dom is currently just an
> abbreviation for "accp parse_len_rel" which is itself defined inductively as
> the call relation of your function.

Out of curiosity, how is is accp defined in Wellfounded.thy? It
doesn't seem to be explicit. My best guess is that "inductive_set x"
defines "xp" as a predicate. (This does seem to be the case.) But this
behavior appears not to be documented in the Isar reference manual.

Chris Capel
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.