[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Michael Norrish]

Christian Urban writes:
 
> Michael mentioned a few times the nominal datatype package; so below
> is attached a solution using nominal datatypes.
 
> However I made a few slight changes:
 
> > Problem 1.
> > Show height is a function.
 
> Since Daniel essentially defined a function over nominal datatypes,
> I defined it immediately as a function - not as a relation. So
> Problem 1 consists of convincing Isabelle to accept this definition.
> It does after a few reasoning steps.

I thought about doing this as well, but you then lose the test of rule
induction facilities, so thought I should provide a closer
transcription of the "spec".  After all, the mathematician's
intention/design should drive the mechanisation not vice versa, even
if in this case, you think their intention should be different :-)
 
But yes, defining height as a function directly is quite a nice
approach.  My HOL4 support for such recursion has it come out
automatically.  I.e., I write

val (hghf_def, hghf_perm) = define_recursive_term_function`
  (hghf (VAR s) = 1) /\
  (hghf (M @@ N) = MAX (hghf M) (hghf N) + 1) /\
  (hghf (LAM v M) = hghf M + 1)
`;

and get back two theorems.  One is the above specification of the hghf
function (which has been proved to exist and satisfy the above).  The
other tells me that

  hghf (tpm pi M) = hghf M

which is generally useful.  (The tpm function applies a permutation pi
to a term.)

Michael.