[isabelle] Strange simplification



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

Thanks in advance,
Cristiano Longo






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