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