[isabelle] proving a class instantiation.



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.