# [isabelle] A Newbie question about forward-proofs.

```Hello Isabelle Theorem Provers!

```
First of all, let me say, this is my first post to the list, hopefully I'm not committing any sins-of-form-or-content, but I claim ignorance, and thus innocence, if I do.
```
My question is as such:

I have a theory which has the following class definition

class Group =
fixes oper :: "'a ⇒ 'a ⇒ 'a" (infixl "[*]" 65)
and ivr  :: "'a ⇒ 'a"
and e    :: "'a"
assumes grp_assoc            : "a [*] (b [*] c) = (a [*] b) [*] c"
and grp_id_propR  [simp] : "a [*] e = a"
and grp_inv_propR [simp] : "(ivr a [*] a) [*] b = b";
notation oper (infixl "⨂" 65);

```
This (obviously) aims to represent a group. You'll of course notice that I didn't provide the left-handed analog of grp_id_propR, since it can be proved as a lemma, given the following lemma, which is where I'm getting stuck, my goal is to prove (in standard notation):
```
a = c => (b [*] a = b [*] c) /\ (a [*] b = c [*] b)

which is easy, simply note:

b [*] a = b [*] a

and

a = c

so substituting

b [*] a = b [*] c

```
And similar. My issue is that while I can get these assumptions "into" the system (so that they're under the `using this` spot) I can't seem to figure out the correct incantation to get a to be replaced with b on one side (or any side, for that matter). My intuition is that I need something like `ssubst`, but I'm not sure how to do it in the forward-proof mode.
```
For reference, my current lemma:

lemma (in Group) grp_mult_id :
assumes a_eq_c: "a = c"
shows "(a [*] b = c [*] b) ∧ (b [*] a = b [*] c)";
proof
assume refl: "a [*] b = a [*] b";
```
from refl and a_eq_c obtain "a [*] b = a [*] c"; (* the `obtain` bit (I think) is wrong,
```							    * or at least incomplete... *)

```
Thanks for any help any of you could provide. I'm really enjoying Isabelle, especially forward proof, it makes theorem proving less eye- straining and more fun!
```

/Joe Fredette

```

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