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

You know what it was, I just had the goal wrong. I mistyped and put "a [*] b = a [*] c". You're advice worked perfectly after I saw that...
```
Teach me to try to prove stuff in the wee hours of the morning!

Thanks so much for your help.

```
If I can bother you with another question. I wanted to get `ivr` to have a prefix unary syntax (or a postfix, the problem (I imagine) is isomorphic), once again, I just can't seem to find a suitable incantation. The big tutorial (the 200+ page one) talks about using datatypes somewhere for this purpose, But I don't see how that helps me here.
```
```
Further, another (semi-related) question. In Haskell (which is where my background lies), one can do associated datatypes, eg
```
class Foo a where
data Bar a :: * -> *
bar :: Bar a b -> b -> (a,b)
--whatever

On Oct 29, 2009, at 5:45 AM, Florian Haftmann wrote:

```
```Hi Joe,

```
```class Group =
```
fixes oper :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "[*]" 65)
``` and ivr :: "'a \<Rightarrow> '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"
begin
```
```
```
What I would recommend from a pragmatic point of view is to use the simp
```method:

```
```lemma grp_mult_id:
assumes a_eq_c: "a = c"
shows "(a [*] b = c [*] b) \<and> (b [*] a = b [*] c)"
proof
have refl: "b [*] a = b [*] a" ..
from refl and a_eq_c have "b [*] a = b [*] c" by simp
```
```
"simp" invokes an automated proof tool which performs equational
rewriting using assumptions in a goal and a predefined set of rewrite

Intermediate results in a proof are stated using "have".  Assumptions
"assume" are part the resulting theorem of a proof and therefore must
fit to an outer proof obligation, which is not the case in your proof
```
because "b [*] a = b [*] a" is not part of the assumptions of the lemma.
```
Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```
```

```

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