Re: [isabelle] Fw : Re: Question on hypothesis



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.
>     >>
>     >>
>     >>
>     >>       
>     >
>     >
>     >
>     >       
> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.