Re: [isabelle] Fw : Re: Question on hypothesis
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