[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Christian Urban]

Dear All,

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. 

> Problem 2.
> Show that  
>   if height(e,n) and height(e',m) then
>       height(e[e'/x],n') and n' < (n -1) +  m
> where x is "free in e' ".

Again since Daniel defined a function, I took the liberty to
re-formulate the problem as

  height(e[e'/x]) <= ((height e) - 1) + (height e')

Hope this does not cause any outrage. In my opinion
one would solve the problem on paper using this formulation.
If anybody cares, I am happy to provide a version that
is more faithful to Daniel's email.

Best wishes,
Christian  


-------------- next part --------------
A non-text attachment was scrubbed...
Name: Height.thy
Type: application/octet-stream
Size: 3893 bytes
Desc: not available
Url : http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20060601/bac0728d/Height-0001.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Height.pdf
Type: application/pdf
Size: 55175 bytes
Desc: not available
Url : http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20060601/bac0728d/Height-0001.pdf