Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
authoroheimb
Wed, 03 Apr 1996 19:27:14 +0200
changeset 1637 b8a8ae2e5de1
parent 1636 e18416e3e1d4
child 1638 69c094639823
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/axioms.ML	Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/axioms.ML	Wed Apr 03 19:27:14 1996 +0200
@@ -1,5 +1,4 @@
 (* axioms.ML
-   ID:         $Id$
    Author : David von Oheimb
    Created: 31-May-95
    Updated: 12-Jun-95 axioms for discriminators, selectors and induction
@@ -24,137 +23,129 @@
 fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
 let
 
-(* ----- axioms and definitions concerning the isomorphism ------------------------ *)
+(* ----- axioms and definitions concerning the isomorphism ------------------ *)
 
   val dc_abs = %%(dname^"_abs");
   val dc_rep = %%(dname^"_rep");
   val x_name'= "x";
   val x_name = idx_name eqs x_name' (n+1);
 
-  val ax_abs_iso = (dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name') === %x_name'));
-  val ax_rep_iso = (dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name') === %x_name'));
+ val ax_abs_iso=(dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
+ val ax_rep_iso=(dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
 
   val ax_when_def = (dname^"_when_def",%%(dname^"_when") == 
-           foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
-                                Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
+     foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
+				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
 
-  val ax_copy_def = let
-    fun simp_oo (Const ("fapp", _) $ (Const ("fapp", _) $ 
-                 Const ("cfcomp", _) $ fc) $ Const ("ID", _)) = fc
-    |   simp_oo t = t;
-    fun simp_app (Const ("fapp", _) $ Const ("ID", _) $ t) = t
-    |   simp_app t = t;
-        fun mk_arg m n arg  = (if is_lazy arg 
-                               then fn t => %%"lift"`(simp_oo (%%"up" oo t)) else Id)
-                              (if_rec arg (cproj (Bound (2*min[n,m])) eqs) (%%"ID"));
-        fun mk_prod (t1,t2)  = %%"ssplit"`(/\ "x" (/\ "y" (%%"spair"`
-                                         simp_app(t1`Bound 1)`simp_app(t2`Bound 0))));
-        fun one_con (_,args) = if args = [] then %%"ID" else
-                               foldr' mk_prod (mapn (mk_arg (length args-1)) 1 args);
-        fun mk_sum  (t1,t2)  = %%"sswhen"`(simp_oo (%%"sinl" oo t1))
-                                         `(simp_oo (%%"sinr" oo t2));
-        in (dname^"_copy_def", %%(dname^"_copy") == /\"f" 
-                          (dc_abs oo foldr' mk_sum (map one_con cons) oo dc_rep)) end;
+  fun con_def outer recu m n (_,args) = let
+     fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id)
+			(if recu andalso is_rec arg then (cproj (Bound z) 
+			(length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x));
+     fun parms [] = %%"one"
+     |   parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs);
+     fun inj y 1 _ = y
+     |   inj y _ 0 = %%"sinl"`y
+     |   inj y i j = %%"sinr"`(inj y (i-1) (j-1));
+  in foldr /\# (args, outer (inj (parms args) m n)) end;
 
-(* ----- definitions concerning the constructors, discriminators and selectors ---- *)
+  val ax_copy_def = (dname^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo 
+	foldl (op `) (%%(dname^"_when") , 
+	              mapn (con_def Id true (length cons)) 0 cons)));
 
-  val axs_con_def = let
-        fun idxs z x arg = (if is_lazy arg then fn x => %%"up"`x else Id)(Bound(z-x));
-        fun prms [] = %%"one"
-        |   prms vs = foldr' (fn(x,t)=> %%"spair"`x`t) (mapn (idxs (length vs)) 1 vs);
-        val injs    = bin_branchr (fn l=> l@["l"]) (fn l=> l@["r"]);
-        fun cdef ((con,args),injs) = (extern_name con ^"_def",%%con == 
-                 foldr /\# (args,dc_abs`
-                (foldr (fn (i,t) => %%("sin"^i)`t ) (injs, prms args))));
-        in map cdef (cons~~(mapn (fn n => K(injs [] cons n)) 0 cons)) end;
+(* -- definitions concerning the constructors, discriminators and selectors - *)
+
+  val axs_con_def = mapn (fn n => fn (con,args) => (extern_name con ^"_def",  
+  %%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons;
 
   val axs_dis_def = let
-        fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
-                 mk_cfapp(%%(dname^"_when"),map 
-                        (fn (con',args) => (foldr /\#
-                           (args,if con'=con then %%"TT" else %%"FF"))) cons))
-        in map ddef cons end;
+	fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
+		 mk_cfapp(%%(dname^"_when"),map 
+			(fn (con',args) => (foldr /\#
+			   (args,if con'=con then %%"TT" else %%"FF"))) cons))
+	in map ddef cons end;
 
   val axs_sel_def = let
-        fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
-                 mk_cfapp(%%(dname^"_when"),map 
-                        (fn (con',args) => if con'<>con then %%"UU" else
-                         foldr /\# (args,Bound (length args - n))) cons));
-        in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+	fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
+		 mk_cfapp(%%(dname^"_when"),map 
+			(fn (con',args) => if con'<>con then %%"UU" else
+			 foldr /\# (args,Bound (length args - n))) cons));
+	in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
 
 
-(* ----- axiom and definitions concerning induction ------------------------------- *)
+(* ----- axiom and definitions concerning induction ------------------------- *)
 
-  fun cproj' T = cproj T eqs n;
-  val ax_reach    = (dname^"_reach"   , mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
-                                        `%x_name === %x_name));
-  val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",
-                    cproj'(%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
+  fun cproj' T = cproj T (length eqs) n;
+  val ax_reach = (dname^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
+					`%x_name === %x_name));
+  val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
+		    (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
   val ax_finite_def = (dname^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
-        mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+	mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
 in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @
     axs_con_def @ axs_dis_def @ axs_sel_def @
-   [ax_reach, ax_take_def, ax_finite_def] end;
+   [ax_reach, ax_take_def, ax_finite_def] 
+end; (* let *)
 
 
 in (* local *)
 
-fun add_axioms (comp_dname, eqs : eq list) thy' =let
+fun add_axioms (comp_dname, eqs : eq list) thy' = let
   val dnames = map (fst o fst) eqs;
   val x_name = idx_name dnames "x"; 
   fun copy_app dname = %%(dname^"_copy")`Bound 0;
-  val ax_copy_def  = (comp_dname^"_copy_def" , %%(comp_dname^"_copy") ==
-                                           /\"f"(foldr' cpair (map copy_app dnames)));
-  val ax_bisim_def = (comp_dname^"_bisim_def",%%(comp_dname^"_bisim") == mk_lam("R",
+  val ax_copy_def =(comp_dname^"_copy_def" , %%(comp_dname^"_copy") ==
+				    /\"f"(foldr' cpair (map copy_app dnames)));
+  val ax_bisim_def=(comp_dname^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
     let
       fun one_con (con,args) = let
-        val nonrec_args = filter_out is_rec args;
-        val    rec_args = filter     is_rec args;
-        val nonrecs_cnt = length nonrec_args;
-        val    recs_cnt = length    rec_args;
-        val allargs     = nonrec_args @ rec_args
-                                      @ map (upd_vname (fn s=> s^"'")) rec_args;
-        val allvns      = map vname allargs;
-        fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
-        val vns1        = map (vname_arg "" ) args;
-        val vns2        = map (vname_arg "'") args;
-        val allargs_cnt = nonrecs_cnt + 2*recs_cnt;
-        val rec_idxs    = (recs_cnt-1) downto 0;
-        val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
-                                           (allargs~~((allargs_cnt-1) downto 0)));
-        fun rel_app i ra = proj (Bound(allargs_cnt+2)) dnames (rec_of ra) $ 
-                           Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
-        val capps = foldr mk_conj (mapn rel_app 1 rec_args,
-         mk_conj(Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
-                 Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2)));
+	val nonrec_args = filter_out is_rec args;
+	val    rec_args = filter     is_rec args;
+	val    recs_cnt = length rec_args;
+	val allargs     = nonrec_args @ rec_args
+				      @ map (upd_vname (fn s=> s^"'")) rec_args;
+	val allvns      = map vname allargs;
+	fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
+	val vns1        = map (vname_arg "" ) args;
+	val vns2        = map (vname_arg "'") args;
+	val allargs_cnt = length nonrec_args + 2*recs_cnt;
+	val rec_idxs    = (recs_cnt-1) downto 0;
+	val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
+					 (allargs~~((allargs_cnt-1) downto 0)));
+	fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $ 
+			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
+	val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
+	   Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
+	   Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2)));
         in foldr mk_ex (allvns, foldr mk_conj 
-                                      (map (defined o Bound) nonlazy_idxs,capps)) end;
-      fun one_comp n (_,cons) = mk_all(x_name (n+1), mk_all(x_name (n+1)^"'", mk_imp(
-                        proj (Bound 2) dnames n $ Bound 1 $ Bound 0,
-         foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)::map one_con cons))));
+			      (map (defined o Bound) nonlazy_idxs,capps)) end;
+      fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
+	 		proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0,
+         		foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+					::map one_con cons))));
     in foldr' mk_conj (mapn one_comp 0 eqs)end ));
   val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @
-                (if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
+		(if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
 in thy' |> add_axioms_i (infer_types thy' thy_axs) end;
 
 
-fun add_gen_by ((tname,finite),(typs,cnstrs)) thy' = let
-  fun pred_name typ ="P"^(if typs=[typ] then "" else string_of_int(1+find(typ,typs)));
-  fun lift_adm t = lift (fn typ => %%"adm" $ %(pred_name typ)) 
-                        (if finite then [] else typs,t);
-  fun lift_pred_UU t = lift (fn typ => %(pred_name typ) $ UU) (typs,t);
+fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
+  fun P_name typ = "P"^(if typs = [typ] then "" 
+			else string_of_int(1 + find(typ,typs)));
+  fun lift_adm t = lift (fn typ => %%"adm" $ %(P_name typ)) 
+			(if finite then [] else typs,t);
+  fun lift_pred_UU t = lift (fn typ => %(P_name typ) $ UU) (typs,t);
   fun one_cnstr (cnstr,vns,(args,res)) = let 
-                        val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args);
-                        val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns);
-                     in foldr mk_All (vns,
-                         lift (fn (vn,typ) => %(pred_name typ) $ bound_arg vns vn)
-                              (rec_args,defined app ==> %(pred_name res)$app)) end;
-  fun one_conc typ = let val pn = pred_name typ in
-                     %pn $ %("x"^implode(tl(explode pn))) end;
+		val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args);
+		val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns);
+	     in foldr mk_All (vns,
+			 lift (fn (vn,typ) => %(P_name typ) $ bound_arg vns vn)
+			      (rec_args,defined app ==> %(P_name res)$app)) end;
+  fun one_conc typ = let val pn = P_name typ 
+		     in %pn $ %("x"^implode(tl(explode pn))) end;
   val concl = mk_trp(foldr' mk_conj (map one_conc typs));
-  val induct =(tname^"_induct",lift_adm(lift_pred_UU(
-                        foldr (op ===>) (map one_cnstr cnstrs,concl))));
+  val induct = (tname^"_induct",lift_adm(lift_pred_UU(
+			foldr (op ===>) (map one_cnstr cnstrs,concl))));
 in thy' |> add_axioms_i (infer_types thy' [induct]) end;
 
 end; (* local *)
