Re: [isabelle] structured induction
On 21 Apr 2008, at 17:35, Randy Pollack wrote:
However consider the following:
fixes G :: "(par * tp) list"
assumes h:"valid G"
shows "\<exists> a A. G \<parallel>- a : A"
proof (induct G) -- "let Isar decide which induction rule"
*** 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