[isabelle] dest_Trueprop question
Hello all, I am puzzled over the first issue and need
some advice on the second.
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
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and