*To*: olfa mraihi <olfa.mraihi at yahoo.fr>*Subject*: Re: [isabelle] Fw : Re: Question on hypothesis*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 15 Dec 2010 22:12:27 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <615601.10287.qm@web26107.mail.ukl.yahoo.com>*References*: <615601.10287.qm@web26107.mail.ukl.yahoo.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

It works. The simplifier simply cannot simplify it any further. You may have hoped that it replaces l2P by [] everywhere, but by default it does not use one conjunct to simplify another. You can explicitly instruct it to use the left conjunct to simplify the right one: apply(simp cong: conj_cong) Regards Tobias PS No need for parentheses in your example. olfa mraihi schrieb: > how to do when I have a conjunction of hypothesis to simplify > I have tried : > theory Scratch > imports Main > begin > example_proof > have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) & (l2P=[]) & (length l1+length l2=length l1P+length l2P)" apply simp > > but it doesn't work. > > Best Regards. > > > >

**Follow-Ups**:**Re: [isabelle] Fw : Re: Question on hypothesis***From:*olfa mraihi

**References**:**[isabelle] Fw : Re: Question on hypothesis***From:*olfa mraihi

- Previous by Date: [isabelle] Fw : Re: Question on hypothesis
- Next by Date: Re: [isabelle] Fw : Re: Question on hypothesis
- Previous by Thread: [isabelle] Fw : Re: Question on hypothesis
- Next by Thread: Re: [isabelle] Fw : Re: Question on hypothesis
- Cl-isabelle-users December 2010 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