--- a/src/ZF/add_ind_def.ML Fri Oct 17 17:40:33 1997 +0200
+++ b/src/ZF/add_ind_def.ML Fri Oct 17 17:42:39 1997 +0200
@@ -87,8 +87,9 @@
val rec_names = map (#1 o dest_Const) rec_hds
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
- val dummy = assert_all Syntax.is_identifier rec_names
- (fn a => "Name of recursive set not an identifier: " ^ a);
+ val rec_base_names = map NameSpace.base rec_names;
+ val dummy = assert_all Syntax.is_identifier rec_base_names
+ (fn a => "Base name of recursive set not an identifier: " ^ a);
local (*Checking the introduction rules*)
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
@@ -147,7 +148,8 @@
(*A key definition:
If no mutual recursion then it equals the one recursive set.
If mutual recursion then it differs from all the recursive sets. *)
- val big_rec_name = space_implode "_" rec_names;
+ val big_rec_base_name = space_implode "_" rec_base_names;
+ val big_rec_name = Sign.full_name sign big_rec_base_name;
(*Big_rec... is the union of the mutually recursive sets*)
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
@@ -167,30 +169,34 @@
(*Expects the recursive sets to have been defined already.
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
-fun add_constructs_def (rec_names, con_ty_lists) thy =
+fun add_constructs_def (rec_base_names, con_ty_lists) thy =
let
val dummy = (*has essential ancestors?*)
- require_thy thy "Datatype" "(co)datatype definitions"
+ require_thy thy "Datatype" "(co)datatype definitions";
+
+ val sign = sign_of thy;
+ val full_name = Sign.full_name sign;
val dummy = writeln" Defining the constructor functions...";
val case_name = "f"; (*name for case variables*)
+
(** Define the constructors **)
(*The empty tuple is 0*)
fun mk_tuple [] = Const("0",iT)
| mk_tuple args = foldr1 (app Pr.pair) args;
- fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
+ fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
- val npart = length rec_names; (*total # of mutually recursive parts*)
+ val npart = length rec_base_names; (*total # of mutually recursive parts*)
(*Make constructor definition; kpart is # of this mutually recursive part*)
fun mk_con_defs (kpart, con_ty_list) =
let val ncon = length con_ty_list (*number of constructors*)
fun mk_def (((id,T,syn), name, args, prems), kcon) =
(*kcon is index of constructor*)
- mk_defpair (list_comb (Const(name,T), args),
+ mk_defpair (list_comb (Const (full_name name, T), args),
mk_inject npart kpart
(mk_inject ncon kcon (mk_tuple args)))
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
@@ -210,45 +216,49 @@
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
(*Treatment of a single constructor*)
- fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
- if Syntax.is_identifier id
- then (opno,
- (Free(case_name ^ "_" ^ id, T), args) :: cases)
- else (opno+1,
- (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) ::
- cases)
+ fun add_case (((_, T, _), name, args, prems), (opno, cases)) =
+ if Syntax.is_identifier name then
+ (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases)
+ else
+ (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
(*Treatment of a list of constructors, for one part*)
- fun add_case_list (con_ty_list, (opno,case_lists)) =
- let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
- in (opno', case_list :: case_lists) end;
+ fun add_case_list (con_ty_list, (opno, case_lists)) =
+ let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
+ in (opno', case_list :: case_lists) end;
(*Treatment of all parts*)
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
- val big_rec_name = space_implode "_" rec_names;
-
- val big_case_name = big_rec_name ^ "_case";
+ val big_rec_base_name = space_implode "_" rec_base_names;
+ val big_case_base_name = big_rec_base_name ^ "_case";
+ val big_case_name = full_name big_case_base_name;
(*The list of all the function variables*)
val big_case_args = flat (map (map #1) case_lists);
- val big_case_tm =
- list_comb (Const(big_case_name, big_case_typ), big_case_args);
+ val big_case_tm =
+ list_comb (Const (big_case_name, big_case_typ), big_case_args);
- val big_case_def = mk_defpair
- (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
+ val big_case_def = mk_defpair
+ (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
- (** Build the new theory **)
+
+ (* Build the new theory *)
val const_decs =
- (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
+ (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
val axpairs =
- big_case_def :: flat (ListPair.map mk_con_defs
- (1 upto npart, con_ty_lists))
+ big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
- in thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs end;
+ in
+ thy
+ |> Theory.add_consts_i const_decs
+ |> Theory.add_defs_i axpairs
+ end;
+
+
end;
--- a/src/ZF/constructor.ML Fri Oct 17 17:40:33 1997 +0200
+++ b/src/ZF/constructor.ML Fri Oct 17 17:42:39 1997 +0200
@@ -47,9 +47,11 @@
(*Each equation has the form
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) =
- Ind_Syntax.mk_tprop
- (Ind_Syntax.eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
- $ (list_comb (case_free, args))) ;
+ Ind_Syntax.mk_tprop
+ (Ind_Syntax.eq_const $
+ (big_case_tm $
+ (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), args))) $
+ (list_comb (case_free, args)));
val case_trans = hd con_defs RS Ind_Syntax.def_trans
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
--- a/src/ZF/ind_syntax.ML Fri Oct 17 17:40:33 1997 +0200
+++ b/src/ZF/ind_syntax.ML Fri Oct 17 17:42:39 1997 +0200
@@ -90,14 +90,15 @@
val read_constructs = map o map o read_construct;
(*convert constructor specifications into introduction rules*)
-fun mk_intr_tms (rec_tm, constructs) =
- let fun mk_intr ((id,T,syn), name, args, prems) =
- Logic.list_implies
- (map mk_tprop prems,
- mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm))
+fun mk_intr_tms sg (rec_tm, constructs) =
+ let
+ fun mk_intr ((id,T,syn), name, args, prems) =
+ Logic.list_implies
+ (map mk_tprop prems,
+ mk_tprop (mem_const $ list_comb (Const (Sign.full_name sg name, T), args) $ rec_tm))
in map mk_intr constructs end;
-fun mk_all_intr_tms arg = List.concat (ListPair.map mk_intr_tms arg);
+fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
val Un = Const("op Un", [iT,iT]--->iT)
and empty = Const("0", iT)
--- a/src/ZF/indrule.ML Fri Oct 17 17:40:33 1997 +0200
+++ b/src/ZF/indrule.ML Fri Oct 17 17:42:39 1997 +0200
@@ -25,7 +25,9 @@
val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
-val big_rec_name = space_implode "_" Intr_elim.rec_names;
+val big_rec_name =
+ Sign.intern_const sign (space_implode "_" (map NameSpace.base Intr_elim.rec_names));
+
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
val _ = writeln " Proving the induction rule...";
@@ -117,7 +119,7 @@
mutual recursion to invariably be a disjoint sum.*)
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
- val pfree = Free(pred_name ^ "_" ^ rec_name,
+ val pfree = Free(pred_name ^ "_" ^ NameSpace.base rec_name,
elem_factors ---> Ind_Syntax.oT)
val qconcl =
foldr Ind_Syntax.mk_all
--- a/src/ZF/intr_elim.ML Fri Oct 17 17:40:33 1997 +0200
+++ b/src/ZF/intr_elim.ML Fri Oct 17 17:42:39 1997 +0200
@@ -48,16 +48,16 @@
let
val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
-val big_rec_name = space_implode "_" rec_names;
+val big_rec_base_name = space_implode "_" (map NameSpace.base rec_names);
-val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy))
- ("Definition " ^ big_rec_name ^
+val _ = deny (big_rec_base_name mem map ! (stamps_of_thy Inductive.thy))
+ ("Definition " ^ big_rec_base_name ^
" would clash with the theory of the same name!");
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
map (get_def Inductive.thy)
- (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
+ (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names);
val sign = sign_of Inductive.thy;
--- a/src/ZF/thy_syntax.ML Fri Oct 17 17:40:33 1997 +0200
+++ b/src/ZF/thy_syntax.ML Fri Oct 17 17:42:39 1997 +0200
@@ -97,7 +97,7 @@
\ val dom_sum\t= " ^ sdom_sum ^ "\n\
\ and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n"
^ scons ^ "\n\
- \ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (rec_tms, con_ty_lists)\n\
+ \ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (sign_of thy) (rec_tms, con_ty_lists)\n\
\ end;\n\n\
\val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^
mk_list (map quote rec_names) ^ ", " ^
@@ -114,7 +114,7 @@
\ structure Result = " ^ co ^ "Data_section_Fun\n\
\\t (open " ^ stri_name ^ "\n\
\\t val thy\t\t= thy\n\
- \\t val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
+ \\t val big_rec_name\t= Sign.intern_const (sign_of thy) \"" ^ big_rec_name ^ "\"\n\
\\t val monos\t\t= " ^ monos ^ "\n\
\\t val type_intrs\t= " ^ type_intrs ^ "\n\
\\t val type_elims\t= " ^ type_elims ^ ");\n\