[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"
  "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?


Attachment: Hyper.thy
Description: Binary data

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