Email Gateway (Aug 17 2022 at 14:43): Email Gateway (Aug 17 2022 at 14:43):From: yug <yug@ios.ac.cn>
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
Email Gateway (Aug 17 2022 at 14:43):From: yug <yug@ios.ac.cn>
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:
Last updated: Nov 21 2024 at 12:39 UTC