# [isabelle] proving a class instantiation.

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] proving a class instantiation.
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Tue, 09 Nov 2010 14:17:37 +0200
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.12) Gecko/20101027 Lightning/1.0b2 Thunderbird/3.1.6

Hello,
I have a problem proving a class instantiation.
after the instance keyword I get the following proof obligation:
OFCLASS('a N, some_algebra_class)
First question is how do I unfold this expression to be able to
use apply scripts and not isar structured proofs.
Second if I start an isar proof using the keyword proof,
then I get 8 proof subgoals:
1. /\ a b c . a * b = a * c ==> b = c
2. /\ b a c . b * a = c * a ==> b = c
...
8. ...
I have 8 lemmas proved already for all these subgoals.
Now if I use:

`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
...
8. ...
I find this proof style very difficult. As I mentioned I have
already lemmas for all these subgoals, but I am not
able to use the lemmas to prove the subgoals. Is there an easier
way of discharging the subgoals without retyping them?
Best regards,
Viorel

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