# HG changeset patch
# User paulson
# Date 912098410 -3600
# Node ID 9f0c8869cf71df89c2da4f007fc32472fd131bae
# Parent  44290b71a85f358106201e7bf4d561c35c4620d6
tidied up list definitions, using type 'a option instead of
unit + 'a, also using real typedefs instead of faking them with extra rules

diff -r 44290b71a85f -r 9f0c8869cf71 src/HOL/Induct/LFilter.thy
--- a/src/HOL/Induct/LFilter.thy	Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/LFilter.thy	Thu Nov 26 17:40:10 1998 +0100
@@ -23,7 +23,7 @@
 
   lfilter	:: ['a => bool, 'a llist] => 'a llist
     "lfilter p l == llist_corec l (%l. case find p l of
-                                            LNil => Inl ()
-                                          | LCons y z => Inr(y,z))"
+                                            LNil => None
+                                          | LCons y z => Some(y,z))"
 
 end
diff -r 44290b71a85f -r 9f0c8869cf71 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/LList.ML	Thu Nov 26 17:40:10 1998 +0100
@@ -10,7 +10,7 @@
 
 (** Simplification **)
 
-Addsplits [split_split, split_sum_case];
+Addsplits [option.split];
 
 (*This justifies using llist in other recursive type definitions*)
 Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
@@ -22,7 +22,7 @@
 Goal "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
 by (fast_tac (claset() addSIs (map rew llist.intrs)
-                      addEs [rew llist.elim]) 1)
+                       addEs [rew llist.elim]) 1)
 end;
 qed "llist_unfold";
 
@@ -63,9 +63,8 @@
 by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
 qed "CONS_UN1";
 
-val prems = goalw LList.thy [CONS_def]
-    "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
-by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
+Goalw [CONS_def] "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
+by (REPEAT (ares_tac [In1_mono,Scons_mono] 1));
 qed "CONS_mono";
 
 Addsimps [LList_corec_fun_def RS def_nat_rec_0,
@@ -74,8 +73,8 @@
 (** The directions of the equality are proved separately **)
 
 Goalw [LList_corec_def]
-    "LList_corec a f <= sum_case (%u. NIL) \
-\                          (split(%z w. CONS z (LList_corec w f))) (f a)";
+    "LList_corec a f <= \
+\    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
 by (rtac UN_least 1);
 by (exhaust_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -84,7 +83,7 @@
 qed "LList_corec_subset1";
 
 Goalw [LList_corec_def]
-    "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
+    "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <= \
 \    LList_corec a f";
 by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
 by Safe_tac;
@@ -93,16 +92,16 @@
 qed "LList_corec_subset2";
 
 (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
-Goal "LList_corec a f = sum_case (%u. NIL) \
-\                           (split(%z w. CONS z (LList_corec w f))) (f a)";
+Goal "LList_corec a f =  \
+\     (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
 by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
                          LList_corec_subset2] 1));
 qed "LList_corec";
 
 (*definitional version of same*)
-val [rew] = goal LList.thy
-    "[| !!x. h(x) == LList_corec x f |] ==>     \
-\    h(a) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f a)";
+val [rew] = 
+Goal "[| !!x. h(x) == LList_corec x f |]     \
+\     ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))";
 by (rewtac rew);
 by (rtac LList_corec 1);
 qed "def_LList_corec";
@@ -117,16 +116,6 @@
 by (Simp_tac 1);
 qed "LList_corec_type";
 
-(*Lemma for the proof of llist_corec*)
-Goal "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
-\   llist(range Leaf)";
-by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac LList_corec 1);
-by (Asm_simp_tac 1);
-qed "LList_corec_type2";
-
 
 (**** llist equality as a gfp; the bisimulation principle ****)
 
@@ -140,9 +129,9 @@
 
 Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
 by (res_inst_tac [("n", "k")] less_induct 1);
-by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
+by (safe_tac (claset() delrules [equalityI]));
 by (etac LListD.elim 1);
