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