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