# Re: [isabelle] Strange simplification

```

Cristiano Longo wrote:
```
```from online exercises ...

```
i have defined a new function
```consts
alls :: "('a  =>  bool)  => 'a list  => bool"

primrec
allsNil : "alls P [] = True"
allsRec : "alls P (x#xs) = (P x  \<and> (alls P xs))"

```
and tried to prove the following lemma
```alls P (xs @  ys) = (alls P xs)  \<and> (alls P ys)

by induction on xs, I obtain two subgoals. The first is

alls P ([] @ ys) = (alls P []) \<and> (alls P ys)

I can't understand why, simplifier transform this goal to

alls P ys
```
```
alls P ([] @ ys) = (alls P []) \<and> (alls P ys)

is understood as (alls P ([] @ ys) = (alls P [])) \<and> (alls P ys)
which rewrites to

(alls P ys = True) \<and> alls P ys

which again rewrites to alls P ys .

```
May be you want to bracket your goal differently, or just use <--> instead of =, which has much nicer priority bindings.
```
Hope this helps.
Amine.

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.