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.