-by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
+by (safe_tac (claset() delrules [equalityI]));
 by (exhaust_tac "n" 1);
 by (Asm_simp_tac 1);
 by (rename_tac "n'" 1);
@@ -251,9 +240,10 @@
 Delsimps [Pair_eq];
 
 (*abstract proof using a bisimulation*)
-val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
-\    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+val [prem1,prem2] = 
+Goal
+ "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
+\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
 \ ==> h1=h2";
 by (rtac ext 1);
 (*next step avoids an unknown (and flexflex pair) in simplification*)
@@ -267,8 +257,9 @@
 				  CollectI RS LListD_Fun_CONS_I]) 1);
 qed "LList_corec_unique";
 
-val [prem] = goal LList.thy
- "[| !!x. h(x) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f x) |] \
+val [prem] = 
+Goal 
+ "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] \
 \ ==> h = (%x. LList_corec x f)";
 by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
 qed "equals_LList_corec";
@@ -288,9 +279,10 @@
 Addsimps [ntrunc_one_CONS, ntrunc_CONS];
 
 
-val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
-\    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+val [prem1,prem2] = 
+Goal 
+ "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
+\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
 \ ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
 by (rename_tac "x k" 1);
@@ -328,14 +320,14 @@
 by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
 qed "Lconst_type";
 
-Goal "Lconst(M) = LList_corec M (%x. Inr((x,x)))";
+Goal "Lconst(M) = LList_corec M (%x. Some((x,x)))";
 by (rtac (equals_LList_corec RS fun_cong) 1);
 by (Simp_tac 1);
 by (rtac Lconst 1);
 qed "Lconst_eq_LList_corec";
 
 (*Thus we could have used gfp in the definition of Lconst*)
-Goal "gfp(%N. CONS M N) = LList_corec M (%x. Inr((x,x)))";
+Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some((x,x)))";
 by (rtac (equals_LList_corec RS fun_cong) 1);
 by (Simp_tac 1);
 by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
@@ -344,21 +336,31 @@
 
 (*** Isomorphisms ***)
 
-Goal "inj(Rep_llist)";
+Goal "inj Rep_LList";
 by (rtac inj_inverseI 1);
-by (rtac Rep_llist_inverse 1);
-qed "inj_Rep_llist";
+by (rtac Rep_LList_inverse 1);
+qed "inj_Rep_LList";
 
-Goal "inj_on Abs_llist (llist(range Leaf))";
+Goal "inj_on Abs_LList LList";
 by (rtac inj_on_inverseI 1);
-by (etac Abs_llist_inverse 1);
-qed "inj_on_Abs_llist";
+by (etac Abs_LList_inverse 1);
+qed "inj_on_Abs_LList";
+
+Goalw [LList_def] "x : llist (range Leaf) ==> x : LList";
+by (Asm_simp_tac 1);
+qed "LListI";
+
+Goalw [LList_def] "x : LList ==> x : llist (range Leaf)";
+by (Asm_simp_tac 1);
+qed "LListD";
+
 
 (** Distinctness of constructors **)
 
 Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil";
-by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1);
-by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
+by (rtac (CONS_not_NIL RS (inj_on_Abs_LList RS inj_on_contraD)) 1);
+by (REPEAT (resolve_tac (llist.intrs @
+			 [rangeI, LListI, Rep_LList RS LListD]) 1));
 qed "LCons_not_LNil";
 
 bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
@@ -368,16 +370,14 @@
 
 (** llist constructors **)
 
-Goalw [LNil_def]
-    "Rep_llist(LNil) = NIL";
-by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
-qed "Rep_llist_LNil";
+Goalw [LNil_def] "Rep_LList LNil = NIL";
+by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1);
+qed "Rep_LList_LNil";
 
-Goalw [LCons_def]
-    "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
-by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
-                         rangeI, Rep_llist] 1));
-qed "Rep_llist_LCons";
+Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)";
+by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse,
+                         rangeI, Rep_LList RS LListD] 1));
+qed "Rep_LList_LCons";
 
 (** Injectiveness of CONS and LCons **)
 
