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