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
--- a/src/HOLCF/domain/axioms.ML Thu Oct 30 14:18:14 1997 +0100
+++ b/src/HOLCF/domain/axioms.ML Thu Oct 30 14:19:01 1997 +0100
@@ -28,10 +28,10 @@
val x_name = idx_name eqs x_name' (n+1);
val dnam = Sign.base_name dname;
- val ax_abs_iso=(dnam^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
- val ax_rep_iso=(dnam^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
+ val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
+ val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
- val ax_when_def = (dnam^"_when_def",%%(dname^"_when") ==
+ val when_def = ("when_def",%%(dname^"_when") ==
foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
@@ -46,23 +46,23 @@
| inj y i j = %%"sinr"`(inj y (i-1) (j-1));
in foldr /\# (args, outer (inj (parms args) m n)) end;
- val ax_copy_def = (dnam^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo
+ val copy_def = ("copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo
foldl (op `) (%%(dname^"_when") ,
mapn (con_def Id true (length cons)) 0 cons)));
(* -- definitions concerning the constructors, discriminators and selectors - *)
- val axs_con_def = mapn (fn n => fn (con,args) => (extern_name con ^"_def",
+ val con_defs = mapn (fn n => fn (con,args) => (extern_name con ^"_def",
%%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons;
- val axs_dis_def = let
+ val dis_defs = let
fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) ==
mk_cfapp(%%(dname^"_when"),map
(fn (con',args) => (foldr /\#
(args,if con'=con then %%"TT" else %%"FF"))) cons))
in map ddef cons end;
- val axs_sel_def = let
+ val sel_defs = let
fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) ==
mk_cfapp(%%(dname^"_when"),map
(fn (con',args) => if con'<>con then %%"UU" else
@@ -73,16 +73,18 @@
(* ----- axiom and definitions concerning induction ------------------------- *)
fun cproj' T = cproj T (length eqs) n;
- val ax_reach = (dnam^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
+ val reach_ax = ("reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
`%x_name === %x_name));
- val ax_take_def = (dnam^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
+ val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj'
(%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
- val ax_finite_def = (dnam^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
+ val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name,
mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
-in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @
- axs_con_def @ axs_dis_def @ axs_sel_def @
- [ax_reach, ax_take_def, ax_finite_def]
+in (dnam,
+ [abs_iso_ax, rep_iso_ax, reach_ax],
+ [when_def, copy_def] @
+ con_defs @ dis_defs @ sel_defs @
+ [take_def, finite_def])
end; (* let *)
@@ -93,9 +95,9 @@
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
fun copy_app dname = %%(dname^"_copy")`Bound 0;
- val ax_copy_def =(comp_dnam^"_copy_def" , %%(comp_dname^"_copy") ==
+ val copy_def = ("copy_def" , %%(comp_dname^"_copy") ==
/\"f"(foldr' cpair (map copy_app dnames)));
- val ax_bisim_def=(comp_dnam^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
+ val bisim_def = ("bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
let
fun one_con (con,args) = let
val nonrec_args = filter_out is_rec args;
@@ -123,9 +125,17 @@
foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
::map one_con cons))));
in foldr' mk_conj (mapn one_comp 0 eqs)end ));
- val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @
- (if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
-in thy' |> Theory.add_axioms_i (infer_types thy' thy_axs) end;
+ fun add_one (thy,(dnam,axs,dfs)) = thy
+ |> Theory.add_path dnam
+ |> PureThy.add_store_axioms_i (infer_types thy' dfs)(*add_store_defs_i*)
+ |> PureThy.add_store_axioms_i (infer_types thy' axs)
+ |> Theory.add_path "..";
+ val thy = foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
+in thy |> Theory.add_path comp_dnam
+ |> PureThy.add_store_axioms_i (infer_types thy'
+ (bisim_def::(if length eqs>1 then [copy_def] else [])))
+ |> Theory.add_path ".."
+end;
fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
--- a/src/HOLCF/domain/extender.ML Thu Oct 30 14:18:14 1997 +0100
+++ b/src/HOLCF/domain/extender.ML Thu Oct 30 14:19:01 1997 +0100
@@ -77,7 +77,7 @@
fun type_of c = case (Sign.const_type sg' c) of Some t => t
| None => error ("Unknown constructor: "^c);
fun args_result_type (t as (Type(tn,[arg,rest]))) =
- if tn = "->" orelse tn = "=>"
+ if tn = cfun_arrow orelse tn = "=>"
then let val (ts,r) = args_result_type rest in (arg::ts,r) end
else ([],t)
| args_result_type t = ([],t);
@@ -139,9 +139,8 @@
)) cons') : cons list;
val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
- val thmss = map (Domain_Theorems.theorems thy eqs) eqs;
- val comp_thms = Domain_Theorems.comp_theorems thy (comp_dnam, eqs, thmss);
- in (thy, thmss, comp_thms) end;
+ in (foldl (fn (thy0,eq) => Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
+ |> Domain_Theorems.comp_theorems (comp_dnam, eqs) end;
fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
--- a/src/HOLCF/domain/interface.ML Thu Oct 30 14:18:14 1997 +0100
+++ b/src/HOLCF/domain/interface.ML Thu Oct 30 14:19:01 1997 +0100
@@ -12,31 +12,34 @@
(* --- generation of bindings for axioms and theorems in .thy.ML - *)
- fun gt_ax name = "get_axiom thy " ^ quote name;
- fun gen_val dname name = "val "^name^" = "^ gt_ax (dname^"_"^name)^";";
- fun gen_vall name l = "val "^name^" = "^ mk_list l^";";
- val rews1 = "iso_rews @ when_rews @\n\
- \con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\
- \copy_rews";
+ fun get dname name = "get_thm thy " ^ quote (dname^"."^name);
+ fun gen_vals dname name = "val "^ name ^ " = get_thm" ^
+ (if hd (rev (explode name)) = "s" then "s" else "")^
+ " thy " ^ quote (dname^"."^name)^";";
+ fun gen_vall name l = "val "^name^" = "^ mk_list l^";";
+ val rews = "iso_rews @ when_rews @\n\
+ \ con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
+ \ copy_rews";
- fun gen_struct thms_str num ((dname,_), cons') = let
+ fun gen_struct num ((dname,_), cons') = let
val axioms1 = ["abs_iso", "rep_iso", "when_def"];
(* con_defs , sel_defs, dis_defs *)
- val axioms2 = ["copy_def"];
- val theorems =
- "iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n \
- \dists_le, dists_eq, inverts, injects, copy_rews";
+ val axioms2 = ["copy_def", "reach", "take_def", "finite_def"];
+ val theorems = ["iso_rews", "exhaust", "casedist", "when_rews", "con_rews",
+ "sel_rews", "dis_rews", "dist_les", "dist_eqs", "inverts",
+ "injects", "copy_rews"];
in
"structure "^dname^" = struct\n"^
- cat_lines(map (gen_val dname) axioms1)^"\n"^
- gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
- gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) =>
- gt_ax(sel^"_def")) args) cons'))^"\n"^
- gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def"))
- cons')^"\n"^
- cat_lines(map (gen_val dname) axioms2)^"\n"^
- "val ("^ theorems ^") = "^thms_str^";\n" ^
- (if num > 1 then "val rews = " ^rews1 ^";\n" else "")
+ cat_lines (map (gen_vals dname) axioms1)^"\n"^
+ gen_vall "con_defs" (map (fn (con,_,_) =>
+ get dname (strip_esc con^"_def")) cons')^"\n"^
+ gen_vall "sel_defs" (flat (map (fn (_,_,args) => map (fn (_,sel,_) =>
+ get dname (sel^"_def")) args) cons'))^"\n"^
+ gen_vall "dis_defs" (map (fn (con,_,_) =>
+ get dname (dis_name_ con^"_def")) cons')^"\n"^
+ cat_lines (map (gen_vals dname) axioms2)^"\n"^
+ cat_lines (map (gen_vals dname) theorems)^"\n"^
+ (if num > 1 then "val rews = " ^rews ^";\n" else "")
end;
fun mk_domain eqs'' = let
@@ -45,10 +48,10 @@
val dnames = map fst dtnvs;
val comp_dname = implode (separate "_" dnames);
val conss' = ListPair.map
- (fn (dname,cons'') => let fun sel n m = upd_second
- (fn None => dname^"_sel_"^(string_of_int n)^
- "_"^(string_of_int m)
- | Some s => s)
+ (fn (dnam,cons'') => let fun sel n m = upd_second
+ (fn None => dnam^"_sel_"^(string_of_int n)^
+ "_"^(string_of_int m)
+ | Some s => s)
fun fill_sels n con = upd_third (mapn (sel n) 1) con;
in mapn fill_sels 1 cons'' end)
(dnames, map snd eqs'');
@@ -61,7 +64,7 @@
mk_list (map (fn (c,syn,ts)=> "\n"^
mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
- in "val (thy, thmss, comp_thms) = thy |> Domain_Extender.add_domain "
+ in "val thy = thy |> Domain_Extender.add_domain "
^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
mk_pair (mk_pair (quote n, mk_list vs),
mk_conslist cs)) eqs'))
@@ -71,35 +74,29 @@
(* ----- string for calling (comp_)theorems and producing the structures ---- *)
val val_gen_string = let
- fun plural s = if num > 1 then s^"s" else "["^s^"]";
val comp_axioms = [(* copy, *) "reach", "take_def", "finite_def"
(*, "bisim_def" *)];
- val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
- ["take_lemma","finite"]))^", finite_ind, ind, coind";
- fun thms_str n = "hd (funpow "^string_of_int n^" tl thmss)";
+ val comp_theorems = ["take_rews", "take_lemmas", "finites",
+ "finite_ind", "ind", "coind"];
fun collect sep name = if num = 1 then name else
- implode (separate sep (map (fn s => s^"."^name) dnames));
+ implode (separate sep (map (fn s => s^"."^name) dnames));
in
implode (separate "end; (* struct *)\n"
- (mapn (fn n => gen_struct (thms_str n) num) 0 eqs')) ^
- (if num > 1 then "end; (* struct *)\n\n\
- \structure "^comp_dname^" = struct\n" else "") ^
- (if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
- implode (map (fn s => gen_vall (plural s)
- (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n")
- comp_axioms) ^
- gen_val comp_dname "bisim_def" ^"\n\
- \val ("^ comp_theorems ^") = comp_thms;\n\
- \val rews = "^(if num>1 then collect" @ " "rews"else rews1)^
+ (map (gen_struct num) eqs')) ^
+ (if num > 1 then "end; (* struct *)\n\
+ \structure "^comp_dname^" = struct\n" ^
+ gen_vals comp_dname "copy_def" ^"\n" ^
+ cat_lines (map (fn name => gen_vall (name^"s")
+ (map (fn dn => dn^"."^name) dnames)) comp_axioms)^"\n"
+ else "") ^
+ gen_vals comp_dname "bisim_def" ^"\n"^
+ cat_lines (map (gen_vals comp_dname) comp_theorems)^"\n"^
+ "val rews = "^(if num>1 then collect" @ " "rews"else rews)^
" @ take_rews;\n\
\end; (* struct *)\n"
end;
- in ("local\n"^
- thy_ext_string^
- "in\n"^
- "val thy = thy;\n"^
+ in (thy_ext_string^
val_gen_string^
- "end; (* local *)\n\n"^
"val thy = thy",
"") end;
@@ -113,7 +110,7 @@
^ mk_pair(mk_pair(quote tname, Bool.toString finite),
mk_pair(mk_list(map quote typs),
mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
- "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
+ "val "^tname^"_induct = " ^get tname "induct" ^";") end;
(* ----- parser for domain declaration equation ----------------------------- *)
@@ -140,14 +137,14 @@
-- ThyOps.opt_cmixfix
>> (fn ((con,args),syn) => (con,syn,args));
in
- val domain_decl = (enum1 "," (con_typ --$$ "=" -- !!
- (enum1 "|" domain_cons))) >> mk_domain;
+ val domain_decl = (enum1 "and" (con_typ --$$ "=" -- !!
+ (enum1 "|" domain_cons))) >> mk_domain;
val gen_by_decl = (optional ($$ "finite" >> K true) false) --
(enum1 "," (name' --$$ "by" -- !!
(enum1 "|" name'))) >> mk_gen_by;
val _ = ThySyn.add_syntax
- ["lazy", "by", "finite"]
+ ["lazy", "and", "by", "finite"]
[("domain", domain_decl), ("generated", gen_by_decl)]
end; (* local *)
--- a/src/HOLCF/domain/library.ML Thu Oct 30 14:18:14 1997 +0100
+++ b/src/HOLCF/domain/library.ML Thu Oct 30 14:19:01 1997 +0100
@@ -60,8 +60,9 @@
forbidding "o", "x..","f..","P.." as names *)
(* a number string is added if necessary *)
fun mk_var_names types : string list = let
+ fun strip ss = drop (find ("'", ss)+1, ss);
fun typid (Type (id,_) ) = hd (explode (Sign.base_name id))
- | typid (TFree (id,_) ) = hd (tl (explode (Sign.base_name id)))
+ | typid (TFree (id,_) ) = hd (strip (tl (explode (Sign.base_name id))))
| typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
fun index_vnames(vn::vns,occupied) =
@@ -110,6 +111,7 @@
fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
infixr 5 -->;
infixr 6 ~>; val op ~> = mk_typ "->";
+val cfun_arrow = fst (rep_Type (dummyT ~> dummyT));
val NoSyn' = ThyOps.Mixfix NoSyn;
(* ----- support for term expressions ----- *)
--- a/src/HOLCF/domain/theorems.ML Thu Oct 30 14:18:14 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Thu Oct 30 14:19:01 1997 +0100
@@ -58,11 +58,7 @@
in
-
-type thms = (thm list * thm * thm * thm list *
- thm list * thm list * thm list * thm list * thm list * thm list *
- thm list * thm list);
-fun (theorems thy: eq list -> eq -> thms) eqs ((dname,_),cons) =
+fun theorems (((dname,_),cons) : eq, eqs : eq list) thy =
let
val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
@@ -79,15 +75,16 @@
(* ----- getting the axioms and definitions --------------------------------- *)
-local val ga = get_axiom thy in
-val ax_abs_iso = ga (dname^"_abs_iso" );
-val ax_rep_iso = ga (dname^"_rep_iso" );
-val ax_when_def = ga (dname^"_when_def" );
-val axs_con_def = map (fn (con,_) => ga (extern_name con ^"_def")) cons;
-val axs_dis_def = map (fn (con,_) => ga ( dis_name con ^"_def")) cons;
+local fun ga s dn = get_axiom thy (dn^"."^s) in
+val ax_abs_iso = ga "abs_iso" dname;
+val ax_rep_iso = ga "rep_iso" dname;
+val ax_when_def = ga "when_def" dname;
+val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
+val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons;
val axs_sel_def = flat(map (fn (_,args) =>
- map (fn arg => ga (sel_of arg ^"_def")) args)cons);
-val ax_copy_def = ga (dname^"_copy_def" );
+ map (fn arg => ga (sel_of arg ^"_def") dname) args)
+ cons);
+val ax_copy_def = ga "copy_def" dname;
end; (* local *)
(* ----- theorems concerning the isomorphism -------------------------------- *)
@@ -118,7 +115,7 @@
map (defined o (var vns)) (nonlazy args))) end
in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
in
-val cases = let
+val casedist = let
fun common_tac thm = rtac thm 1 THEN contr_tac 1;
fun unit_tac true = common_tac upE1
| unit_tac _ = all_tac;
@@ -161,7 +158,7 @@
simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
else sum_tac cons (tl prems)])end;
val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
- rtac cases 1,
+ rtac casedist 1,
UNTIL_SOLVED(fast_tac HOL_cs 1)];
end;
@@ -198,7 +195,7 @@
in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==>
defined(%%(dis_name con)`%x_name)) [
- rtac cases 1,
+ rtac casedist 1,
contr_tac 1,
UNTIL_SOLVED (CHANGED(asm_simp_tac
(HOLCF_ss addsimps dis_apps) 1))]) cons;
@@ -238,7 +235,7 @@
flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==>
defined(%%(sel_of arg)`%x_name)) [
- rtac cases 1,
+ rtac casedist 1,
contr_tac 1,
UNTIL_SOLVED (CHANGED(asm_simp_tac
(HOLCF_ss addsimps sel_apps) 1))])
@@ -262,8 +259,8 @@
fun distincts [] = []
| distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
in distincts cons end;
-val dists_le = flat (flat distincts_le);
-val dists_eq = let
+val dist_les = flat (flat distincts_le);
+val dist_eqs = let
fun distinct (_,args1) ((_,args2),leqs) = let
val (le1,le2) = (hd leqs, hd(tl leqs));
val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
@@ -324,18 +321,25 @@
asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
(filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
val copy_rews = copy_strict::copy_apps @ copy_stricts;
-
-in (iso_rews, exhaust, cases, when_rews,
- con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
- copy_rews)
+in thy |> Theory.add_path (Sign.base_name dname)
+ |> PureThy.store_thmss [
+ ("iso_rews" , iso_rews ),
+ ("exhaust" , [exhaust] ),
+ ("casedist" , [casedist]),
+ ("when_rews", when_rews ),
+ ("con_rews", con_rews),
+ ("sel_rews", sel_rews),
+ ("dis_rews", dis_rews),
+ ("dist_les", dist_les),
+ ("dist_eqs", dist_eqs),
+ ("inverts" , inverts ),
+ ("injects" , injects ),
+ ("copy_rews", copy_rews)]
+ |> Theory.add_path ".."
end; (* let *)
-
-fun comp_theorems thy (comp_dnam, eqs: eq list, thmss: thms list) =
+fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
-val casess = map #3 thmss;
-val con_rews = flat (map #5 thmss);
-val copy_rews = flat (map #12 thmss);
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
@@ -345,12 +349,19 @@
(* ----- getting the composite axiom and definitions ------------------------ *)
-local val ga = get_axiom thy in
-val axs_reach = map (fn dn => ga (dn ^ "_reach" )) dnames;
-val axs_take_def = map (fn dn => ga (dn ^ "_take_def")) dnames;
-val axs_finite_def = map (fn dn => ga (dn ^"_finite_def")) dnames;
-val ax_copy2_def = ga (comp_dname^ "_copy_def");
-val ax_bisim_def = ga (comp_dname^"_bisim_def");
+local fun ga s dn = get_axiom thy (dn^"."^s) in
+val axs_reach = map (ga "reach" ) dnames;
+val axs_take_def = map (ga "take_def" ) dnames;
+val axs_finite_def = map (ga "finite_def") dnames;
+val ax_copy2_def = ga "copy_def" comp_dnam;
+val ax_bisim_def = ga "bisim_def" comp_dnam;
+end; (* local *)
+
+local fun gt s dn = get_thm thy (dn^"."^s);
+ fun gts s dn = get_thms thy (dn^"."^s) in
+val cases = map (gt "casedist" ) dnames;
+val con_rews = flat (map (gts "con_rews" ) dnames);
+val copy_rews = flat (map (gts "copy_rews") dnames);
end; (* local *)
fun dc_take dn = %%(dn^"_take");
@@ -367,7 +378,6 @@
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
strict(dc_take dn $ %"n")) eqs))) ([
- if n_eqs = 1 then all_tac else rewtac ax_copy2_def,
nat_ind_tac "n" 1,
simp_tac iterate_Cprod_ss 1,
asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
@@ -455,7 +465,7 @@
map (K (atac 1)) (nonlazy args) @
map (K (etac spec 1)) (filter is_rec args))
cons))
- (conss~~casess)));
+ (conss~~cases)));
val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
mk_trp(dc_take dn $ Bound 0 `%(x_name n) ===
@@ -508,7 +518,7 @@
asm_simp_tac take_ss 1])
(nonlazy_rec args)))
cons))
- 1 (conss~~casess)));
+ 1 (conss~~cases)));
val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
%%(dn^"_finite") $ %"x"))[
case_UU_tac take_rews 1 "x",
@@ -586,8 +596,15 @@
end; (* local *)
-in (take_rews, take_lemmas, finites, finite_ind, ind, coind)
-
+in thy |> Theory.add_path comp_dnam
+ |> PureThy.store_thmss [
+ ("take_rews" , take_rews ),
+ ("take_lemmas", take_lemmas),
+ ("finites" , finites ),
+ ("finite_ind", [finite_ind]),
+ ("ind" , [ind ]),
+ ("coind" , [coind ])]
+ |> Theory.add_path ".."
end; (* let *)
end; (* local *)
end; (* struct *)