Re: [isabelle] proving a class instantiation.



On Tue, Nov 9, 2010 at 4:17 AM, Viorel Preoteasa
<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 = c

Isar proofs behave strangely when you 'show' something with a
meta-implication (==>) in it, as you've done here. This has been
discussed on the mailing list before:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-April/msg00052.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-September/msg00044.html

The 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 of
Isabelle, because using 'show' with meta-implications is useful
sometimes, and users seem to get stuck on the same problem on a
regular basis.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.