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