diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/LList.thy --- a/src/HOL/ex/LList.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/LList.thy Fri Mar 24 12:30:35 1995 +0100 @@ -19,8 +19,8 @@ Previous definition of llistD_Fun was explicit: llistD_Fun_def "llistD_Fun(r) == \ -\ {} Un \ -\ (UN x. (split(%l1 l2.))``r)" +\ {(LNil,LNil)} Un \ +\ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)" *) LList = Gfp + SList + @@ -69,9 +69,9 @@ coinductive "LListD(r)" intrs - NIL_I " : LListD(r)" - CONS_I "[| : r; : LListD(r) \ -\ |] ==> : LListD(r)" + 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*) @@ -79,9 +79,9 @@ \ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}" LListD_Fun_def "LListD_Fun r X == \ -\ {z. z = | \ -\ (? M N a b. z = & \ -\ : 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)" @@ -102,7 +102,7 @@ llist_corec_def "llist_corec a f == \ \ Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \ -\ (split(%v w. Inr())) (f z)))" +\ (split(%v w. Inr((Leaf(v), w)))) (f z)))" llistD_Fun_def "llistD_Fun(r) == \ @@ -113,28 +113,28 @@ Lconst_def "Lconst(M) == lfp(%N. CONS M N)" Lmap_def - "Lmap f M == LList_corec M (List_case (Inl Unity) (%x M'. Inr()))" + "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))" lmap_def - "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr()))" + "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))" - iterates_def "iterates f a == llist_corec a (%x. Inr())" + iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))" (*Append generates its result by applying f, where - f() = Inl(Unity) - f() = Inr() - f() = Inr() + f((NIL,NIL)) = Inl(()) + 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 \ -\ (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(>))) \ -\ (%M1 M2 N. Inr(>))))" + "Lappend M N == LList_corec (M,N) \ +\ (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \ +\ (%M1 M2 N. Inr((M1, (M2,N))))))" lappend_def - "lappend l n == llist_corec \ -\ (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(>))) \ -\ (%l1 l2 n. Inr(>))))" + "lappend l n == llist_corec (l,n) \ +\ (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \ +\ (%l1 l2 n. Inr((l1, (l2,n))))))" rules (*faking a type definition...*)