@@ -385,14 +385,16 @@
 by (fast_tac (claset() addSEs [Scons_inject]) 1);
 qed "CONS_CONS_eq2";
 
-bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
+bind_thm ("CONS_inject", CONS_CONS_eq RS iffD1 RS conjE);
 
 
 (*For reasoning about abstract llist constructors*)
 
-AddIs ([Rep_llist]@llist.intrs);
-AddSDs [inj_on_Abs_llist RS inj_onD,
-        inj_Rep_llist RS injD, Leaf_inject];
+AddIs [Rep_LList RS LListD, LListI];
+AddIs llist.intrs;
+
+AddSDs [inj_on_Abs_LList RS inj_onD,
+        inj_Rep_LList RS injD];
 
 Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
 by (Fast_tac 1);
@@ -400,8 +402,8 @@
 
 AddIffs [LCons_LCons_eq];
 
-val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
-by (rtac (major RS llist.elim) 1);
+Goal "CONS M N: llist(A) ==> M: A & N: llist(A)";
+by (etac llist.elim 1);
 by (etac CONS_neq_NIL 1);
 by (Fast_tac 1);
 qed "CONS_D2";
@@ -412,7 +414,8 @@
 Addsimps [List_case_NIL, List_case_CONS];
 
 (*A special case of list_equality for functions over lazy lists*)
-val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
+val [Mlist,gMlist,NILcase,CONScase] = 
+Goal
  "[| M: llist(A); g(NIL): llist(A);                             \
 \    f(NIL)=g(NIL);                                             \
 \    !!x l. [| x:A;  l: llist(A) |] ==>                         \
@@ -447,8 +450,8 @@
 Addsimps [Lmap_NIL, Lmap_CONS];
 
 (*Another type-checking proof by coinduction*)
-val [major,minor] = goal LList.thy
-    "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
+val [major,minor] = 
+Goal "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
 by (rtac (major RS imageI RS llist_coinduct) 1);
 by Safe_tac;
 by (etac llist.elim 1);
@@ -458,16 +461,16 @@
 qed "Lmap_type";
 
 (*This type checking rule synthesises a sufficiently large set for f*)
-val [major] = goal LList.thy  "M: llist(A) ==> Lmap f M: llist(f``A)";
-by (rtac (major RS Lmap_type) 1);
+Goal "M: llist(A) ==> Lmap f M: llist(f``A)";
+by (etac Lmap_type 1);
 by (etac imageI 1);
 qed "Lmap_type2";
 
 (** Two easy results about Lmap **)
 
-val [prem] = goalw LList.thy [o_def]
-    "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
+Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
+by (dtac imageI 1);
+by (etac LList_equalityI 1);
 by Safe_tac;
 by (etac llist.elim 1);
 by (ALLGOALS Asm_simp_tac);
@@ -475,8 +478,9 @@
                       rangeI RS LListD_Fun_CONS_I] 1));
 qed "Lmap_compose";
 
-val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
+Goal "M: llist(A) ==> Lmap (%x. x) M = M";
+by (dtac imageI 1);
+by (etac LList_equalityI 1);
 by Safe_tac;
 by (etac llist.elim 1);
 by (ALLGOALS Asm_simp_tac);
@@ -549,8 +553,8 @@
 
 (** llist_case: case analysis for 'a llist **)
 
-Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
-           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
+Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse,
+           Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
 
 Goalw [llist_case_def,LNil_def]  "llist_case c d LNil = c";
 by (Simp_tac 1);
@@ -562,39 +566,47 @@
 qed "llist_case_LCons";
 
 (*Elimination is case analysis, not induction.*)
-val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
-    "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P \
-\    |] ==> P";
-by (rtac (Rep_llist RS llist.elim) 1);
-by (rtac (inj_Rep_llist RS injD RS prem1) 1);
-by (stac Rep_llist_LNil 1);
+val [prem1,prem2] = 
+Goalw [NIL_def,CONS_def]
+     "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P";
+by (rtac (Rep_LList RS LListD RS llist.elim) 1);
+by (rtac (inj_Rep_LList RS injD RS prem1) 1);
+by (stac Rep_LList_LNil 1);
 by (assume_tac 1);
 by (etac rangeE 1);
-by (rtac (inj_Rep_llist RS injD RS prem2) 1);
+by (rtac (inj_Rep_LList RS injD RS prem2) 1);
 by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] 
