Re: [isabelle] Something about case rule

Many thanks to Christian Urban!!

I have solved it clearly!

After I have defined the mutually inductive datatype ('a,'b)lt and
('a,'b) val.

I get the following two rules on induct and type

thm val_lt.induct (* induct rule *)
thm lt.exhaust (* case rule *)

we can see that case rule is in the form of

“?y = C x1...xn ==> .. ” (* where C is the constructor *)

so, if we'd like to define another rule on cases ,we should do
declaration as follows:

lemma ltnormalcase[case_names Var Const Abs App, cases type]:
assumes "!! x . y=V (Var x) P " "!!b. y=V (Const b)P " "!! x M. y=V (Abs
x M) P "
"!! M N. y=M$N P " shows "P "

and explicitly declare the cases on type:

lemma lttypecase[case_names Value App, cases type]:
assumes "!! x. y=V x P " "!! M N. y=M$N P" shows "P"

now we can switch between the two rules:
proof(cases "N" rule:ltnormalcase) or proof(cases "N" rule:lttypecase)

I also give the induct rule declarations

lemma ltinductnormal[case_names Var Const Abs App, induct type]:
assumes "!! x. P (V (Var x))" "!!b. P(V (Const b))" "!! x M. [| P M |]
==> P (V (Abs x M))"
"!! L M. [| P L; P M |] ==> P (L $ M)" shows "P N"

lemma ltinductv[case_names Value App,induct type]:
assumes "!! x. P (V x)" "!! L M.[| P L;P M |] ==> P(L$M)" shows "P N"

yug wrote:

>First of all , the type declaration:
>('a,'b) val= Var 'a | Const "'b"| Abs 'a "('a,'b) lt"
>('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
>"!! 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

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