*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] dest_Trueprop question*From*: Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>*Date*: Fri, 16 Jun 2006 14:26:42 -0400*User-agent*: Thunderbird 1.5.0.2 (X11/20060411)

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

**Follow-Ups**:**Re: [isabelle] dest_Trueprop question***From:*Lawrence Paulson

**Re: [isabelle] dest_Trueprop question***From:*Jeremy Dawson

**Re: [isabelle] dest_Trueprop question***From:*Makarius

**Re: [isabelle] dest_Trueprop question***From:*Makarius

- Previous by Date: [isabelle] [Live Stream Saturday] 50 Years AI - Perspectives Symposium
- Next by Date: Re: [isabelle] dest_Trueprop question
- Previous by Thread: [isabelle] [Live Stream Saturday] 50 Years AI - Perspectives Symposium
- Next by Thread: Re: [isabelle] dest_Trueprop question
- Cl-isabelle-users June 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list