--- a/src/HOLCF/domain/extender.ML	Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/extender.ML	Wed Apr 03 19:27:14 1996 +0200
@@ -1,5 +1,4 @@
 (* extender.ML
-   ID:         $Id$
    Author : David von Oheimb
    Created: 17-May-95
    Updated: 31-May-95 extracted syntax.ML, theorems.ML
@@ -10,7 +9,7 @@
 *)
 
 
-structure Extender =
+structure Domain_Extender =
 struct
 
 local
@@ -20,78 +19,77 @@
 (* ----- general testing and preprocessing of constructor list -------------------- *)
 
   fun check_domain(eqs':((string * typ list) *
-                  (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
+		  (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
     val dtnvs = map fst eqs';
     val cons' = flat (map snd eqs');
     val test_dupl_typs = (case duplicates (map fst dtnvs) of 
-        [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
+	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
     val test_dupl_cons = (case duplicates (map first cons') of 
-        [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
+	[] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
     val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of
         [] => false | dups => error ("Duplicate selectors: "^commas_quote dups));
     val test_dupl_tvars = let fun vname (TFree(v,_)) = v
-                              |   vname _            = Imposs "extender:vname";
-                          in exists (fn tvars => case duplicates (map vname tvars) of
-        [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
-        (map snd dtnvs) end;
+			      |   vname _            = Imposs "extender:vname";
+			  in exists (fn tvars => case duplicates (map vname tvars) of
+	[] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
+	(map snd dtnvs) end;
     (*test for free type variables and invalid use of recursive type*)
     val analyse_types = forall (fn ((_,typevars),cons') => 
-        forall (fn con' => let
-          val types = map third (third con');
+	forall (fn con' => let
+	  val types = map third (third con');
           fun analyse(t as TFree(v,_)) = t mem typevars orelse
-                                        error ("Free type variable " ^ v ^ " on rhs.")
-            | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
-                                      | Some tvs => tvs = typl orelse 
-                       error ("Recursion of type " ^ s ^ " with different arguments"))
-            | analyse(TVar _) = Imposs "extender:analyse"
-          and analyses ts = forall analyse ts;
-          in analyses types end) cons' 
-        ) eqs';
+					error ("Free type variable " ^ v ^ " on rhs.")
+	    | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
+				      | Some tvs => tvs = typl orelse 
+		       error ("Recursion of type " ^ s ^ " with different arguments"))
+	    | analyse(TVar _) = Imposs "extender:analyse"
+	  and analyses ts = forall analyse ts;
+	  in analyses types end) cons' 
+	) eqs';
     in true end; (* let *)
 
   fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let
     val test_dupl_typs = (case duplicates typs' of [] => false
-          | dups => error ("Duplicate types: " ^ commas_quote dups));
+	  | dups => error ("Duplicate types: " ^ commas_quote dups));
     val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false
-          | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
+	  | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
     val tsig = #tsig(Sign.rep_sg(sign_of thy'));
     val tycons = map fst (#tycons(Type.rep_tsig tsig));
     val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs';
     val cnstrss = let
-        fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
-                                | None => error ("Unknown constructor: "^c);
-        fun args_result_type (t as (Type(tn,[arg,rest]))) = 
-                        if tn = "->" orelse tn = "=>"
-                        then let val (ts,r) = args_result_type rest in (arg::ts,r) end
-                        else ([],t)
-        |   args_result_type t = ([],t);
+	fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
+				| None => error ("Unknown constructor: "^c);
+	fun args_result_type (t as (Type(tn,[arg,rest]))) = 
+			if tn = "->" orelse tn = "=>"
+			then let val (ts,r) = args_result_type rest in (arg::ts,r) end
+			else ([],t)
+	|   args_result_type t = ([],t);
     in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in
-                         (cn,mk_var_names args,(args,res)) end)) cnstrss' 
-        : (string *                     (* operator name of constr *)
-           string list *                (* argument name list *)
-           (typ list *                  (* argument types *)
-            typ))                       (* result type *)
-          list list end;
+	                 (cn,mk_var_names args,(args,res)) end)) cnstrss' 
+	: (string * 			(* operator name of constr *)
+	   string list *		(* argument name list *)
+	   (typ list *			(* argument types *)
+	    typ))			(* result type *)
+	  list list end;
     fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse
-                               error("Inappropriate result type for constructor "^cn);
-    val typs = map (fn (tn, cnstrs) => 
-                     (map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs)))))
-                   (typs'~~cnstrss);
+			       error("Inappropriate result type for constructor "^cn);
+    val typs = map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs; 
+					snd(third(hd(cnstrs)))))  (typs'~~cnstrss);
     val test_typs = map (fn (typ,cnstrs) => 
-                        if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
-                        then error("Not a pcpo type: "^fst(type_name_vars typ))
-                        else map (fn (cn,_,(_,rt)) => rt=typ 
-                          orelse error("Non-identical result types for constructors "^
-                          first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
+			if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
+			then error("Not a pcpo type: "^fst(type_name_vars typ))
+			else map (fn (cn,_,(_,rt)) => rt=typ 
+		 	  orelse error("Non-identical result types for constructors "^
+			  first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
     val proper_args = let
-        fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
-        |   occurs _  _              = false;
-        fun proper_arg cn atyp = forall (fn typ => let 
-                                   val tn = fst(type_name_vars typ) 
-                                   in atyp=typ orelse not (occurs tn atyp) orelse 
-                                      error("Illegal use of type "^ tn ^
-                                         " as argument of constructor " ^cn)end )typs;
-        fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
+	fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
+	|   occurs _  _              = false;
+	fun proper_arg cn atyp = forall (fn typ => let 
+				   val tn = fst(type_name_vars typ) 
+				   in atyp=typ orelse not (occurs tn atyp) orelse 
+				      error("Illegal use of type "^ tn ^
+					 " as argument of constructor " ^cn)end )typs;
+	fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
     in map (map proper_curry) cnstrss end;
   in (typs, flat cnstrss) end;
 
@@ -100,16 +98,16 @@
 in
 
   fun add_domain (comp_dname,eqs') thy'' = let
-    val ok_dummy = check_domain eqs';
+    val ok   = check_domain eqs';
     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs');
     val dts  = map (Type o fst) eqs';
     fun cons cons' = (map (fn (con,syn,args) =>
-        (ThyOps.const_name con syn,
-         map (fn ((lazy,sel,tp),vn) => ((lazy,
-                                         find (tp,dts) handle LIST "find" => ~1),
-                                        sel,vn))
-             (args~~(mk_var_names(map third args)))
-         )) cons') : cons list;
+	(ThyOps.const_name con syn,
+	 map (fn ((lazy,sel,tp),vn) => ((lazy,
+					 find (tp,dts) handle LIST "find" => ~1),
+					sel,vn))
+	     (args~~(mk_var_names(map third args)))
+	 )) cons') : cons list;
     val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
     val thy         = thy' |> Domain_Axioms.add_axioms (comp_dname,eqs);
   in (thy,eqs) end;
@@ -117,7 +115,7 @@
   fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
    val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss');
   in
-   Domain_Axioms.add_gen_by ((tname,finite),(typs,cnstrs)) thy' end;
+   Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
 
 end (* local *)
 end (* struct *)
--- a/src/HOLCF/domain/interface.ML	Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/interface.ML	Wed Apr 03 19:27:14 1996 +0200
@@ -1,6 +1,5 @@
 (* interface.ML
-   ID:         $Id$
-   Author:      David von Oheimb
+   Author:  David von Oheimb
    Created: 17-May-95
    Updated: 24-May-95
    Updated: 03-Jun-95 incremental change of ThySyn
@@ -11,39 +10,38 @@
    Copyright 1995 TU Muenchen
 *)
 
-local
+structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *)
 
-structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData!!!!!!! *)
 struct
 
 local 
   open ThyParse;
   open Domain_Library;
 
-(* ----- generation of bindings for axioms and theorems in trailer of .thy.ML ----- *)
+(* --- generation of bindings for axioms and theorems in trailer of .thy.ML - *)
 
-  fun gt_ax         name   = "get_axiom thy "^quote name;
-  fun gen_val dname name   = "val "^name^" = " ^gt_ax (dname^"_"^name)^";";
-  fun gen_vall      name l = "val "^name^" = " ^mk_list l^";";
+  fun gt_ax         name   = "get_axiom thy " ^ quote name;
+  fun gen_val dname name   = "val "^name^" = "^ gt_ax (dname^"_"^name)^";";
+  fun gen_vall      name l = "val "^name^" = "^ mk_list l^";";
   val rews1 = "iso_rews @ when_rews @\n\
-              \con_rews @ sel_rews @ dis_rews @ dists_eq @ dists_le @\n\
-              \copy_rews";
+ 	      \con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\
+	      \copy_rews";
 
   fun gen_domain eqname num ((dname,_), cons') = let
     val axioms1 = ["abs_iso", "rep_iso", "when_def"];
-                   (* con_defs , sel_defs, dis_defs *) 
+		   (* con_defs , sel_defs, dis_defs *) 
     val axioms2 = ["copy_def"];
     val theorems = 
-        "iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
-        \dists_eq, dists_le, inverts, injects, copy_rews";
+	"iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
+	\dists_le, dists_eq, inverts, injects, copy_rews";
     in
       "structure "^dname^" = struct\n"^
       cat_lines(map (gen_val dname) axioms1)^"\n"^
       gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
       gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => 
-                                             gt_ax(sel^"_def")) args)    cons'))^"\n"^
+					     gt_ax(sel^"_def")) args)    cons'))^"\n"^
       gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) 
-                                                                          cons')^"\n"^
+								          cons')^"\n"^
       cat_lines(map (gen_val dname) axioms2)^"\n"^
       "val ("^ theorems ^") =\n\
       \Domain_Theorems.theorems thy "^eqname^";\n" ^
@@ -57,117 +55,112 @@
     val comp_dname = implode (separate "_" dnames);
     val conss' = map (fn (dname,cons'') =>
       let
-        fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
-                                                         "_"^(string_of_int m)
-                                  |  Some s => s)
-        fun fill_sels n con = upd_third (mapn (sel n) 1) con;
+	fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
+							 "_"^(string_of_int m)
+				  |  Some s => s)
+	fun fill_sels n con = upd_third (mapn (sel n) 1) con;
       in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs''));
     val eqs' = dtnvs~~conss';
 
