Email Gateway (Aug 18 2022 at 10:41): Email Gateway (Aug 18 2022 at 10:41):From: Cristiano Longo <cristiano.longo@tvblob.com>
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
Email Gateway (Aug 18 2022 at 10:42):From: Alexander Krauss <krauss@in.tum.de>
Hi Christiano,
[...]
What you see is not what you mean(tm): Equality binds stronger than
conjunction, so you are actually proving
(alls P (xs @ ys) = alls P xs) \<and> (alls P ys)
instead of
alls P (xs @ ys) = (alls P xs \<and> alls P ys) .
Hence the "strange" behaviour.
Alex
Email Gateway (Aug 18 2022 at 10:42):From: Lawrence Paulson <lp15@cam.ac.uk>
I think because it is parsed as
(alls P ([] @ ys) = (alls P [])) \<and> (alls P ys)
when you want it to be interpreted as
alls P ([] @ ys) = ((alls P []) \<and> (alls P ys))
Larry Paulson
Email Gateway (Aug 18 2022 at 10:42):From: Amine Chaieb <chaieb@in.tum.de>
Cristiano Longo wrote:
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.
Last updated: May 03 2024 at 12:27 UTC