LList.thy

renamed theory files

(*  Title: 	HOL/llist.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

Definition of type 'a llist by a greatest fixed point

Shares NIL, CONS, List_Fun, List_case with list.thy

Still needs filter and flatten functions -- hard because they need
bounds on the amount of lookahead required.

Could try (but would it work for the gfp analogue of term?)
  LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"

A nice but complex example would be [ML for the Working Programmer, page 176]
  from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))

Previous definition of llistD_Fun was explicit:
  llistD_Fun_def
   "llistD_Fun(r) == 	\
\       {<LNil,LNil>}  Un  	\
\       (UN x. (%z.split(z, %l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
*)

LList = Gfp + List +

types
  'a llist

arities
   llist :: (term)term

consts
  LList      :: "'a node set set => 'a node set set"
  LListD_Fun :: 
      "[('a node set * 'a node set)set, ('a node set * 'a node set)set] => \
\      ('a node set * 'a node set)set"
  LListD     :: 
      "('a node set * 'a node set)set => ('a node set * 'a node set)set"
  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"

  Rep_LList  :: "'a llist => 'a node set"
  Abs_LList  :: "'a node set => 'a llist"
  LNil       :: "'a llist"
  LCons      :: "['a, 'a llist] => 'a llist"
  
  llist_case :: "['a llist, 'b, ['a, 'a llist]=>'b] => 'b"

  LList_corec_fun :: "[nat, 'a=>unit+('b node set * 'a), 'a] => 'b node set"
  LList_corec     :: "['a, 'a => unit + ('b node set * 'a)] => 'b node set"
  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"

  Lmap	     :: "('a node set => 'b node set) => ('a node set => 'b node set)"
  lmap	     :: "('a=>'b) => ('a llist => 'b llist)"

  iterates   :: "['a => 'a, 'a] => 'a llist"

  Lconst     :: "'a node set => 'a node set"
  Lappend    :: "['a node set, 'a node set] => 'a node set"
  lappend    :: "['a llist, 'a llist] => 'a llist"


rules
  LListD_Fun_def    "LListD_Fun(r) == (%Z.diag({Numb(0)}) <++> r <**> Z)"
  LList_def	    "LList(A) == gfp(List_Fun(A))"
  LListD_def	    "LListD(r) == gfp(LListD_Fun(r))"
    (*faking a type definition...*)
  Rep_LList 	    "Rep_LList(xs): LList(range(Leaf))"
  Rep_LList_inverse "Abs_LList(Rep_LList(xs)) = xs"
  Abs_LList_inverse "M: LList(range(Leaf)) ==> Rep_LList(Abs_LList(M)) = M"
     (*defining the abstract constructors*)
  LNil_def  	"LNil == Abs_LList(NIL)"
  LCons_def 	"LCons(x,xs) == Abs_LList(CONS(Leaf(x), Rep_LList(xs)))"

  llist_case_def
   "llist_case(l,c,d) == \
\       List_case(Rep_LList(l), c, %x y. d(Inv(Leaf,x), Abs_LList(y)))"

  LList_corec_fun_def
    "LList_corec_fun(k,f) == \
\     nat_rec(k, %x. {}, 			\
\	        %j r x. sum_case(f(x), %u.NIL, 	\
\			   %v. split(v, %z w. CONS(z, r(w)))))"

  LList_corec_def
    "LList_corec(a,f) == UN k. LList_corec_fun(k,f,a)"

  llist_corec_def
   "llist_corec(a,f) == \
\       Abs_LList(LList_corec(a, %z.sum_case(f(z), %x.Inl(x), \
\                                    %y.split(y, %v w. Inr(<Leaf(v), w>)))))"

  llistD_Fun_def
   "llistD_Fun(r) == 	\
\	prod_fun(Abs_LList,Abs_LList) ``  	\
\                LListD_Fun(diag(range(Leaf)), 	\
\		            prod_fun(Rep_LList,Rep_LList) `` r)"

  Lconst_def	"Lconst(M) == lfp(%N. CONS(M, N))"     

  Lmap_def
   "Lmap(f,M) == \
\       LList_corec(M, %M. List_case(M, Inl(Unity), %x M'. Inr(<f(x), M'>)))"

  lmap_def
   "lmap(f,l) == \
\       llist_corec(l, %l. llist_case(l, Inl(Unity), %y z. Inr(<f(y), z>)))"

  iterates_def	"iterates(f,a) == llist_corec(a, %x. Inr(<x, f(x)>))"     

(*Append generates its result by applying f, where
    f(<NIL,NIL>) = Inl(Unity)
    f(<NIL, CONS(N1,N2)>) = Inr(<N1, <NIL,N2>)
    f(<CONS(M1,M2), N>)    = Inr(<M1, <M2,N>)
*)

  Lappend_def
   "Lappend(M,N) == LList_corec(<M,N>, %p. split(p,  \
\     %M N. List_case(M, List_case(N, Inl(Unity), \
\                                  %N1 N2. Inr(<N1, <NIL,N2>>)),	\
\                         %M1 M2. Inr(<M1, <M2,N>>))))"

  lappend_def
   "lappend(l,n) == llist_corec(<l,n>, %p. split(p,  \
\     %l n. llist_case(l, llist_case(n, Inl(Unity), \
\                                    %n1 n2. Inr(<n1, <LNil,n2>>)),	\
\                         %l1 l2. Inr(<l1, <l2,n>>))))"


end