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



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