Re: [isabelle] structured induction

On 21 Apr 2008, at 17:35, Randy Pollack wrote:

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.

By "using h" the fact "valid G" is chained into the proof and the induct method uses the first chained fact to choose the induction rule. (The Isar Ref manual contains useful table detailing what induct and cases do in which situations.)


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