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.