[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.