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