-(* ----- generation of argument string for calling add_domain --------------------- *)
-
-
-     fun string_of_sort_emb [] = ""
-     |   string_of_sort_emb [x] = "\"" ^x^ "\"" 
-        |   string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs);
-
-        fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
+(* ----- string for calling add_domain -------------------------------------- *)
 
-    fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
-    and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)
-    |   mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args)
-    |   mk_typ _                  = Imposs "interface:mk_typ";
-    fun mk_conslist cons' = mk_list (map 
-          (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
-     (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
-                                    mk_typ tp)) ts))) cons');
+    val thy_ext_string = let
+      fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
+      and mk_typ (TFree(name,sort))= "TFree"^mk_pair(quote name,
+						     mk_list(map quote sort))
+      |   mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args)
+      |   mk_typ _                 = Imposs "interface:mk_typ";
+      fun mk_conslist cons' = mk_list (map 
+	    (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
+       (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
+				      mk_typ tp)) ts))) cons');
+    in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n"
+       ^ mk_pair(quote comp_dname,
+		 mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
+       ^ ";\nval thy = thy"
+    end;
+
+(* ----- string for calling (comp_)theorems and producing the structures ---------- *)
+
+    val val_gen_string =  let
+      fun plural s = if num > 1 then s^"s" else "["^s^"]";
+      val comp_axioms   = [(* copy, *) "reach", "take_def", "finite_def"
+			   (*, "bisim_def" *)];
+      val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
+			       ["take_lemma","finite"]))^", finite_ind, ind, coind";
+      fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
+							 ^comp_dname^"_equations)";
+      fun collect sep name = if num = 1 then name else
+			     implode (separate sep (map (fn s => s^"."^name) dnames));
     in
