*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*: Fri, 17 Dec 2010 14:43:12 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <713949.62638.qm@web26107.mail.ukl.yahoo.com>*References*: <713949.62638.qm@web26107.mail.ukl.yahoo.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

olfa mraihi schrieb: > 0)thank you very much for your usefull answer > 1)what does it mean [| |]? > 2)what does it mean P? Please refer to the extensive Isabelle documentation. This mailing list is intended to discuss technical questions and not to give an introduction to the system to save you reading the basic material. > 3)it works only with assumption l2P=[] or l1P=[] but when I put l1=[], > the last assumption (which is l1+length l2=length l1P+length l2P) > disappears in the output and the same thing happens when I put l2=[]!! Assumptions that simplify to True disappear. Tobias > > > --- En date de : *Jeu 16.12.10, Tobias Nipkow /<nipkow at in.tum.de>/* a > écrit : > > > De: Tobias Nipkow <nipkow at in.tum.de> > Objet: Re: [isabelle] Fw : Re: Question on hypothesis > À: "olfa mraihi" <olfa.mraihi at yahoo.fr> > Cc: cl-isabelle-users at lists.cam.ac.uk > Date: Jeudi 16 décembre 2010, 7h37 > > olfa mraihi schrieb: > > this is what I have as output > > i + length l2 = iP + length l2P & > > l1 @ l2 = l1P @ l2P & l2P = [] & length l1 + length l2 = > length l1P > > > > but the simplification should return > > i + length l2 = iP & l1 @ l2 = l1P & length l1 + length l2 = > length l1P > > is it possible?if yes how? > > That is not directly possible. If the formulas you want to simplify are > assumptions, it works. Try > > lemma "[| i+length l2=iP+length l2P; l1 @ l2=l1P @ l2P; l2P=[]; length > l1+length l2=length l1P+length l2P |] ==> P" > apply simp > > Tobias > > > thank you very much. > > > > --- En date de : Mer 15.12.10, Tobias Nipkow <nipkow at in.tum.de > <http://fr.mc261.mail.yahoo.com/mc/compose?to=nipkow at in.tum.de>> a > écrit : > > > > > > De: Tobias Nipkow <nipkow at in.tum.de > <http://fr.mc261.mail.yahoo.com/mc/compose?to=nipkow at in.tum.de>> > > Objet: Re: [isabelle] Fw : Re: Question on hypothesis > > À: "olfa mraihi" <olfa.mraihi at yahoo.fr > <http://fr.mc261.mail.yahoo.com/mc/compose?to=olfa.mraihi at yahoo.fr>> > > Cc: cl-isabelle-users at lists.cam.ac.uk > <http://fr.mc261.mail.yahoo.com/mc/compose?to=cl-isabelle-users at lists.cam.ac.uk> > > Date: Mercredi 15 décembre 2010, 22h12 > > > > > > 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:*Jeremy Dawson

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

- Previous by Date: Re: [isabelle] rep_datatype and Datatype exception
- Next by Date: Re: [isabelle] Fw : Re: Question on hypothesis
- Previous by Thread: Re: [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