Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
authoroheimb
Wed Apr 03 19:27:14 1996 +0200 (1996-04-03)
changeset 1637b8a8ae2e5de1
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
     1.1 --- a/src/HOLCF/domain/axioms.ML	Wed Apr 03 19:02:04 1996 +0200
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Wed Apr 03 19:27:14 1996 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (* axioms.ML
     1.5 -   ID:         $Id$
     1.6     Author : David von Oheimb
     1.7     Created: 31-May-95
     1.8     Updated: 12-Jun-95 axioms for discriminators, selectors and induction
     1.9 @@ -24,137 +23,129 @@
    1.10  fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
    1.11  let
    1.12  
    1.13 -(* ----- axioms and definitions concerning the isomorphism ------------------------ *)
    1.14 +(* ----- axioms and definitions concerning the isomorphism ------------------ *)
    1.15  
    1.16    val dc_abs = %%(dname^"_abs");
    1.17    val dc_rep = %%(dname^"_rep");
    1.18    val x_name'= "x";
    1.19    val x_name = idx_name eqs x_name' (n+1);
    1.20  
    1.21 -  val ax_abs_iso = (dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name') === %x_name'));
    1.22 -  val ax_rep_iso = (dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name') === %x_name'));
    1.23 + val ax_abs_iso=(dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
    1.24 + val ax_rep_iso=(dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
    1.25  
    1.26    val ax_when_def = (dname^"_when_def",%%(dname^"_when") == 
    1.27 -           foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
    1.28 -                                Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
    1.29 +     foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
    1.30 +				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
    1.31  
    1.32 -  val ax_copy_def = let
    1.33 -    fun simp_oo (Const ("fapp", _) $ (Const ("fapp", _) $ 
    1.34 -                 Const ("cfcomp", _) $ fc) $ Const ("ID", _)) = fc
    1.35 -    |   simp_oo t = t;
    1.36 -    fun simp_app (Const ("fapp", _) $ Const ("ID", _) $ t) = t
    1.37 -    |   simp_app t = t;
    1.38 -        fun mk_arg m n arg  = (if is_lazy arg 
    1.39 -                               then fn t => %%"lift"`(simp_oo (%%"up" oo t)) else Id)
    1.40 -                              (if_rec arg (cproj (Bound (2*min[n,m])) eqs) (%%"ID"));
    1.41 -        fun mk_prod (t1,t2)  = %%"ssplit"`(/\ "x" (/\ "y" (%%"spair"`
    1.42 -                                         simp_app(t1`Bound 1)`simp_app(t2`Bound 0))));
    1.43 -        fun one_con (_,args) = if args = [] then %%"ID" else
    1.44 -                               foldr' mk_prod (mapn (mk_arg (length args-1)) 1 args);
    1.45 -        fun mk_sum  (t1,t2)  = %%"sswhen"`(simp_oo (%%"sinl" oo t1))
    1.46 -                                         `(simp_oo (%%"sinr" oo t2));
    1.47 -        in (dname^"_copy_def", %%(dname^"_copy") == /\"f" 
    1.48 -                          (dc_abs oo foldr' mk_sum (map one_con cons) oo dc_rep)) end;
    1.49 +  fun con_def outer recu m n (_,args) = let
    1.50 +     fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id)
    1.51 +			(if recu andalso is_rec arg then (cproj (Bound z) 
    1.52 +			(length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x));
    1.53 +     fun parms [] = %%"one"
    1.54 +     |   parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs);
    1.55 +     fun inj y 1 _ = y
    1.56 +     |   inj y _ 0 = %%"sinl"`y
    1.57 +     |   inj y i j = %%"sinr"`(inj y (i-1) (j-1));
    1.58 +  in foldr /\# (args, outer (inj (parms args) m n)) end;
    1.59  
    1.60 -(* ----- definitions concerning the constructors, discriminators and selectors ---- *)
    1.61 +  val ax_copy_def = (dname^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo 
    1.62 +	foldl (op `) (%%(dname^"_when") , 
    1.63 +	              mapn (con_def Id true (length cons)) 0 cons)));
    1.64  
    1.65 -  val axs_con_def = let
    1.66 -        fun idxs z x arg = (if is_lazy arg then fn x => %%"up"`x else Id)(Bound(z-x));
    1.67 -        fun prms [] = %%"one"
    1.68 -        |   prms vs = foldr' (fn(x,t)=> %%"spair"`x`t) (mapn (idxs (length vs)) 1 vs);
    1.69 -        val injs    = bin_branchr (fn l=> l@["l"]) (fn l=> l@["r"]);
    1.70 -        fun cdef ((con,args),injs) = (extern_name con ^"_def",%%con == 
    1.71 -                 foldr /\# (args,dc_abs`
    1.72 -                (foldr (fn (i,t) => %%("sin"^i)`t ) (injs, prms args))));
    1.73 -        in map cdef (cons~~(mapn (fn n => K(injs [] cons n)) 0 cons)) end;
    1.74 +(* -- definitions concerning the constructors, discriminators and selectors - *)
    1.75 +
    1.76 +  val axs_con_def = mapn (fn n => fn (con,args) => (extern_name con ^"_def",  
    1.77 +  %%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons;
    1.78  
    1.79    val axs_dis_def = let
    1.80 -        fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
    1.81 -                 mk_cfapp(%%(dname^"_when"),map 
    1.82 -                        (fn (con',args) => (foldr /\#
    1.83 -                           (args,if con'=con then %%"TT" else %%"FF"))) cons))
    1.84 -        in map ddef cons end;
    1.85 +	fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
    1.86 +		 mk_cfapp(%%(dname^"_when"),map 
    1.87 +			(fn (con',args) => (foldr /\#
    1.88 +			   (args,if con'=con then %%"TT" else %%"FF"))) cons))
    1.89 +	in map ddef cons end;
    1.90  
    1.91    val axs_sel_def = let
    1.92 -        fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
    1.93 -                 mk_cfapp(%%(dname^"_when"),map 
    1.94 -                        (fn (con',args) => if con'<>con then %%"UU" else
    1.95 -                         foldr /\# (args,Bound (length args - n))) cons));
    1.96 -        in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
    1.97 +	fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
    1.98 +		 mk_cfapp(%%(dname^"_when"),map 
    1.99 +			(fn (con',args) => if con'<>con then %%"UU" else
   1.100 +			 foldr /\# (args,Bound (length args - n))) cons));
   1.101 +	in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
   1.102  
   1.103  
   1.104 -(* ----- axiom and definitions concerning induction ------------------------------- *)
   1.105 +(* ----- axiom and definitions concerning induction ------------------------- *)
   1.106  
   1.107 -  fun cproj' T = cproj T eqs n;
   1.108 -  val ax_reach    = (dname^"_reach"   , mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
   1.109 -                                        `%x_name === %x_name));
   1.110 -  val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",
   1.111 -                    cproj'(%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
   1.112 +  fun cproj' T = cproj T (length eqs) n;
   1.113 +  val ax_reach = (dname^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
   1.114 +					`%x_name === %x_name));
   1.115 +  val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
   1.116 +		    (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
   1.117    val ax_finite_def = (dname^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
   1.118 -        mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
   1.119 +	mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
   1.120  
   1.121  in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @
   1.122      axs_con_def @ axs_dis_def @ axs_sel_def @
   1.123 -   [ax_reach, ax_take_def, ax_finite_def] end;
   1.124 +   [ax_reach, ax_take_def, ax_finite_def] 
   1.125 +end; (* let *)
   1.126  
   1.127  
   1.128  in (* local *)
   1.129  
   1.130 -fun add_axioms (comp_dname, eqs : eq list) thy' =let
   1.131 +fun add_axioms (comp_dname, eqs : eq list) thy' = let
   1.132    val dnames = map (fst o fst) eqs;
   1.133    val x_name = idx_name dnames "x"; 
   1.134    fun copy_app dname = %%(dname^"_copy")`Bound 0;
   1.135 -  val ax_copy_def  = (comp_dname^"_copy_def" , %%(comp_dname^"_copy") ==
   1.136 -                                           /\"f"(foldr' cpair (map copy_app dnames)));
   1.137 -  val ax_bisim_def = (comp_dname^"_bisim_def",%%(comp_dname^"_bisim") == mk_lam("R",
   1.138 +  val ax_copy_def =(comp_dname^"_copy_def" , %%(comp_dname^"_copy") ==
   1.139 +				    /\"f"(foldr' cpair (map copy_app dnames)));
   1.140 +  val ax_bisim_def=(comp_dname^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
   1.141      let
   1.142        fun one_con (con,args) = let
   1.143 -        val nonrec_args = filter_out is_rec args;
   1.144 -        val    rec_args = filter     is_rec args;
   1.145 -        val nonrecs_cnt = length nonrec_args;
   1.146 -        val    recs_cnt = length    rec_args;
   1.147 -        val allargs     = nonrec_args @ rec_args
   1.148 -                                      @ map (upd_vname (fn s=> s^"'")) rec_args;
   1.149 -        val allvns      = map vname allargs;
   1.150 -        fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
   1.151 -        val vns1        = map (vname_arg "" ) args;
   1.152 -        val vns2        = map (vname_arg "'") args;
   1.153 -        val allargs_cnt = nonrecs_cnt + 2*recs_cnt;
   1.154 -        val rec_idxs    = (recs_cnt-1) downto 0;
   1.155 -        val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
   1.156 -                                           (allargs~~((allargs_cnt-1) downto 0)));
   1.157 -        fun rel_app i ra = proj (Bound(allargs_cnt+2)) dnames (rec_of ra) $ 
   1.158 -                           Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
   1.159 -        val capps = foldr mk_conj (mapn rel_app 1 rec_args,
   1.160 -         mk_conj(Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
   1.161 -                 Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2)));
   1.162 +	val nonrec_args = filter_out is_rec args;
   1.163 +	val    rec_args = filter     is_rec args;
   1.164 +	val    recs_cnt = length rec_args;
   1.165 +	val allargs     = nonrec_args @ rec_args
   1.166 +				      @ map (upd_vname (fn s=> s^"'")) rec_args;
   1.167 +	val allvns      = map vname allargs;
   1.168 +	fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
   1.169 +	val vns1        = map (vname_arg "" ) args;
   1.170 +	val vns2        = map (vname_arg "'") args;
   1.171 +	val allargs_cnt = length nonrec_args + 2*recs_cnt;
   1.172 +	val rec_idxs    = (recs_cnt-1) downto 0;
   1.173 +	val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
   1.174 +					 (allargs~~((allargs_cnt-1) downto 0)));
   1.175 +	fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $ 
   1.176 +			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
   1.177 +	val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
   1.178 +	   Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
   1.179 +	   Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2)));
   1.180          in foldr mk_ex (allvns, foldr mk_conj 
   1.181 -                                      (map (defined o Bound) nonlazy_idxs,capps)) end;
   1.182 -      fun one_comp n (_,cons) = mk_all(x_name (n+1), mk_all(x_name (n+1)^"'", mk_imp(
   1.183 -                        proj (Bound 2) dnames n $ Bound 1 $ Bound 0,
   1.184 -         foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)::map one_con cons))));
   1.185 +			      (map (defined o Bound) nonlazy_idxs,capps)) end;
   1.186 +      fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
   1.187 +	 		proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0,
   1.188 +         		foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
   1.189 +					::map one_con cons))));
   1.190      in foldr' mk_conj (mapn one_comp 0 eqs)end ));
   1.191    val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @
   1.192 -                (if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
   1.193 +		(if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
   1.194  in thy' |> add_axioms_i (infer_types thy' thy_axs) end;
   1.195  
   1.196  
   1.197 -fun add_gen_by ((tname,finite),(typs,cnstrs)) thy' = let
   1.198 -  fun pred_name typ ="P"^(if typs=[typ] then "" else string_of_int(1+find(typ,typs)));
   1.199 -  fun lift_adm t = lift (fn typ => %%"adm" $ %(pred_name typ)) 
   1.200 -                        (if finite then [] else typs,t);
   1.201 -  fun lift_pred_UU t = lift (fn typ => %(pred_name typ) $ UU) (typs,t);
   1.202 +fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
   1.203 +  fun P_name typ = "P"^(if typs = [typ] then "" 
   1.204 +			else string_of_int(1 + find(typ,typs)));
   1.205 +  fun lift_adm t = lift (fn typ => %%"adm" $ %(P_name typ)) 
   1.206 +			(if finite then [] else typs,t);
   1.207 +  fun lift_pred_UU t = lift (fn typ => %(P_name typ) $ UU) (typs,t);
   1.208    fun one_cnstr (cnstr,vns,(args,res)) = let 
   1.209 -                        val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args);
   1.210 -                        val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns);
   1.211 -                     in foldr mk_All (vns,
   1.212 -                         lift (fn (vn,typ) => %(pred_name typ) $ bound_arg vns vn)
   1.213 -                              (rec_args,defined app ==> %(pred_name res)$app)) end;
   1.214 -  fun one_conc typ = let val pn = pred_name typ in
   1.215 -                     %pn $ %("x"^implode(tl(explode pn))) end;
   1.216 +		val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args);
   1.217 +		val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns);
   1.218 +	     in foldr mk_All (vns,
   1.219 +			 lift (fn (vn,typ) => %(P_name typ) $ bound_arg vns vn)
   1.220 +			      (rec_args,defined app ==> %(P_name res)$app)) end;
   1.221 +  fun one_conc typ = let val pn = P_name typ 
   1.222 +		     in %pn $ %("x"^implode(tl(explode pn))) end;
   1.223    val concl = mk_trp(foldr' mk_conj (map one_conc typs));
   1.224 -  val induct =(tname^"_induct",lift_adm(lift_pred_UU(
   1.225 -                        foldr (op ===>) (map one_cnstr cnstrs,concl))));
   1.226 +  val induct = (tname^"_induct",lift_adm(lift_pred_UU(
   1.227 +			foldr (op ===>) (map one_cnstr cnstrs,concl))));
   1.228  in thy' |> add_axioms_i (infer_types thy' [induct]) end;
   1.229  
   1.230  end; (* local *)
     2.1 --- a/src/HOLCF/domain/extender.ML	Wed Apr 03 19:02:04 1996 +0200
     2.2 +++ b/src/HOLCF/domain/extender.ML	Wed Apr 03 19:27:14 1996 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  (* extender.ML
     2.5 -   ID:         $Id$
     2.6     Author : David von Oheimb
     2.7     Created: 17-May-95
     2.8     Updated: 31-May-95 extracted syntax.ML, theorems.ML
     2.9 @@ -10,7 +9,7 @@
    2.10  *)
    2.11  
    2.12  
    2.13 -structure Extender =
    2.14 +structure Domain_Extender =
    2.15  struct
    2.16  
    2.17  local
    2.18 @@ -20,78 +19,77 @@
    2.19  (* ----- general testing and preprocessing of constructor list -------------------- *)
    2.20  
    2.21    fun check_domain(eqs':((string * typ list) *
    2.22 -                  (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
    2.23 +		  (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
    2.24      val dtnvs = map fst eqs';
    2.25      val cons' = flat (map snd eqs');
    2.26      val test_dupl_typs = (case duplicates (map fst dtnvs) of 
    2.27 -        [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    2.28 +	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    2.29      val test_dupl_cons = (case duplicates (map first cons') of 
    2.30 -        [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
    2.31 +	[] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
    2.32      val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of
    2.33          [] => false | dups => error ("Duplicate selectors: "^commas_quote dups));
    2.34      val test_dupl_tvars = let fun vname (TFree(v,_)) = v
    2.35 -                              |   vname _            = Imposs "extender:vname";
    2.36 -                          in exists (fn tvars => case duplicates (map vname tvars) of
    2.37 -        [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
    2.38 -        (map snd dtnvs) end;
    2.39 +			      |   vname _            = Imposs "extender:vname";
    2.40 +			  in exists (fn tvars => case duplicates (map vname tvars) of
    2.41 +	[] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
    2.42 +	(map snd dtnvs) end;
    2.43      (*test for free type variables and invalid use of recursive type*)
    2.44      val analyse_types = forall (fn ((_,typevars),cons') => 
    2.45 -        forall (fn con' => let
    2.46 -          val types = map third (third con');
    2.47 +	forall (fn con' => let
    2.48 +	  val types = map third (third con');
    2.49            fun analyse(t as TFree(v,_)) = t mem typevars orelse
    2.50 -                                        error ("Free type variable " ^ v ^ " on rhs.")
    2.51 -            | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
    2.52 -                                      | Some tvs => tvs = typl orelse 
    2.53 -                       error ("Recursion of type " ^ s ^ " with different arguments"))
    2.54 -            | analyse(TVar _) = Imposs "extender:analyse"
    2.55 -          and analyses ts = forall analyse ts;
    2.56 -          in analyses types end) cons' 
    2.57 -        ) eqs';
    2.58 +					error ("Free type variable " ^ v ^ " on rhs.")
    2.59 +	    | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
    2.60 +				      | Some tvs => tvs = typl orelse 
    2.61 +		       error ("Recursion of type " ^ s ^ " with different arguments"))
    2.62 +	    | analyse(TVar _) = Imposs "extender:analyse"
    2.63 +	  and analyses ts = forall analyse ts;
    2.64 +	  in analyses types end) cons' 
    2.65 +	) eqs';
    2.66      in true end; (* let *)
    2.67  
    2.68    fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let
    2.69      val test_dupl_typs = (case duplicates typs' of [] => false
    2.70 -          | dups => error ("Duplicate types: " ^ commas_quote dups));
    2.71 +	  | dups => error ("Duplicate types: " ^ commas_quote dups));
    2.72      val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false
    2.73 -          | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
    2.74 +	  | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
    2.75      val tsig = #tsig(Sign.rep_sg(sign_of thy'));
    2.76      val tycons = map fst (#tycons(Type.rep_tsig tsig));
    2.77      val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs';
    2.78      val cnstrss = let
    2.79 -        fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
    2.80 -                                | None => error ("Unknown constructor: "^c);
    2.81 -        fun args_result_type (t as (Type(tn,[arg,rest]))) = 
    2.82 -                        if tn = "->" orelse tn = "=>"
    2.83 -                        then let val (ts,r) = args_result_type rest in (arg::ts,r) end
    2.84 -                        else ([],t)
    2.85 -        |   args_result_type t = ([],t);
    2.86 +	fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
    2.87 +				| None => error ("Unknown constructor: "^c);
    2.88 +	fun args_result_type (t as (Type(tn,[arg,rest]))) = 
    2.89 +			if tn = "->" orelse tn = "=>"
    2.90 +			then let val (ts,r) = args_result_type rest in (arg::ts,r) end
    2.91 +			else ([],t)
    2.92 +	|   args_result_type t = ([],t);
    2.93      in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in
    2.94 -                         (cn,mk_var_names args,(args,res)) end)) cnstrss' 
    2.95 -        : (string *                     (* operator name of constr *)
    2.96 -           string list *                (* argument name list *)
    2.97 -           (typ list *                  (* argument types *)
    2.98 -            typ))                       (* result type *)
    2.99 -          list list end;
   2.100 +	                 (cn,mk_var_names args,(args,res)) end)) cnstrss' 
   2.101 +	: (string * 			(* operator name of constr *)
   2.102 +	   string list *		(* argument name list *)
   2.103 +	   (typ list *			(* argument types *)
   2.104 +	    typ))			(* result type *)
   2.105 +	  list list end;
   2.106      fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse
   2.107 -                               error("Inappropriate result type for constructor "^cn);
   2.108 -    val typs = map (fn (tn, cnstrs) => 
   2.109 -                     (map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs)))))
   2.110 -                   (typs'~~cnstrss);
   2.111 +			       error("Inappropriate result type for constructor "^cn);
   2.112 +    val typs = map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs; 
   2.113 +					snd(third(hd(cnstrs)))))  (typs'~~cnstrss);
   2.114      val test_typs = map (fn (typ,cnstrs) => 
   2.115 -                        if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
   2.116 -                        then error("Not a pcpo type: "^fst(type_name_vars typ))
   2.117 -                        else map (fn (cn,_,(_,rt)) => rt=typ 
   2.118 -                          orelse error("Non-identical result types for constructors "^
   2.119 -                          first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
   2.120 +			if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
   2.121 +			then error("Not a pcpo type: "^fst(type_name_vars typ))
   2.122 +			else map (fn (cn,_,(_,rt)) => rt=typ 
   2.123 +		 	  orelse error("Non-identical result types for constructors "^
   2.124 +			  first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
   2.125      val proper_args = let
   2.126 -        fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
   2.127 -        |   occurs _  _              = false;
   2.128 -        fun proper_arg cn atyp = forall (fn typ => let 
   2.129 -                                   val tn = fst(type_name_vars typ) 
   2.130 -                                   in atyp=typ orelse not (occurs tn atyp) orelse 
   2.131 -                                      error("Illegal use of type "^ tn ^
   2.132 -                                         " as argument of constructor " ^cn)end )typs;
   2.133 -        fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
   2.134 +	fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
   2.135 +	|   occurs _  _              = false;
   2.136 +	fun proper_arg cn atyp = forall (fn typ => let 
   2.137 +				   val tn = fst(type_name_vars typ) 
   2.138 +				   in atyp=typ orelse not (occurs tn atyp) orelse 
   2.139 +				      error("Illegal use of type "^ tn ^
   2.140 +					 " as argument of constructor " ^cn)end )typs;
   2.141 +	fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
   2.142      in map (map proper_curry) cnstrss end;
   2.143    in (typs, flat cnstrss) end;
   2.144  
   2.145 @@ -100,16 +98,16 @@
   2.146  in
   2.147  
   2.148    fun add_domain (comp_dname,eqs') thy'' = let
   2.149 -    val ok_dummy = check_domain eqs';
   2.150 +    val ok   = check_domain eqs';
   2.151      val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs');
   2.152      val dts  = map (Type o fst) eqs';
   2.153      fun cons cons' = (map (fn (con,syn,args) =>
   2.154 -        (ThyOps.const_name con syn,
   2.155 -         map (fn ((lazy,sel,tp),vn) => ((lazy,
   2.156 -                                         find (tp,dts) handle LIST "find" => ~1),
   2.157 -                                        sel,vn))
   2.158 -             (args~~(mk_var_names(map third args)))
   2.159 -         )) cons') : cons list;
   2.160 +	(ThyOps.const_name con syn,
   2.161 +	 map (fn ((lazy,sel,tp),vn) => ((lazy,
   2.162 +					 find (tp,dts) handle LIST "find" => ~1),
   2.163 +					sel,vn))
   2.164 +	     (args~~(mk_var_names(map third args)))
   2.165 +	 )) cons') : cons list;
   2.166      val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
   2.167      val thy         = thy' |> Domain_Axioms.add_axioms (comp_dname,eqs);
   2.168    in (thy,eqs) end;
   2.169 @@ -117,7 +115,7 @@
   2.170    fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
   2.171     val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss');
   2.172    in
   2.173 -   Domain_Axioms.add_gen_by ((tname,finite),(typs,cnstrs)) thy' end;
   2.174 +   Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
   2.175  
   2.176  end (* local *)
   2.177  end (* struct *)
     3.1 --- a/src/HOLCF/domain/interface.ML	Wed Apr 03 19:02:04 1996 +0200
     3.2 +++ b/src/HOLCF/domain/interface.ML	Wed Apr 03 19:27:14 1996 +0200
     3.3 @@ -1,6 +1,5 @@
     3.4  (* interface.ML
     3.5 -   ID:         $Id$
     3.6 -   Author:      David von Oheimb
     3.7 +   Author:  David von Oheimb
     3.8     Created: 17-May-95
     3.9     Updated: 24-May-95
    3.10     Updated: 03-Jun-95 incremental change of ThySyn
    3.11 @@ -11,39 +10,38 @@
    3.12     Copyright 1995 TU Muenchen
    3.13  *)
    3.14  
    3.15 -local
    3.16 +structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *)
    3.17  
    3.18 -structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData!!!!!!! *)
    3.19  struct
    3.20  
    3.21  local 
    3.22    open ThyParse;
    3.23    open Domain_Library;
    3.24  
    3.25 -(* ----- generation of bindings for axioms and theorems in trailer of .thy.ML ----- *)
    3.26 +(* --- generation of bindings for axioms and theorems in trailer of .thy.ML - *)
    3.27  
    3.28 -  fun gt_ax         name   = "get_axiom thy "^quote name;
    3.29 -  fun gen_val dname name   = "val "^name^" = " ^gt_ax (dname^"_"^name)^";";
    3.30 -  fun gen_vall      name l = "val "^name^" = " ^mk_list l^";";
    3.31 +  fun gt_ax         name   = "get_axiom thy " ^ quote name;
    3.32 +  fun gen_val dname name   = "val "^name^" = "^ gt_ax (dname^"_"^name)^";";
    3.33 +  fun gen_vall      name l = "val "^name^" = "^ mk_list l^";";
    3.34    val rews1 = "iso_rews @ when_rews @\n\
    3.35 -              \con_rews @ sel_rews @ dis_rews @ dists_eq @ dists_le @\n\
    3.36 -              \copy_rews";
    3.37 + 	      \con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\
    3.38 +	      \copy_rews";
    3.39  
    3.40    fun gen_domain eqname num ((dname,_), cons') = let
    3.41      val axioms1 = ["abs_iso", "rep_iso", "when_def"];
    3.42 -                   (* con_defs , sel_defs, dis_defs *) 
    3.43 +		   (* con_defs , sel_defs, dis_defs *) 
    3.44      val axioms2 = ["copy_def"];
    3.45      val theorems = 
    3.46 -        "iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
    3.47 -        \dists_eq, dists_le, inverts, injects, copy_rews";
    3.48 +	"iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
    3.49 +	\dists_le, dists_eq, inverts, injects, copy_rews";
    3.50      in
    3.51        "structure "^dname^" = struct\n"^
    3.52        cat_lines(map (gen_val dname) axioms1)^"\n"^
    3.53        gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
    3.54        gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => 
    3.55 -                                             gt_ax(sel^"_def")) args)    cons'))^"\n"^
    3.56 +					     gt_ax(sel^"_def")) args)    cons'))^"\n"^
    3.57        gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) 
    3.58 -                                                                          cons')^"\n"^
    3.59 +								          cons')^"\n"^
    3.60        cat_lines(map (gen_val dname) axioms2)^"\n"^
    3.61        "val ("^ theorems ^") =\n\
    3.62        \Domain_Theorems.theorems thy "^eqname^";\n" ^
    3.63 @@ -57,117 +55,112 @@
    3.64      val comp_dname = implode (separate "_" dnames);
    3.65      val conss' = map (fn (dname,cons'') =>
    3.66        let
    3.67 -        fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
    3.68 -                                                         "_"^(string_of_int m)
    3.69 -                                  |  Some s => s)
    3.70 -        fun fill_sels n con = upd_third (mapn (sel n) 1) con;
    3.71 +	fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
    3.72 +							 "_"^(string_of_int m)
    3.73 +				  |  Some s => s)
    3.74 +	fun fill_sels n con = upd_third (mapn (sel n) 1) con;
    3.75        in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs''));
    3.76      val eqs' = dtnvs~~conss';
    3.77  
    3.78 -(* ----- generation of argument string for calling add_domain --------------------- *)
    3.79 -
    3.80 -
    3.81 -     fun string_of_sort_emb [] = ""
    3.82 -     |   string_of_sort_emb [x] = "\"" ^x^ "\"" 
    3.83 -        |   string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs);
    3.84 -
    3.85 -        fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
    3.86 +(* ----- string for calling add_domain -------------------------------------- *)
    3.87  
    3.88 -    fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
    3.89 -    and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)
    3.90 -    |   mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args)
    3.91 -    |   mk_typ _                  = Imposs "interface:mk_typ";
    3.92 -    fun mk_conslist cons' = mk_list (map 
    3.93 -          (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
    3.94 -     (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
    3.95 -                                    mk_typ tp)) ts))) cons');
    3.96 +    val thy_ext_string = let
    3.97 +      fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
    3.98 +      and mk_typ (TFree(name,sort))= "TFree"^mk_pair(quote name,
    3.99 +						     mk_list(map quote sort))
   3.100 +      |   mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args)
   3.101 +      |   mk_typ _                 = Imposs "interface:mk_typ";
   3.102 +      fun mk_conslist cons' = mk_list (map 
   3.103 +	    (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
   3.104 +       (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
   3.105 +				      mk_typ tp)) ts))) cons');
   3.106 +    in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n"
   3.107 +       ^ mk_pair(quote comp_dname,
   3.108 +		 mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
   3.109 +       ^ ";\nval thy = thy"
   3.110 +    end;
   3.111 +
   3.112 +(* ----- string for calling (comp_)theorems and producing the structures ---------- *)
   3.113 +
   3.114 +    val val_gen_string =  let
   3.115 +      fun plural s = if num > 1 then s^"s" else "["^s^"]";
   3.116 +      val comp_axioms   = [(* copy, *) "reach", "take_def", "finite_def"
   3.117 +			   (*, "bisim_def" *)];
   3.118 +      val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
   3.119 +			       ["take_lemma","finite"]))^", finite_ind, ind, coind";
   3.120 +      fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
   3.121 +							 ^comp_dname^"_equations)";
   3.122 +      fun collect sep name = if num = 1 then name else
   3.123 +			     implode (separate sep (map (fn s => s^"."^name) dnames));
   3.124      in
   3.125 -      ("val (thy, "^comp_dname^"_equations) = thy |> Extender.add_domain \n"
   3.126 -      ^ mk_pair(quote comp_dname,
   3.127 -                mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
   3.128 -      ^ ";\nval thy = thy",
   3.129 -      let
   3.130 -        fun plural s = if num > 1 then s^"s" else "["^s^"]";
   3.131 -        val comp_axioms   = [(* copy, *) "take_def", "finite_def", "reach" 
   3.132 -                             (*, "bisim_def" *)];
   3.133 -        val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
   3.134 -                                ["take_lemma","finite"]))^", finite_ind, ind, coind";
   3.135 -        fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
   3.136 -                                                           ^comp_dname^"_equations)";
   3.137 -        fun collect sep name = if num = 1 then name else
   3.138 -                           implode (separate sep (map (fn s => s^"."^name) dnames));
   3.139 -      in
   3.140 -        implode (separate "end; (* struct *)\n\n" 
   3.141 -                 (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
   3.142 -        "end; (* struct *)\n\n\
   3.143 -        \structure "^comp_dname^" = struct\n" else "") ^
   3.144 -         (if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
   3.145 -         implode ((map (fn s => gen_vall (plural s)
   3.146 -                  (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
   3.147 -         gen_val comp_dname "bisim_def" ^"\n\
   3.148 +      implode (separate "end; (* struct *)\n\n" 
   3.149 +        	 (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
   3.150 +      "end; (* struct *)\n\n\
   3.151 +      \structure "^comp_dname^" = struct\n" else "") ^
   3.152 +	(if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
   3.153 +	implode ((map (fn s => gen_vall (plural s)
   3.154 +	           (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
   3.155 +	 gen_val comp_dname "bisim_def" ^"\n\
   3.156          \val ("^ comp_theorems ^") =\n\
   3.157 -        \Domain_Theorems.comp_theorems thy \
   3.158 -        \(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
   3.159 -        \ ["^collect "," "cases"    ^"],\n\
   3.160 -        \ "^ collect "@" "con_rews " ^",\n\
   3.161 -        \ "^ collect "@" "copy_rews" ^");\n\
   3.162 -        \val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
   3.163 -        \end; (* struct *)"
   3.164 -      end
   3.165 -      ) end;
   3.166 +	\Domain_Theorems.comp_theorems thy \
   3.167 +	\(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
   3.168 +	\ ["^collect "    ," "cases"    ^"],\n\
   3.169 +	\  "^collect "@"     "con_rews " ^",\n\
   3.170 +	\  "^collect " @"    "copy_rews" ^");\n\
   3.171 +	\val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
   3.172 +      \end; (* struct *)"
   3.173 +    end;
   3.174 +  in (thy_ext_string, val_gen_string) end;
   3.175 +
   3.176 +(* ----- strings for calling add_gen_by and producing the value binding ----------- *)
   3.177  
   3.178    fun mk_gen_by (finite,eqs) = let
   3.179        val typs    = map fst eqs;
   3.180        val cnstrss = map snd eqs;
   3.181        val tname = implode (separate "_" typs) in
   3.182 -      ("|> Extender.add_gen_by "
   3.183 -      ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
   3.184 -                mk_pair(mk_list(map quote typs), 
   3.185 -                        mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
   3.186 -      "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
   3.187 +      ("|> Domain_Extender.add_gen_by "
   3.188 +       ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
   3.189 +		 mk_pair(mk_list(map quote typs), 
   3.190 +			 mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
   3.191 +       "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
   3.192  
   3.193  (* ----- parser for domain declaration equation ----------------------------------- *)
   3.194  
   3.195  (**
   3.196    val sort = name >> (fn s => [strip_quotes s])
   3.197 -          || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
   3.198 +	  || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
   3.199    val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree
   3.200  **)
   3.201    val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));
   3.202  
   3.203    val type_args = "(" $$-- !! (list1 tvar --$$ ")")
   3.204 -               || tvar  >> (fn x => [x])
   3.205 -               || empty >> K [];
   3.206 +	       || tvar  >> (fn x => [x])
   3.207 +	       || empty >> K [];
   3.208    val con_typ     = type_args -- ident >> (fn (x,y) => Type(y,x));
   3.209    val typ         = con_typ 
   3.210 -                 || tvar;
   3.211 +		 || tvar;
   3.212    val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
   3.213 -                          -- (optional ((ident >> Some) --$$ "::") None)
   3.214 -                          -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
   3.215 -                 || ident >> (fn x => (false,None,Type(x,[])))
   3.216 -                 || tvar  >> (fn x => (false,None,x));
   3.217 +			  -- (optional ((ident >> Some) --$$ "::") None)
   3.218 +			  -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
   3.219 +		 || ident >> (fn x => (false,None,Type(x,[])))
   3.220 +		 || tvar  >> (fn x => (false,None,x));
   3.221    val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) 
   3.222 -                    -- ThyOps.opt_cmixfix
   3.223 -                    >> (fn ((con,args),syn) => (con,syn,args));
   3.224 +		    -- ThyOps.opt_cmixfix
   3.225 +		    >> (fn ((con,args),syn) => (con,syn,args));
   3.226  in
   3.227    val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
   3.228 -                               (enum1 "|" domain_cons)))            >> mk_domain;
   3.229 +			       (enum1 "|" domain_cons))) 	    >> mk_domain;
   3.230    val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
   3.231 -                    (enum1 "," (ident   --$$ "by" -- !!
   3.232 -                               (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
   3.233 -end;
   3.234 +		    (enum1 "," (ident   --$$ "by" -- !!
   3.235 +			       (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
   3.236 +end; (* local *)
   3.237  
   3.238  val user_keywords = "lazy"::"by"::"finite"::
   3.239 -                (**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
   3.240 -                    ThySynData.user_keywords;
   3.241 +		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
   3.242 +		    ThySynData.user_keywords;
   3.243  val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
   3.244 -                (**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
   3.245 -                    ThySynData.user_sections;
   3.246 -end;
   3.247 -
   3.248 -in
   3.249 +		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
   3.250 +		    ThySynData.user_sections;
   3.251 +end; (* struct *)
   3.252  
   3.253  structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)
   3.254 -
   3.255 -end; (* local *)
   3.256 -
     4.1 --- a/src/HOLCF/domain/library.ML	Wed Apr 03 19:02:04 1996 +0200
     4.2 +++ b/src/HOLCF/domain/library.ML	Wed Apr 03 19:27:14 1996 +0200
     4.3 @@ -1,26 +1,25 @@
     4.4  (* library.ML
     4.5 -   ID:         $Id$
     4.6 -   Author:      David von Oheimb
     4.7 +   Author : David von Oheimb
     4.8     Created: 18-Jul-95 extracted from syntax.ML, axioms.ML, extender.ML, interface.ML
     4.9     Updated: 30-Aug-95
    4.10 +   Updated: 20-Oct-95 small improvement for atomize
    4.11     Copyright 1995 TU Muenchen
    4.12  *)
    4.13  
    4.14 -(* ----- general support ---------------------------------------------------------- *)
    4.15 +(* ----- general support ---------------------------------------------------- *)
    4.16  
    4.17  fun Id x = x;
    4.18  
    4.19  fun mapn f n []      = []
    4.20  |   mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
    4.21  
    4.22 -fun foldr'' f (l,f2) =
    4.23 -  let fun itr []  = raise LIST "foldr''"
    4.24 -        | itr [a] = f2 a
    4.25 -        | itr (a::l) = f(a, itr l)
    4.26 -  in  itr l  end;
    4.27 +fun foldr'' f (l,f2) = let fun itr []  = raise LIST "foldr''"
    4.28 +			     | itr [a] = f2 a
    4.29 +			     | itr (a::l) = f(a, itr l)
    4.30 +in  itr l  end;
    4.31  fun foldr' f l = foldr'' f (l,Id);
    4.32 -fun map_cumulr f start xs = foldr (fn (x,(ys,res)) => case f(x,res) of (y,res2) => 
    4.33 -                                                      (y::ys,res2)) (xs,([],start));
    4.34 +fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
    4.35 +						  (y::ys,res2)) (xs,([],start));
    4.36  
    4.37  
    4.38  fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    4.39 @@ -28,21 +27,14 @@
    4.40  fun upd_second f (x,y,z) = (  x, f y,   z);
    4.41  fun upd_third  f (x,y,z) = (  x,   y, f z);
    4.42  
    4.43 -(* fn : ('a -> 'a) -> ('a -> 'a) -> 'a -> 'b list -> int -> 'a *)
    4.44 -fun bin_branchr f1 f2 y is j = let
    4.45 -fun bb y 1 _ = y
    4.46 -|   bb y _ 0 = f1 y
    4.47 -|   bb y i j = if i=2 then (f2 y) else bb (f2 y) (i-1) (j-1)
    4.48 -in bb y (length is) j end;
    4.49 +fun atomize thm = let val r_inst = read_instantiate;
    4.50 +    fun at  thm = case concl_of thm of
    4.51 +      _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    4.52 +    | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
    4.53 +    | _				    => [thm];
    4.54 +in map zero_var_indexes (at thm) end;
    4.55  
    4.56 -fun atomize thm = case concl_of thm of
    4.57 -      _ $ (Const("op &",_) $ _ $ _)       => atomize (thm RS conjunct1) @
    4.58 -                                             atomize (thm RS conjunct2)
    4.59 -    | _ $ (Const("All" ,_) $ Abs (s,_,_)) => atomize (thm RS 
    4.60 -                                             (read_instantiate [("x","?"^s)] spec))
    4.61 -    | _                               => [thm];
    4.62 -
    4.63 -(* ----- specific support for domain ---------------------------------------------- *)
    4.64 +(* ----- specific support for domain ---------------------------------------- *)
    4.65  
    4.66  structure Domain_Library = struct
    4.67  
    4.68 @@ -51,29 +43,28 @@
    4.69  
    4.70  (* ----- name handling ----- *)
    4.71  
    4.72 -val strip_esc = let
    4.73 -  fun strip ("'" :: c :: cs) = c :: strip cs
    4.74 -  |   strip ["'"] = []
    4.75 -  |   strip (c :: cs) = c :: strip cs
    4.76 -  |   strip [] = [];
    4.77 +val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs
    4.78 +		    |   strip ["'"] = []
    4.79 +		    |   strip (c :: cs) = c :: strip cs
    4.80 +		    |   strip [] = [];
    4.81  in implode o strip o explode end;
    4.82  
    4.83  fun extern_name con = case explode con of 
    4.84 -                   ("o"::"p"::" "::rest) => implode rest
    4.85 -                   | _ => con;
    4.86 +		   ("o"::"p"::" "::rest) => implode rest
    4.87 +		   | _ => con;
    4.88  fun dis_name  con = "is_"^ (extern_name con);
    4.89  fun dis_name_ con = "is_"^ (strip_esc   con);
    4.90  
    4.91 -(*make distinct names out of the type list, 
    4.92 -  forbidding "o", "x..","f..","P.." as names *)
    4.93 -(*a number string is added if necessary *)
    4.94 +(* make distinct names out of the type list, 
    4.95 +   forbidding "o", "x..","f..","P.." as names *)
    4.96 +(* a number string is added if necessary *)
    4.97  fun mk_var_names types : string list = let
    4.98      fun typid (Type  (id,_)   ) = hd     (explode id)
    4.99        | typid (TFree (id,_)   ) = hd (tl (explode id))
   4.100        | typid (TVar ((id,_),_)) = hd (tl (explode id));
   4.101      fun nonreserved id = let val cs = explode id in
   4.102 -                         if not(hd cs mem ["x","f","P"]) then id
   4.103 -                         else implode(chr(1+ord (hd cs))::tl cs) end;
   4.104 +			 if not(hd cs mem ["x","f","P"]) then id
   4.105 +			 else implode(chr(1+ord (hd cs))::tl cs) end;
   4.106      fun index_vnames(vn::vns,tab) =
   4.107            (case assoc(tab,vn) of
   4.108               None => if vn mem vns
   4.109 @@ -86,24 +77,16 @@
   4.110  fun type_name_vars (Type(name,typevars)) = (name,typevars)
   4.111  |   type_name_vars _                     = Imposs "library:type_name_vars";
   4.112  
   4.113 -(* ----- support for type and mixfix expressions ----- *)
   4.114 -
   4.115 -fun mk_tvar s = TFree("'"^s,["pcpo"]);
   4.116 -fun mk_typ t (S,T) = Type(t,[S,T]);
   4.117 -infixr 5 -->;
   4.118 -infixr 6 ~>; val op ~> = mk_typ "->";
   4.119 -val NoSyn' = ThyOps.Mixfix NoSyn;
   4.120 -
   4.121  (* ----- constructor list handling ----- *)
   4.122  
   4.123 -type cons = (string *                   (* operator name of constr *)
   4.124 -            ((bool*int)*                (*  (lazy,recursive element or ~1) *)
   4.125 -              string*                   (*   selector name    *)
   4.126 -              string)                   (*   argument name    *)
   4.127 -            list);                      (* argument list      *)
   4.128 -type eq = (string *             (* name      of abstracted type *)
   4.129 -           typ list) *          (* arguments of abstracted type *)
   4.130 -          cons list;            (* represented type, as a constructor list *)
   4.131 +type cons = (string *			(* operator name of constr *)
   4.132 +	    ((bool*int)*		(*  (lazy,recursive element or ~1) *)
   4.133 +	      string*			(*   selector name    *)
   4.134 +	      string)			(*   argument name    *)
   4.135 +	    list);			(* argument list      *)
   4.136 +type eq = (string *		(* name      of abstracted type *)
   4.137 +	   typ list) *		(* arguments of abstracted type *)
   4.138 +	  cons list;		(* represented type, as a constructor list *)
   4.139  
   4.140  val rec_of    = snd o first;
   4.141  val is_lazy   = fst o first;
   4.142 @@ -112,9 +95,16 @@
   4.143  val upd_vname =   upd_third;
   4.144  fun is_rec         arg = rec_of arg >=0;
   4.145  fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
   4.146 -fun nonlazy args       = map vname (filter_out is_lazy args);
   4.147 -fun is_one_con_one_arg p cons = length cons = 1 andalso let val args = snd(hd cons) in
   4.148 -                                length args = 1 andalso p (hd args) end;
   4.149 +fun nonlazy     args   = map vname (filter_out is_lazy    args);
   4.150 +fun nonlazy_rec args   = map vname (filter is_nonlazy_rec args);
   4.151 +
   4.152 +(* ----- support for type and mixfix expressions ----- *)
   4.153 +
   4.154 +fun mk_tvar s = TFree("'"^s,["pcpo"]);
   4.155 +fun mk_typ t (S,T) = Type(t,[S,T]);
   4.156 +infixr 5 -->;
   4.157 +infixr 6 ~>; val op ~> = mk_typ "->";
   4.158 +val NoSyn' = ThyOps.Mixfix NoSyn;
   4.159  
   4.160  (* ----- support for term expressions ----- *)
   4.161  
   4.162 @@ -130,26 +120,26 @@
   4.163  fun mk_lam  (x,T) = Abs(x,dummyT,T);
   4.164  fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
   4.165  local 
   4.166 -                    fun tf (Type (s,args)) = foldl (op $) (%s,map tf args)
   4.167 -                    |   tf (TFree(s,_   )) = %s
   4.168 -                    |   tf _              = Imposs "mk_constrainall";
   4.169 +		    fun tf (Type (s,args)) = foldl (op $) (%s,map tf args)
   4.170 +		    |   tf (TFree(s,_   )) = %s
   4.171 +		    |   tf _              = Imposs "mk_constrainall";
   4.172  in
   4.173  fun mk_constrain      (typ,T) = %%"_constrain" $ T $ tf typ;
   4.174 -fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs"$Abs(x,dummyT,P)$tf typ);
   4.175 +fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ);
   4.176  end;
   4.177 -                        
   4.178 +			
   4.179  fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
   4.180  fun mk_not     P  = Const("not" ,boolT --> boolT) $ P;
   4.181  end;
   4.182  
   4.183  fun mk_All  (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *)
   4.184  
   4.185 -infixr 0 ===>;fun S ===> T = Const("==>", dummyT) $ S $ T;
   4.186 +infixr 0 ===>;fun S ===> T = %%"==>" $ S $ T;
   4.187  infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T;
   4.188 -infix 0 ==;  fun S ==  T = Const("==", dummyT) $ S $ T;
   4.189 -infix 1 ===; fun S === T = Const("op =", dummyT) $ S $ T;
   4.190 +infix 0 ==;  fun S ==  T = %%"==" $ S $ T;
   4.191 +infix 1 ===; fun S === T = %%"op =" $ S $ T;
   4.192  infix 1 ~=;  fun S ~=  T = mk_not (S === T);
   4.193 -infix 1 <<;  fun S <<  T = Const("op <<", dummyT) $ S $ T;
   4.194 +infix 1 <<;  fun S <<  T = %%"op <<" $ S $ T;
   4.195  infix 1 ~<<; fun S ~<< T = mk_not (S << T);
   4.196  
   4.197  infix 9 `  ; fun f`  x = %%"fapp" $ f $ x;
   4.198 @@ -160,8 +150,11 @@
   4.199  fun con_app con = con_app2 con %#;
   4.200  fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
   4.201  fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
   4.202 -val cproj    = bin_branchr (fn S => %%"cfst"`S) (fn S => %%"csnd"`S);
   4.203 -val  proj    = bin_branchr (fn S => %%"fst" $S) (fn S => %%"snd" $S);
   4.204 +fun prj _  _  y 1 _ = y
   4.205 +|   prj f1 _  y _ 0 = f1 y
   4.206 +|   prj f1 f2 y i j = prj f1 f2 (f2 y) (i-1) (j-1);
   4.207 +val cproj    = prj (fn S => %%"cfst"`S) (fn S => %%"csnd"`S);
   4.208 +val  proj    = prj (fn S => %%"fst" $S) (fn S => %%"snd" $S);
   4.209  fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
   4.210  
   4.211  fun /\ v T = %%"fabs" $ mk_lam(v,T);
   4.212 @@ -177,26 +170,27 @@
   4.213  fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = 
   4.214        (case cont_eta_contract body  of
   4.215          body' as (Const("fapp",Ta) $ f $ Bound 0) => 
   4.216 -          if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
   4.217 -          else   Const("fabs",TT) $ Abs(a,T,body')
   4.218 +	  if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
   4.219 +	  else   Const("fabs",TT) $ Abs(a,T,body')
   4.220        | body' => Const("fabs",TT) $ Abs(a,T,body'))
   4.221  |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
   4.222  |   cont_eta_contract t    = t;
   4.223  
   4.224 -fun idx_name dnames s n = s ^ (if length dnames = 1 then "" else string_of_int n);
   4.225 +fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
   4.226  fun when_funs cons = if length cons = 1 then ["f"] 
   4.227 -                     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
   4.228 +		     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
   4.229  fun when_body cons funarg = let
   4.230 -        fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   4.231 -        |   one_fun n (_,args) = let
   4.232 -                val l2 = length args;
   4.233 -                fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
   4.234 -                                                 else Id) (Bound(l2-m));
   4.235 -                in cont_eta_contract (foldr'' 
   4.236 -                         (fn (a,t) => %%"ssplit"`(/\# (a,t)))
   4.237 -                         (args,
   4.238 -                          fn a => /\# (a,(mk_cfapp(funarg (l2,n),mapn idxs 1 args))))
   4.239 -                         ) end;
   4.240 -in foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons) end;
   4.241 -
   4.242 +	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   4.243 +	|   one_fun n (_,args) = let
   4.244 +		val l2 = length args;
   4.245 +		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
   4.246 +					         else Id) (Bound(l2-m));
   4.247 +		in cont_eta_contract (foldr'' 
   4.248 +			(fn (a,t) => %%"ssplit"`(/\# (a,t)))
   4.249 +			(args,
   4.250 +			fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args))))
   4.251 +			) end;
   4.252 +in (if length cons = 1 andalso length(snd(hd cons)) <= 1
   4.253 +    then fn t => %%"strictify"`t else Id)
   4.254 +     (foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons)) end;
   4.255  end; (* struct *)
     5.1 --- a/src/HOLCF/domain/syntax.ML	Wed Apr 03 19:02:04 1996 +0200
     5.2 +++ b/src/HOLCF/domain/syntax.ML	Wed Apr 03 19:27:14 1996 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (* syntax.ML
     5.5 -   ID:         $Id$
     5.6     Author:  David von Oheimb
     5.7     Created: 31-May-95
     5.8     Updated: 16-Aug-95 case translation
     5.9 @@ -14,21 +13,24 @@
    5.10  
    5.11  open Domain_Library;
    5.12  infixr 5 -->; infixr 6 ~>;
    5.13 -fun calc_syntax dtypeprod ((dname,typevars),
    5.14 -                (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
    5.15 +fun calc_syntax dtypeprod ((dname, typevars), (cons':
    5.16 +			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
    5.17  let
    5.18  (* ----- constants concerning the isomorphism ------------------------------------- *)
    5.19  
    5.20  local
    5.21    fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
    5.22 -  fun prod (_,_,args) = if args = [] then Type("one",[])
    5.23 -                                     else foldr' (mk_typ "**") (map opt_lazy args);
    5.24 -
    5.25 +  fun prod     (_,_,args) = if args = [] then Type("one",[])
    5.26 +				         else foldr'(mk_typ "**") (map opt_lazy args);
    5.27 +  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    5.28 +  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    5.29  in
    5.30    val dtype  = Type(dname,typevars);
    5.31    val dtype2 = foldr' (mk_typ "++") (map prod cons');
    5.32    val const_rep  = (dname^"_rep" ,              dtype  ~> dtype2, NoSyn');
    5.33    val const_abs  = (dname^"_abs" ,              dtype2 ~> dtype , NoSyn');
    5.34 +  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    5.35 +						 dtype ~> freetvar "t"), NoSyn');
    5.36    val const_copy = (dname^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    5.37  end;
    5.38  
    5.39 @@ -42,20 +44,16 @@
    5.40  
    5.41  local
    5.42    val escape = let
    5.43 -        fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    5.44 -                                                           else        c :: esc cs
    5.45 -        |   esc []        = []
    5.46 -        in implode o esc o explode end;
    5.47 -  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    5.48 -  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    5.49 +	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    5.50 +							   else        c :: esc cs
    5.51 +	|   esc []        = []
    5.52 +	in implode o esc o explode end;
    5.53    fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
    5.54    fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
    5.55 -                                 ThyOps.Mixfix(Mixfix("is'_"^
    5.56 -                                 (if is_infix s then Id else escape)con,[],max_pri)));
    5.57 +			 	 ThyOps.Mixfix(Mixfix("is'_"^
    5.58 +				 (if is_infix s then Id else escape)con,[],max_pri)));
    5.59    fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
    5.60  in
    5.61 -  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    5.62 -                                                 dtype ~> freetvar "t"), NoSyn');
    5.63    val consts_con = map con cons';
    5.64    val consts_dis = map dis cons';
    5.65    val consts_sel = flat(map sel cons');
    5.66 @@ -63,32 +61,32 @@
    5.67  
    5.68  (* ----- constants concerning induction ------------------------------------------- *)
    5.69  
    5.70 -  val const_take   = (dname^"_take"  ,Type("nat",[]) --> dtype ~> dtype    ,NoSyn');
    5.71 -  val const_finite = (dname^"_finite",dtype-->HOLogic.boolT                ,NoSyn');
    5.72 +  val const_take   = (dname^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    5.73 +  val const_finite = (dname^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    5.74  
    5.75  (* ----- case translation --------------------------------------------------------- *)
    5.76  
    5.77  local open Syntax in
    5.78    val case_trans = let 
    5.79 -        fun c_ast con syn = Constant (ThyOps.const_name con syn);
    5.80 -        fun expvar n      = Variable ("e"^(string_of_int n));
    5.81 -        fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    5.82 -        fun app s (l,r)   = mk_appl (Constant s) [l,r];
    5.83 -        fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    5.84 -                 [if is_infix syn
    5.85 -                  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    5.86 -                  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    5.87 -                  expvar n];
    5.88 -        fun arg1 n (con,_,args) = if args = [] then expvar n
    5.89 -                                  else mk_appl (Constant "LAM ") 
    5.90 -                 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    5.91 +	fun c_ast con syn = Constant (ThyOps.const_name con syn);
    5.92 +	fun expvar n      = Variable ("e"^(string_of_int n));
    5.93 +	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    5.94 +	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    5.95 +	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    5.96 +		 [if is_infix syn
    5.97 +		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    5.98 +		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    5.99 +		  expvar n];
   5.100 +	fun arg1 n (con,_,args) = if args = [] then expvar n 
   5.101 +				  else mk_appl (Constant "LAM ") 
   5.102 +		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
   5.103    in mk_appl (Constant "@case") [Variable "x", foldr'
   5.104 -                                 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
   5.105 -                                 (mapn case1 1 cons')] <->
   5.106 +				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
   5.107 +				 (mapn case1 1 cons')] <->
   5.108       mk_appl (Constant "@fapp") [foldl 
   5.109 -                                 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
   5.110 -                                 (Constant (dname^"_when"),mapn arg1 1 cons'),
   5.111 -                                 Variable "x"]
   5.112 +				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
   5.113 +				 (Constant (dname^"_when"),mapn arg1 1 cons'),
   5.114 +				 Variable "x"]
   5.115    end;
   5.116  end;
   5.117  
   5.118 @@ -103,11 +101,10 @@
   5.119  in (* local *)
   5.120  
   5.121  fun add_syntax (comp_dname,eqs': ((string * typ list) *
   5.122 -                (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   5.123 +		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   5.124  let
   5.125    fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
   5.126    fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
   5.127 -  (**                 (fn TFree(_,sort) => sort | _ => Imposs "syntax:thy_arities")**)
   5.128    val thy_types   = map (thy_type  o fst) eqs';
   5.129    val thy_arities = map (thy_arity o fst) eqs';
   5.130    val dtypes      = map (Type      o fst) eqs';
   5.131 @@ -118,10 +115,10 @@
   5.132    val ctt           = map (calc_syntax funprod) eqs';
   5.133    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
   5.134  in thy'' |> add_types      thy_types
   5.135 -         |> add_arities    thy_arities
   5.136 -         |> add_cur_ops_i (flat(map fst ctt))
   5.137 -         |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   5.138 -         |> add_trrules_i (flat(map snd ctt))
   5.139 +	 |> add_arities    thy_arities
   5.140 +	 |> add_cur_ops_i (flat(map fst ctt))
   5.141 +	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   5.142 +	 |> add_trrules_i (flat(map snd ctt))
   5.143  end; (* let *)
   5.144  
   5.145  end; (* local *)
     6.1 --- a/src/HOLCF/domain/theorems.ML	Wed Apr 03 19:02:04 1996 +0200
     6.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Apr 03 19:27:14 1996 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4  (* theorems.ML
     6.5 -   ID:         $Id$
     6.6     Author : David von Oheimb
     6.7     Created: 06-Jun-95
     6.8     Updated: 08-Jun-95 first proof from cterms
     6.9 @@ -12,10 +11,12 @@
    6.10     Updated: 05-Sep-95 simultaneous domain equations (main part)
    6.11     Updated: 11-Sep-95 simultaneous domain equations (coding finished)
    6.12     Updated: 13-Sep-95 simultaneous domain equations (debugging)
    6.13 -   Copyright 1995 TU Muenchen
    6.14 +   Updated: 26-Oct-95 debugging and enhancement of proofs for take_apps, ind
    6.15 +   Updated: 16-Feb-96 bug concerning  domain Triv = triv  fixed
    6.16 +   Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
    6.17 +   Copyright 1995, 1996 TU Muenchen
    6.18  *)
    6.19  
    6.20 -
    6.21  structure Domain_Theorems = struct
    6.22  
    6.23  local
    6.24 @@ -25,58 +26,58 @@
    6.25  infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
    6.26  infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
    6.27  
    6.28 -(* ----- general proof facilities ------------------------------------------------- *)
    6.29 -
    6.30 -fun inferT sg pre_tm = #2(Sign.infer_types sg (K None)(K None)[]true([pre_tm],propT));
    6.31 +(* ----- general proof facilities ------------------------------------------- *)
    6.32  
    6.33 -(*
    6.34 -infix 0 y;
    6.35 -val b=0;
    6.36 -fun _ y t = by t;
    6.37 -fun  g  defs t = let val sg = sign_of thy;
    6.38 -                     val ct = Thm.cterm_of sg (inferT sg t);
    6.39 -                 in goalw_cterm defs ct end;
    6.40 -*)
    6.41 +fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true 
    6.42 +			   ([pre_tm],propT));
    6.43  
    6.44  fun pg'' thy defs t = let val sg = sign_of thy;
    6.45 -                          val ct = Thm.cterm_of sg (inferT sg t);
    6.46 -                      in prove_goalw_cterm defs ct end;
    6.47 +		          val ct = Thm.cterm_of sg (inferT sg t);
    6.48 +		      in prove_goalw_cterm defs ct end;
    6.49  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
    6.50 -                                            | prems=> (cut_facts_tac prems 1)::tacsf);
    6.51 +				| prems=> (cut_facts_tac prems 1)::tacsf);
    6.52  
    6.53  fun REPEAT_DETERM_UNTIL p tac = 
    6.54  let fun drep st = if p st then Sequence.single st
    6.55 -                          else (case Sequence.pull(tac st) of
    6.56 -                                  None        => Sequence.null
    6.57 -                                | Some(st',_) => drep st')
    6.58 -in drep end;
    6.59 +			  else (case Sequence.pull(tapply(tac,st)) of
    6.60 +		                  None        => Sequence.null
    6.61 +				| Some(st',_) => drep st')
    6.62 +in Tactic drep end;
    6.63  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
    6.64  
    6.65 -local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in
    6.66 +local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in
    6.67  val kill_neq_tac = dtac trueI2 end;
    6.68 -fun case_UU_tac rews i v =      res_inst_tac [("Q",v^"=UU")] classical2 i THEN
    6.69 -                                asm_simp_tac (HOLCF_ss addsimps rews) i;
    6.70 +fun case_UU_tac rews i v =	res_inst_tac [("Q",v^"=UU")] classical2 i THEN
    6.71 +				asm_simp_tac (HOLCF_ss addsimps rews) i;
    6.72  
    6.73  val chain_tac = REPEAT_DETERM o resolve_tac 
    6.74 -                [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
    6.75 +		[is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
    6.76 +
    6.77 +(* ----- general proofs ----------------------------------------------------- *)
    6.78  
    6.79 -(* ----- general proofs ----------------------------------------------------------- *)
    6.80 +val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
    6.81 +		fast_tac HOL_cs 1]))["(x. P x  Q)=((x. P x)  Q)",
    6.82 +			    	     "(x. P  Q x) = (P  (x. Q x))"]);
    6.83 +
    6.84 +val all2E = prove_goal HOL.thy " x y . P x y; P x y  R   R" (fn prems =>[
    6.85 +				resolve_tac prems 1,
    6.86 +				cut_facts_tac prems 1,
    6.87 +				fast_tac HOL_cs 1]);
    6.88  
    6.89  val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [
    6.90                                  cut_facts_tac prems 1,
    6.91                                  etac swap 1,
    6.92                                  dtac notnotD 1,
    6.93 -                                etac (hd prems) 1]);
    6.94 +				etac (hd prems) 1]);
    6.95  
    6.96 -val dist_eqI = prove_goal Porder0.thy "~ x << y ==> x ~= y" (fn prems => [
    6.97 -                                cut_facts_tac prems 1,
    6.98 -                                etac swap 1,
    6.99 -                                dtac notnotD 1,
   6.100 -                                asm_simp_tac HOLCF_ss 1]);
   6.101 -val cfst_strict  = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
   6.102 -                                (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   6.103 -val csnd_strict  = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
   6.104 -                        (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   6.105 +val dist_eqI = prove_goal Porder.thy " x  y  x  y" (fn prems => [
   6.106 +                                rtac swap3 1,
   6.107 +				etac (antisym_less_inverse RS conjunct1) 1,
   6.108 +				resolve_tac prems 1]);
   6.109 +val cfst_strict  = prove_goal Cprod3.thy "cfst` = " (fn _ => [
   6.110 +			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   6.111 +val csnd_strict  = prove_goal Cprod3.thy "csnd` = " (fn _ => [
   6.112 +			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   6.113  
   6.114  in
   6.115  
   6.116 @@ -86,8 +87,17 @@
   6.117  
   6.118  val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
   6.119  val pg = pg' thy;
   6.120 +(*
   6.121 +infixr 0 y;
   6.122 +val b = 0;
   6.123 +fun _ y t = by t;
   6.124 +fun  g  defs t = let val sg = sign_of thy;
   6.125 +		     val ct = Thm.cterm_of sg (inferT sg t);
   6.126 +		 in goalw_cterm defs ct end;
   6.127 +*)
   6.128  
   6.129 -(* ----- getting the axioms and definitions --------------------------------------- *)
   6.130 +
   6.131 +(* ----- getting the axioms and definitions --------------------------------- *)
   6.132  
   6.133  local val ga = get_axiom thy in
   6.134  val ax_abs_iso    = ga (dname^"_abs_iso"   );
   6.135 @@ -96,11 +106,11 @@
   6.136  val axs_con_def   = map (fn (con,_) => ga (extern_name con ^"_def")) cons;
   6.137  val axs_dis_def   = map (fn (con,_) => ga (   dis_name con ^"_def")) cons;
   6.138  val axs_sel_def   = flat(map (fn (_,args) => 
   6.139 -                    map (fn     arg => ga (sel_of arg      ^"_def")) args) cons);
   6.140 +		    map (fn     arg => ga (sel_of arg      ^"_def")) args)cons);
   6.141  val ax_copy_def   = ga (dname^"_copy_def"  );
   6.142  end; (* local *)
   6.143  
   6.144 -(* ----- theorems concerning the isomorphism -------------------------------------- *)
   6.145 +(* ----- theorems concerning the isomorphism -------------------------------- *)
   6.146  
   6.147  val dc_abs  = %%(dname^"_abs");
   6.148  val dc_rep  = %%(dname^"_rep");
   6.149 @@ -108,251 +118,243 @@
   6.150  val x_name = "x";
   6.151  
   6.152  val (rep_strict, abs_strict) = let 
   6.153 -               val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
   6.154 -               in (r RS conjunct1, r RS conjunct2) end;
   6.155 +	 val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
   6.156 +	       in (r RS conjunct1, r RS conjunct2) end;
   6.157  val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [
   6.158 -                                res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
   6.159 -                                etac ssubst 1,
   6.160 -                                rtac rep_strict 1];
   6.161 +			   res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
   6.162 +				etac ssubst 1, rtac rep_strict 1];
   6.163  val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [
   6.164 -                                res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
   6.165 -                                etac ssubst 1,
   6.166 -                                rtac abs_strict 1];
   6.167 +			   res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
   6.168 +				etac ssubst 1, rtac abs_strict 1];
   6.169  val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
   6.170  
   6.171  local 
   6.172  val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [
   6.173 -                                dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
   6.174 -                                etac (ax_rep_iso RS subst) 1];
   6.175 +			    dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
   6.176 +			    etac (ax_rep_iso RS subst) 1];
   6.177  fun exh foldr1 cn quant foldr2 var = let
   6.178    fun one_con (con,args) = let val vns = map vname args in
   6.179      foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns)::
   6.180 -                              map (defined o (var vns)) (nonlazy args))) end
   6.181 +			      map (defined o (var vns)) (nonlazy args))) end
   6.182    in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
   6.183  in
   6.184  val cases = let 
   6.185 -            fun common_tac thm = rtac thm 1 THEN contr_tac 1;
   6.186 -            fun unit_tac true = common_tac liftE1
   6.187 -            |   unit_tac _    = all_tac;
   6.188 -            fun prod_tac []          = common_tac oneE
   6.189 -            |   prod_tac [arg]       = unit_tac (is_lazy arg)
   6.190 -            |   prod_tac (arg::args) = 
   6.191 -                                common_tac sprodE THEN
   6.192 -                                kill_neq_tac 1 THEN
   6.193 -                                unit_tac (is_lazy arg) THEN
   6.194 -                                prod_tac args;
   6.195 -            fun sum_one_tac p = SELECT_GOAL(EVERY[
   6.196 -                                rtac p 1,
   6.197 -                                rewrite_goals_tac axs_con_def,
   6.198 -                                dtac iso_swap 1,
   6.199 -                                simp_tac HOLCF_ss 1,
   6.200 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
   6.201 -            fun sum_tac [(_,args)]       [p]        = 
   6.202 -                                prod_tac args THEN sum_one_tac p
   6.203 -            |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
   6.204 -                                common_tac ssumE THEN
   6.205 -                                kill_neq_tac 1 THEN kill_neq_tac 2 THEN
   6.206 -                                prod_tac args THEN sum_one_tac p) THEN
   6.207 -                                sum_tac cons' prems
   6.208 -            |   sum_tac _ _ = Imposs "theorems:sum_tac";
   6.209 -          in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
   6.210 -                              (fn T => T ==> %"P") mk_All
   6.211 -                              (fn l => foldr (op ===>) (map mk_trp l,mk_trp(%"P")))
   6.212 -                              bound_arg)
   6.213 -                             (fn prems => [
   6.214 -                                cut_facts_tac [excluded_middle] 1,
   6.215 -                                etac disjE 1,
   6.216 -                                rtac (hd prems) 2,
   6.217 -                                etac rep_defin' 2,
   6.218 -                                if is_one_con_one_arg (not o is_lazy) cons
   6.219 -                                then rtac (hd (tl prems)) 1 THEN atac 2 THEN
   6.220 -                                     rewrite_goals_tac axs_con_def THEN
   6.221 -                                     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
   6.222 -                                else sum_tac cons (tl prems)])end;
   6.223 -val exhaust = pg [] (mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %))) [
   6.224 -                                rtac cases 1,
   6.225 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)];
   6.226 +	    fun common_tac thm = rtac thm 1 THEN contr_tac 1;
   6.227 +	    fun unit_tac true = common_tac liftE1
   6.228 +	    |   unit_tac _    = all_tac;
   6.229 +	    fun prod_tac []          = common_tac oneE
   6.230 +	    |   prod_tac [arg]       = unit_tac (is_lazy arg)
   6.231 +	    |   prod_tac (arg::args) = 
   6.232 +				common_tac sprodE THEN
   6.233 +				kill_neq_tac 1 THEN
   6.234 +				unit_tac (is_lazy arg) THEN
   6.235 +				prod_tac args;
   6.236 +	    fun sum_rest_tac p = SELECT_GOAL(EVERY[
   6.237 +				rtac p 1,
   6.238 +				rewrite_goals_tac axs_con_def,
   6.239 +				dtac iso_swap 1,
   6.240 +				simp_tac HOLCF_ss 1,
   6.241 +				UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
   6.242 +	    fun sum_tac [(_,args)]       [p]        = 
   6.243 +				prod_tac args THEN sum_rest_tac p
   6.244 +	    |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
   6.245 +				common_tac ssumE THEN
   6.246 +				kill_neq_tac 1 THEN kill_neq_tac 2 THEN
   6.247 +				prod_tac args THEN sum_rest_tac p) THEN
   6.248 +				sum_tac cons' prems
   6.249 +	    |   sum_tac _ _ = Imposs "theorems:sum_tac";
   6.250 +	  in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
   6.251 +			      (fn T => T ==> %"P") mk_All
   6.252 +			      (fn l => foldr (op ===>) (map mk_trp l,
   6.253 +							    mk_trp(%"P")))
   6.254 +			      bound_arg)
   6.255 +			     (fn prems => [
   6.256 +				cut_facts_tac [excluded_middle] 1,
   6.257 +				etac disjE 1,
   6.258 +				rtac (hd prems) 2,
   6.259 +				etac rep_defin' 2,
   6.260 +				if length cons = 1 andalso 
   6.261 +				   length (snd(hd cons)) = 1 andalso 
   6.262 +				   not(is_lazy(hd(snd(hd cons))))
   6.263 +				then rtac (hd (tl prems)) 1 THEN atac 2 THEN
   6.264 +				     rewrite_goals_tac axs_con_def THEN
   6.265 +				     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
   6.266 +				else sum_tac cons (tl prems)])end;
   6.267 +val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
   6.268 +				rtac cases 1,
   6.269 +				UNTIL_SOLVED(fast_tac HOL_cs 1)];
   6.270  end;
   6.271  
   6.272  local 
   6.273 -val when_app = foldl (op `) (%%(dname^"_when"), map % (when_funs cons));
   6.274 -val when_appl = pg [ax_when_def] (mk_trp(when_app`%x_name===when_body cons 
   6.275 -                (fn (_,n) => %(nth_elem(n-1,when_funs cons)))`(dc_rep`%x_name))) [
   6.276 -                                simp_tac HOLCF_ss 1];
   6.277 +  val when_app  = foldl (op `) (%%(dname^"_when"), map % (when_funs cons));
   6.278 +  val when_appl = pg [ax_when_def] (mk_trp(when_app`%x_name===when_body cons 
   6.279 +		(fn (_,n)=> %(nth_elem(n-1,when_funs cons)))`(dc_rep`%x_name)))[
   6.280 +				simp_tac HOLCF_ss 1];
   6.281  in
   6.282 -val when_strict = pg [] ((if is_one_con_one_arg (K true) cons 
   6.283 -        then fn t => mk_trp(strict(%"f")) ===> t else Id)(mk_trp(strict when_app))) [
   6.284 -                                simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
   6.285 -val when_apps = let fun one_when n (con,args) = pg axs_con_def
   6.286 -                (lift_defined % (nonlazy args, mk_trp(when_app`(con_app con args) ===
   6.287 -                 mk_cfapp(%(nth_elem(n,when_funs cons)),map %# args))))[
   6.288 -                        asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
   6.289 -                in mapn one_when 0 cons end;
   6.290 +val when_strict = pg [] (mk_trp(strict when_app)) [
   6.291 +			simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
   6.292 +val when_apps = let fun one_when n (con,args) = pg axs_con_def (lift_defined % 
   6.293 +   (nonlazy args, mk_trp(when_app`(con_app con args) ===
   6.294 +	 mk_cfapp(%(nth_elem(n,when_funs cons)),map %# args))))[
   6.295 +		asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
   6.296 +	in mapn one_when 0 cons end;
   6.297  end;
   6.298  val when_rews = when_strict::when_apps;
   6.299  
   6.300 -(* ----- theorems concerning the constructors, discriminators and selectors ------- *)
   6.301 +(* ----- theorems concerning the constructors, discriminators and selectors - *)
   6.302  
   6.303 -val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
   6.304 -                        (if is_one_con_one_arg (K true) cons then mk_not else Id)
   6.305 -                         (strict(%%(dis_name con))))) [
   6.306 -                simp_tac (HOLCF_ss addsimps (if is_one_con_one_arg (K true) cons 
   6.307 -                                        then [ax_when_def] else when_rews)) 1]) cons;
   6.308 -val dis_apps = let fun one_dis c (con,args)= pg (axs_dis_def)
   6.309 -                   (lift_defined % (nonlazy args, (*(if is_one_con_one_arg is_lazy cons
   6.310 -                        then curry (lift_defined %#) args else Id)
   6.311 -#################*)
   6.312 -                        (mk_trp((%%(dis_name c))`(con_app con args) ===
   6.313 -                              %%(if con=c then "TT" else "FF"))))) [
   6.314 -                                asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   6.315 -        in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
   6.316 -val dis_defins = map (fn (con,args) => pg [] (defined(%x_name)==> 
   6.317 -                      defined(%%(dis_name con)`%x_name)) [
   6.318 -                                rtac cases 1,
   6.319 -                                contr_tac 1,
   6.320 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
   6.321 -                                              (HOLCF_ss addsimps dis_apps) 1))]) cons;
   6.322 -val dis_rews = dis_stricts @ dis_defins @ dis_apps;
   6.323 +val dis_rews = let
   6.324 +  val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
   6.325 +		      	     strict(%%(dis_name con)))) [
   6.326 +				simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
   6.327 +  val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
   6.328 +		   (lift_defined % (nonlazy args,
   6.329 +			(mk_trp((%%(dis_name c))`(con_app con args) ===
   6.330 +			      %%(if con=c then "TT" else "FF"))))) [
   6.331 +				asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   6.332 +	in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
   6.333 +  val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==> 
   6.334 +		      defined(%%(dis_name con)`%x_name)) [
   6.335 +				rtac cases 1,
   6.336 +				contr_tac 1,
   6.337 +				UNTIL_SOLVED (CHANGED(asm_simp_tac 
   6.338 +				        (HOLCF_ss addsimps dis_apps) 1))]) cons;
   6.339 +in dis_stricts @ dis_defins @ dis_apps end;
   6.340  
   6.341  val con_stricts = flat(map (fn (con,args) => map (fn vn =>
   6.342 -                        pg (axs_con_def) 
   6.343 -                           (mk_trp(con_app2 con (fn arg => if vname arg = vn 
   6.344 -                                        then UU else %# arg) args === UU))[
   6.345 -                                asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
   6.346 -                        ) (nonlazy args)) cons);
   6.347 +			pg (axs_con_def) 
   6.348 +			   (mk_trp(con_app2 con (fn arg => if vname arg = vn 
   6.349 +					then UU else %# arg) args === UU))[
   6.350 +				asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
   6.351 +			) (nonlazy args)) cons);
   6.352  val con_defins = map (fn (con,args) => pg []
   6.353 -                        (lift_defined % (nonlazy args,
   6.354 -                                mk_trp(defined(con_app con args)))) ([
   6.355 -                                rtac swap3 1] @ (if is_one_con_one_arg (K true) cons 
   6.356 -                                then [
   6.357 -                                  if is_lazy (hd args) then rtac defined_up 2
   6.358 -                                                       else atac 2,
   6.359 -                                  rtac abs_defin' 1,    
   6.360 -                                  asm_full_simp_tac (HOLCF_ss addsimps axs_con_def) 1]
   6.361 -                                else [
   6.362 -                                  eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
   6.363 -                                  asm_simp_tac (HOLCF_ss addsimps dis_rews) 1])))cons;
   6.364 +			(lift_defined % (nonlazy args,
   6.365 +				mk_trp(defined(con_app con args)))) ([
   6.366 +			  rtac swap3 1, 
   6.367 +			  eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
   6.368 +			  asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
   6.369  val con_rews = con_stricts @ con_defins;
   6.370  
   6.371  val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [
   6.372 -                                simp_tac (HOLCF_ss addsimps when_rews) 1];
   6.373 -in flat(map (fn (_,args) => map (fn arg => one_sel (sel_of arg)) args) cons) end;
   6.374 +				simp_tac (HOLCF_ss addsimps when_rews) 1];
   6.375 +in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
   6.376  val sel_apps = let fun one_sel c n sel = map (fn (con,args) => 
   6.377 -                let val nlas = nonlazy args;
   6.378 -                    val vns  = map vname args;
   6.379 -                in pg axs_sel_def (lift_defined %
   6.380 -                   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
   6.381 -   mk_trp((%%sel)`(con_app con args) === (if con=c then %(nth_elem(n,vns)) else UU))))
   6.382 -                            ( (if con=c then [] 
   6.383 -                               else map(case_UU_tac(when_rews@con_stricts)1) nlas)
   6.384 -                             @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
   6.385 -                                         then[case_UU_tac (when_rews @ con_stricts) 1 
   6.386 -                                                          (nth_elem(n,vns))] else [])
   6.387 -                             @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
   6.388 +		let val nlas = nonlazy args;
   6.389 +		    val vns  = map vname args;
   6.390 +		in pg axs_sel_def (lift_defined %
   6.391 +		   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
   6.392 +				mk_trp((%%sel)`(con_app con args) === 
   6.393 +				(if con=c then %(nth_elem(n,vns)) else UU))))
   6.394 +			    ( (if con=c then [] 
   6.395 +		       else map(case_UU_tac(when_rews@con_stricts)1) nlas)
   6.396 +		     @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
   6.397 +				 then[case_UU_tac (when_rews @ con_stricts) 1 
   6.398 +						  (nth_elem(n,vns))] else [])
   6.399 +		     @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
   6.400  in flat(map  (fn (c,args) => 
   6.401 -        flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
   6.402 -val sel_defins = if length cons = 1 then map (fn arg => pg [] (defined(%x_name) ==> 
   6.403 -                        defined(%%(sel_of arg)`%x_name)) [
   6.404 -                                rtac cases 1,
   6.405 -                                contr_tac 1,
   6.406 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
   6.407 -                                              (HOLCF_ss addsimps sel_apps) 1))]) 
   6.408 -                 (filter_out is_lazy (snd(hd cons))) else [];
   6.409 +     flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
   6.410 +val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==> 
   6.411 +			defined(%%(sel_of arg)`%x_name)) [
   6.412 +				rtac cases 1,
   6.413 +				contr_tac 1,
   6.414 +				UNTIL_SOLVED (CHANGED(asm_simp_tac 
   6.415 +				             (HOLCF_ss addsimps sel_apps) 1))]) 
   6.416 +		 (filter_out is_lazy (snd(hd cons))) else [];
   6.417  val sel_rews = sel_stricts @ sel_defins @ sel_apps;
   6.418  
   6.419  val distincts_le = let
   6.420      fun dist (con1, args1) (con2, args2) = pg []
   6.421 -              (lift_defined % ((nonlazy args1),
   6.422 -                             (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
   6.423 -                        rtac swap3 1,
   6.424 -                        eres_inst_tac [("fo5",dis_name con1)] monofun_cfun_arg 1]
   6.425 -                      @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
   6.426 -                      @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
   6.427 +	      (lift_defined % ((nonlazy args1),
   6.428 +			(mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
   6.429 +			rtac swap3 1,
   6.430 +			eres_inst_tac[("fo5",dis_name con1)] monofun_cfun_arg 1]
   6.431 +		      @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
   6.432 +		      @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
   6.433      fun distinct (con1,args1) (con2,args2) =
   6.434 -        let val arg1 = (con1, args1);
   6.435 -            val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
   6.436 -                              (args2~~variantlist(map vname args2,map vname args1))));
   6.437 -        in [dist arg1 arg2, dist arg2 arg1] end;
   6.438 +	let val arg1 = (con1, args1);
   6.439 +	    val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
   6.440 +			(args2~~variantlist(map vname args2,map vname args1))));
   6.441 +	in [dist arg1 arg2, dist arg2 arg1] end;
   6.442      fun distincts []      = []
   6.443      |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
   6.444  in distincts cons end;
   6.445  val dists_le = flat (flat distincts_le);
   6.446  val dists_eq = let
   6.447      fun distinct (_,args1) ((_,args2),leqs) = let
   6.448 -        val (le1,le2) = (hd leqs, hd(tl leqs));
   6.449 -        val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
   6.450 -        if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
   6.451 -        if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
   6.452 -                                        [eq1, eq2] end;
   6.453 +	val (le1,le2) = (hd leqs, hd(tl leqs));
   6.454 +	val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
   6.455 +	if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
   6.456 +	if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
   6.457 +					[eq1, eq2] end;
   6.458      fun distincts []      = []
   6.459      |   distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @
   6.460 -                                   distincts cs;
   6.461 +				   distincts cs;
   6.462      in distincts (cons~~distincts_le) end;
   6.463  
   6.464  local 
   6.465    fun pgterm rel con args = let
   6.466 -                fun append s = upd_vname(fn v => v^s);
   6.467 -                val (largs,rargs) = (args, map (append "'") args);
   6.468 -                in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
   6.469 -                      lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
   6.470 -                            mk_trp (foldr' mk_conj 
   6.471 -                                (map rel (map %# largs ~~ map %# rargs)))))) end;
   6.472 +		fun append s = upd_vname(fn v => v^s);
   6.473 +		val (largs,rargs) = (args, map (append "'") args);
   6.474 +		in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
   6.475 +		      lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
   6.476 +			    mk_trp (foldr' mk_conj 
   6.477 +				(map rel (map %# largs ~~ map %# rargs)))))) end;
   6.478    val cons' = filter (fn (_,args) => args<>[]) cons;
   6.479  in
   6.480  val inverts = map (fn (con,args) => 
   6.481 -                pgterm (op <<) con args (flat(map (fn arg => [
   6.482 -                                TRY(rtac conjI 1),
   6.483 -                                dres_inst_tac [("fo5",sel_of arg)] monofun_cfun_arg 1,
   6.484 -                                asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
   6.485 -                                                      ) args))) cons';
   6.486 +		pgterm (op <<) con args (flat(map (fn arg => [
   6.487 +				TRY(rtac conjI 1),
   6.488 +				dres_inst_tac [("fo5",sel_of arg)] monofun_cfun_arg 1,
   6.489 +				asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
   6.490 +			     			      ) args))) cons';
   6.491  val injects = map (fn ((con,args),inv_thm) => 
   6.492 -                           pgterm (op ===) con args [
   6.493 -                                etac (antisym_less_inverse RS conjE) 1,
   6.494 -                                dtac inv_thm 1, REPEAT(atac 1),
   6.495 -                                dtac inv_thm 1, REPEAT(atac 1),
   6.496 -                                TRY(safe_tac HOL_cs),
   6.497 -                                REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
   6.498 -                  (cons'~~inverts);
   6.499 +			   pgterm (op ===) con args [
   6.500 +				etac (antisym_less_inverse RS conjE) 1,
   6.501 +				dtac inv_thm 1, REPEAT(atac 1),
   6.502 +				dtac inv_thm 1, REPEAT(atac 1),
   6.503 +				TRY(safe_tac HOL_cs),
   6.504 +				REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
   6.505 +		  (cons'~~inverts);
   6.506  end;
   6.507  
   6.508 -(* ----- theorems concerning one induction step ----------------------------------- *)
   6.509 +(* ----- theorems concerning one induction step ----------------------------- *)
   6.510  
   6.511 -val copy_strict = pg [ax_copy_def] ((if is_one_con_one_arg (K true) cons then fn t =>
   6.512 -         mk_trp(strict(cproj (%"f") eqs (rec_of (hd(snd(hd cons)))))) ===> t
   6.513 -        else Id) (mk_trp(strict(dc_copy`%"f")))) [
   6.514 -                                asm_simp_tac(HOLCF_ss addsimps [abs_strict,rep_strict,
   6.515 -                                                        cfst_strict,csnd_strict]) 1];
   6.516 -val copy_apps = map (fn (con,args) => pg (ax_copy_def::axs_con_def)
   6.517 -                    (lift_defined %# (filter is_nonlazy_rec args,
   6.518 -                        mk_trp(dc_copy`%"f"`(con_app con args) ===
   6.519 -                           (con_app2 con (app_rec_arg (cproj (%"f") eqs)) args))))
   6.520 -                                 (map (case_UU_tac [ax_abs_iso] 1 o vname)
   6.521 -                                   (filter(fn a=>not(is_rec a orelse is_lazy a))args)@
   6.522 -                                 [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1])
   6.523 -                )cons;
   6.524 -val copy_stricts = map(fn(con,args)=>pg[](mk_trp(dc_copy`UU`(con_app con args) ===UU))
   6.525 -             (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
   6.526 -                         in map (case_UU_tac rews 1) (nonlazy args) @ [
   6.527 -                             asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
   6.528 -                   (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
   6.529 +val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
   6.530 +		   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
   6.531 +						   cfst_strict,csnd_strict]) 1];
   6.532 +val copy_apps = map (fn (con,args) => pg [ax_copy_def]
   6.533 +		    (lift_defined % (nonlazy_rec args,
   6.534 +			mk_trp(dc_copy`%"f"`(con_app con args) ===
   6.535 +		(con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
   6.536 +			(map (case_UU_tac (abs_strict::when_strict::con_stricts)
   6.537 +				 1 o vname)
   6.538 +			 (filter (fn a => not (is_rec a orelse is_lazy a)) args)
   6.539 +			@[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
   6.540 +		          simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
   6.541 +val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
   6.542 +					(con_app con args) ===UU))
   6.543 +     (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
   6.544 +			 in map (case_UU_tac rews 1) (nonlazy args) @ [
   6.545 +			     asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
   6.546 +  		        (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
   6.547  val copy_rews = copy_strict::copy_apps @ copy_stricts;
   6.548  
   6.549  in     (iso_rews, exhaust, cases, when_rews,
   6.550 -        con_rews, sel_rews, dis_rews, dists_eq, dists_le, inverts, injects,
   6.551 -        copy_rews)
   6.552 +	con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
   6.553 +	copy_rews)
   6.554  end; (* let *)
   6.555  
   6.556  
   6.557  fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) =
   6.558  let
   6.559  
   6.560 -val dummy = writeln ("Proving induction properties of domain "^comp_dname^"...");
   6.561 +val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
   6.562  val pg = pg' thy;
   6.563  
   6.564  val dnames = map (fst o fst) eqs;
   6.565  val conss  = map  snd        eqs;
   6.566  
   6.567 -(* ----- getting the composite axiom and definitions ------------------------------ *)
   6.568 +(* ----- getting the composite axiom and definitions ------------------------ *)
   6.569  
   6.570  local val ga = get_axiom thy in
   6.571  val axs_reach      = map (fn dn => ga (dn ^  "_reach"   )) dnames;
   6.572 @@ -362,230 +364,235 @@
   6.573  val ax_bisim_def   = ga (comp_dname^"_bisim_def");
   6.574  end; (* local *)
   6.575  
   6.576 -(* ----- theorems concerning finiteness and induction ----------------------------- *)
   6.577 -
   6.578  fun dc_take dn = %%(dn^"_take");
   6.579  val x_name = idx_name dnames "x"; 
   6.580  val P_name = idx_name dnames "P";
   6.581 +val n_eqs = length eqs;
   6.582 +
   6.583 +(* ----- theorems concerning finite approximation and finite induction ------ *)
   6.584  
   6.585  local
   6.586 -  val iterate_ss = simpset_of "Fix";    
   6.587 -  val iterate_Cprod_strict_ss = iterate_ss addsimps [cfst_strict, csnd_strict];
   6.588 -  val iterate_Cprod_ss = iterate_ss addsimps [cfst2,csnd2,csplit2];
   6.589 +  val iterate_Cprod_ss = simpset_of "Fix"
   6.590 +			 addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
   6.591    val copy_con_rews  = copy_rews @ con_rews;
   6.592 -  val copy_take_defs = (if length dnames=1 then [] else [ax_copy2_def]) @axs_take_def;
   6.593 -  val take_stricts = pg copy_take_defs (mk_trp(foldr' mk_conj (map (fn ((dn,args),_)=>
   6.594 -                  (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
   6.595 -                                nat_ind_tac "n" 1,
   6.596 -                                simp_tac iterate_ss 1,
   6.597 -                                simp_tac iterate_Cprod_strict_ss 1,
   6.598 -                                asm_simp_tac iterate_Cprod_ss 1,
   6.599 -                                TRY(safe_tac HOL_cs)] @
   6.600 -                        map(K(asm_simp_tac (HOL_ss addsimps copy_rews)1))dnames);
   6.601 +  val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   6.602 +  val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
   6.603 +	    (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
   6.604 +			nat_ind_tac "n" 1,
   6.605 +			simp_tac iterate_Cprod_ss 1,
   6.606 +			asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
   6.607    val take_stricts' = rewrite_rule copy_take_defs take_stricts;
   6.608 -  val take_0s = mapn (fn n => fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
   6.609 -                                                                `%x_name n === UU))[
   6.610 -                                simp_tac iterate_Cprod_strict_ss 1]) 1 dnames;
   6.611 +  val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
   6.612 +							`%x_name n === UU))[
   6.613 +				simp_tac iterate_Cprod_ss 1]) 1 dnames;
   6.614 +  val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
   6.615    val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj 
   6.616 -            (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all 
   6.617 -                (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
   6.618 -                 con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
   6.619 -                              args)) cons) eqs)))) ([
   6.620 -                                nat_ind_tac "n" 1,
   6.621 -                                simp_tac iterate_Cprod_strict_ss 1,
   6.622 -                                simp_tac (HOLCF_ss addsimps copy_con_rews) 1,
   6.623 -                                TRY(safe_tac HOL_cs)] @
   6.624 -                        (flat(map (fn ((dn,_),cons) => map (fn (con,args) => EVERY (
   6.625 -                                asm_full_simp_tac iterate_Cprod_ss 1::
   6.626 -                                map (case_UU_tac (take_stricts'::copy_con_rews) 1)
   6.627 -                                    (nonlazy args) @[
   6.628 -                                asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1])
   6.629 -                        ) cons) eqs)));
   6.630 +	    (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all 
   6.631 +	(map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
   6.632 +  	 con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
   6.633 +			      args)) cons) eqs)))) ([
   6.634 +				simp_tac iterate_Cprod_ss 1,
   6.635 +				nat_ind_tac "n" 1,
   6.636 +			    simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
   6.637 +				asm_full_simp_tac (HOLCF_ss addsimps 
   6.638 +				      (filter (has_fewer_prems 1) copy_rews)) 1,
   6.639 +				TRY(safe_tac HOL_cs)] @
   6.640 +			(flat(map (fn ((dn,_),cons) => map (fn (con,args) => 
   6.641 +				if nonlazy_rec args = [] then all_tac else
   6.642 +				EVERY(map c_UU_tac (nonlazy_rec args)) THEN
   6.643 +				asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
   6.644 +		 					   ) cons) eqs)));
   6.645  in
   6.646  val take_rews = atomize take_stricts @ take_0s @ atomize take_apps;
   6.647  end; (* local *)
   6.648  
   6.649 -val take_lemmas = mapn (fn n => fn(dn,ax_reach) => pg'' thy axs_take_def (mk_All("n",
   6.650 -                mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
   6.651 -                       dc_take dn $ Bound 0 `%(x_name n^"'")))
   6.652 -           ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
   6.653 -                                res_inst_tac[("t",x_name n    )](ax_reach RS subst) 1,
   6.654 -                                res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
   6.655 -                                rtac (fix_def2 RS ssubst) 1,
   6.656 -                                REPEAT(CHANGED(rtac (contlub_cfun_arg RS ssubst) 1
   6.657 -                                               THEN chain_tac 1)),
   6.658 -                                rtac (contlub_cfun_fun RS ssubst) 1,
   6.659 -                                rtac (contlub_cfun_fun RS ssubst) 2,
   6.660 -                                rtac lub_equal 3,
   6.661 -                                chain_tac 1,
   6.662 -                                rtac allI 1,
   6.663 -                                resolve_tac prems 1])) 1 (dnames~~axs_reach);
   6.664 -
   6.665  local
   6.666    fun one_con p (con,args) = foldr mk_All (map vname args,
   6.667 -        lift_defined (bound_arg (map vname args)) (nonlazy args,
   6.668 -        lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
   6.669 -             (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
   6.670 +	lift_defined (bound_arg (map vname args)) (nonlazy args,
   6.671 +	lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
   6.672 +         (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
   6.673    fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===> 
   6.674 -                           foldr (op ===>) (map (one_con p) cons,concl));
   6.675 -  fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x)) 1 conss,
   6.676 -        mk_trp(foldr' mk_conj (mapn (fn n => concf (P_name n,x_name n)) 1 dnames)));
   6.677 +			   foldr (op ===>) (map (one_con p) cons,concl));
   6.678 +  fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
   6.679 +			mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
   6.680    val take_ss = HOL_ss addsimps take_rews;
   6.681 -  fun ind_tacs tacsf thms1 thms2 prems = TRY(safe_tac HOL_cs)::
   6.682 -                                flat (mapn (fn n => fn (thm1,thm2) => 
   6.683 -                                  tacsf (n,prems) (thm1,thm2) @ 
   6.684 -                                  flat (map (fn cons =>
   6.685 -                                    (resolve_tac prems 1 ::
   6.686 -                                     flat (map (fn (_,args) => 
   6.687 -                                       resolve_tac prems 1::
   6.688 -                                       map (K(atac 1)) (nonlazy args) @
   6.689 -                                       map (K(atac 1)) (filter is_rec args))
   6.690 -                                     cons)))
   6.691 -                                   conss))
   6.692 -                                0 (thms1~~thms2));
   6.693 +  fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i)
   6.694 +			       1 dnames);
   6.695 +  fun ind_prems_tac prems = EVERY(flat (map (fn cons => (
   6.696 +				     resolve_tac prems 1 ::
   6.697 +				     flat (map (fn (_,args) => 
   6.698 +				       resolve_tac prems 1 ::
   6.699 +				       map (K(atac 1)) (nonlazy args) @
   6.700 +				       map (K(atac 1)) (filter is_rec args))
   6.701 +				     cons))) conss));
   6.702    local 
   6.703 -    fun all_rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
   6.704 -                  is_rec arg andalso not(rec_of arg mem ns) andalso
   6.705 -                  ((rec_of arg =  n andalso not(lazy_rec orelse is_lazy arg)) orelse 
   6.706 -                    rec_of arg <> n andalso all_rec_to (rec_of arg::ns) 
   6.707 -                      (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
   6.708 -                  ) o snd) cons;
   6.709 -    fun warn (n,cons) = if all_rec_to [] false (n,cons) then (writeln 
   6.710 -                           ("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true)
   6.711 -                        else false;
   6.712 -    fun lazy_rec_to ns lazy_rec (n,cons) = exists (exists (fn arg => 
   6.713 -                  is_rec arg andalso not(rec_of arg mem ns) andalso
   6.714 -                  ((rec_of arg =  n andalso (lazy_rec orelse is_lazy arg)) orelse 
   6.715 -                    rec_of arg <> n andalso lazy_rec_to (rec_of arg::ns)
   6.716 -                     (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
   6.717 -                 ) o snd) cons;
   6.718 -  in val is_emptys = map warn (mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs);
   6.719 -     val is_finite = forall (not o lazy_rec_to [] false) 
   6.720 -                            (mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs)
   6.721 +    (* check whether every/exists constructor of the n-th part of the equation:
   6.722 +       it has a possibly indirectly recursive argument that isn't/is possibly 
   6.723 +       indirectly lazy *)
   6.724 +    fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
   6.725 +	  is_rec arg andalso not(rec_of arg mem ns) andalso
   6.726 +	  ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
   6.727 +	    rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
   6.728 +	      (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
   6.729 +	  ) o snd) cons;
   6.730 +    fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
   6.731 +    fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (writeln 
   6.732 +        ("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
   6.733 +    fun lazy_rec_to ns = rec_to exists Id  lazy_rec_to ns;
   6.734 +
   6.735 +  in val n__eqs     = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
   6.736 +     val is_emptys = map warn n__eqs;
   6.737 +     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
   6.738    end;
   6.739 -in
   6.740 -val finite_ind = pg'' thy [] (ind_term (fn (P,x) => fn dn => 
   6.741 -                          mk_all(x,%P $ (dc_take dn $ %"n" `Bound 0)))) (fn prems=> [
   6.742 -                                nat_ind_tac "n" 1,
   6.743 -                                simp_tac (take_ss addsimps prems) 1,
   6.744 -                                TRY(safe_tac HOL_cs)]
   6.745 -                                @ flat(mapn (fn n => fn (cons,cases) => [
   6.746 -                                 res_inst_tac [("x",x_name n)] cases 1,
   6.747 -                                 asm_simp_tac (take_ss addsimps prems) 1]
   6.748 -                                 @ flat(map (fn (con,args) => 
   6.749 -                                  asm_simp_tac take_ss 1 ::
   6.750 -                                  map (fn arg =>
   6.751 -                                   case_UU_tac (prems@con_rews) 1 (
   6.752 -                                   nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
   6.753 -                                  (filter is_nonlazy_rec args) @ [
   6.754 -                                  resolve_tac prems 1] @
   6.755 -                                  map (K (atac 1))      (nonlazy args) @
   6.756 -                                  map (K (etac spec 1)) (filter is_rec args)) 
   6.757 -                                 cons))
   6.758 -                                1 (conss~~casess)));
   6.759 +in (* local *)
   6.760 +val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$
   6.761 +			     (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
   6.762 +				quant_tac 1,
   6.763 +				simp_tac quant_ss 1,
   6.764 +				nat_ind_tac "n" 1,
   6.765 +				simp_tac (take_ss addsimps prems) 1,
   6.766 +				TRY(safe_tac HOL_cs)]
   6.767 +				@ flat(map (fn (cons,cases) => [
   6.768 +				 res_inst_tac [("x","x")] cases 1,
   6.769 +				 asm_simp_tac (take_ss addsimps prems) 1]
   6.770 +				 @ flat(map (fn (con,args) => 
   6.771 +				  asm_simp_tac take_ss 1 ::
   6.772 +				  map (fn arg =>
   6.773 +				   case_UU_tac (prems@con_rews) 1 (
   6.774 +			   nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
   6.775 +				  (filter is_nonlazy_rec args) @ [
   6.776 +				  resolve_tac prems 1] @
   6.777 +				  map (K (atac 1))      (nonlazy args) @
   6.778 +				  map (K (etac spec 1)) (filter is_rec args)) 
   6.779 +				 cons))
   6.780 +				(conss~~casess)));
   6.781 +
   6.782 +val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
   6.783 +		mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
   6.784 +		       dc_take dn $ Bound 0 `%(x_name n^"'")))
   6.785 +	   ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
   6.786 +			res_inst_tac[("t",x_name n    )](ax_reach RS subst) 1,
   6.787 +			res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
   6.788 +				rtac (fix_def2 RS ssubst) 1,
   6.789 +				REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1
   6.790 +					       THEN chain_tac 1)),
   6.791 +				rtac (contlub_cfun_fun RS ssubst) 1,
   6.792 +				rtac (contlub_cfun_fun RS ssubst) 2,
   6.793 +				rtac lub_equal 3,
   6.794 +				chain_tac 1,
   6.795 +				rtac allI 1,
   6.796 +				resolve_tac prems 1])) 1 (dnames~~axs_reach);
   6.797 +
   6.798 +(* ----- theorems concerning finiteness and induction ----------------------- *)
   6.799  
   6.800  val (finites,ind) = if is_finite then
   6.801 -let 
   6.802 -  fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
   6.803 -  val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> 
   6.804 -        mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
   6.805 -        take_enough dn)) ===> mk_trp(take_enough dn)) [
   6.806 -                                etac disjE 1,
   6.807 -                                etac notE 1,
   6.808 -                                resolve_tac take_lemmas 1,
   6.809 -                                asm_simp_tac take_ss 1,
   6.810 -                                atac 1]) dnames;
   6.811 -  val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn 
   6.812 -        (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
   6.813 -         mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
   6.814 -                 dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
   6.815 -                                rtac allI 1,
   6.816 -                                nat_ind_tac "n" 1,
   6.817 -                                simp_tac take_ss 1,
   6.818 -                                TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
   6.819 -                                flat(mapn (fn n => fn (cons,cases) => [
   6.820 -                                  simp_tac take_ss 1,
   6.821 -                                  rtac allI 1,
   6.822 -                                  res_inst_tac [("x",x_name n)] cases 1,
   6.823 -                                  asm_simp_tac take_ss 1] @ 
   6.824 -                                  flat(map (fn (con,args) => 
   6.825 -                                    asm_simp_tac take_ss 1 ::
   6.826 -                                    flat(map (fn arg => [
   6.827 -                                      eres_inst_tac [("x",vname arg)] all_dupE 1,
   6.828 -                                      etac disjE 1,
   6.829 -                                      asm_simp_tac (HOL_ss addsimps con_rews) 1,
   6.830 -                                      asm_simp_tac take_ss 1])
   6.831 -                                    (filter is_nonlazy_rec args)))
   6.832 -                                  cons))
   6.833 -                                1 (conss~~casess))) handle ERROR => raise ERROR;
   6.834 -  val all_finite=map (fn(dn,l1b)=>pg axs_finite_def (mk_trp(%%(dn^"_finite") $ %"x"))[
   6.835 -                                case_UU_tac take_rews 1 "x",
   6.836 -                                eresolve_tac finite_lemmas1a 1,
   6.837 -                                step_tac HOL_cs 1,
   6.838 -                                step_tac HOL_cs 1,
   6.839 -                                cut_facts_tac [l1b] 1,
   6.840 -                                fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
   6.841 -in
   6.842 -(all_finite,
   6.843 - pg'' thy [] (ind_term (fn (P,x) => fn dn => %P $ %x))
   6.844 -                               (ind_tacs (fn _ => fn (all_fin,finite_ind) => [
   6.845 -                                rtac (rewrite_rule axs_finite_def all_fin RS exE) 1,
   6.846 -                                etac subst 1,
   6.847 -                                rtac finite_ind 1]) all_finite (atomize finite_ind))
   6.848 +  let 
   6.849 +    fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
   6.850 +    val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> 
   6.851 +	mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
   6.852 +	take_enough dn)) ===> mk_trp(take_enough dn)) [
   6.853 +				etac disjE 1,
   6.854 +				etac notE 1,
   6.855 +				resolve_tac take_lemmas 1,
   6.856 +				asm_simp_tac take_ss 1,
   6.857 +				atac 1]) dnames;
   6.858 +    val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn 
   6.859 +	(fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
   6.860 +	 mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
   6.861 +		 dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
   6.862 +				rtac allI 1,
   6.863 +				nat_ind_tac "n" 1,
   6.864 +				simp_tac take_ss 1,
   6.865 +			TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
   6.866 +				flat(mapn (fn n => fn (cons,cases) => [
   6.867 +				  simp_tac take_ss 1,
   6.868 +				  rtac allI 1,
   6.869 +				  res_inst_tac [("x",x_name n)] cases 1,
   6.870 +				  asm_simp_tac take_ss 1] @ 
   6.871 +				  flat(map (fn (con,args) => 
   6.872 +				    asm_simp_tac take_ss 1 ::
   6.873 +				    flat(map (fn vn => [
   6.874 +				      eres_inst_tac [("x",vn)] all_dupE 1,
   6.875 +				      etac disjE 1,
   6.876 +				      asm_simp_tac (HOL_ss addsimps con_rews) 1,
   6.877 +				      asm_simp_tac take_ss 1])
   6.878 +				    (nonlazy_rec args)))
   6.879 +				  cons))
   6.880 +				1 (conss~~casess))) handle ERROR => raise ERROR;
   6.881 +    val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
   6.882 +						%%(dn^"_finite") $ %"x"))[
   6.883 +				case_UU_tac take_rews 1 "x",
   6.884 +				eresolve_tac finite_lemmas1a 1,
   6.885 +				step_tac HOL_cs 1,
   6.886 +				step_tac HOL_cs 1,
   6.887 +				cut_facts_tac [l1b] 1,
   6.888 +			fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
   6.889 +  in
   6.890 +  (finites,
   6.891 +   pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems =>
   6.892 +				TRY(safe_tac HOL_cs) ::
   6.893 +			 flat (map (fn (finite,fin_ind) => [
   6.894 +			       rtac(rewrite_rule axs_finite_def finite RS exE)1,
   6.895 +				etac subst 1,
   6.896 +				rtac fin_ind 1,
   6.897 +				ind_prems_tac prems]) 
   6.898 +			           (finites~~(atomize finite_ind)) ))
   6.899  ) end (* let *) else
   6.900 -(mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) 
   6.901 -                    [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
   6.902 - pg'' thy [] (foldr (op ===>) (mapn (fn n =>K(mk_trp(%%"adm" $ %(P_name n))))1
   6.903 -                                       dnames,ind_term (fn(P,x)=>fn dn=> %P $ %x)))
   6.904 -                               (ind_tacs (fn (n,prems) => fn (ax_reach,finite_ind) =>[
   6.905 -                                rtac (ax_reach RS subst) 1,
   6.906 -                                res_inst_tac [("x",x_name n)] spec 1,
   6.907 -                                rtac wfix_ind 1,
   6.908 -                                rtac adm_impl_admw 1,
   6.909 -                                resolve_tac adm_thms 1,
   6.910 -                                rtac adm_subst 1,
   6.911 -                                cont_tacR 1,
   6.912 -                                resolve_tac prems 1,
   6.913 -                                strip_tac 1,
   6.914 -                                rtac(rewrite_rule axs_take_def finite_ind) 1])
   6.915 -                                 axs_reach (atomize finite_ind))
   6.916 +  (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) 
   6.917 +	  	    [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
   6.918 +   pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n))))
   6.919 +	       1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
   6.920 +		   (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) 
   6.921 +				    axs_reach @ [
   6.922 +				quant_tac 1,
   6.923 +				rtac (adm_impl_admw RS wfix_ind) 1,
   6.924 +				REPEAT_DETERM(rtac adm_all2 1),
   6.925 +				REPEAT_DETERM(TRY(rtac adm_conj 1) THEN 
   6.926 +						  rtac adm_subst 1 THEN 
   6.927 +					cont_tacR 1 THEN resolve_tac prems 1),
   6.928 +				strip_tac 1,
   6.929 +				rtac (rewrite_rule axs_take_def finite_ind) 1,
   6.930 +				ind_prems_tac prems])
   6.931  )
   6.932  end; (* local *)
   6.933  
   6.934 +(* ----- theorem concerning coinduction ------------------------------------- *)
   6.935 +
   6.936  local
   6.937    val xs = mapn (fn n => K (x_name n)) 1 dnames;
   6.938 -  fun bnd_arg n i = Bound(2*(length dnames - n)-i-1);
   6.939 +  fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   6.940    val take_ss = HOL_ss addsimps take_rews;
   6.941 -  val sproj   = bin_branchr (fn s => "fst("^s^")") (fn s => "snd("^s^")");
   6.942 -  val coind_lemma = pg [ax_bisim_def] (mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
   6.943 -                foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
   6.944 -                  foldr mk_imp (mapn (fn n => K(proj (%"R") dnames n $ 
   6.945 -                                      bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
   6.946 -                    foldr' mk_conj (mapn (fn n => fn dn => 
   6.947 -                                (dc_take dn $ %"n" `bnd_arg n 0 === 
   6.948 -                                (dc_take dn $ %"n" `bnd_arg n 1))) 0 dnames)))))) ([
   6.949 -                                rtac impI 1,
   6.950 -                                nat_ind_tac "n" 1,
   6.951 -                                simp_tac take_ss 1,
   6.952 -                                safe_tac HOL_cs] @
   6.953 -                                flat(mapn (fn n => fn x => [
   6.954 -                                  etac allE 1, etac allE 1, 
   6.955 -                                  eres_inst_tac [("P1",sproj "R" dnames n^
   6.956 -                                                  " "^x^" "^x^"'")](mp RS disjE) 1,
   6.957 -                                  TRY(safe_tac HOL_cs),
   6.958 -                                  REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
   6.959 -                                0 xs));
   6.960 +  val sproj   = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
   6.961 +  val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
   6.962 +		foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
   6.963 +		  foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ 
   6.964 +				      bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
   6.965 +		    foldr' mk_conj (mapn (fn n => fn dn => 
   6.966 +				(dc_take dn $ %"n" `bnd_arg n 0 === 
   6.967 +				(dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
   6.968 +			     ([ rtac impI 1,
   6.969 +				nat_ind_tac "n" 1,
   6.970 +				simp_tac take_ss 1,
   6.971 +				safe_tac HOL_cs] @
   6.972 +				flat(mapn (fn n => fn x => [
   6.973 +				  rotate_tac (n+1) 1,
   6.974 +				  etac all2E 1,
   6.975 +				  eres_inst_tac [("P1", sproj "R" n_eqs n^
   6.976 +					" "^x^" "^x^"'")](mp RS disjE) 1,
   6.977 +				  TRY(safe_tac HOL_cs),
   6.978 +				  REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
   6.979 +				0 xs));
   6.980  in
   6.981  val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
   6.982 -                foldr (op ===>) (mapn (fn n => fn x => 
   6.983 -                        mk_trp(proj (%"R") dnames n $ %x $ %(x^"'"))) 0 xs,
   6.984 -                        mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
   6.985 -                                TRY(safe_tac HOL_cs)] @
   6.986 -                                flat(map (fn take_lemma => [
   6.987 -                                  rtac take_lemma 1,
   6.988 -                                  cut_facts_tac [coind_lemma] 1,
   6.989 -                                  fast_tac HOL_cs 1])
   6.990 -                                take_lemmas));
   6.991 +		foldr (op ===>) (mapn (fn n => fn x => 
   6.992 +		  mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
   6.993 +		  mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
   6.994 +				TRY(safe_tac HOL_cs)] @
   6.995 +				flat(map (fn take_lemma => [
   6.996 +				  rtac take_lemma 1,
   6.997 +				  cut_facts_tac [coind_lemma] 1,
   6.998 +				  fast_tac HOL_cs 1])
   6.999 +				take_lemmas));
  6.1000  end; (* local *)
  6.1001  
  6.1002