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