-		            addsimps [Rep_llist_LCons]) 1);
-by (etac (Abs_llist_inverse RS ssubst) 1);
+		            addsimps [Rep_LList_LCons]) 1);
+by (etac (LListI RS Abs_LList_inverse RS ssubst) 1);
 by (rtac refl 1);
 qed "llistE";
 
 (** llist_corec: corecursion for 'a llist **)
 
-Goalw [llist_corec_def,LNil_def,LCons_def]
-    "llist_corec a f = sum_case (%u. LNil) \
-\                           (split(%z w. LCons z (llist_corec w f))) (f a)";
+(*Lemma for the proof of llist_corec*)
+Goal "LList_corec a \
+\          (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) : \
+\       llist(range Leaf)";
+by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
+by (rtac rangeI 1);
+by Safe_tac;
 by (stac LList_corec 1);
-by (res_inst_tac [("s","f(a)")] sumE 1);
+by (Force_tac 1);
+qed "LList_corec_type2";
+
+Goalw [llist_corec_def,LNil_def,LCons_def]
+    "llist_corec a f =  \
+\    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
+by (stac LList_corec 1);
+by (exhaust_tac "f a" 1);
 by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
-by (res_inst_tac [("p","y")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
-(*FIXME: correct case splits usd to be found automatically:
-by (ASM_SIMP_TAC(simpset() addsimps [LList_corec_type2]) 1);*)
+by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
 qed "llist_corec";
 
 (*definitional version of same*)
-val [rew] = goal LList.thy
-    "[| !!x. h(x) == llist_corec x f |] ==>     \
-\    h(a) = sum_case (%u. LNil) (split(%z w. LCons z (h w))) (f a)";
+val [rew] = 
+Goal "[| !!x. h(x) == llist_corec x f |] ==>     \
+\     h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))";
 by (rewtac rew);
 by (rtac llist_corec 1);
 qed "def_llist_corec";
@@ -611,48 +623,47 @@
 by (Fast_tac 1);
 qed "LListD_Fun_subset_Sigma_llist";
 
-Goal "prod_fun Rep_llist Rep_llist `` r <= \
+Goal "prod_fun Rep_LList Rep_LList `` r <= \
 \    (llist(range Leaf)) Times (llist(range Leaf))";
 by (fast_tac (claset() delrules [image_subsetI]
-		       addIs [Rep_llist]) 1);
+		       addIs [Rep_LList RS LListD]) 1);
 qed "subset_Sigma_llist";
 
-val [prem] = goal LList.thy
-    "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
-\    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
+Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
+\    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
 by Safe_tac;
-by (rtac (prem RS subsetD RS SigmaE2) 1);
+by (etac (subsetD RS SigmaE2) 1);
 by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
 qed "prod_fun_lemma";
 
-Goal "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
+Goal "prod_fun Rep_LList  Rep_LList `` range(%x. (x, x)) = \
 \    diag(llist(range Leaf))";
 by (rtac equalityI 1);
-by (fast_tac (claset() addIs [Rep_llist]) 1);
+by (Blast_tac 1);
 by (fast_tac (claset() delSWrapper "split_all_tac"
-		       addSEs [Abs_llist_inverse RS subst]) 1);
+		       addSEs [LListI RS Abs_LList_inverse RS subst]) 1);
 qed "prod_fun_range_eq_diag";
 
-(*Surprisingly hard to prove.  Used with lfilter*)
+(*Used with lfilter*)
 Goalw [llistD_Fun_def, prod_fun_def]
     "A<=B ==> llistD_Fun A <= llistD_Fun B";
 by Auto_tac;
 by (rtac image_eqI 1);
