*To*: yug <yug at ios.ac.cn>*Subject*: Re: [isabelle] Something about case rule*From*: yug <yug at ios.ac.cn>*Date*: Wed, 10 May 2006 09:26:56 +0800*Cc*: isabelle-users at cl.cam.ac.uk, urbanc at in.tum.de*In-reply-to*: <44600454.6090507@ios.ac.cn>*References*: <44600454.6090507@ios.ac.cn>*User-agent*: Debian Thunderbird 1.0.2 (X11/20050331)

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: > >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 > >YuGang > > >

**References**:**[isabelle] Something about case rule***From:*yug

- Previous by Date: Re: [isabelle] Why does "also" fail in this proof?
- Next by Date: [isabelle] HOR 2006: extended deadline
- Previous by Thread: [isabelle] Something about case rule
- Next by Thread: [isabelle] HOR 2006: extended deadline
- Cl-isabelle-users May 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list