# HG changeset patch # User oheimb # Date 878217541 -3600 # Node ID 35766855f344cb8b56357331357c7a3b3321bfd7 # Parent 8abc33930ff01adf3bceb583570d147fee58f423 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 diff -r 8abc33930ff0 -r 35766855f344 src/HOLCF/domain/axioms.ML --- 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 diff -r 8abc33930ff0 -r 35766855f344 src/HOLCF/domain/extender.ML --- 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'); diff -r 8abc33930ff0 -r 35766855f344 src/HOLCF/domain/interface.ML --- 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 *) diff -r 8abc33930ff0 -r 35766855f344 src/HOLCF/domain/library.ML --- 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 ----- *) diff -r 8abc33930ff0 -r 35766855f344 src/HOLCF/domain/theorems.ML --- 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 *)