domain package:
authoroheimb
Thu Oct 30 14:19:01 1997 +0100 (1997-10-30)
changeset 404335766855f344
parent 4042 8abc33930ff0
child 4044 fdfef2d484ca
domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/axioms.ML	Thu Oct 30 14:18:14 1997 +0100
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Thu Oct 30 14:19:01 1997 +0100
     1.3 @@ -28,10 +28,10 @@
     1.4    val x_name = idx_name eqs x_name' (n+1);
     1.5    val dnam = Sign.base_name dname;
     1.6  
     1.7 - val ax_abs_iso=(dnam^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
     1.8 - val ax_rep_iso=(dnam^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
     1.9 + val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
    1.10 + val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
    1.11  
    1.12 -  val ax_when_def = (dnam^"_when_def",%%(dname^"_when") == 
    1.13 +  val when_def = ("when_def",%%(dname^"_when") == 
    1.14       foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
    1.15  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
    1.16  
    1.17 @@ -46,23 +46,23 @@
    1.18       |   inj y i j = %%"sinr"`(inj y (i-1) (j-1));
    1.19    in foldr /\# (args, outer (inj (parms args) m n)) end;
    1.20  
    1.21 -  val ax_copy_def = (dnam^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo 
    1.22 +  val copy_def = ("copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo 
    1.23  	foldl (op `) (%%(dname^"_when") , 
    1.24  	              mapn (con_def Id true (length cons)) 0 cons)));
    1.25  
    1.26  (* -- definitions concerning the constructors, discriminators and selectors - *)
    1.27  
    1.28 -  val axs_con_def = mapn (fn n => fn (con,args) => (extern_name con ^"_def",  
    1.29 +  val con_defs = mapn (fn n => fn (con,args) => (extern_name con ^"_def",  
    1.30    %%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons;
    1.31  
    1.32 -  val axs_dis_def = let
    1.33 +  val dis_defs = let
    1.34  	fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
    1.35  		 mk_cfapp(%%(dname^"_when"),map 
    1.36  			(fn (con',args) => (foldr /\#
    1.37  			   (args,if con'=con then %%"TT" else %%"FF"))) cons))
    1.38  	in map ddef cons end;
    1.39  
    1.40 -  val axs_sel_def = let
    1.41 +  val sel_defs = let
    1.42  	fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
    1.43  		 mk_cfapp(%%(dname^"_when"),map 
    1.44  			(fn (con',args) => if con'<>con then %%"UU" else
    1.45 @@ -73,16 +73,18 @@
    1.46  (* ----- axiom and definitions concerning induction ------------------------- *)
    1.47  
    1.48    fun cproj' T = cproj T (length eqs) n;
    1.49 -  val ax_reach = (dnam^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
    1.50 +  val reach_ax = ("reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
    1.51  					`%x_name === %x_name));
    1.52 -  val ax_take_def = (dnam^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
    1.53 +  val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj'
    1.54  		    (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
    1.55 -  val ax_finite_def = (dnam^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
    1.56 +  val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name,
    1.57  	mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    1.58  
    1.59 -in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @
    1.60 -    axs_con_def @ axs_dis_def @ axs_sel_def @
    1.61 -   [ax_reach, ax_take_def, ax_finite_def] 
    1.62 +in (dnam,
    1.63 +    [abs_iso_ax, rep_iso_ax, reach_ax],
    1.64 +    [when_def, copy_def] @
    1.65 +     con_defs @ dis_defs @ sel_defs @
    1.66 +    [take_def, finite_def])
    1.67  end; (* let *)
    1.68  
    1.69  
    1.70 @@ -93,9 +95,9 @@
    1.71    val dnames = map (fst o fst) eqs;
    1.72    val x_name = idx_name dnames "x"; 
    1.73    fun copy_app dname = %%(dname^"_copy")`Bound 0;
    1.74 -  val ax_copy_def =(comp_dnam^"_copy_def" , %%(comp_dname^"_copy") ==
    1.75 +  val copy_def = ("copy_def" , %%(comp_dname^"_copy") ==
    1.76  				    /\"f"(foldr' cpair (map copy_app dnames)));
    1.77 -  val ax_bisim_def=(comp_dnam^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
    1.78 +  val bisim_def = ("bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
    1.79      let
    1.80        fun one_con (con,args) = let
    1.81  	val nonrec_args = filter_out is_rec args;
    1.82 @@ -123,9 +125,17 @@
    1.83           		foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
    1.84  					::map one_con cons))));
    1.85      in foldr' mk_conj (mapn one_comp 0 eqs)end ));
    1.86 -  val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @
    1.87 -		(if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
    1.88 -in thy' |> Theory.add_axioms_i (infer_types thy' thy_axs) end;
    1.89 +  fun add_one (thy,(dnam,axs,dfs)) = thy 
    1.90 +	|> Theory.add_path dnam
    1.91 +	|> PureThy.add_store_axioms_i (infer_types thy' dfs)(*add_store_defs_i*)
    1.92 +	|> PureThy.add_store_axioms_i (infer_types thy' axs)
    1.93 +	|> Theory.add_path "..";
    1.94 +  val thy = foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
    1.95 +in thy |> Theory.add_path comp_dnam  
    1.96 +       |> PureThy.add_store_axioms_i (infer_types thy' 
    1.97 +		(bisim_def::(if length eqs>1 then [copy_def] else [])))
    1.98 +       |> Theory.add_path ".."
    1.99 +end;
   1.100  
   1.101  
   1.102  fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
     2.1 --- a/src/HOLCF/domain/extender.ML	Thu Oct 30 14:18:14 1997 +0100
     2.2 +++ b/src/HOLCF/domain/extender.ML	Thu Oct 30 14:19:01 1997 +0100
     2.3 @@ -77,7 +77,7 @@
     2.4  	fun type_of c = case (Sign.const_type sg' c) of Some t => t
     2.5  				| None => error ("Unknown constructor: "^c);
     2.6  	fun args_result_type (t as (Type(tn,[arg,rest]))) = 
     2.7 -		if tn = "->" orelse tn = "=>"
     2.8 +		if tn = cfun_arrow orelse tn = "=>"
     2.9  		then let val (ts,r) = args_result_type rest in (arg::ts,r) end
    2.10  		else ([],t)
    2.11  	|   args_result_type t = ([],t);
    2.12 @@ -139,9 +139,8 @@
    2.13  	 )) cons') : cons list;
    2.14      val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
    2.15      val thy       = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
    2.16 -    val thmss     = map (Domain_Theorems.theorems thy eqs) eqs;
    2.17 -    val comp_thms = Domain_Theorems.comp_theorems thy (comp_dnam, eqs, thmss);
    2.18 -  in (thy, thmss, comp_thms) end;
    2.19 +  in (foldl (fn (thy0,eq) => Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) 
    2.20 +                          |> Domain_Theorems.comp_theorems (comp_dnam, eqs) end;
    2.21  
    2.22    fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
    2.23     val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
     3.1 --- a/src/HOLCF/domain/interface.ML	Thu Oct 30 14:18:14 1997 +0100
     3.2 +++ b/src/HOLCF/domain/interface.ML	Thu Oct 30 14:19:01 1997 +0100
     3.3 @@ -12,31 +12,34 @@
     3.4  
     3.5  (* --- generation of bindings for axioms and theorems in .thy.ML - *)
     3.6  
     3.7 -  fun gt_ax         name   = "get_axiom thy " ^ quote name;
     3.8 -  fun gen_val dname name   = "val "^name^" = "^ gt_ax (dname^"_"^name)^";";
     3.9 -  fun gen_vall      name l = "val "^name^" = "^ mk_list l^";";
    3.10 -  val rews1 = "iso_rews @ when_rews @\n\
    3.11 - 	      \con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\
    3.12 -	      \copy_rews";
    3.13 +  fun get      dname name   = "get_thm thy " ^ quote (dname^"."^name);
    3.14 +  fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
    3.15 +			(if hd (rev (explode name)) = "s" then "s" else "")^
    3.16 +			" thy " ^ quote (dname^"."^name)^";";
    3.17 +  fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
    3.18 +  val rews = "iso_rews @ when_rews @\n\
    3.19 + 	   \  con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
    3.20 +	   \  copy_rews";
    3.21  
    3.22 -  fun gen_struct thms_str num ((dname,_), cons') = let
    3.23 +  fun gen_struct num ((dname,_), cons') = let
    3.24      val axioms1 = ["abs_iso", "rep_iso", "when_def"];
    3.25  		   (* con_defs , sel_defs, dis_defs *) 
    3.26 -    val axioms2 = ["copy_def"];
    3.27 -    val theorems = 
    3.28 -	"iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
    3.29 -	\dists_le, dists_eq, inverts, injects, copy_rews";
    3.30 +    val axioms2 = ["copy_def", "reach", "take_def", "finite_def"];
    3.31 +    val theorems = ["iso_rews", "exhaust", "casedist", "when_rews", "con_rews", 
    3.32 +		    "sel_rews", "dis_rews", "dist_les", "dist_eqs", "inverts", 
    3.33 +		    "injects", "copy_rews"];
    3.34      in
    3.35        "structure "^dname^" = struct\n"^
    3.36 -      cat_lines(map (gen_val dname) axioms1)^"\n"^
    3.37 -      gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
    3.38 -      gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => 
    3.39 -					     gt_ax(sel^"_def")) args)    cons'))^"\n"^
    3.40 -      gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) 
    3.41 -								          cons')^"\n"^
    3.42 -      cat_lines(map (gen_val dname) axioms2)^"\n"^
    3.43 -      "val ("^ theorems ^") = "^thms_str^";\n" ^
    3.44 -      (if num > 1 then "val rews = " ^rews1 ^";\n" else "")
    3.45 +      cat_lines (map (gen_vals dname) axioms1)^"\n"^
    3.46 +      gen_vall "con_defs"       (map (fn (con,_,_) => 
    3.47 +		get dname (strip_esc con^"_def")) cons')^"\n"^
    3.48 +      gen_vall "sel_defs" (flat (map (fn (_,_,args) => map (fn (_,sel,_) => 
    3.49 +		get dname (sel^"_def")) args)    cons'))^"\n"^
    3.50 +      gen_vall "dis_defs"       (map (fn (con,_,_) => 
    3.51 +		get dname (dis_name_ con^"_def")) cons')^"\n"^
    3.52 +      cat_lines (map (gen_vals dname) axioms2)^"\n"^
    3.53 +      cat_lines (map (gen_vals dname) theorems)^"\n"^
    3.54 +      (if num > 1 then "val rews = " ^rews ^";\n" else "")
    3.55      end;
    3.56  
    3.57    fun mk_domain eqs'' = let
    3.58 @@ -45,10 +48,10 @@
    3.59      val dnames = map fst dtnvs;
    3.60      val comp_dname = implode (separate "_" dnames);
    3.61      val conss' = ListPair.map 
    3.62 -	(fn (dname,cons'') => let fun sel n m = upd_second 
    3.63 -			      (fn None   => dname^"_sel_"^(string_of_int n)^
    3.64 -						      "_"^(string_of_int m)
    3.65 -				| Some s => s)
    3.66 +	(fn (dnam,cons'') => let fun sel n m = upd_second 
    3.67 +			     (fn None   => dnam^"_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  	  in mapn fill_sels 1 cons'' end)
    3.72  	(dnames, map snd eqs'');
    3.73 @@ -61,7 +64,7 @@
    3.74  	  mk_list (map (fn (c,syn,ts)=> "\n"^
    3.75  		    mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
    3.76  		    mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
    3.77 -    in "val (thy, thmss, comp_thms) = thy |> Domain_Extender.add_domain "
    3.78 +    in "val thy = thy |> Domain_Extender.add_domain "
    3.79         ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
    3.80  				   mk_pair (mk_pair (quote n, mk_list vs), 
    3.81  					    mk_conslist cs)) eqs'))
    3.82 @@ -71,35 +74,29 @@
    3.83  (* ----- string for calling (comp_)theorems and producing the structures ---- *)
    3.84  
    3.85      val val_gen_string =  let
    3.86 -      fun plural s = if num > 1 then s^"s" else "["^s^"]";
    3.87        val comp_axioms   = [(* copy, *) "reach", "take_def", "finite_def"
    3.88  			   (*, "bisim_def" *)];
    3.89 -      val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
    3.90 -			   ["take_lemma","finite"]))^", finite_ind, ind, coind";
    3.91 -      fun thms_str n = "hd (funpow "^string_of_int n^" tl thmss)";
    3.92 +      val comp_theorems = ["take_rews", "take_lemmas", "finites", 
    3.93 +			   "finite_ind", "ind", "coind"];
    3.94        fun collect sep name = if num = 1 then name else
    3.95 -			     implode (separate sep (map (fn s => s^"."^name) dnames));
    3.96 +		   implode (separate sep (map (fn s => s^"."^name) dnames));
    3.97      in
    3.98  	implode (separate "end; (* struct *)\n" 
    3.99 -			  (mapn (fn n => gen_struct (thms_str n) num) 0 eqs')) ^
   3.100 -	(if num > 1 then "end; (* struct *)\n\n\
   3.101 -		       \structure "^comp_dname^" = struct\n" else "") ^
   3.102 -	(if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
   3.103 -	implode (map (fn s => gen_vall (plural s)
   3.104 -			      (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n")
   3.105 -		 comp_axioms) ^
   3.106 -	gen_val comp_dname "bisim_def" ^"\n\
   3.107 -        \val ("^ comp_theorems ^") = comp_thms;\n\
   3.108 -	\val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ 
   3.109 +			  (map (gen_struct num) eqs')) ^
   3.110 +	(if num > 1 then "end; (* struct *)\n\
   3.111 +		         \structure "^comp_dname^" = struct\n" ^
   3.112 +			 gen_vals comp_dname "copy_def" ^"\n" ^
   3.113 +			 cat_lines (map (fn name => gen_vall (name^"s")
   3.114 +			 (map (fn dn => dn^"."^name) dnames)) comp_axioms)^"\n"
   3.115 +		    else "") ^
   3.116 +	gen_vals comp_dname "bisim_def" ^"\n"^
   3.117 +        cat_lines (map (gen_vals comp_dname) comp_theorems)^"\n"^
   3.118 +	"val rews = "^(if num>1 then collect" @ " "rews"else rews)^ 
   3.119  		    " @ take_rews;\n\
   3.120        \end; (* struct *)\n"
   3.121      end;
   3.122 -  in ("local\n"^
   3.123 -      thy_ext_string^
   3.124 -      "in\n"^
   3.125 -      "val thy = thy;\n"^
   3.126 +  in (thy_ext_string^
   3.127        val_gen_string^
   3.128 -      "end; (* local *)\n\n"^
   3.129        "val thy = thy",
   3.130        "") end;
   3.131  
   3.132 @@ -113,7 +110,7 @@
   3.133         ^ mk_pair(mk_pair(quote tname, Bool.toString finite),
   3.134  		 mk_pair(mk_list(map quote typs), 
   3.135  			 mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
   3.136 -       "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
   3.137 +       "val "^tname^"_induct = " ^get tname "induct" ^";") end;
   3.138  
   3.139  (* ----- parser for domain declaration equation ----------------------------- *)
   3.140  
   3.141 @@ -140,14 +137,14 @@
   3.142  		    -- ThyOps.opt_cmixfix
   3.143  		    >> (fn ((con,args),syn) => (con,syn,args));
   3.144  in
   3.145 -  val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
   3.146 -			       (enum1 "|" domain_cons))) >> mk_domain;
   3.147 +  val domain_decl = (enum1 "and" (con_typ --$$ "="  -- !! 
   3.148 +				 (enum1 "|" domain_cons))) >> mk_domain;
   3.149    val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
   3.150  		    (enum1 "," (name'   --$$ "by" -- !!
   3.151  			       (enum1 "|" name'))) >> mk_gen_by;
   3.152  
   3.153    val _ = ThySyn.add_syntax
   3.154 -    ["lazy", "by", "finite"]
   3.155 +    ["lazy", "and", "by", "finite"]
   3.156      [("domain", domain_decl), ("generated", gen_by_decl)]
   3.157  
   3.158  end; (* local *)
     4.1 --- a/src/HOLCF/domain/library.ML	Thu Oct 30 14:18:14 1997 +0100
     4.2 +++ b/src/HOLCF/domain/library.ML	Thu Oct 30 14:19:01 1997 +0100
     4.3 @@ -60,8 +60,9 @@
     4.4     forbidding "o", "x..","f..","P.." as names *)
     4.5  (* a number string is added if necessary *)
     4.6  fun mk_var_names types : string list = let
     4.7 +    fun strip ss = drop (find ("'", ss)+1, ss);
     4.8      fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
     4.9 -      | typid (TFree (id,_)   ) = hd (tl (explode (Sign.base_name id)))
    4.10 +      | typid (TFree (id,_)   ) = hd (strip (tl (explode (Sign.base_name id))))
    4.11        | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
    4.12      fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
    4.13      fun index_vnames(vn::vns,occupied) =
    4.14 @@ -110,6 +111,7 @@
    4.15  fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
    4.16  infixr 5 -->;
    4.17  infixr 6 ~>; val op ~> = mk_typ "->";
    4.18 +val cfun_arrow = fst (rep_Type (dummyT ~> dummyT));
    4.19  val NoSyn' = ThyOps.Mixfix NoSyn;
    4.20  
    4.21  (* ----- support for term expressions ----- *)
     5.1 --- a/src/HOLCF/domain/theorems.ML	Thu Oct 30 14:18:14 1997 +0100
     5.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Oct 30 14:19:01 1997 +0100
     5.3 @@ -58,11 +58,7 @@
     5.4  
     5.5  in
     5.6  
     5.7 -
     5.8 -type thms = (thm list * thm * thm * thm list *
     5.9 -	     thm list * thm list * thm list * thm list * thm  list * thm list *
    5.10 -	     thm list * thm list);
    5.11 -fun (theorems thy: eq list -> eq -> thms) eqs ((dname,_),cons)  =
    5.12 +fun theorems (((dname,_),cons) : eq, eqs : eq list) thy =
    5.13  let
    5.14  
    5.15  val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
    5.16 @@ -79,15 +75,16 @@
    5.17  
    5.18  (* ----- getting the axioms and definitions --------------------------------- *)
    5.19  
    5.20 -local val ga = get_axiom thy in
    5.21 -val ax_abs_iso    = ga (dname^"_abs_iso"   );
    5.22 -val ax_rep_iso    = ga (dname^"_rep_iso"   );
    5.23 -val ax_when_def   = ga (dname^"_when_def"  );
    5.24 -val axs_con_def   = map (fn (con,_) => ga (extern_name con ^"_def")) cons;
    5.25 -val axs_dis_def   = map (fn (con,_) => ga (   dis_name con ^"_def")) cons;
    5.26 +local fun ga s dn = get_axiom thy (dn^"."^s) in
    5.27 +val ax_abs_iso    = ga "abs_iso"  dname;
    5.28 +val ax_rep_iso    = ga "rep_iso"  dname;
    5.29 +val ax_when_def   = ga "when_def" dname;
    5.30 +val axs_con_def   = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
    5.31 +val axs_dis_def   = map (fn (con,_) => ga (   dis_name con^"_def") dname) cons;
    5.32  val axs_sel_def   = flat(map (fn (_,args) => 
    5.33 -                    map (fn     arg => ga (sel_of arg      ^"_def")) args)cons);
    5.34 -val ax_copy_def   = ga (dname^"_copy_def"  );
    5.35 +                    map (fn     arg => ga (sel_of arg     ^"_def") dname) args)
    5.36 +									  cons);
    5.37 +val ax_copy_def   = ga "copy_def" dname;
    5.38  end; (* local *)
    5.39  
    5.40  (* ----- theorems concerning the isomorphism -------------------------------- *)
    5.41 @@ -118,7 +115,7 @@
    5.42                                map (defined o (var vns)) (nonlazy args))) end
    5.43    in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
    5.44  in
    5.45 -val cases = let 
    5.46 +val casedist = let 
    5.47              fun common_tac thm = rtac thm 1 THEN contr_tac 1;
    5.48              fun unit_tac true = common_tac upE1
    5.49              |   unit_tac _    = all_tac;
    5.50 @@ -161,7 +158,7 @@
    5.51                                       simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
    5.52                                  else sum_tac cons (tl prems)])end;
    5.53  val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
    5.54 -                                rtac cases 1,
    5.55 +                                rtac casedist 1,
    5.56                                  UNTIL_SOLVED(fast_tac HOL_cs 1)];
    5.57  end;
    5.58  
    5.59 @@ -198,7 +195,7 @@
    5.60          in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
    5.61    val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==> 
    5.62                        defined(%%(dis_name con)`%x_name)) [
    5.63 -                                rtac cases 1,
    5.64 +                                rtac casedist 1,
    5.65                                  contr_tac 1,
    5.66                                  UNTIL_SOLVED (CHANGED(asm_simp_tac 
    5.67                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
    5.68 @@ -238,7 +235,7 @@
    5.69       flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
    5.70  val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==> 
    5.71                          defined(%%(sel_of arg)`%x_name)) [
    5.72 -                                rtac cases 1,
    5.73 +                                rtac casedist 1,
    5.74                                  contr_tac 1,
    5.75                                  UNTIL_SOLVED (CHANGED(asm_simp_tac 
    5.76                                               (HOLCF_ss addsimps sel_apps) 1))]) 
    5.77 @@ -262,8 +259,8 @@
    5.78      fun distincts []      = []
    5.79      |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
    5.80  in distincts cons end;
    5.81 -val dists_le = flat (flat distincts_le);
    5.82 -val dists_eq = let
    5.83 +val dist_les = flat (flat distincts_le);
    5.84 +val dist_eqs = let
    5.85      fun distinct (_,args1) ((_,args2),leqs) = let
    5.86          val (le1,le2) = (hd leqs, hd(tl leqs));
    5.87          val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
    5.88 @@ -324,18 +321,25 @@
    5.89                               asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
    5.90                          (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
    5.91  val copy_rews = copy_strict::copy_apps @ copy_stricts;
    5.92 -
    5.93 -in     (iso_rews, exhaust, cases, when_rews,
    5.94 -        con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
    5.95 -        copy_rews)
    5.96 +in thy |> Theory.add_path (Sign.base_name dname)
    5.97 +       |> PureThy.store_thmss [
    5.98 +		("iso_rews" , iso_rews  ),
    5.99 +		("exhaust"  , [exhaust] ),
   5.100 +		("casedist" , [casedist]),
   5.101 +		("when_rews", when_rews ),
   5.102 +		("con_rews", con_rews),
   5.103 +		("sel_rews", sel_rews),
   5.104 +		("dis_rews", dis_rews),
   5.105 +		("dist_les", dist_les),
   5.106 +		("dist_eqs", dist_eqs),
   5.107 +		("inverts" , inverts ),
   5.108 +		("injects" , injects ),
   5.109 +		("copy_rews", copy_rews)]
   5.110 +       |> Theory.add_path ".."
   5.111  end; (* let *)
   5.112  
   5.113 -
   5.114 -fun comp_theorems thy (comp_dnam, eqs: eq list, thmss: thms list) =
   5.115 +fun comp_theorems (comp_dnam, eqs: eq list) thy =
   5.116  let
   5.117 -val casess    =       map #3  thmss;
   5.118 -val con_rews  = flat (map #5  thmss);
   5.119 -val copy_rews = flat (map #12 thmss);
   5.120  val dnames = map (fst o fst) eqs;
   5.121  val conss  = map  snd        eqs;
   5.122  val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
   5.123 @@ -345,12 +349,19 @@
   5.124  
   5.125  (* ----- getting the composite axiom and definitions ------------------------ *)
   5.126  
   5.127 -local val ga = get_axiom thy in
   5.128 -val axs_reach      = map (fn dn => ga (dn ^  "_reach"   )) dnames;
   5.129 -val axs_take_def   = map (fn dn => ga (dn ^  "_take_def")) dnames;
   5.130 -val axs_finite_def = map (fn dn => ga (dn ^"_finite_def")) dnames;
   5.131 -val ax_copy2_def   = ga (comp_dname^ "_copy_def");
   5.132 -val ax_bisim_def   = ga (comp_dname^"_bisim_def");
   5.133 +local fun ga s dn = get_axiom thy (dn^"."^s) in
   5.134 +val axs_reach      = map (ga "reach"     ) dnames;
   5.135 +val axs_take_def   = map (ga "take_def"  ) dnames;
   5.136 +val axs_finite_def = map (ga "finite_def") dnames;
   5.137 +val ax_copy2_def   =      ga "copy_def"  comp_dnam;
   5.138 +val ax_bisim_def   =      ga "bisim_def" comp_dnam;
   5.139 +end; (* local *)
   5.140 +
   5.141 +local fun gt  s dn = get_thm  thy (dn^"."^s);
   5.142 +      fun gts s dn = get_thms thy (dn^"."^s) in
   5.143 +val cases     =       map (gt  "casedist" ) dnames;
   5.144 +val con_rews  = flat (map (gts "con_rews" ) dnames);
   5.145 +val copy_rews = flat (map (gts "copy_rews") dnames);
   5.146  end; (* local *)
   5.147  
   5.148  fun dc_take dn = %%(dn^"_take");
   5.149 @@ -367,7 +378,6 @@
   5.150    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   5.151    val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
   5.152              strict(dc_take dn $ %"n")) eqs))) ([
   5.153 -			if n_eqs = 1 then all_tac else rewtac ax_copy2_def,
   5.154                          nat_ind_tac "n" 1,
   5.155                           simp_tac iterate_Cprod_ss 1,
   5.156                          asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
   5.157 @@ -455,7 +465,7 @@
   5.158                                    map (K (atac 1))      (nonlazy args) @
   5.159                                    map (K (etac spec 1)) (filter is_rec args)) 
   5.160                                   cons))
   5.161 -                                (conss~~casess)));
   5.162 +                                (conss~~cases)));
   5.163  
   5.164  val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
   5.165                  mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
   5.166 @@ -508,7 +518,7 @@
   5.167                                        asm_simp_tac take_ss 1])
   5.168                                      (nonlazy_rec args)))
   5.169                                    cons))
   5.170 -                                1 (conss~~casess)));
   5.171 +                                1 (conss~~cases)));
   5.172      val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
   5.173                                                  %%(dn^"_finite") $ %"x"))[
   5.174                                  case_UU_tac take_rews 1 "x",
   5.175 @@ -586,8 +596,15 @@
   5.176  end; (* local *)
   5.177  
   5.178  
   5.179 -in (take_rews, take_lemmas, finites, finite_ind, ind, coind)
   5.180 -
   5.181 +in thy |> Theory.add_path comp_dnam
   5.182 +       |> PureThy.store_thmss [
   5.183 +		("take_rews"  , take_rews  ),
   5.184 +		("take_lemmas", take_lemmas),
   5.185 +		("finites"    , finites    ),
   5.186 +		("finite_ind", [finite_ind]),
   5.187 +		("ind"       , [ind       ]),
   5.188 +		("coind"     , [coind     ])]
   5.189 +       |> Theory.add_path ".."
   5.190  end; (* let *)
   5.191  end; (* local *)
   5.192  end; (* struct *)