-by (fast_tac (claset() addss (simpset())) 1);
-by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);
+by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2);
+by (Force_tac 1);
 qed "llistD_Fun_mono";
 
 (** To show two llists are equal, exhibit a bisimulation! 
       [also admits true equality] **)
-val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
+Goalw [llistD_Fun_def]
     "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
-by (rtac (inj_Rep_llist RS injD) 1);
-by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
+by (rtac (inj_Rep_LList RS injD) 1);
+by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList ``r"),
                   ("A", "range(Leaf)")] 
         LList_equalityI 1);
-by (rtac (prem1 RS prod_fun_imageI) 1);
-by (rtac (prem2 RS image_mono RS subset_trans) 1);
+by (etac prod_fun_imageI 1);
+by (etac (image_mono RS subset_trans) 1);
 by (rtac (image_compose RS subst) 1);
 by (rtac (prod_fun_compose RS subst) 1);
 by (stac image_Un 1);
@@ -667,28 +678,27 @@
 by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
 qed "llistD_Fun_LNil_I";
 
-val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
+Goalw [llistD_Fun_def,LCons_def]
     "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
 by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
-by (rtac (prem RS prod_fun_imageI) 1);
+by (etac prod_fun_imageI 1);
 qed "llistD_Fun_LCons_I";
 
 (*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw [llistD_Fun_def]
-     "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
-by (rtac (Rep_llist_inverse RS subst) 1);
+Goalw [llistD_Fun_def] "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
+by (rtac (Rep_LList_inverse RS subst) 1);
 by (rtac prod_fun_imageI 1);
 by (stac image_Un 1);
 by (stac prod_fun_range_eq_diag 1);
-by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
+by (rtac (Rep_LList RS LListD RS LListD_Fun_diag_I) 1);
 qed "llistD_Fun_range_I";
 
 (*A special case of list_equality for functions over lazy lists*)
-val [prem1,prem2] = goal LList.thy
-    "[| f(LNil)=g(LNil);                                                \
-\       !!x l. (f(LCons x l),g(LCons x l)) :                            \
-\              llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
-\    |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
+val [prem1,prem2] =
+Goal "[| f(LNil)=g(LNil);                                                \
+\        !!x l. (f(LCons x l),g(LCons x l)) :                            \
+\               llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
+\     |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
 by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
 by (rtac rangeI 1);
 by (rtac subsetI 1);
@@ -777,8 +787,7 @@
 
 (*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
   for all u and all n::nat.*)
-val [prem] = goal LList.thy
-    "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
+val [prem] = Goal "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
 by (rtac ext 1);
 by (res_inst_tac [("r", 
    "UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
diff -r 44290b71a85f -r 9f0c8869cf71 src/HOL/Induct/LList.thy
--- 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
diff -r 44290b71a85f -r 9f0c8869cf71 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/SList.ML	Thu Nov 26 17:40:10 1998 +0100
@@ -6,6 +6,15 @@
 Definition of type 'a list by a least fixed point
 *)
 
+
+Goalw [List_def] "x : list (range Leaf) ==> x : List";
+by (Asm_simp_tac 1);
+qed "ListI";
+
+Goalw [List_def] "x : List ==> x : list (range Leaf)";
+by (Asm_simp_tac 1);
+qed "ListD";
+
 val list_con_defs = [NIL_def, CONS_def];
 
 Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
@@ -28,16 +37,17 @@
 qed "list_sexp";
 
 (* A <= sexp ==> list(A) <= sexp *)
-bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
+bind_thm ("list_subset_sexp", [list_mono, list_sexp] MRS subset_trans);
 
 (*Induction for the type 'a list *)
-val prems = goalw SList.thy [Nil_def,Cons_def]
+val prems = Goalw [Nil_def,Cons_def]
     "[| P(Nil);   \
 \       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
-by (rtac (Rep_list_inverse RS subst) 1);   (*types force good instantiation*)
-by (rtac (Rep_list RS list.induct) 1);
+by (rtac (Rep_List_inverse RS subst) 1);   (*types force good instantiation*)
+by (rtac (Rep_List RS ListD RS list.induct) 1);
 by (REPEAT (ares_tac prems 1
-     ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
+     ORELSE eresolve_tac [rangeE, ssubst, 
+			  ListI RS Abs_List_inverse RS subst] 1));
 qed "list_induct2";
 
 (*Perform induction on xs. *)
@@ -47,15 +57,15 @@
 
 (*** Isomorphisms ***)
 
-Goal "inj(Rep_list)";
+Goal "inj Rep_List";
 by (rtac inj_inverseI 1);
-by (rtac Rep_list_inverse 1);
-qed "inj_Rep_list";
+by (rtac Rep_List_inverse 1);
+qed "inj_Rep_List";
 
-Goal "inj_on Abs_list (list(range Leaf))";
+Goal "inj_on Abs_List List";
 by (rtac inj_on_inverseI 1);
-by (etac Abs_list_inverse 1);
-qed "inj_on_Abs_list";
+by (etac Abs_List_inverse 1);
+qed "inj_on_Abs_List";
 
 (** Distinctness of constructors **)
 
@@ -68,8 +78,8 @@
 val NIL_neq_CONS = sym RS CONS_neq_NIL;
 
 Goalw [Nil_def,Cons_def] "x # xs ~= Nil";
-by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1);
-by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
+by (rtac (CONS_not_NIL RS (inj_on_Abs_List RS inj_on_contraD)) 1);
+by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_List RS ListD, ListI]) 1));
 qed "Cons_not_Nil";
 
 bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
