*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] A Newbie question about forward-proofs.*From*: Joe Fredette <jfredett at gmail.com>*Date*: Thu, 29 Oct 2009 11:44:32 -0400*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4AE9644E.9080106@informatik.tu-muenchen.de>*References*: <EA6D7A3F-52CD-48DB-9508-6489EF4F802E@gmail.com> <4AE9644E.9080106@informatik.tu-muenchen.de>

Teach me to try to prove stuff in the wee hours of the morning! Thanks so much for your help.

class Foo a where data Bar a :: * -> * bar :: Bar a b -> b -> (a,b) --whatever is there an analog in Isabelle? 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" beginWhat I would recommend from a pragmatic point of view is to use thesimpmethod: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 proofbecause "b [*] a = b [*] a" is not part of the assumptions of thelemma.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

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

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

**Re: [isabelle] A Newbie question about forward-proofs.***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] A Newbie question about forward-proofs.
- Next by Date: Re: [isabelle] A Newbie question about forward-proofs.
- Previous by Thread: Re: [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