Re: [isabelle] Hiding import of SList

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.


Denis Bueno wrote:
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"
  "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?

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