[isabelle] Hiding import of SList



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?

-- 
 Denis

Attachment: Hyper.thy
Description: Binary data



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