*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] On Recursion Induction*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Fri, 11 May 2012 14:34:33 +0900*In-reply-to*: <CAAMXsibWFJ5MrpKrivVqkhKX8xgay-Nn-m18VdZSY3Ltv3jR=A@mail.gmail.com>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com> <4FA8AB8A.9000705@jaist.ac.jp> <CAAPnxw1OQXEw7TaWg8Ft2G9q5=SEp-8FeYCGeS_Oiz2RZFn_2Q@mail.gmail.com> <4FA9E98D.6020302@jaist.ac.jp> <CAAPnxw10SB2Z8vhWKCBqOZYNkyVaHQUU8qTaJiZ4Q-0BcBaEXQ@mail.gmail.com> <4FAC9CB3.1030404@jaist.ac.jp> <CAAMXsibWFJ5MrpKrivVqkhKX8xgay-Nn-m18VdZSY3Ltv3jR=A@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

On 05/11/2012 02:27 PM, Brian Huffman wrote:

On Fri, May 11, 2012 at 6:59 AM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote:Since I was not able to find any rule that directly reduces a meta-equality into two implications with find_theorems "(?A ==> ?B) ==> (?B ==> ?A) ==> ?A == ?B" but such a rule is obviously applied. This step is somewhat "magic" (I guess it is part of the Isabelle/Isar/Pure framework).You used a too-specific pattern with your theorem search. A term like "?A ==> ?B" is parsed as "Trueprop ?A ==> Trueprop ?B", with ?A and ?B of type "bool". Of course you want ?A and ?B to be parsed as type "prop" here, so you need to add "PROP" tags to tell the parser what you want: find_theorems "(PROP ?A ==> PROP ?B) ==> (PROP ?B ==> PROP ?A) ==> PROP ?A == PROP ?B" found 1 theorem(s): Pure.equal_intr_rule: [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |] ==> PROP ?phi == PROP ?psi If there is any "magic" it is in the parser, which magically inserts "Trueprop" everywhere unless you tell it not to. ;)

Thanks, what a relief ;)

- Brian

**References**:**[isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**Re: [isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**Re: [isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**Re: [isabelle] On Recursion Induction***From:*Brian Huffman

- Previous by Date: Re: [isabelle] On Recursion Induction
- Next by Date: Re: [isabelle] On Recursion Induction
- Previous by Thread: Re: [isabelle] On Recursion Induction
- Next by Thread: Re: [isabelle] On Recursion Induction
- Cl-isabelle-users May 2012 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