Email Gateway (Aug 18 2022 at 11:50): Email Gateway (Aug 18 2022 at 11:50):From: Denis Bueno <dbueno@gmail.com>
Hi all,
I have a theory (attached) which imports Main and LList2 (available
from afp). LList2 imports LList which imports SList, and the
importing of SList makes defining recursive functions over normal
lists (from List) very difficult, because it seems all names have to
be qualified.
The following, for example, is not admitted due to a type clash:
consts zipn :: "'a List.list List.list => 'a List.list List.list"
any :: "('a => bool) => 'a List.list => bool"
primrec
"any f List.Nil = False"
"any f (List.Cons x xs) = (if f x then True else any f xs)"
"zipn xss = (if any (%x. x = List.Nil) xss
then []
else List.Cons (map hd xss) (zipn (map tl xss)))"
Can I hide all SList-related stuff so I don't have to play games and
qualify every list-related function I call?
Hyper.thy
Email Gateway (Aug 18 2022 at 11:50):From: Tobias Nipkow <nipkow@in.tum.de>
An aside: It is usually better to avoid tests on lists like "any".
Instead of "any f xs" write "EX x:set xs. f x". Because now the existing
automation for quatifiers and sets will kick in automatically.
Tobias
Denis Bueno wrote:
Email Gateway (Aug 18 2022 at 11:52):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
I use the no_notation command for this kind of thing, for example to
overwrite the "+" symbol:
no_notation plus (infixl "+" 65)
consts "myplus" :: "nat => nat => nat"
notation "myplus" (infixl "+" 65)
defs myplus: "a + b == ..."
I imagine you can do the same kind of thing to get the original List
notation as you want it.
best,
lucas
Denis Bueno wrote:
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.7 (GNU/Linux)
Comment: Using GnuPG with Fedora - http://enigmail.mozdev.org
iD8DBQFIKGPuiUn2r+81A2gRAlFTAJwOFey3pjJpY9nD0roGRvVUw4cO9wCeI+jV
/erb5NhNCEzvYlNuLBOD+7E=
=lxYN
-----END PGP SIGNATURE-----
Last updated: May 03 2024 at 04:19 UTC