@@ -81,27 +91,26 @@
 qed "CONS_CONS_eq";
 
 (*For reasoning about abstract list constructors*)
-AddIs ([Rep_list] @ list.intrs);
+AddIs [Rep_List RS ListD, ListI];
+AddIs list.intrs;
 
 AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
 
-AddSDs [inj_on_Abs_list RS inj_onD,
-        inj_Rep_list RS injD, Leaf_inject];
+AddSDs [inj_on_Abs_List RS inj_onD,
+        inj_Rep_List RS injD, Leaf_inject];
 
 Goalw [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
 by (Fast_tac 1);
 qed "Cons_Cons_eq";
-bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
+bind_thm ("Cons_inject2", Cons_Cons_eq RS iffD1 RS conjE);
 
-val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
-by (rtac (major RS setup_induction) 1);
+Goal "CONS M N: list(A) ==> M: A & N: list(A)";
+by (etac setup_induction 1);
 by (etac list.induct 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Fast_tac);
 qed "CONS_D";
 
-val prems = goalw SList.thy [CONS_def,In1_def]
-    "CONS M N: sexp ==> M: sexp & N: sexp";
-by (cut_facts_tac prems 1);
+Goalw [CONS_def,In1_def] "CONS M N: sexp ==> M: sexp & N: sexp";
 by (fast_tac (claset() addSDs [Scons_D]) 1);
 qed "sexp_CONS_D";
 
@@ -199,13 +208,14 @@
 
 (*** list_rec -- by List_rec ***)
 
-val Rep_list_in_sexp =
-    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
+val Rep_List_in_sexp =
+    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_List RS ListD] 
+    MRS subsetD;
 
 local
-  val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
-                        Rep_list, rangeI, inj_Leaf, inv_f_f,
-                        sexp.LeafI, Rep_list_in_sexp]
+  val list_rec_simps = [ListI RS Abs_List_inverse, Rep_List_inverse,
+                        Rep_List RS ListD, rangeI, inj_Leaf, inv_f_f,
+                        sexp.LeafI, Rep_List_in_sexp]
 in
   val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
       "list_rec Nil c h = c"
@@ -220,12 +230,12 @@
 
 
 (*Type checking.  Useful?*)