-      ("val (thy, "^comp_dname^"_equations) = thy |> Extender.add_domain \n"
-      ^ mk_pair(quote comp_dname,
-                mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
-      ^ ";\nval thy = thy",
-      let
-        fun plural s = if num > 1 then s^"s" else "["^s^"]";
-        val comp_axioms   = [(* copy, *) "take_def", "finite_def", "reach" 
-                             (*, "bisim_def" *)];
-        val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
-                                ["take_lemma","finite"]))^", finite_ind, ind, coind";
-        fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
-                                                           ^comp_dname^"_equations)";
-        fun collect sep name = if num = 1 then name else
-                           implode (separate sep (map (fn s => s^"."^name) dnames));
-      in
-        implode (separate "end; (* struct *)\n\n" 
-                 (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
-        "end; (* struct *)\n\n\
-        \structure "^comp_dname^" = struct\n" else "") ^
-         (if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
-         implode ((map (fn s => gen_vall (plural s)
-                  (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
-         gen_val comp_dname "bisim_def" ^"\n\
+      implode (separate "end; (* struct *)\n\n" 
+        	 (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
+      "end; (* struct *)\n\n\
+      \structure "^comp_dname^" = struct\n" else "") ^
+	(if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
+	implode ((map (fn s => gen_vall (plural s)
+	           (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
+	 gen_val comp_dname "bisim_def" ^"\n\
         \val ("^ comp_theorems ^") =\n\
-        \Domain_Theorems.comp_theorems thy \
-        \(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
-        \ ["^collect "," "cases"    ^"],\n\
-        \ "^ collect "@" "con_rews " ^",\n\
-        \ "^ collect "@" "copy_rews" ^");\n\
-        \val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
-        \end; (* struct *)"
-      end
-      ) end;
+	\Domain_Theorems.comp_theorems thy \
+	\(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
+	\ ["^collect "    ," "cases"    ^"],\n\
+	\  "^collect "@"     "con_rews " ^",\n\
+	\  "^collect " @"    "copy_rews" ^");\n\
+	\val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
+      \end; (* struct *)"
+    end;
+  in (thy_ext_string, val_gen_string) end;
+
+(* ----- strings for calling add_gen_by and producing the value binding ----------- *)
 
   fun mk_gen_by (finite,eqs) = let
       val typs    = map fst eqs;
       val cnstrss = map snd eqs;
       val tname = implode (separate "_" typs) in
-      ("|> Extender.add_gen_by "
-      ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
-                mk_pair(mk_list(map quote typs), 
-                        mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
-      "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
+      ("|> Domain_Extender.add_gen_by "
+       ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
+		 mk_pair(mk_list(map quote typs), 
+			 mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
+       "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
 
 (* ----- parser for domain declaration equation ----------------------------------- *)
 
 (**
   val sort = name >> (fn s => [strip_quotes s])
-          || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
+	  || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
   val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree
 **)
   val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));
 
   val type_args = "(" $$-- !! (list1 tvar --$$ ")")
-               || tvar  >> (fn x => [x])
-               || empty >> K [];
+	       || tvar  >> (fn x => [x])
+	       || empty >> K [];
   val con_typ     = type_args -- ident >> (fn (x,y) => Type(y,x));
   val typ         = con_typ 
-                 || tvar;
+		 || tvar;
   val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
-                          -- (optional ((ident >> Some) --$$ "::") None)
-                          -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
-                 || ident >> (fn x => (false,None,Type(x,[])))
-                 || tvar  >> (fn x => (false,None,x));
+			  -- (optional ((ident >> Some) --$$ "::") None)
+			  -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
+		 || ident >> (fn x => (false,None,Type(x,[])))
+		 || tvar  >> (fn x => (false,None,x));
   val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) 
-                    -- ThyOps.opt_cmixfix
-                    >> (fn ((con,args),syn) => (con,syn,args));
+		    -- ThyOps.opt_cmixfix
+		    >> (fn ((con,args),syn) => (con,syn,args));
 in
   val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
-                               (enum1 "|" domain_cons)))            >> mk_domain;
+			       (enum1 "|" domain_cons))) 	    >> mk_domain;
   val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
-                    (enum1 "," (ident   --$$ "by" -- !!
-                               (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
-end;
+		    (enum1 "," (ident   --$$ "by" -- !!
+			       (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
+end; (* local *)
 
 val user_keywords = "lazy"::"by"::"finite"::
-                (**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
-                    ThySynData.user_keywords;
+		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
+		    ThySynData.user_keywords;
 val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
-                (**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
-                    ThySynData.user_sections;
-end;
-
-in
+		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
+		    ThySynData.user_sections;
+end; (* struct *)
 
 structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)
-
-end; (* local *)
-
--- a/src/HOLCF/domain/library.ML	Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/library.ML	Wed Apr 03 19:27:14 1996 +0200
@@ -1,26 +1,25 @@
 (* library.ML
-   ID:         $Id$
-   Author:      David von Oheimb
+   Author : David von Oheimb
    Created: 18-Jul-95 extracted from syntax.ML, axioms.ML, extender.ML, interface.ML
    Updated: 30-Aug-95
+   Updated: 20-Oct-95 small improvement for atomize
    Copyright 1995 TU Muenchen
 *)
 
-(* ----- general support ---------------------------------------------------------- *)
+(* ----- general support ---------------------------------------------------- *)
 
 fun Id x = x;
 
 fun mapn f n []      = []
 |   mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
 
-fun foldr'' f (l,f2) =
-  let fun itr []  = raise LIST "foldr''"
-        | itr [a] = f2 a
-        | itr (a::l) = f(a, itr l)
-  in  itr l  end;
+fun foldr'' f (l,f2) = let fun itr []  = raise LIST "foldr''"
+			     | itr [a] = f2 a
+			     | itr (a::l) = f(a, itr l)
+in  itr l  end;
 fun foldr' f l = foldr'' f (l,Id);
-fun map_cumulr f start xs = foldr (fn (x,(ys,res)) => case f(x,res) of (y,res2) => 
-                                                      (y::ys,res2)) (xs,([],start));
+fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
+						  (y::ys,res2)) (xs,([],start));
 
 
 fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
@@ -28,21 +27,14 @@
 fun upd_second f (x,y,z) = (  x, f y,   z);
 fun upd_third  f (x,y,z) = (  x,   y, f z);
 
-(* fn : ('a -> 'a) -> ('a -> 'a) -> 'a -> 'b list -> int -> 'a *)
-fun bin_branchr f1 f2 y is j = let
-fun bb y 1 _ = y
-|   bb y _ 0 = f1 y
-|   bb y i j = if i=2 then (f2 y) else bb (f2 y) (i-1) (j-1)
-in bb y (length is) j end;
+fun atomize thm = let val r_inst = read_instantiate;
+    fun at  thm = case concl_of thm of
+      _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
+    | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
+    | _				    => [thm];
+in map zero_var_indexes (at thm) end;
 
-fun atomize thm = case concl_of thm of
-      _ $ (Const("op &",_) $ _ $ _)       => atomize (thm RS conjunct1) @
-                                             atomize (thm RS conjunct2)
-    | _ $ (Const("All" ,_) $ Abs (s,_,_)) => atomize (thm RS 
-                                             (read_instantiate [("x","?"^s)] spec))
-    | _                               => [thm];
-
-(* ----- specific support for domain ---------------------------------------------- *)
+(* ----- specific support for domain ---------------------------------------- *)
 
 structure Domain_Library = struct
 
@@ -51,29 +43,28 @@
 
 (* ----- name handling ----- *)
 
-val strip_esc = let
-  fun strip ("'" :: c :: cs) = c :: strip cs
-  |   strip ["'"] = []
-  |   strip (c :: cs) = c :: strip cs
-  |   strip [] = [];
+val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs
+		    |   strip ["'"] = []
+		    |   strip (c :: cs) = c :: strip cs
+		    |   strip [] = [];
 in implode o strip o explode end;
 
 fun extern_name con = case explode con of 
-                   ("o"::"p"::" "::rest) => implode rest
-                   | _ => con;
+		   ("o"::"p"::" "::rest) => implode rest
+		   | _ => con;
 fun dis_name  con = "is_"^ (extern_name con);
 fun dis_name_ con = "is_"^ (strip_esc   con);
 
-(*make distinct names out of the type list, 
-  forbidding "o", "x..","f..","P.." as names *)
-(*a number string is added if necessary *)
+(* make distinct names out of the type list, 
+   forbidding "o", "x..","f..","P.." as names *)
+(* a number string is added if necessary *)
 fun mk_var_names types : string list = let
     fun typid (Type  (id,_)   ) = hd     (explode id)
       | typid (TFree (id,_)   ) = hd (tl (explode id))
       | typid (TVar ((id,_),_)) = hd (tl (explode id));
     fun nonreserved id = let val cs = explode id in
-                         if not(hd cs mem ["x","f","P"]) then id
-                         else implode(chr(1+ord (hd cs))::tl cs) end;
+			 if not(hd cs mem ["x","f","P"]) then id
+			 else implode(chr(1+ord (hd cs))::tl cs) end;
     fun index_vnames(vn::vns,tab) =
           (case assoc(tab,vn) of
              None => if vn mem vns
@@ -86,24 +77,16 @@
 fun type_name_vars (Type(name,typevars)) = (name,typevars)
 |   type_name_vars _                     = Imposs "library:type_name_vars";
 
-(* ----- support for type and mixfix expressions ----- *)
-
-fun mk_tvar s = TFree("'"^s,["pcpo"]);
-fun mk_typ t (S,T) = Type(t,[S,T]);
-infixr 5 -->;
-infixr 6 ~>; val op ~> = mk_typ "->";
-val NoSyn' = ThyOps.Mixfix NoSyn;
-
 (* ----- constructor list handling ----- *)
 
-type cons = (string *                   (* operator name of constr *)
-            ((bool*int)*                (*  (lazy,recursive element or ~1) *)
-              string*                   (*   selector name    *)
-              string)                   (*   argument name    *)
-            list);                      (* argument list      *)
-type eq = (string *             (* name      of abstracted type *)
-           typ list) *          (* arguments of abstracted type *)
-          cons list;            (* represented type, as a constructor list *)
+type cons = (string *			(* operator name of constr *)
+	    ((bool*int)*		(*  (lazy,recursive element or ~1) *)
+	      string*			(*   selector name    *)
+	      string)			(*   argument name    *)
+	    list);			(* argument list      *)
+type eq = (string *		(* name      of abstracted type *)
+	   typ list) *		(* arguments of abstracted type *)
+	  cons list;		(* represented type, as a constructor list *)
 
 val rec_of    = snd o first;
 val is_lazy   = fst o first;
@@ -112,9 +95,16 @@
 val upd_vname =   upd_third;
 fun is_rec         arg = rec_of arg >=0;
 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
-fun nonlazy args       = map vname (filter_out is_lazy args);
-fun is_one_con_one_arg p cons = length cons = 1 andalso let val args = snd(hd cons) in
-                                length args = 1 andalso p (hd args) end;
+fun nonlazy     args   = map vname (filter_out is_lazy    args);
+fun nonlazy_rec args   = map vname (filter is_nonlazy_rec args);
+
+(* ----- support for type and mixfix expressions ----- *)
+
+fun mk_tvar s = TFree("'"^s,["pcpo"]);
+fun mk_typ t (S,T) = Type(t,[S,T]);
+infixr 5 -->;
+infixr 6 ~>; val op ~> = mk_typ "->";
+val NoSyn' = ThyOps.Mixfix NoSyn;
 
 (* ----- support for term expressions ----- *)
 
@@ -130,26 +120,26 @@
 fun mk_lam  (x,T) = Abs(x,dummyT,T);
 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
 local 
-                    fun tf (Type (s,args)) = foldl (op $) (%s,map tf args)
-                    |   tf (TFree(s,_   )) = %s
-                    |   tf _              = Imposs "mk_constrainall";
+		    fun tf (Type (s,args)) = foldl (op $) (%s,map tf args)
+		    |   tf (TFree(s,_   )) = %s
+		    |   tf _              = Imposs "mk_constrainall";
 in
 fun mk_constrain      (typ,T) = %%"_constrain" $ T $ tf typ;
-fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs"$Abs(x,dummyT,P)$tf typ);
+fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ);
 end;
-                        
+			
 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
 fun mk_not     P  = Const("not" ,boolT --> boolT) $ P;
 end;
 
 fun mk_All  (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *)
 
-infixr 0 ===>;fun S ===> T = Const("==>", dummyT) $ S $ T;
+infixr 0 ===>;fun S ===> T = %%"==>" $ S $ T;
 infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T;
-infix 0 ==;  fun S ==  T = Const("==", dummyT) $ S $ T;
-infix 1 ===; fun S === T = Const("op =", dummyT) $ S $ T;
+infix 0 ==;  fun S ==  T = %%"==" $ S $ T;
+infix 1 ===; fun S === T = %%"op =" $ S $ T;
 infix 1 ~=;  fun S ~=  T = mk_not (S === T);
-infix 1 <<;  fun S <<  T = Const("op <<", dummyT) $ S $ T;
+infix 1 <<;  fun S <<  T = %%"op <<" $ S $ T;
 infix 1 ~<<; fun S ~<< T = mk_not (S << T);
 
 infix 9 `  ; fun f`  x = %%"fapp" $ f $ x;
@@ -160,8 +150,11 @@
 fun con_app con = con_app2 con %#;
 fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
 fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
-val cproj    = bin_branchr (fn S => %%"cfst"`S) (fn S => %%"csnd"`S);
-val  proj    = bin_branchr (fn S => %%"fst" $S) (fn S => %%"snd" $S);
+fun prj _  _  y 1 _ = y
+|   prj f1 _  y _ 0 = f1 y
+|   prj f1 f2 y i j = prj f1 f2 (f2 y) (i-1) (j-1);
+val cproj    = prj (fn S => %%"cfst"`S) (fn S => %%"csnd"`S);
+val  proj    = prj (fn S => %%"fst" $S) (fn S => %%"snd" $S);
 fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
 fun /\ v T = %%"fabs" $ mk_lam(v,T);
@@ -177,26 +170,27 @@
 fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = 
       (case cont_eta_contract body  of
         body' as (Const("fapp",Ta) $ f $ Bound 0) => 
-          if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
-          else   Const("fabs",TT) $ Abs(a,T,body')
+	  if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
+	  else   Const("fabs",TT) $ Abs(a,T,body')
       | body' => Const("fabs",TT) $ Abs(a,T,body'))
 |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
 |   cont_eta_contract t    = t;
 
-fun idx_name dnames s n = s ^ (if length dnames = 1 then "" else string_of_int n);
+fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
 fun when_funs cons = if length cons = 1 then ["f"] 
-                     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
+		     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
 fun when_body cons funarg = let
-        fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
-        |   one_fun n (_,args) = let
-                val l2 = length args;
-                fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
-                                                 else Id) (Bound(l2-m));
-                in cont_eta_contract (foldr'' 
-                         (fn (a,t) => %%"ssplit"`(/\# (a,t)))
-                         (args,
-                          fn a => /\# (a,(mk_cfapp(funarg (l2,n),mapn idxs 1 args))))
-                         ) end;
-in foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons) end;
-
+	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
+	|   one_fun n (_,args) = let
+		val l2 = length args;
+		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
+					         else Id) (Bound(l2-m));
+		in cont_eta_contract (foldr'' 
+			(fn (a,t) => %%"ssplit"`(/\# (a,t)))
+			(args,
+			fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args))))
+			) end;
+in (if length cons = 1 andalso length(snd(hd cons)) <= 1
+    then fn t => %%"strictify"`t else Id)
+     (foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons)) end;
 end; (* struct *)
--- a/src/HOLCF/domain/syntax.ML	Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/syntax.ML	Wed Apr 03 19:27:14 1996 +0200
@@ -1,5 +1,4 @@
 (* syntax.ML
-   ID:         $Id$
    Author:  David von Oheimb
    Created: 31-May-95
    Updated: 16-Aug-95 case translation
@@ -14,21 +13,24 @@
 
 open Domain_Library;
 infixr 5 -->; infixr 6 ~>;
-fun calc_syntax dtypeprod ((dname,typevars),
-                (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
+fun calc_syntax dtypeprod ((dname, typevars), (cons':
+			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
 let
 (* ----- constants concerning the isomorphism ------------------------------------- *)
 
 local
   fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
-  fun prod (_,_,args) = if args = [] then Type("one",[])
-                                     else foldr' (mk_typ "**") (map opt_lazy args);
-
+  fun prod     (_,_,args) = if args = [] then Type("one",[])
+				         else foldr'(mk_typ "**") (map opt_lazy args);
+  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
+  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
 in
   val dtype  = Type(dname,typevars);
   val dtype2 = foldr' (mk_typ "++") (map prod cons');
   val const_rep  = (dname^"_rep" ,              dtype  ~> dtype2, NoSyn');
   val const_abs  = (dname^"_abs" ,              dtype2 ~> dtype , NoSyn');
+  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
+						 dtype ~> freetvar "t"), NoSyn');
   val const_copy = (dname^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
 end;
 
@@ -42,20 +44,16 @@
 
 local
   val escape = let
-        fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
-                                                           else        c :: esc cs
-        |   esc []        = []
-        in implode o esc o explode end;
-  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
-  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
+	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
+							   else        c :: esc cs
+	|   esc []        = []
+	in implode o esc o explode end;
   fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
   fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
-                                 ThyOps.Mixfix(Mixfix("is'_"^
-                                 (if is_infix s then Id else escape)con,[],max_pri)));
+			 	 ThyOps.Mixfix(Mixfix("is'_"^
+				 (if is_infix s then Id else escape)con,[],max_pri)));
   fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
 in
-  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
-                                                 dtype ~> freetvar "t"), NoSyn');
   val consts_con = map con cons';
   val consts_dis = map dis cons';
   val consts_sel = flat(map sel cons');
@@ -63,32 +61,32 @@
 
 (* ----- constants concerning induction ------------------------------------------- *)
 
-  val const_take   = (dname^"_take"  ,Type("nat",[]) --> dtype ~> dtype    ,NoSyn');
-  val const_finite = (dname^"_finite",dtype-->HOLogic.boolT                ,NoSyn');
+  val const_take   = (dname^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
+  val const_finite = (dname^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
 
 (* ----- case translation --------------------------------------------------------- *)
 
 local open Syntax in
   val case_trans = let 
-        fun c_ast con syn = Constant (ThyOps.const_name con syn);
-        fun expvar n      = Variable ("e"^(string_of_int n));
-        fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
-        fun app s (l,r)   = mk_appl (Constant s) [l,r];
-        fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
-                 [if is_infix syn
-                  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
-                  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
-                  expvar n];
-        fun arg1 n (con,_,args) = if args = [] then expvar n
-                                  else mk_appl (Constant "LAM ") 
-                 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
+	fun c_ast con syn = Constant (ThyOps.const_name con syn);
+	fun expvar n      = Variable ("e"^(string_of_int n));
+	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
+	fun app s (l,r)   = mk_appl (Constant s) [l,r];
+	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
+		 [if is_infix syn
+		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
+		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
+		  expvar n];
+	fun arg1 n (con,_,args) = if args = [] then expvar n 
+				  else mk_appl (Constant "LAM ") 
+		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
   in mk_appl (Constant "@case") [Variable "x", foldr'
-                                 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
-                                 (mapn case1 1 cons')] <->
+				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
+				 (mapn case1 1 cons')] <->
      mk_appl (Constant "@fapp") [foldl 
-                                 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
-                                 (Constant (dname^"_when"),mapn arg1 1 cons'),
-                                 Variable "x"]
+				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
+				 (Constant (dname^"_when"),mapn arg1 1 cons'),
+				 Variable "x"]
   end;
 end;
 
@@ -103,11 +101,10 @@
 in (* local *)
 
 fun add_syntax (comp_dname,eqs': ((string * typ list) *
-                (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
+		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
 let
   fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
   fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
-  (**                 (fn TFree(_,sort) => sort | _ => Imposs "syntax:thy_arities")**)
   val thy_types   = map (thy_type  o fst) eqs';
   val thy_arities = map (thy_arity o fst) eqs';
   val dtypes      = map (Type      o fst) eqs';
@@ -118,10 +115,10 @@
   val ctt           = map (calc_syntax funprod) eqs';
   val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
 in thy'' |> add_types      thy_types
-         |> add_arities    thy_arities
-         |> add_cur_ops_i (flat(map fst ctt))
-         |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
-         |> add_trrules_i (flat(map snd ctt))
+	 |> add_arities    thy_arities
+	 |> add_cur_ops_i (flat(map fst ctt))
+	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
+	 |> add_trrules_i (flat(map snd ctt))
 end; (* let *)
 
 end; (* local *)
--- a/src/HOLCF/domain/theorems.ML	Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed Apr 03 19:27:14 1996 +0200
@@ -1,5 +1,4 @@
 (* theorems.ML
-   ID:         $Id$
    Author : David von Oheimb
    Created: 06-Jun-95
    Updated: 08-Jun-95 first proof from cterms
@@ -12,10 +11,12 @@
    Updated: 05-Sep-95 simultaneous domain equations (main part)
    Updated: 11-Sep-95 simultaneous domain equations (coding finished)
    Updated: 13-Sep-95 simultaneous domain equations (debugging)
-   Copyright 1995 TU Muenchen
+   Updated: 26-Oct-95 debugging and enhancement of proofs for take_apps, ind
+   Updated: 16-Feb-96 bug concerning  domain Triv = triv  fixed
+   Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
+   Copyright 1995, 1996 TU Muenchen
 *)
 
-
 structure Domain_Theorems = struct
 
 local
@@ -25,58 +26,58 @@
 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
 infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
 
-(* ----- general proof facilities ------------------------------------------------- *)
-
-fun inferT sg pre_tm = #2(Sign.infer_types sg (K None)(K None)[]true([pre_tm],propT));
+(* ----- general proof facilities ------------------------------------------- *)
 
-(*
-infix 0 y;
-val b=0;
-fun _ y t = by t;
-fun  g  defs t = let val sg = sign_of thy;
-                     val ct = Thm.cterm_of sg (inferT sg t);
-                 in goalw_cterm defs ct end;
-*)
+fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true 
+			   ([pre_tm],propT));
 
 fun pg'' thy defs t = let val sg = sign_of thy;
-                          val ct = Thm.cterm_of sg (inferT sg t);
-                      in prove_goalw_cterm defs ct end;
+		          val ct = Thm.cterm_of sg (inferT sg t);
+		      in prove_goalw_cterm defs ct end;
 fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
-                                            | prems=> (cut_facts_tac prems 1)::tacsf);
+				| prems=> (cut_facts_tac prems 1)::tacsf);
 
 fun REPEAT_DETERM_UNTIL p tac = 
 let fun drep st = if p st then Sequence.single st
-                          else (case Sequence.pull(tac st) of
-                                  None        => Sequence.null
-                                | Some(st',_) => drep st')
-in drep end;
+			  else (case Sequence.pull(tapply(tac,st)) of
+		                  None        => Sequence.null
+				| Some(st',_) => drep st')
+in Tactic drep end;
 val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
 
-local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in
+local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in
 val kill_neq_tac = dtac trueI2 end;
-fun case_UU_tac rews i v =      res_inst_tac [("Q",v^"=UU")] classical2 i THEN
-                                asm_simp_tac (HOLCF_ss addsimps rews) i;
+fun case_UU_tac rews i v =	res_inst_tac [("Q",v^"=UU")] classical2 i THEN
+				asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac = REPEAT_DETERM o resolve_tac 
-                [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
+		[is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
+
+(* ----- general proofs ----------------------------------------------------- *)
 
-(* ----- general proofs ----------------------------------------------------------- *)
+val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
+		fast_tac HOL_cs 1]))["(x. P x  Q)=((x. P x)  Q)",
+			    	     "(x. P  Q x) = (P  (x. Q x))"]);
+
+val all2E = prove_goal HOL.thy " x y . P x y; P x y  R   R" (fn prems =>[
+				resolve_tac prems 1,
+				cut_facts_tac prems 1,
+				fast_tac HOL_cs 1]);
 
 val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [
                                 cut_facts_tac prems 1,
                                 etac swap 1,
                                 dtac notnotD 1,
-                                etac (hd prems) 1]);
+				etac (hd prems) 1]);
 
-val dist_eqI = prove_goal Porder0.thy "~ x << y ==> x ~= y" (fn prems => [
-                                cut_facts_tac prems 1,
-                                etac swap 1,
-                                dtac notnotD 1,
-                                asm_simp_tac HOLCF_ss 1]);
-val cfst_strict  = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
-                                (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
-val csnd_strict  = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
-                        (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
+val dist_eqI = prove_goal Porder.thy " x  y  x  y" (fn prems => [
+                                rtac swap3 1,
+				etac (antisym_less_inverse RS conjunct1) 1,
+				resolve_tac prems 1]);
+val cfst_strict  = prove_goal Cprod3.thy "cfst` = " (fn _ => [
+			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
+val csnd_strict  = prove_goal Cprod3.thy "csnd` = " (fn _ => [
+			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
 
 in
 
@@ -86,8 +87,17 @@
 
 val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
 val pg = pg' thy;
+(*
+infixr 0 y;
+val b = 0;
+fun _ y t = by t;
+fun  g  defs t = let val sg = sign_of thy;
+		     val ct = Thm.cterm_of sg (inferT sg t);
+		 in goalw_cterm defs ct end;
+*)
 
-(* ----- getting the axioms and definitions --------------------------------------- *)
+
+(* ----- getting the axioms and definitions --------------------------------- *)
 
 local val ga = get_axiom thy in
 val ax_abs_iso    = ga (dname^"_abs_iso"   );
@@ -96,11 +106,11 @@
 val axs_con_def   = map (fn (con,_) => ga (extern_name con ^"_def")) cons;
 val axs_dis_def   = map (fn (con,_) => ga (   dis_name con ^"_def")) cons;
 val axs_sel_def   = flat(map (fn (_,args) => 
-                    map (fn     arg => ga (sel_of arg      ^"_def")) args) cons);
+		    map (fn     arg => ga (sel_of arg      ^"_def")) args)cons);
 val ax_copy_def   = ga (dname^"_copy_def"  );
 end; (* local *)
 
-(* ----- theorems concerning the isomorphism -------------------------------------- *)
+(* ----- theorems concerning the isomorphism -------------------------------- *)
 
 val dc_abs  = %%(dname^"_abs");
 val dc_rep  = %%(dname^"_rep");
@@ -108,251 +118,243 @@
 val x_name = "x";
 
 val (rep_strict, abs_strict) = let 
-               val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
-               in (r RS conjunct1, r RS conjunct2) end;
+	 val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
+	       in (r RS conjunct1, r RS conjunct2) end;
 val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [
-                                res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
-                                etac ssubst 1,
-                                rtac rep_strict 1];
+			   res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
+				etac ssubst 1, rtac rep_strict 1];
 val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [
-                                res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
-                                etac ssubst 1,
-                                rtac abs_strict 1];
+			   res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
+				etac ssubst 1, rtac abs_strict 1];
 val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
 
 local 
 val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [
-                                dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
-                                etac (ax_rep_iso RS subst) 1];
+			    dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
+			    etac (ax_rep_iso RS subst) 1];
 fun exh foldr1 cn quant foldr2 var = let
   fun one_con (con,args) = let val vns = map vname args in
     foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns)::
-                              map (defined o (var vns)) (nonlazy args))) end
+			      map (defined o (var vns)) (nonlazy args))) end
   in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
 in
 val cases = let 
-            fun common_tac thm = rtac thm 1 THEN contr_tac 1;
-            fun unit_tac true = common_tac liftE1
-            |   unit_tac _    = all_tac;
-            fun prod_tac []          = common_tac oneE
-            |   prod_tac [arg]       = unit_tac (is_lazy arg)
-            |   prod_tac (arg::args) = 
-                                common_tac sprodE THEN
-                                kill_neq_tac 1 THEN
-                                unit_tac (is_lazy arg) THEN
-                                prod_tac args;
-            fun sum_one_tac p = SELECT_GOAL(EVERY[
-                                rtac p 1,
-                                rewrite_goals_tac axs_con_def,
-                                dtac iso_swap 1,
-                                simp_tac HOLCF_ss 1,
-                                UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
-            fun sum_tac [(_,args)]       [p]        = 
-                                prod_tac args THEN sum_one_tac p
-            |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
-                                common_tac ssumE THEN
-                                kill_neq_tac 1 THEN kill_neq_tac 2 THEN
-                                prod_tac args THEN sum_one_tac p) THEN
-                                sum_tac cons' prems
-            |   sum_tac _ _ = Imposs "theorems:sum_tac";
-          in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
-                              (fn T => T ==> %"P") mk_All
-                              (fn l => foldr (op ===>) (map mk_trp l,mk_trp(%"P")))
-                              bound_arg)
-                             (fn prems => [
-                                cut_facts_tac [excluded_middle] 1,
-                                etac disjE 1,
-                                rtac (hd prems) 2,
-                                etac rep_defin' 2,
-                                if is_one_con_one_arg (not o is_lazy) cons
-                                then rtac (hd (tl prems)) 1 THEN atac 2 THEN
-                                     rewrite_goals_tac axs_con_def THEN
-                                     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
-                                else sum_tac cons (tl prems)])end;
-val exhaust = pg [] (mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %))) [
-                                rtac cases 1,
-                                UNTIL_SOLVED(fast_tac HOL_cs 1)];
+	    fun common_tac thm = rtac thm 1 THEN contr_tac 1;
+	    fun unit_tac true = common_tac liftE1
+	    |   unit_tac _    = all_tac;
+	    fun prod_tac []          = common_tac oneE
+	    |   prod_tac [arg]       = unit_tac (is_lazy arg)
+	    |   prod_tac (arg::args) = 
+				common_tac sprodE THEN
+				kill_neq_tac 1 THEN
+				unit_tac (is_lazy arg) THEN
+				prod_tac args;
+	    fun sum_rest_tac p = SELECT_GOAL(EVERY[
+				rtac p 1,
+				rewrite_goals_tac axs_con_def,
+				dtac iso_swap 1,
+				simp_tac HOLCF_ss 1,
+				UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
+	    fun sum_tac [(_,args)]       [p]        = 
+				prod_tac args THEN sum_rest_tac p
+	    |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
+				common_tac ssumE THEN
+				kill_neq_tac 1 THEN kill_neq_tac 2 THEN
+				prod_tac args THEN sum_rest_tac p) THEN
+				sum_tac cons' prems
+	    |   sum_tac _ _ = Imposs "theorems:sum_tac";
+	  in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
+			      (fn T => T ==> %"P") mk_All
+			      (fn l => foldr (op ===>) (map mk_trp l,
+							    mk_trp(%"P")))
+			      bound_arg)
+			     (fn prems => [
+				cut_facts_tac [excluded_middle] 1,
+				etac disjE 1,
+				rtac (hd prems) 2,
+				etac rep_defin' 2,
+				if length cons = 1 andalso 
+				   length (snd(hd cons)) = 1 andalso 
+				   not(is_lazy(hd(snd(hd cons))))
+				then rtac (hd (tl prems)) 1 THEN atac 2 THEN
+				     rewrite_goals_tac axs_con_def THEN
+				     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
+				else sum_tac cons (tl prems)])end;
+val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
+				rtac cases 1,
+				UNTIL_SOLVED(fast_tac HOL_cs 1)];
 end;
 
 local 
-val when_app = foldl (op `) (%%(dname^"_when"), map % (when_funs cons));
-val when_appl = pg [ax_when_def] (mk_trp(when_app`%x_name===when_body cons 
-                (fn (_,n) => %(nth_elem(n-1,when_funs cons)))`(dc_rep`%x_name))) [
-                                simp_tac HOLCF_ss 1];
+  val when_app  = foldl (op `) (%%(dname^"_when"), map % (when_funs cons));
+  val when_appl = pg [ax_when_def] (mk_trp(when_app`%x_name===when_body cons 
+		(fn (_,n)=> %(nth_elem(n-1,when_funs cons)))`(dc_rep`%x_name)))[
+				simp_tac HOLCF_ss 1];
 in
