# [isabelle] structured induction

Consider the following example:
lemma valid_fitch:
fixes G :: "(par * tp) list"
assumes h:"valid G"
shows "\<exists> a A. G \<parallel>- a : A"
using h
proof (induct G rule: list.induct) -- "explicit induction rule"
case Nil
...
This induction behaves as exected, i.e. induction over the list G (I
was explicit about the induction rule to use).
However consider the following:
lemma valid_fitch:
fixes G :: "(par * tp) list"
assumes h:"valid G"
shows "\<exists> a A. G \<parallel>- a : A"
using h
proof (induct G) -- "let Isar decide which induction rule"
case Nil
*** Unknown case: "Nil"
*** At command "case".
Isar did induction over the judgement "valid G" instead of over the
list G. This seems unintended.
Am I missing something about the syntax? (BTW, this example is in
nominal Isabelle, but I guess that doesn't play any role in the
situation.)
Thanks,
Randy
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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