Re: [isabelle] Passing arguments in rule induction.



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


On 21 Oct 2011, at 01:39, Anh Le wrote:

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