Re: [isabelle] dest_Trueprop question



On Fri, 16 Jun 2006, Dimitrios Vytiniotis wrote:

> I have an inductive relation and some of the inference rules
> use meta-level quantifiers on the premises.

> I found that more convenient because at use sites it is easier for me to
> instantiate these things than when using object-level quantifiers.

Very good.  This is usually the way to do it, because the resulting rules
can be used natively, without having to walk through object-logic
connectives.


> lemma blabla: ...
>   by(induct X, auto elim: MyRelation.elims)

Just note that the initial induct and terminal auto method are normally
separated like this:

  by (induct X) (auto ...)

The difference shows up when there are facts being used for the first
part.  These are usually irrelevant for the second, so don't pass them to
auto in the first place.


> And although I feel it should work, I get back the error:
>    *** exception TERM raised: dest_Trueprop

Is this caused by induct or auto?  Sometimes a meta-level quantifier gets
a more general type than expected (e.g. 'a::{}).  Then certain tools fail
to internalize a problem into the object-logic.


	Makarius





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