*To*: Joe Fredette <jfredett at gmail.com>*Subject*: Re: [isabelle] A Newbie question about forward-proofs.*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 29 Oct 2009 10:45:50 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <EA6D7A3F-52CD-48DB-9508-6489EF4F802E@gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <EA6D7A3F-52CD-48DB-9508-6489EF4F802E@gmail.com>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

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 rules (see the Isabelle tutorial for more information on this). 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

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] A Newbie question about forward-proofs.***From:*Joe Fredette

**References**:**[isabelle] A Newbie question about forward-proofs.***From:*Joe Fredette

- Previous by Date: Re: [isabelle] Simplifier problem (Congruence rules?)
- Next by Date: Re: [isabelle] A Newbie question about forward-proofs.
- Previous by Thread: [isabelle] A Newbie question about forward-proofs.
- Next by Thread: Re: [isabelle] A Newbie question about forward-proofs.
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list