--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Aug 07 14:44:51 2024 +0200
@@ -112,7 +112,7 @@
: (term list * term list) =
let
val Ts = map snd args
- val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list taken (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
in
@@ -167,7 +167,7 @@
fun vars_of args =
let
val Ts = map snd args
- val ns = Old_Datatype_Prop.make_tnames Ts
+ val ns = Case_Translation.make_tnames Ts
in
map Free (ns ~~ Ts)
end
@@ -409,7 +409,7 @@
val tns = map fst (Term.add_tfreesT lhsT [])
val resultT = TFree (singleton (Name.variant_list tns) "'t", \<^sort>\<open>pcpo\<close>)
fun fTs T = map (fn (_, args) => map snd args -->> T) spec
- val fns = Old_Datatype_Prop.indexify_names (map (K "f") spec)
+ val fns = Case_Translation.indexify_names (map (K "f") spec)
val fs = map Free (fns ~~ fTs resultT)
fun caseT T = fTs T -->> (lhsT ->> T)
@@ -424,7 +424,7 @@
fun one_con f (_, args) =
let
val Ts = map snd args
- val ns = Name.variant_list fns (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list fns (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
in
lambda_args (map fst args ~~ vs) (list_ccomb (f, vs))
@@ -606,7 +606,7 @@
fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
let
val Ts : typ list = map #3 args
- val ns : string list = Old_Datatype_Prop.make_tnames Ts
+ val ns : string list = Case_Translation.make_tnames Ts
val vs : term list = map Free (ns ~~ Ts)
val con_app : term = list_ccomb (con, vs)
val vs' : (bool * term) list = map #1 args ~~ vs
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Aug 07 14:44:51 2024 +0200
@@ -63,7 +63,7 @@
fun prove_take_app (con_const, args) =
let
val Ts = map snd args
- val ns = Name.variant_list ["n"] (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list ["n"] (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs))
val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts)
@@ -108,8 +108,8 @@
val {take_consts, take_induct_thms, ...} = take_info
val newTs = map #absT iso_infos
- val P_names = Old_Datatype_Prop.indexify_names (map (K "P") newTs)
- val x_names = Old_Datatype_Prop.indexify_names (map (K "x") newTs)
+ val P_names = Case_Translation.indexify_names (map (K "P") newTs)
+ val x_names = Case_Translation.indexify_names (map (K "x") newTs)
val P_types = map (fn T => T --> \<^Type>\<open>bool\<close>) newTs
val Ps = map Free (P_names ~~ P_types)
val xs = map Free (x_names ~~ newTs)
@@ -118,7 +118,7 @@
fun con_assm defined p (con, args) =
let
val Ts = map snd args
- val ns = Name.variant_list P_names (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list P_names (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
fun ind_hyp (v, T) t =
@@ -256,7 +256,7 @@
val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info
- val R_names = Old_Datatype_Prop.indexify_names (map (K "R") newTs)
+ val R_names = Case_Translation.indexify_names (map (K "R") newTs)
val R_types = map (fn T => T --> T --> \<^Type>\<open>bool\<close>) newTs
val Rs = map Free (R_names ~~ R_types)
val n = Free ("n", \<^Type>\<open>nat\<close>)
@@ -273,7 +273,7 @@
fun one_con T (con, args) =
let
val Ts = map snd args
- val ns1 = Name.variant_list reserved (Old_Datatype_Prop.make_tnames Ts)
+ val ns1 = Name.variant_list reserved (Case_Translation.make_tnames Ts)
val ns2 = map (fn n => n^"'") ns1
val vs1 = map Free (ns1 ~~ Ts)
val vs2 = map Free (ns2 ~~ Ts)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Aug 07 14:44:51 2024 +0200
@@ -422,7 +422,7 @@
: (term list * term list) =
let
val Ts = map snd args;
- val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts);
+ val ns = Name.variant_list taken (Case_Translation.make_tnames Ts);
val vs = map Free (ns ~~ Ts);
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
in
@@ -469,10 +469,10 @@
val Ts = map snd args;
val Vs =
(map (K "'t") args)
- |> Old_Datatype_Prop.indexify_names
+ |> Case_Translation.indexify_names
|> Name.variant_list tns
|> map (fn t => TFree (t, \<^sort>\<open>pcpo\<close>));
- val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args);
+ val patNs = Case_Translation.indexify_names (map (K "pat") args);
val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
val pats = map Free (patNs ~~ patTs);
val fail = mk_fail (mk_tupleT Vs);
@@ -535,10 +535,10 @@
val Ts = map snd args;
val Vs =
(map (K "'t") args)
- |> Old_Datatype_Prop.indexify_names
+ |> Case_Translation.indexify_names
|> Name.variant_list (rn::tns)
|> map (fn t => TFree (t, \<^sort>\<open>pcpo\<close>));
- val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args);
+ val patNs = Case_Translation.indexify_names (map (K "pat") args);
val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
val pats = map Free (patNs ~~ patTs);
val k = Free ("rhs", mk_tupleT Vs ->> R);
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 07 14:44:51 2024 +0200
@@ -214,7 +214,7 @@
val perm_types = map (fn (i, _) =>
let val T = nth_dtyp i
in permT --> T --> T end) descr;
- val perm_names' = Old_Datatype_Prop.indexify_names (map (fn (i, _) =>
+ val perm_names' = Case_Translation.indexify_names (map (fn (i, _) =>
"perm_" ^ Old_Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
val perm_names = replicate (length new_type_names) \<^const_name>\<open>Nominal.perm\<close> @
map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
@@ -226,7 +226,7 @@
in map (fn (cname, dts) =>
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) dts;
- val names = Name.variant_list ["pi"] (Old_Datatype_Prop.make_tnames Ts);
+ val names = Name.variant_list ["pi"] (Case_Translation.make_tnames Ts);
val args = map Free (names ~~ Ts);
val c = Const (cname, Ts ---> T);
fun perm_arg (dt, x) =
@@ -264,7 +264,7 @@
val _ = warning ("length descr: " ^ string_of_int (length descr));
val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
- val perm_indnames = Old_Datatype_Prop.make_tnames (map body_type perm_types);
+ val perm_indnames = Case_Translation.make_tnames (map body_type perm_types);
val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
val unfolded_perm_eq_thms =
@@ -465,10 +465,10 @@
val _ = warning "representing sets";
val rep_set_names =
- Old_Datatype_Prop.indexify_names
+ Case_Translation.indexify_names
(map (fn (i, _) => Old_Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
val big_rep_name =
- space_implode "_" (Old_Datatype_Prop.indexify_names (map_filter
+ space_implode "_" (Case_Translation.indexify_names (map_filter
(fn (i, (\<^type_name>\<open>noption\<close>, _, _)) => NONE
| (i, _) => SOME (Old_Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
@@ -1084,7 +1084,7 @@
val _ = warning "proving finite support for the new datatype";
- val indnames = Old_Datatype_Prop.make_tnames recTs;
+ val indnames = Case_Translation.make_tnames recTs;
val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
@@ -1147,7 +1147,7 @@
val fsT' = TFree ("'n", \<^sort>\<open>type\<close>);
val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
- (Old_Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
+ (Case_Translation.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT);
@@ -1168,7 +1168,7 @@
val recs = filter Old_Datatype_Aux.is_rec_type cargs;
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr'') cargs;
val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr'') recs;
- val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+ val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val frees' = partition_cargs idxs frees;
@@ -1202,7 +1202,7 @@
map (make_ind_prem fsT (fn T => fn t => fn u =>
fresh_const T fsT $ t $ u) i T)
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
- val tnames = Old_Datatype_Prop.make_tnames recTs;
+ val tnames = Case_Translation.make_tnames recTs;
val zs = Name.variant_list tnames (replicate (length descr'') "z");
val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
(map (fn ((((i, _), T), tname), z) =>
@@ -1226,7 +1226,7 @@
val induct' = Logic.list_implies (ind_prems', ind_concl');
val aux_ind_vars =
- (Old_Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
+ (Case_Translation.indexify_names (replicate (length dt_atomTs) "pi") ~~
map mk_permT dt_atomTs) @ [("z", fsT')];
val aux_ind_Ts = rev (map snd aux_ind_vars);
val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
@@ -1679,10 +1679,10 @@
val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
val fun_tupleT = fastype_of fun_tuple;
val rec_unique_frees =
- Old_Datatype_Prop.indexify_names (replicate (length recTs) "x") ~~ recTs;
+ Case_Translation.indexify_names (replicate (length recTs) "x") ~~ recTs;
val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
val rec_unique_frees' =
- Old_Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
+ Case_Translation.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
val rec_unique_concls = map (fn ((x, U), R) =>
Const (\<^const_name>\<open>Ex1\<close>, (U --> HOLogic.boolT) --> HOLogic.boolT) $
Abs ("y", U, R $ Free x $ Bound 0))
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Aug 07 14:44:51 2024 +0200
@@ -250,7 +250,7 @@
end) prems);
val ind_vars =
- (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+ (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
val ind_Ts = rev (map snd ind_vars);
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 07 14:44:51 2024 +0200
@@ -267,7 +267,7 @@
in abs_params params' prem end) prems);
val ind_vars =
- (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+ (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
val ind_Ts = rev (map snd ind_vars);
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Aug 07 14:44:51 2024 +0200
@@ -731,7 +731,7 @@
| rename t _ = t
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
- val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
+ val new_names = Case_Translation.make_tnames (all_typs fixed_def_t)
in
rename term new_names
end
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Aug 07 14:44:51 2024 +0200
@@ -220,7 +220,7 @@
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
fun induct_cases descr =
- Old_Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr));
+ Case_Translation.indexify_names (maps (dt_cases descr) (map #2 descr));
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 07 14:44:51 2024 +0200
@@ -7,8 +7,6 @@
signature OLD_DATATYPE_PROP =
sig
type descr = Old_Datatype_Aux.descr
- val indexify_names: string list -> string list
- val make_tnames: typ list -> string list
val make_injs : descr list -> term list list
val make_distincts : descr list -> term list list (*no symmetric inequalities*)
val make_ind : descr list -> term
@@ -28,9 +26,6 @@
type descr = Old_Datatype_Aux.descr;
-val indexify_names = Case_Translation.indexify_names;
-val make_tnames = Case_Translation.make_tnames;
-
(************************* injectivity of constructors ************************)
@@ -43,7 +38,7 @@
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val constr_t = Const (cname, Ts ---> T);
- val tnames = make_tnames Ts;
+ val tnames = Case_Translation.make_tnames Ts;
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (map (suffix "'") tnames ~~ Ts);
in
@@ -71,12 +66,13 @@
fun make_distincts' _ [] = []
| make_distincts' T ((cname, cargs) :: constrs) =
let
- val frees = map Free (make_tnames cargs ~~ cargs);
+ val frees = map Free (Case_Translation.make_tnames cargs ~~ cargs);
val t = list_comb (Const (cname, cargs ---> T), frees);
fun make_distincts'' (cname', cargs') =
let
- val frees' = map Free (map (suffix "'") (make_tnames cargs') ~~ cargs');
+ val frees' =
+ map Free (map (suffix "'") (Case_Translation.make_tnames cargs') ~~ cargs');
val t' = list_comb (Const (cname', cargs' ---> T), frees');
in
HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))
@@ -114,7 +110,7 @@
val recs = filter Old_Datatype_Aux.is_rec_type cargs;
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr') recs;
- val tnames = Name.variant_list pnames (make_tnames Ts);
+ val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -127,7 +123,7 @@
val prems =
maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
- val tnames = make_tnames recTs;
+ val tnames = Case_Translation.make_tnames recTs;
val concl =
HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
@@ -144,7 +140,7 @@
fun make_casedist_prem T (cname, cargs) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
+ val frees = Name.variant_list ["P", "y"] (Case_Translation.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
in
fold_rev (Logic.all o Free) frees
@@ -208,7 +204,7 @@
val recs = filter Old_Datatype_Aux.is_rec_type cargs;
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr') recs;
- val tnames = make_tnames Ts;
+ val tnames = Case_Translation.make_tnames Ts;
val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (rec_tnames ~~ recTs');
@@ -265,7 +261,7 @@
fun make_case T comb_t ((cname, cargs), f) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val frees = map Free ((make_tnames Ts) ~~ Ts);
+ val frees = map Free ((Case_Translation.make_tnames Ts) ~~ Ts);
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -297,7 +293,7 @@
fun process_constr ((cname, cargs), f) (t1s, t2s) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
+ val frees = map Free (Name.variant_list used (Case_Translation.make_tnames Ts) ~~ Ts);
val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
val P' = P $ list_comb (f, frees);
in
@@ -366,7 +362,7 @@
fun mk_clause ((f, g), (cname, _)) =
let
val Ts = binder_types (fastype_of f);
- val tnames = Name.variant_list used (make_tnames Ts);
+ val tnames = Name.variant_list used (Case_Translation.make_tnames Ts);
val frees = map Free (tnames ~~ Ts);
in
fold_rev Logic.all frees
@@ -400,7 +396,7 @@
fun mk_eqn T (cname, cargs) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val tnames = Name.variant_list ["v"] (make_tnames Ts);
+ val tnames = Name.variant_list ["v"] (Case_Translation.make_tnames Ts);
val frees = tnames ~~ Ts;
in
fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
--- a/src/HOL/Tools/datatype_realizer.ML Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Aug 07 14:44:51 2024 +0200
@@ -49,7 +49,7 @@
(fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
- val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+ val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
@@ -88,7 +88,7 @@
else if (j: int) = i then HOLogic.mk_fst t
else mk_proj j is (HOLogic.mk_snd t);
- val tnames = Old_Datatype_Prop.make_tnames recTs;
+ val tnames = Case_Translation.make_tnames recTs;
val fTs = map fastype_of rec_fns;
val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
@@ -168,7 +168,7 @@
fun make_casedist_prem T (cname, cargs) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
- val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
+ val frees = Name.variant_list ["P", "y"] (Case_Translation.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
in