# [isabelle] Something about case rule

yug writes:
> First of all , the type declaration:
>
> datatype
> ('a,'b) val= Var 'a | Const "'b"| Abs 'a "('a,'b) lt"
> and
> ('a,'b) lt= V "('a,'b) val" | App "('a,'b) lt" "('a,'b) lt"
>
> I have declared a case rule
>
> lemma ltnormalcase[case_names Var Const Abs App, cases type]:
> assumes "!! x. P (V (Var x))" "!!b. P(V (Const b))" "!! x M. P (V (Abs x
> M))"
> "!! L M. P (L $ M)" shows "P N"
>
> then how can I use it in the proof context?
>
> I try it in this way (Isar reference Page 85 ,section 4.3.5) :
>
> proof(cases "N" rule:ltnormalcase)
>
> but Isar says:
> "
> *** Ill-typed instantiation:
> *** N :: ('a, 'b) lt
> *** At command "proof".
> "
>
> Any help?? thanks a lot
I have not yet found out myself why, but if you write
proof(induct "N" rule: ltnormalcase)
then you should get what you expect.
Hope this helps for the moment,
Christian

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