*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] proving a class instantiation.*From*: Makarius <makarius at sketis.net>*Date*: Tue, 9 Nov 2010 15:02:19 +0100 (CET)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AANLkTimoW5NDiPYez+RavGKXEHokjRHJMF35OwQfy5aV@mail.gmail.com>*References*: <4CD93BE1.1080609@abo.fi> <AANLkTimoW5NDiPYez+RavGKXEHokjRHJMF35OwQfy5aV@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Tue, 9 Nov 2010, Brian Huffman wrote:

<viorel.preoteasa at abo.fi> wrote:fix a b c::"'a N" show "a * b = a * c ==> b = c" by (rule cancel_times_left, simp) next; I cannot get rid of the first suboal. The first subgoal changes to: 1. /\ a b c . a * b = a * c ==> ?a12 a b c * b =?a12 a b c * c 2. /\ b a c . b * a = c * a ==> b = cThe quick fix is to avoid using this:fix a b c::"'a N" show "a * b = a * c ==> b = c"and instead use explicit 'assume' commands: fix a b c::"'a N" assume "a * b = a * c" thus "b = c"Hopefully this strange behavior can be changed in a future release ofIsabelle,

users seem to get stuck on the same problem on a regular basis.

because using 'show' with meta-implications is useful sometimes

Can you give an example for that? I.e. where show "!!x. A x ==> B x" is needed as such, instead of something that is equivalent to { fix x assume "A x" then show "B x" ... } ? Makarius

**Follow-Ups**:**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

**References**:**[isabelle] proving a class instantiation.***From:*Viorel Preoteasa

**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

- Previous by Date: Re: [isabelle] proving a class instantiation.
- Next by Date: [isabelle] CfP TAP
- Previous by Thread: Re: [isabelle] proving a class instantiation.
- Next by Thread: Re: [isabelle] proving a class instantiation.
- Cl-isabelle-users November 2010 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