Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Something about case rule

Email Gateway (Aug 17 2022 at 14:43):

From: Christian Urban <urbanc@in.tum.de>
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

Last updated: May 03 2024 at 04:19 UTC