[isabelle] data type problems



Hi,

Working with Isabelle data types I have come across some odd behavior.

In the 21_Jun_2007 edition I get the following when stepping through the
code below. Some of the behavior, but not all, is the same in the 2005
edition.

The  data type declaration results in:
### Theorem database already contains a copy of "test.D.arity_size_*"

The primitive recursive function definition results in:
### No function definition for datatype "List.list"

### No function definition for datatype "*"

### No function definition for datatype "*"

And the case NE results in:
*** Illegal schematic variable(s) in case "NE"
*** At command "case".

What am I experiencing here? Is this how it is suppose to be?

theory test imports Main
begin

types 'a EE = "nat �'a �nat"

datatype D =
     B
  |  Elem "D EE"
  |  NE "(D list)"

consts E :: "D �nat"
primrec
"E B = 1"
"E (Elem e) = 2"
"E (NE e) = 3"

lemma "E d > 0"
proof (induct d)
case B thus ?case by auto next
case NE

Carsten

--
It is forbidden to kill; therefore all murderers are punished unless they kill
in large numbers and to the sound of trumpets.                       Voltaire.


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