[isabelle] dest_Trueprop question



Hello all, I am puzzled over the first issue and need
some advice on the second.

First issue
===========================================================
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.

I very often in my development use the style:

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

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

This is a bit annoying, because I did not encounter these problems
when the premises of the rules contained just object level forall's.

Additionally I have noticed that if I prove an inversion theorem
using (inductive_cases) and use that theorem instead of MyRelation.elims
things tend to (but not always) work more smoothly.

Is there more information on this? Should I send over more information?
I have not been able to figure out when exactly these errors occur but
any information would be valuable.

Second issue (advice)
=======================================================
I have a datatype which has only one constructor that takes a pair.
Values of this datatype are paired with naturals and
contained in a list. I have very often
found out that when I do induction on the list to prove a theorem,
in the inductive case I often have to do
a "by(cases "x", cases "snd x", blast)"
which I hate but want to do it in a one-line step because it is
a very ``obvious'' fact for the reader of the proof. How do I do
this elegantly (e.g with a single tactic like
(cases_deep_break "x", auto) or similar)

thanks!
-d







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