[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.