-val when_strict = pg [] ((if is_one_con_one_arg (K true) cons 
-        then fn t => mk_trp(strict(%"f")) ===> t else Id)(mk_trp(strict when_app))) [
-                                simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
-val when_apps = let fun one_when n (con,args) = pg axs_con_def
-                (lift_defined % (nonlazy args, mk_trp(when_app`(con_app con args) ===
-                 mk_cfapp(%(nth_elem(n,when_funs cons)),map %# args))))[
-                        asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
-                in mapn one_when 0 cons end;
+val when_strict = pg [] (mk_trp(strict when_app)) [
+			simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
+val when_apps = let fun one_when n (con,args) = pg axs_con_def (lift_defined % 
+   (nonlazy args, mk_trp(when_app`(con_app con args) ===
+	 mk_cfapp(%(nth_elem(n,when_funs cons)),map %# args))))[
+		asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
+	in mapn one_when 0 cons end;
 end;
 val when_rews = when_strict::when_apps;
 
-(* ----- theorems concerning the constructors, discriminators and selectors ------- *)
+(* ----- theorems concerning the constructors, discriminators and selectors - *)
 
-val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
-                        (if is_one_con_one_arg (K true) cons then mk_not else Id)
-                         (strict(%%(dis_name con))))) [
-                simp_tac (HOLCF_ss addsimps (if is_one_con_one_arg (K true) cons 
-                                        then [ax_when_def] else when_rews)) 1]) cons;
-val dis_apps = let fun one_dis c (con,args)= pg (axs_dis_def)
-                   (lift_defined % (nonlazy args, (*(if is_one_con_one_arg is_lazy cons
-                        then curry (lift_defined %#) args else Id)
-#################*)
-                        (mk_trp((%%(dis_name c))`(con_app con args) ===
-                              %%(if con=c then "TT" else "FF"))))) [
-                                asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-        in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
-val dis_defins = map (fn (con,args) => pg [] (defined(%x_name)==> 
-                      defined(%%(dis_name con)`%x_name)) [
-                                rtac cases 1,
-                                contr_tac 1,
-                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
-                                              (HOLCF_ss addsimps dis_apps) 1))]) cons;
-val dis_rews = dis_stricts @ dis_defins @ dis_apps;
+val dis_rews = let
+  val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
+		      	     strict(%%(dis_name con)))) [
+				simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
+  val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
+		   (lift_defined % (nonlazy args,
+			(mk_trp((%%(dis_name c))`(con_app con args) ===
+			      %%(if con=c then "TT" else "FF"))))) [
+				asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+	in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
+  val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==> 
+		      defined(%%(dis_name con)`%x_name)) [
+				rtac cases 1,
+				contr_tac 1,
+				UNTIL_SOLVED (CHANGED(asm_simp_tac 
+				        (HOLCF_ss addsimps dis_apps) 1))]) cons;
+in dis_stricts @ dis_defins @ dis_apps end;
 
 val con_stricts = flat(map (fn (con,args) => map (fn vn =>
-                        pg (axs_con_def) 
-                           (mk_trp(con_app2 con (fn arg => if vname arg = vn 
-                                        then UU else %# arg) args === UU))[
-                                asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
-                        ) (nonlazy args)) cons);
+			pg (axs_con_def) 
+			   (mk_trp(con_app2 con (fn arg => if vname arg = vn 
+					then UU else %# arg) args === UU))[
+				asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
+			) (nonlazy args)) cons);
 val con_defins = map (fn (con,args) => pg []
-                        (lift_defined % (nonlazy args,
-                                mk_trp(defined(con_app con args)))) ([
-                                rtac swap3 1] @ (if is_one_con_one_arg (K true) cons 
-                                then [
-                                  if is_lazy (hd args) then rtac defined_up 2
-                                                       else atac 2,
-                                  rtac abs_defin' 1,    
-                                  asm_full_simp_tac (HOLCF_ss addsimps axs_con_def) 1]
-                                else [
-                                  eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
-                                  asm_simp_tac (HOLCF_ss addsimps dis_rews) 1])))cons;
+			(lift_defined % (nonlazy args,
+				mk_trp(defined(con_app con args)))) ([
+			  rtac swap3 1, 
+			  eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
+			  asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
 val con_rews = con_stricts @ con_defins;
 
 val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [
-                                simp_tac (HOLCF_ss addsimps when_rews) 1];
-in flat(map (fn (_,args) => map (fn arg => one_sel (sel_of arg)) args) cons) end;
+				simp_tac (HOLCF_ss addsimps when_rews) 1];
+in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
 val sel_apps = let fun one_sel c n sel = map (fn (con,args) => 
-                let val nlas = nonlazy args;
-                    val vns  = map vname args;
-                in pg axs_sel_def (lift_defined %
-                   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
-   mk_trp((%%sel)`(con_app con args) === (if con=c then %(nth_elem(n,vns)) else UU))))
-                            ( (if con=c then [] 
-                               else map(case_UU_tac(when_rews@con_stricts)1) nlas)
-                             @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
-                                         then[case_UU_tac (when_rews @ con_stricts) 1 
-                                                          (nth_elem(n,vns))] else [])
-                             @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
+		let val nlas = nonlazy args;
+		    val vns  = map vname args;
+		in pg axs_sel_def (lift_defined %
+		   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
+				mk_trp((%%sel)`(con_app con args) === 
+				(if con=c then %(nth_elem(n,vns)) else UU))))
+			    ( (if con=c then [] 
+		       else map(case_UU_tac(when_rews@con_stricts)1) nlas)
+		     @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
+				 then[case_UU_tac (when_rews @ con_stricts) 1 
+						  (nth_elem(n,vns))] else [])
+		     @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
 in flat(map  (fn (c,args) => 
-        flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
-val sel_defins = if length cons = 1 then map (fn arg => pg [] (defined(%x_name) ==> 
-                        defined(%%(sel_of arg)`%x_name)) [
-                                rtac cases 1,
-                                contr_tac 1,
-                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
-                                              (HOLCF_ss addsimps sel_apps) 1))]) 
-                 (filter_out is_lazy (snd(hd cons))) else [];
+     flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
+val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==> 
+			defined(%%(sel_of arg)`%x_name)) [
+				rtac cases 1,
+				contr_tac 1,
+				UNTIL_SOLVED (CHANGED(asm_simp_tac 
+				             (HOLCF_ss addsimps sel_apps) 1))]) 
+		 (filter_out is_lazy (snd(hd cons))) else [];
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
 
 val distincts_le = let
     fun dist (con1, args1) (con2, args2) = pg []
-              (lift_defined % ((nonlazy args1),
-                             (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
-                        rtac swap3 1,
-                        eres_inst_tac [("fo5",dis_name con1)] monofun_cfun_arg 1]
-                      @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
-                      @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
+	      (lift_defined % ((nonlazy args1),
+			(mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
+			rtac swap3 1,
+			eres_inst_tac[("fo5",dis_name con1)] monofun_cfun_arg 1]
+		      @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
+		      @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
     fun distinct (con1,args1) (con2,args2) =
-        let val arg1 = (con1, args1);
-            val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
-                              (args2~~variantlist(map vname args2,map vname args1))));
-        in [dist arg1 arg2, dist arg2 arg1] end;
+	let val arg1 = (con1, args1);
+	    val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
+			(args2~~variantlist(map vname args2,map vname args1))));
+	in [dist arg1 arg2, dist arg2 arg1] end;
     fun distincts []      = []
     |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
 in distincts cons end;
 val dists_le = flat (flat distincts_le);
 val dists_eq = let
     fun distinct (_,args1) ((_,args2),leqs) = let
-        val (le1,le2) = (hd leqs, hd(tl leqs));
-        val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
-        if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
-        if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
-                                        [eq1, eq2] end;
+	val (le1,le2) = (hd leqs, hd(tl leqs));
+	val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
+	if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
+	if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
+					[eq1, eq2] end;
     fun distincts []      = []
     |   distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @
-                                   distincts cs;
+				   distincts cs;
     in distincts (cons~~distincts_le) end;
 
 local 
   fun pgterm rel con args = let
-                fun append s = upd_vname(fn v => v^s);
-                val (largs,rargs) = (args, map (append "'") args);
-                in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
-                      lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
-                            mk_trp (foldr' mk_conj 
-                                (map rel (map %# largs ~~ map %# rargs)))))) end;
+		fun append s = upd_vname(fn v => v^s);
+		val (largs,rargs) = (args, map (append "'") args);
+		in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
+		      lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
+			    mk_trp (foldr' mk_conj 
+				(map rel (map %# largs ~~ map %# rargs)))))) end;
   val cons' = filter (fn (_,args) => args<>[]) cons;
 in
 val inverts = map (fn (con,args) => 
-                pgterm (op <<) con args (flat(map (fn arg => [
-                                TRY(rtac conjI 1),
-                                dres_inst_tac [("fo5",sel_of arg)] monofun_cfun_arg 1,
-                                asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
-                                                      ) args))) cons';
+		pgterm (op <<) con args (flat(map (fn arg => [
+				TRY(rtac conjI 1),
+				dres_inst_tac [("fo5",sel_of arg)] monofun_cfun_arg 1,
+				asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
+			     			      ) args))) cons';
 val injects = map (fn ((con,args),inv_thm) => 
-                           pgterm (op ===) con args [
-                                etac (antisym_less_inverse RS conjE) 1,
-                                dtac inv_thm 1, REPEAT(atac 1),
-                                dtac inv_thm 1, REPEAT(atac 1),
-                                TRY(safe_tac HOL_cs),
-                                REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
-                  (cons'~~inverts);
+			   pgterm (op ===) con args [
+				etac (antisym_less_inverse RS conjE) 1,
+				dtac inv_thm 1, REPEAT(atac 1),
+				dtac inv_thm 1, REPEAT(atac 1),
+				TRY(safe_tac HOL_cs),
+				REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
+		  (cons'~~inverts);
 end;
 
-(* ----- theorems concerning one induction step ----------------------------------- *)
+(* ----- theorems concerning one induction step ----------------------------- *)
 
-val copy_strict = pg [ax_copy_def] ((if is_one_con_one_arg (K true) cons then fn t =>
-         mk_trp(strict(cproj (%"f") eqs (rec_of (hd(snd(hd cons)))))) ===> t
-        else Id) (mk_trp(strict(dc_copy`%"f")))) [
-                                asm_simp_tac(HOLCF_ss addsimps [abs_strict,rep_strict,
-                                                        cfst_strict,csnd_strict]) 1];
-val copy_apps = map (fn (con,args) => pg (ax_copy_def::axs_con_def)
-                    (lift_defined %# (filter is_nonlazy_rec args,
-                        mk_trp(dc_copy`%"f"`(con_app con args) ===
-                           (con_app2 con (app_rec_arg (cproj (%"f") eqs)) args))))
-                                 (map (case_UU_tac [ax_abs_iso] 1 o vname)
-                                   (filter(fn a=>not(is_rec a orelse is_lazy a))args)@
-                                 [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1])
-                )cons;
-val copy_stricts = map(fn(con,args)=>pg[](mk_trp(dc_copy`UU`(con_app con args) ===UU))
-             (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
-                         in map (case_UU_tac rews 1) (nonlazy args) @ [
-                             asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
-                   (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
+val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
+		   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
+						   cfst_strict,csnd_strict]) 1];
+val copy_apps = map (fn (con,args) => pg [ax_copy_def]
+		    (lift_defined % (nonlazy_rec args,
+			mk_trp(dc_copy`%"f"`(con_app con args) ===
+		(con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
+			(map (case_UU_tac (abs_strict::when_strict::con_stricts)
+				 1 o vname)
+			 (filter (fn a => not (is_rec a orelse is_lazy a)) args)
+			@[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
+		          simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
+val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
+					(con_app con args) ===UU))
+     (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
+			 in map (case_UU_tac rews 1) (nonlazy args) @ [
+			     asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
+  		        (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
 val copy_rews = copy_strict::copy_apps @ copy_stricts;
 
 in     (iso_rews, exhaust, cases, when_rews,
-        con_rews, sel_rews, dis_rews, dists_eq, dists_le, inverts, injects,
-        copy_rews)
+	con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
+	copy_rews)
 end; (* let *)
 
 
 fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) =
 let
 
-val dummy = writeln ("Proving induction properties of domain "^comp_dname^"...");
+val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
 val pg = pg' thy;
 
 val dnames = map (fst o fst) eqs;
 val conss  = map  snd        eqs;
 
-(* ----- getting the composite axiom and definitions ------------------------------ *)
+(* ----- getting the composite axiom and definitions ------------------------ *)
 
 local val ga = get_axiom thy in
 val axs_reach      = map (fn dn => ga (dn ^  "_reach"   )) dnames;
@@ -362,230 +364,235 @@
 val ax_bisim_def   = ga (comp_dname^"_bisim_def");
 end; (* local *)
 
-(* ----- theorems concerning finiteness and induction ----------------------------- *)
-
 fun dc_take dn = %%(dn^"_take");
 val x_name = idx_name dnames "x"; 
 val P_name = idx_name dnames "P";
+val n_eqs = length eqs;
+
+(* ----- theorems concerning finite approximation and finite induction ------ *)
 
 local
-  val iterate_ss = simpset_of "Fix";    
-  val iterate_Cprod_strict_ss = iterate_ss addsimps [cfst_strict, csnd_strict];
-  val iterate_Cprod_ss = iterate_ss addsimps [cfst2,csnd2,csplit2];
+  val iterate_Cprod_ss = simpset_of "Fix"
+			 addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
   val copy_con_rews  = copy_rews @ con_rews;
-  val copy_take_defs = (if length dnames=1 then [] else [ax_copy2_def]) @axs_take_def;
-  val take_stricts = pg copy_take_defs (mk_trp(foldr' mk_conj (map (fn ((dn,args),_)=>
-                  (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
-                                nat_ind_tac "n" 1,
-                                simp_tac iterate_ss 1,
-                                simp_tac iterate_Cprod_strict_ss 1,
-                                asm_simp_tac iterate_Cprod_ss 1,
-                                TRY(safe_tac HOL_cs)] @
-                        map(K(asm_simp_tac (HOL_ss addsimps copy_rews)1))dnames);
+  val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+  val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
+	    (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
+			nat_ind_tac "n" 1,
+			simp_tac iterate_Cprod_ss 1,
+			asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
   val take_stricts' = rewrite_rule copy_take_defs take_stricts;
-  val take_0s = mapn (fn n => fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
-                                                                `%x_name n === UU))[
-                                simp_tac iterate_Cprod_strict_ss 1]) 1 dnames;
+  val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
+							`%x_name n === UU))[
+				simp_tac iterate_Cprod_ss 1]) 1 dnames;
+  val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
   val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj 
-            (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all 
-                (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
-                 con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
-                              args)) cons) eqs)))) ([
-                                nat_ind_tac "n" 1,
-                                simp_tac iterate_Cprod_strict_ss 1,
-                                simp_tac (HOLCF_ss addsimps copy_con_rews) 1,
-                                TRY(safe_tac HOL_cs)] @
-                        (flat(map (fn ((dn,_),cons) => map (fn (con,args) => EVERY (
-                                asm_full_simp_tac iterate_Cprod_ss 1::
-                                map (case_UU_tac (take_stricts'::copy_con_rews) 1)
-                                    (nonlazy args) @[
-                                asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1])
-                        ) cons) eqs)));
+	    (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all 
+	(map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
+  	 con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
+			      args)) cons) eqs)))) ([
+				simp_tac iterate_Cprod_ss 1,
+				nat_ind_tac "n" 1,
+			    simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
+				asm_full_simp_tac (HOLCF_ss addsimps 
+				      (filter (has_fewer_prems 1) copy_rews)) 1,
+				TRY(safe_tac HOL_cs)] @
+			(flat(map (fn ((dn,_),cons) => map (fn (con,args) => 
+				if nonlazy_rec args = [] then all_tac else
+				EVERY(map c_UU_tac (nonlazy_rec args)) THEN
+				asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
+		 					   ) cons) eqs)));
 in
 val take_rews = atomize take_stricts @ take_0s @ atomize take_apps;
 end; (* local *)
 
-val take_lemmas = mapn (fn n => fn(dn,ax_reach) => pg'' thy axs_take_def (mk_All("n",
-                mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
-                       dc_take dn $ Bound 0 `%(x_name n^"'")))
-           ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
-                                res_inst_tac[("t",x_name n    )](ax_reach RS subst) 1,
-                                res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
-                                rtac (fix_def2 RS ssubst) 1,
-                                REPEAT(CHANGED(rtac (contlub_cfun_arg RS ssubst) 1
-                                               THEN chain_tac 1)),
-                                rtac (contlub_cfun_fun RS ssubst) 1,
-                                rtac (contlub_cfun_fun RS ssubst) 2,
-                                rtac lub_equal 3,
-                                chain_tac 1,
-                                rtac allI 1,
-                                resolve_tac prems 1])) 1 (dnames~~axs_reach);
-
 local
   fun one_con p (con,args) = foldr mk_All (map vname args,
-        lift_defined (bound_arg (map vname args)) (nonlazy args,
-        lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
-             (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
+	lift_defined (bound_arg (map vname args)) (nonlazy args,
+	lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
+         (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
   fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===> 
-                           foldr (op ===>) (map (one_con p) cons,concl));
-  fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x)) 1 conss,
-        mk_trp(foldr' mk_conj (mapn (fn n => concf (P_name n,x_name n)) 1 dnames)));
+			   foldr (op ===>) (map (one_con p) cons,concl));
+  fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
+			mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
   val take_ss = HOL_ss addsimps take_rews;
-  fun ind_tacs tacsf thms1 thms2 prems = TRY(safe_tac HOL_cs)::
-                                flat (mapn (fn n => fn (thm1,thm2) => 
-                                  tacsf (n,prems) (thm1,thm2) @ 
-                                  flat (map (fn cons =>
-                                    (resolve_tac prems 1 ::
-                                     flat (map (fn (_,args) => 
-                                       resolve_tac prems 1::
-                                       map (K(atac 1)) (nonlazy args) @
-                                       map (K(atac 1)) (filter is_rec args))
-                                     cons)))
-                                   conss))
-                                0 (thms1~~thms2));
+  fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i)
+			       1 dnames);
+  fun ind_prems_tac prems = EVERY(flat (map (fn cons => (
+				     resolve_tac prems 1 ::
+				     flat (map (fn (_,args) => 
+				       resolve_tac prems 1 ::
+				       map (K(atac 1)) (nonlazy args) @
+				       map (K(atac 1)) (filter is_rec args))
+				     cons))) conss));
   local 
-    fun all_rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
-                  is_rec arg andalso not(rec_of arg mem ns) andalso
-                  ((rec_of arg =  n andalso not(lazy_rec orelse is_lazy arg)) orelse 
-                    rec_of arg <> n andalso all_rec_to (rec_of arg::ns) 
-                      (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
-                  ) o snd) cons;
-    fun warn (n,cons) = if all_rec_to [] false (n,cons) then (writeln 
-                           ("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true)
-                        else false;
-    fun lazy_rec_to ns lazy_rec (n,cons) = exists (exists (fn arg => 
-                  is_rec arg andalso not(rec_of arg mem ns) andalso
-                  ((rec_of arg =  n andalso (lazy_rec orelse is_lazy arg)) orelse 
-                    rec_of arg <> n andalso lazy_rec_to (rec_of arg::ns)
-                     (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
-                 ) o snd) cons;
-  in val is_emptys = map warn (mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs);
-     val is_finite = forall (not o lazy_rec_to [] false) 
-                            (mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs)
+    (* check whether every/exists constructor of the n-th part of the equation:
+       it has a possibly indirectly recursive argument that isn't/is possibly 
+       indirectly lazy *)
+    fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
+	  is_rec arg andalso not(rec_of arg mem ns) andalso
+	  ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
+	    rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
+	      (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
+	  ) o snd) cons;
+    fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
+    fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (writeln 
+        ("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
+    fun lazy_rec_to ns = rec_to exists Id  lazy_rec_to ns;
+
+  in val n__eqs     = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
+     val is_emptys = map warn n__eqs;
+     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
   end;
-in
-val finite_ind = pg'' thy [] (ind_term (fn (P,x) => fn dn => 
-                          mk_all(x,%P $ (dc_take dn $ %"n" `Bound 0)))) (fn prems=> [
-                                nat_ind_tac "n" 1,
-                                simp_tac (take_ss addsimps prems) 1,
-                                TRY(safe_tac HOL_cs)]
-                                @ flat(mapn (fn n => fn (cons,cases) => [
-                                 res_inst_tac [("x",x_name n)] cases 1,
-                                 asm_simp_tac (take_ss addsimps prems) 1]
-                                 @ flat(map (fn (con,args) => 
-                                  asm_simp_tac take_ss 1 ::
-                                  map (fn arg =>
-                                   case_UU_tac (prems@con_rews) 1 (
-                                   nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
-                                  (filter is_nonlazy_rec args) @ [
-                                  resolve_tac prems 1] @
-                                  map (K (atac 1))      (nonlazy args) @
-                                  map (K (etac spec 1)) (filter is_rec args)) 
-                                 cons))
-                                1 (conss~~casess)));
+in (* local *)
+val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$
+			     (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
+				quant_tac 1,
+				simp_tac quant_ss 1,
+				nat_ind_tac "n" 1,
+				simp_tac (take_ss addsimps prems) 1,
+				TRY(safe_tac HOL_cs)]
+				@ flat(map (fn (cons,cases) => [
+				 res_inst_tac [("x","x")] cases 1,
+				 asm_simp_tac (take_ss addsimps prems) 1]
+				 @ flat(map (fn (con,args) => 
+				  asm_simp_tac take_ss 1 ::
+				  map (fn arg =>
+				   case_UU_tac (prems@con_rews) 1 (
+			   nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
+				  (filter is_nonlazy_rec args) @ [
+				  resolve_tac prems 1] @
+				  map (K (atac 1))      (nonlazy args) @
+				  map (K (etac spec 1)) (filter is_rec args)) 
+				 cons))
+				(conss~~casess)));
+
+val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
+		mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
+		       dc_take dn $ Bound 0 `%(x_name n^"'")))
+	   ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
+			res_inst_tac[("t",x_name n    )](ax_reach RS subst) 1,
+			res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
+				rtac (fix_def2 RS ssubst) 1,
+				REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1
+					       THEN chain_tac 1)),
+				rtac (contlub_cfun_fun RS ssubst) 1,
+				rtac (contlub_cfun_fun RS ssubst) 2,
+				rtac lub_equal 3,
+				chain_tac 1,
+				rtac allI 1,
+				resolve_tac prems 1])) 1 (dnames~~axs_reach);
+
+(* ----- theorems concerning finiteness and induction ----------------------- *)
 
 val (finites,ind) = if is_finite then
-let 
-  fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
-  val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> 
-        mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
-        take_enough dn)) ===> mk_trp(take_enough dn)) [
-                                etac disjE 1,
-                                etac notE 1,
-                                resolve_tac take_lemmas 1,
-                                asm_simp_tac take_ss 1,
-                                atac 1]) dnames;
-  val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn 
-        (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
-         mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
-                 dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
-                                rtac allI 1,
-                                nat_ind_tac "n" 1,
-                                simp_tac take_ss 1,
-                                TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
-                                flat(mapn (fn n => fn (cons,cases) => [
-                                  simp_tac take_ss 1,
-                                  rtac allI 1,
-                                  res_inst_tac [("x",x_name n)] cases 1,
-                                  asm_simp_tac take_ss 1] @ 
-                                  flat(map (fn (con,args) => 
-                                    asm_simp_tac take_ss 1 ::
-                                    flat(map (fn arg => [
-                                      eres_inst_tac [("x",vname arg)] all_dupE 1,
-                                      etac disjE 1,
-                                      asm_simp_tac (HOL_ss addsimps con_rews) 1,
-                                      asm_simp_tac take_ss 1])
-                                    (filter is_nonlazy_rec args)))
-                                  cons))
-                                1 (conss~~casess))) handle ERROR => raise ERROR;
-  val all_finite=map (fn(dn,l1b)=>pg axs_finite_def (mk_trp(%%(dn^"_finite") $ %"x"))[
-                                case_UU_tac take_rews 1 "x",
-                                eresolve_tac finite_lemmas1a 1,
-                                step_tac HOL_cs 1,
-                                step_tac HOL_cs 1,
-                                cut_facts_tac [l1b] 1,
-                                fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
-in
-(all_finite,
- pg'' thy [] (ind_term (fn (P,x) => fn dn => %P $ %x))
-                               (ind_tacs (fn _ => fn (all_fin,finite_ind) => [
-                                rtac (rewrite_rule axs_finite_def all_fin RS exE) 1,
-                                etac subst 1,
-                                rtac finite_ind 1]) all_finite (atomize finite_ind))
+  let 
+    fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
+    val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> 
+	mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
+	take_enough dn)) ===> mk_trp(take_enough dn)) [
+				etac disjE 1,
+				etac notE 1,
+				resolve_tac take_lemmas 1,
+				asm_simp_tac take_ss 1,
+				atac 1]) dnames;
+    val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn 
+	(fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
+	 mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
+		 dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
+				rtac allI 1,
+				nat_ind_tac "n" 1,
+				simp_tac take_ss 1,
+			TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
+				flat(mapn (fn n => fn (cons,cases) => [
+				  simp_tac take_ss 1,
+				  rtac allI 1,
+				  res_inst_tac [("x",x_name n)] cases 1,
+				  asm_simp_tac take_ss 1] @ 
+				  flat(map (fn (con,args) => 
+				    asm_simp_tac take_ss 1 ::
+				    flat(map (fn vn => [
+				      eres_inst_tac [("x",vn)] all_dupE 1,
+				      etac disjE 1,
+				      asm_simp_tac (HOL_ss addsimps con_rews) 1,
+				      asm_simp_tac take_ss 1])
+				    (nonlazy_rec args)))
+				  cons))
+				1 (conss~~casess))) handle ERROR => raise ERROR;
+    val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
+						%%(dn^"_finite") $ %"x"))[
+				case_UU_tac take_rews 1 "x",
+				eresolve_tac finite_lemmas1a 1,
+				step_tac HOL_cs 1,
+				step_tac HOL_cs 1,
+				cut_facts_tac [l1b] 1,
+			fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
+  in
+  (finites,
+   pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems =>
+				TRY(safe_tac HOL_cs) ::
+			 flat (map (fn (finite,fin_ind) => [
+			       rtac(rewrite_rule axs_finite_def finite RS exE)1,
+				etac subst 1,
+				rtac fin_ind 1,
+				ind_prems_tac prems]) 
+			           (finites~~(atomize finite_ind)) ))
 ) end (* let *) else
-(mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) 
-                    [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
- pg'' thy [] (foldr (op ===>) (mapn (fn n =>K(mk_trp(%%"adm" $ %(P_name n))))1
-                                       dnames,ind_term (fn(P,x)=>fn dn=> %P $ %x)))
-                               (ind_tacs (fn (n,prems) => fn (ax_reach,finite_ind) =>[
-                                rtac (ax_reach RS subst) 1,
-                                res_inst_tac [("x",x_name n)] spec 1,
-                                rtac wfix_ind 1,
-                                rtac adm_impl_admw 1,
-                                resolve_tac adm_thms 1,
-                                rtac adm_subst 1,
-                                cont_tacR 1,
-                                resolve_tac prems 1,
-                                strip_tac 1,
-                                rtac(rewrite_rule axs_take_def finite_ind) 1])
-                                 axs_reach (atomize finite_ind))
+  (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) 
+	  	    [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
+   pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n))))
+	       1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
+		   (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) 
+				    axs_reach @ [
+				quant_tac 1,
+				rtac (adm_impl_admw RS wfix_ind) 1,
+				REPEAT_DETERM(rtac adm_all2 1),
+				REPEAT_DETERM(TRY(rtac adm_conj 1) THEN 
+						  rtac adm_subst 1 THEN 
+					cont_tacR 1 THEN resolve_tac prems 1),
+				strip_tac 1,
+				rtac (rewrite_rule axs_take_def finite_ind) 1,
+				ind_prems_tac prems])
 )
 end; (* local *)
 
+(* ----- theorem concerning coinduction ------------------------------------- *)
+
 local
   val xs = mapn (fn n => K (x_name n)) 1 dnames;
-  fun bnd_arg n i = Bound(2*(length dnames - n)-i-1);
+  fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   val take_ss = HOL_ss addsimps take_rews;
-  val sproj   = bin_branchr (fn s => "fst("^s^")") (fn s => "snd("^s^")");
-  val coind_lemma = pg [ax_bisim_def] (mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
-                foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
-                  foldr mk_imp (mapn (fn n => K(proj (%"R") dnames n $ 
-                                      bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
-                    foldr' mk_conj (mapn (fn n => fn dn => 
-                                (dc_take dn $ %"n" `bnd_arg n 0 === 
-                                (dc_take dn $ %"n" `bnd_arg n 1))) 0 dnames)))))) ([
-                                rtac impI 1,
-                                nat_ind_tac "n" 1,
-                                simp_tac take_ss 1,
-                                safe_tac HOL_cs] @
-                                flat(mapn (fn n => fn x => [
-                                  etac allE 1, etac allE 1, 
-                                  eres_inst_tac [("P1",sproj "R" dnames n^
-                                                  " "^x^" "^x^"'")](mp RS disjE) 1,
-                                  TRY(safe_tac HOL_cs),
-                                  REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
-                                0 xs));
+  val sproj   = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
+  val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
+		foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
+		  foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ 
+				      bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
+		    foldr' mk_conj (mapn (fn n => fn dn => 
+				(dc_take dn $ %"n" `bnd_arg n 0 === 
+				(dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
+			     ([ rtac impI 1,
+				nat_ind_tac "n" 1,
+				simp_tac take_ss 1,
+				safe_tac HOL_cs] @
+				flat(mapn (fn n => fn x => [
+				  rotate_tac (n+1) 1,
+				  etac all2E 1,
+				  eres_inst_tac [("P1", sproj "R" n_eqs n^
+					" "^x^" "^x^"'")](mp RS disjE) 1,
+				  TRY(safe_tac HOL_cs),
+				  REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
+				0 xs));
 in
 val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
-                foldr (op ===>) (mapn (fn n => fn x => 
-                        mk_trp(proj (%"R") dnames n $ %x $ %(x^"'"))) 0 xs,
-                        mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
-                                TRY(safe_tac HOL_cs)] @
-                                flat(map (fn take_lemma => [
-                                  rtac take_lemma 1,
-                                  cut_facts_tac [coind_lemma] 1,
-                                  fast_tac HOL_cs 1])
-                                take_lemmas));
+		foldr (op ===>) (mapn (fn n => fn x => 
+		  mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
+		  mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
+				TRY(safe_tac HOL_cs)] @
+				flat(map (fn take_lemma => [
+				  rtac take_lemma 1,
+				  cut_facts_tac [coind_lemma] 1,
+				  fast_tac HOL_cs 1])
+				take_lemmas));
 end; (* local *)