Email Gateway (Aug 18 2022 at 18:33): Email Gateway (Aug 18 2022 at 18:33):From: Anh Le <anhlevn@cims.nyu.edu>
Hi everyone,
I am trying to do something I thought it should be valid, but it seems that
Isar does not allow it. The followings are some simple code.
(* Simple data type*)
datatype Type =
ClassType "nat"
| FunctionType "(Type) list" "Type"
(Defining some rules)
inductive subtyping :: "ClassTable => Type => Type => bool"
where
sRefl : "(subtyping CT t t)"
| ...
(Some theorem)
theorem ..
proof(induction rule:subtyping.induct)
case (sRefl CT t)
...
qed
What I am trying to do is to pass "ClassType c" to the case sRefl, instead
of 't'. So, it would look like: case(sRefl CT "ClassType c"). But it doesn't
compile because Isar only allows variables there.
Is there any way to work around this? I tried to use 'let t = "Classtype
c"', but it didn't work either.
Thank you very much
Anh
Email Gateway (Aug 18 2022 at 18:33):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm not sure I understand what you are trying to do. The proof has to handle every possible value of your datatype Type, not just those of the form ClassType c. If you want to do a case analysis on the form of t, you can do that afterwards, but you must handle both cases.
Larry Paulson
Last updated: May 06 2024 at 20:16 UTC