diff -r 8ff6c8c95870 -r 13b15899c528 ex/LList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/LList.thy	Wed Sep 28 12:39:32 1994 +0100
@@ -0,0 +1,145 @@
+(*  Title: 	HOL/LList.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Definition of type 'a llist by a greatest fixed point
+
+Shares NIL, CONS, 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. (split(%l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
+*)
+
+LList = Gfp + List +
+
+types
+  'a llist
+
+arities
+   llist :: (term)term
+
+consts
+  list_Fun   :: "['a item set, 'a item set] => 'a item set"
+  LListD_Fun :: 
+      "[('a item * 'a item)set, ('a item * 'a item)set] => \
+\      ('a item * 'a item)set"
+
+  llist      :: "'a item set => 'a item set"
+  LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
+  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
+
+  Rep_llist  :: "'a llist => 'a item"
+  Abs_llist  :: "'a item => 'a llist"
+  LNil       :: "'a llist"
+  LCons      :: "['a, 'a llist] => 'a llist"
+  
+  llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
+
+  LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
+  LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
+  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
+
+  Lmap	     :: "('a item => 'b item) => ('a item => 'b item)"
+  lmap	     :: "('a=>'b) => ('a llist => 'b llist)"
+
+  iterates   :: "['a => 'a, 'a] => 'a llist"
+
+  Lconst     :: "'a item => 'a item"
+  Lappend    :: "['a item, 'a item] => 'a item"
+  lappend    :: "['a llist, 'a llist] => 'a llist"
+
+
+coinductive "llist(A)"
+  intrs
+    NIL_I  "NIL: llist(A)"
+    CONS_I "[| a: A;  M: llist(A) |] ==> CONS(a,M) : llist(A)"
+
+coinductive "LListD(r)"
+  intrs
+    NIL_I  "<NIL, NIL> : LListD(r)"
+    CONS_I "[| <a,b>: r;  <M,N> : LListD(r)   \
+\	    |] ==> <CONS(a,M), CONS(b,N)> : LListD(r)"
+
+defs
+  (*Now used exclusively for abbreviating the coinduction rule*)
+  list_Fun_def   "list_Fun(A,X) ==   \
+\		  {z. z = NIL | (? M a. z = CONS(a, M) & a : A & M : X)}"
+
+  LListD_Fun_def "LListD_Fun(r,X) ==   \
+\		  {z. z = <NIL, NIL> |   \
+\		      (? M N a b. z = <CONS(a, M), CONS(b, N)> &   \
+\		                  <a, b> : r & <M, N> : X)}"
+
+  (*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(c,d,l) == \
+\       List_case(c, %x y. d(Inv(Leaf,x), Abs_llist(y)), Rep_llist(l))"
+
+  LList_corec_fun_def
+    "LList_corec_fun(k,f) == \
+\     nat_rec(k, %x. {}, 			\
+\	        %j r x. sum_case(%u.NIL, split(%z w. CONS(z, r(w))), f(x)))"
+
+  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(%x.Inl(x), \
+\                                    split(%v w. Inr(<Leaf(v), w>)), f(z))))"
+
+  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, List_case(Inl(Unity), %x M'. Inr(<f(x), M'>)))"
+
+  lmap_def
+   "lmap(f,l) == llist_corec(l, llist_case(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>,   				\
+\     split(List_case(List_case(Inl(Unity), %N1 N2. Inr(<N1, <NIL,N2>>)), \
+\                     %M1 M2 N. Inr(<M1, <M2,N>>))))"
+
+  lappend_def
+   "lappend(l,n) == llist_corec(<l,n>,   				\
+\     split(llist_case(llist_case(Inl(Unity), %n1 n2. Inr(<n1, <LNil,n2>>)), \
+\                         %l1 l2 n. Inr(<l1, <l2,n>>))))"
+
+rules
+    (*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"
+
+end