--- a/src/HOL/Induct/LList.thy Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/LList.thy Thu Nov 26 17:40:10 1998 +0100
@@ -23,43 +23,12 @@
(UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
*)
-LList = Gfp + SList +
-
-types
- 'a llist
-
-arities
- llist :: (term)term
+LList = Main + SList +
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)"
@@ -73,81 +42,92 @@
CONS_I "[| (a,b): r; (M,N) : LListD(r)
|] ==> (CONS a M, CONS b N) : LListD(r)"
+
+typedef (LList)
+ 'a llist = "llist(range Leaf)" (llist.NIL_I)
+
+constdefs
+ (*Now used exclusively for abbreviating the coinduction rule*)
+ list_Fun :: ['a item set, 'a item set] => 'a item set
+ "list_Fun A X == {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+
+ LListD_Fun ::
+ "[('a item * 'a item)set, ('a item * 'a item)set] =>
+ ('a item * 'a item)set"
+ "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)}"
+
+ (*the abstract constructors*)
+ LNil :: 'a llist
+ "LNil == Abs_LList NIL"
+
+ LCons :: ['a, 'a llist] => 'a llist
+ "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
+
+ llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
+ "llist_case c d l ==
+ List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
+
+ LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item"
+ "LList_corec_fun k f ==
+ nat_rec (%x. {})
+ (%j r x. case f x of None => NIL
+ | Some(z,w) => CONS z (r w))
+ k"
+
+ LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item"
+ "LList_corec a f == UN k. LList_corec_fun k f a"
+
+ llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist"
+ "llist_corec a f ==
+ Abs_LList(LList_corec a
+ (%z. case f z of None => None
+ | Some(v,w) => Some(Leaf(v), w)))"
+
+ llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
+ "llistD_Fun(r) ==
+ prod_fun Abs_LList Abs_LList ``
+ LListD_Fun (diag(range Leaf))
+ (prod_fun Rep_LList Rep_LList `` r)"
+
+
+
+(*The case syntax for type 'a llist*)
translations
"case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
-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)}"
+(** Sample function definitions. Item-based ones start with L ***)
- (*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 (%x. {})
- (%j r x. case f x of Inl u => NIL
- | Inr(z,w) => CONS z (r w))
- k"
+constdefs
+ Lmap :: ('a item => 'b item) => ('a item => 'b item)
+ "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
- 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. case f z of Inl x => Inl(x)
- | Inr(v,w) => Inr(Leaf(v), w)))"
+ lmap :: ('a=>'b) => ('a llist => 'b llist)
+ "lmap f l == llist_corec l (%z. case z of LNil => None
+ | LCons y z => Some(f(y), 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)"
+ iterates :: ['a => 'a, 'a] => 'a llist
+ "iterates f a == llist_corec a (%x. Some((x, f(x))))"
- Lmap_def
- "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
-
- lmap_def
- "lmap f l == llist_corec l (%z. case z of LNil => (Inl ())
- | LCons y z => Inr(f(y), z))"
-
- iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))"
+ Lconst :: 'a item => 'a item
+ "Lconst(M) == lfp(%N. CONS M N)"
(*Append generates its result by applying f, where
- f((NIL,NIL)) = Inl(())
- f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2))
- f((CONS M1 M2, N)) = Inr((M1, (M2,N))
+ f((NIL,NIL)) = None
+ f((NIL, CONS N1 N2)) = Some((N1, (NIL,N2))
+ f((CONS M1 M2, N)) = Some((M1, (M2,N))
*)
- Lappend_def
+ Lappend :: ['a item, 'a item] => 'a item
"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))))))"
+ (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2)))))
+ (%M1 M2 N. Some((M1, (M2,N))))))"
- lappend_def
- "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...*)
- 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"
+ lappend :: ['a llist, 'a llist] => 'a llist
+ "lappend l n == llist_corec (l,n)
+ (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2)))))
+ (%l1 l2 n. Some((l1, (l2,n))))))"
end