Email Gateway (Aug 18 2022 at 10:36): Email Gateway (Aug 18 2022 at 10:36):From: Carsten Varming <varming@cmu.edu>
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:
The primitive recursive function definition results in:
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
Email Gateway (Aug 18 2022 at 10:36):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 12:27 UTC