[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
a = c
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
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)";
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and