[isabelle-dev] functions over abstract data

Alexander Krauss krauss at in.tum.de
Sat Aug 24 23:20:19 CEST 2013

Hi Chris,


> When defining a function "f", whose result type is "T", it might be
> necessary to "peek under the hood" in order to show termination. When
> doing this manually, we destroy the abstraction and always have to
> reason about the raw-level and even worse, also all the existing
> constants with result type T have to be deconstructed in the definition.

I discussed similar ideas with John Matthews around 2007/8, where we 
also had a recursive specification of a value that could "internally" be 
expressed as a recursive function, even though it was not of function 
type itself. The (single) motivation at the time was the attempt to 
define infinite streams, modelled basically as "nat => 'a". However, I 
abandoned the approach as too complicated. For streams, I believe they 
should be more naturally defined corecursively. The same might hold for 
your parsers if you find a good way of expressing it: Your "par" 
definition is well-formed because the recursive call is wrapped into 
something else... This looks more like a productivity argument then a 
termination one, even though, when unfolding, one can be seen as the other.

Do you know the work of Nils Anders Danielsson on parsers, in particular
I'm not sure what this would mean in HOL, but it is certainly relevant.

> Here comes my suggestion

What you are proposing would add substantial complexity to pretty much 
everything in the function package. While it might be possible to do 
such a thing ("no obvious deficiencies"), you would pay later when 
maintaining the stuff. This is too much for what seems to me like a 

> PS: I started to dive into the function package. My first hurdle is that
> for "f" not of function type (as in "par"), no recursive calls are
> generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules
> could be found".

The analysis in the function package assumes basically a form where the 
arguments of recursive calls can be extracted explicitly. This is a hard 
assumption, and I see no chance of getting rid of it. The only sensible 
way of lifting this restriction is to build some sort of wrapper that 
reduces some other format to a normal function definition.


More information about the isabelle-dev mailing list