*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] typo in isar-ref?*From*: Makarius <makarius at sketis.net>*Date*: Tue, 17 Jul 2012 21:34:38 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5004D86C.2070902@jaist.ac.jp>*References*: <CAMej=27qR3T0sJyh0hNR-d1wucJg==frxNhATCukGAqPpsh30Q@mail.gmail.com> <CAMej=25_JRn3jjofs1t=bfxrACMjh0hPM70SPni5diD8S_i_5A@mail.gmail.com> <CAMej=248JJvSk2Bh4_z1=JhxXaHGjd2nKTHtFT4SBbOdN1Q2HA@mail.gmail.com> <5004D86C.2070902@jaist.ac.jp>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 17 Jul 2012, Christian Sternagel wrote:

On 07/15/2012 04:52 PM, Ramana Kumar wrote:I'm trying to understand exactly what Isabelle/HOL proofs are at a low level so I have a chance at understanding how to extract OpenTheory proofs for Isabelle/HOL theories. On page 30 (pdf page 41) of isar-ref.pdf the example of goal oriented reasoning is either wrong or too confusing for me. In particular the third application of the resolution seems to introduce the wrong subgoal, and then the application of assumption seems magical.

where we use "my_print_tac" to reproduce internal goal states aspresented in isar-ref, "rule" stands for resolution with a given rule,and the rules conjI [of B A], conjunct2 [of A B], and conjunct1 [of A B]correspond to "B ==> A ==> B & A", "A & B ==> B", and "A & B ==> A",from the example trace.Thus I agree that after the third "rule"-application the subgoal shouldbe "A & B ==> A & B", rather than "A & B ==> B & A".

Makarius

**References**:**[isabelle] typo in isar-ref?***From:*Ramana Kumar

**Re: [isabelle] typo in isar-ref?***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] [isabelle-dev] Locale interpretation introduces abbreviations rather than definitions
- Next by Date: [isabelle] refute refutes my simple axiom
- Previous by Thread: Re: [isabelle] typo in isar-ref?
- Next by Thread: [isabelle] datatype display problem of type_synonym
- Cl-isabelle-users July 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