-val major::A_subset_sexp::prems = goal SList.thy
-    "[| M: list(A);     \
-\       A<=sexp;        \
-\       c: C(NIL);      \
-\       !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
-\    |] ==> List_rec M c h : C(M :: 'a item)";
+val major::A_subset_sexp::prems = 
+Goal "[| M: list(A);     \
+\        A<=sexp;        \
+\        c: C(NIL);      \
+\        !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
+\     |] ==> List_rec M c h : C(M :: 'a item)";
 val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
 val sexp_A_I = A_subset_sexp RS subsetD;
 by (rtac (major RS list.induct) 1);
@@ -238,8 +248,7 @@
 by (rtac list_rec_Nil 1);
 qed "Rep_map_Nil";
 
-Goalw [Rep_map_def]
-    "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
+Goalw [Rep_map_def] "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
 by (rtac list_rec_Cons 1);
 qed "Rep_map_Cons";
 
@@ -252,21 +261,20 @@
 by (rtac List_rec_NIL 1);
 qed "Abs_map_NIL";
 
-val prems = goalw SList.thy [Abs_map_def]
-    "[| M: sexp;  N: sexp |] ==> \
-\    Abs_map g (CONS M N) = g(M) # Abs_map g N";
-by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
+Goalw [Abs_map_def]
+    "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N";
+by (REPEAT (ares_tac [List_rec_CONS] 1));
 qed "Abs_map_CONS";
 
 (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
-val [rew] = goal SList.thy
-    "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
+val [rew] = 
+Goal "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
 by (rewtac rew);
 by (rtac list_rec_Nil 1);
 qed "def_list_rec_Nil";
 
-val [rew] = goal SList.thy
-    "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
+val [rew] = 
+Goal "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
 by (rewtac rew);
 by (rtac list_rec_Cons 1);
 qed "def_list_rec_Cons";
@@ -327,11 +335,12 @@
 
 Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
 
-val [major,A_subset_sexp,minor] = goal SList.thy 
-    "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
-\    ==> Rep_map f (Abs_map g M) = M";
+val [major,A_subset_sexp,minor] = 
+Goal "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
+\     ==> Rep_map f (Abs_map g M) = M";
 by (rtac (major RS list.induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
+by (ALLGOALS 
+    (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
 qed "Abs_map_inverse";
 
 (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
@@ -339,7 +348,7 @@
 (** list_case **)
 
 Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\                        (!y ys. xs=y#ys --> P(f y ys)))";
+\                           (!y ys. xs=y#ys --> P(f y ys)))";
 by (list_ind_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "split_list_case2";
diff -r 44290b71a85f -r 9f0c8869cf71 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/SList.thy	Thu Nov 26 17:40:10 1998 +0100
@@ -12,53 +12,14 @@
 
 SList = Sexp +
 
-types
-  'a list
-
-arities
-  list :: (term) term
-
-
 consts
 
   list        :: 'a item set => 'a item set
-  Rep_list    :: 'a list => 'a item
-  Abs_list    :: 'a item => 'a list
   NIL         :: 'a item
   CONS        :: ['a item, 'a item] => 'a item
-  Nil         :: 'a list
-  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
   List_case   :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
   List_rec    :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
-  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
-  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
-  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
-  Abs_map     :: ('a item => 'b) => 'a item => 'b list
-  null        :: 'a list => bool
-  hd          :: 'a list => 'a
-  tl,ttl      :: 'a list => 'a list
-  set         :: ('a list => 'a set)
-  mem         :: ['a, 'a list] => bool                            (infixl 55)
-  map         :: ('a=>'b) => ('a list => 'b list)
-  "@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
-  filter      :: ['a => bool, 'a list] => 'a list
 
-  (* list Enumeration *)
-
-  "[]"        :: 'a list                              ("[]")
-  "@list"     :: args => 'a list                      ("[(_)]")
-
-  (* Special syntax for filter *)
-  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
-
-translations
-  "[x, xs]"     == "x#[xs]"
-  "[x]"         == "x#[]"
-  "[]"          == "Nil"
-
-  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
-
-  "[x:xs . P]"  == "filter (%x. P) xs"
 
 defs
   (* Defining the Concrete Constructors *)
@@ -70,17 +31,34 @@
     NIL_I  "NIL: list(A)"
     CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"
 
-rules
-  (* Faking a Type Definition ... *)
-  Rep_list          "Rep_list(xs): list(range(Leaf))"
-  Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
-  Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
+
+typedef (List)
+  'a list = "list(range Leaf)" (list.NIL_I)
+
+  
+(*Declaring the abstract list constructors*)
+consts
+  Nil         :: 'a list
+  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
+
+  (* list Enumeration *)
+
+  "[]"        :: 'a list                              ("[]")
+  "@list"     :: args => 'a list                      ("[(_)]")
+
+  (* Special syntax for filter *)
+  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
+
+
+translations
+  "[x, xs]"     == "x#[xs]"
+  "[x]"         == "x#[]"
+  "[]"          == "Nil"
 
 
 defs
-  (* Defining the Abstract Constructors *)
-  Nil_def       "Nil == Abs_list(NIL)"
-  Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
+  Nil_def       "Nil  == Abs_List NIL"
+  Cons_def      "x#xs == Abs_List(CONS (Leaf x) (Rep_List xs))"
 
   List_case_def "List_case c d == Case (%x. c) (Split d)"
 
@@ -90,30 +68,61 @@
    "List_rec M c d == wfrec (trancl pred_sexp)
                             (%g. List_case c (%x y. d x y (g y))) M"
 
-  list_rec_def
-   "list_rec l c d == 
-   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
+
+
+
+constdefs
+  (* Generalized Map Functionals *)
+  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
+    "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
+  
+  Abs_map     :: ('a item => 'b) => 'a item => 'b list
+    "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+
 
-  (* Generalized Map Functionals *)
+  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
+    "list_rec l c d == 
+     List_rec (Rep_List l) c (%x y r. d (inv Leaf x) (Abs_List y) r)"
 
-  Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
-  Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+  null        :: 'a list => bool
+    "null(xs)            == list_rec xs True (%x xs r. False)"
+
+  hd          :: 'a list => 'a
+    "hd(xs)              == list_rec xs arbitrary (%x xs r. x)"
+
+  tl          :: 'a list => 'a list
+     "tl(xs)              == list_rec xs arbitrary (%x xs r. xs)"
 
-  null_def      "null(xs)            == list_rec xs True (%x xs r. False)"
-  hd_def        "hd(xs)              == list_rec xs arbitrary (%x xs r. x)"
-  tl_def        "tl(xs)              == list_rec xs arbitrary (%x xs r. xs)"
-  (* a total version of tl: *)
-  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r. xs)"
+  (* a total version of tl *)
+  ttl         :: 'a list => 'a list
+    "ttl(xs)             == list_rec xs [] (%x xs r. xs)"
+
+  set         :: ('a list => 'a set)
+    "set xs              == list_rec xs {} (%x l r. insert x r)"
 
-  set_def       "set xs              == list_rec xs {} (%x l r. insert x r)"
+  mem         :: ['a, 'a list] => bool                            (infixl 55)
+    "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
+
+  map         :: ('a=>'b) => ('a list => 'b list)
+    "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
+
+  filter      :: ['a => bool, 'a list] => 'a list
+    "filter P xs == list_rec xs [] (%x xs r. if P(x) then x#r else r)"
 
-  mem_def       "x mem xs            == 
-                   list_rec xs False (%y ys r. if y=x then True else r)"
-  map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
-  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
-  filter_def    "filter P xs         == 
-                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
+  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
+    "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+
+
+consts
+  "@" :: ['a list, 'a list] => 'a list                    (infixr 65)
 
-  list_case_def  "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+defs
+  append_def  "xs@ys == list_rec xs ys (%x l r. x#r)"
+
+
+translations
+  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
+
+  "[x:xs . P]"  == "filter (%x. P) xs"
 
 end