*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] equality of functions*From*: IG BI <igbi at gmx.com>*Date*: Fri, 10 Jan 2014 10:57:10 -0600*In-reply-to*: <DUB124-W437699E714D19647864BCD8FB30@phx.gbl>*References*: <DUB124-W437699E714D19647864BCD8FB30@phx.gbl>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/10/2014 9:54 AM, Roger H. wrote:

Hi, the lemma "[1 ↦ [4], 2 ↦ [5]] = [2 ↦ [5], 1 ↦ [4]]" can be proven by auto, but is there any automatic proof, meaning some existing lemma, which i can add to the simplifier, so that such identities that occur in the middle of proofs are solved automatically?

Hi,

http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/prog-prove.pdf http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/tutorial.pdf

http://www.cs.colorado.edu/~siek/7000/spring07/ http://www.cs.colorado.edu/~siek/7000/spring07/isabelle-notes.pdf

Regards, GB

**References**:**[isabelle] equality of functions***From:*Roger H .

- Previous by Date: [isabelle] equality of functions
- Next by Date: Re: [isabelle] equality of functions
- Previous by Thread: [isabelle] equality of functions
- Next by Thread: Re: [isabelle] equality of functions
- Cl-isabelle-users January 2014 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