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



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