# 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.*