# Re: [isabelle] data type problems

On Sat, 23 Jun 2007, Carsten Varming wrote:
> 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.
> 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
> 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?
Since D is a nested datatype, the induction principle works via several
predicates simultaneaously. Just inspect the theorem list D.inducts to
see how this looks internally. An induction proof needs to follow that
structure, by stating multiple goals and invoking theses rules properly
(which can be a bit tricky). E.g. see the simple example in
HOL/Induct/Term.thy
As your primrec function is not recursive anyhow, but uses plain case
analyis only, you may finish the proof like this:
lemma "E d > 0"
proof (cases d)
case B then show ?thesis by simp
next
case Elem then show ?thesis by simp
next
case NE then show ?thesis by simp
qed
or even like this:
lemma "E d > 0"
by (cases d) simp_all
> Some of the behavior, but not all, is the same in the 2005 edition.
There have been some changes here concerning the "induct" method and
corresponding rules produced by nested/mutual datatypes etc. The NEWS
file provides some further clues.
Makarius

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