[isabelle] Passing arguments in rule induction.
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 =
| FunctionType "(Type) list" "Type"
(*Defining some rules*)
inductive subtyping :: "ClassTable => Type => Type => bool"
sRefl : "(subtyping CT t t)"
case (sRefl CT t)
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and