# [isabelle] Passing arguments in rule induction.

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

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