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