[isabelle] Strange simplification
from online exercises ...
i have defined a new function
alls :: "('a => bool) => 'a list => bool"
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and