--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 23:21:48 2013 +0200
@@ -66,7 +66,12 @@
val m = live - n; (*passive, if 0 don't generate a new BNF*)
val ls = 1 upto m;
val b_names = map Binding.name_of bs;
- val b = Binding.name (mk_common_name b_names);
+ val common_name = mk_common_name b_names;
+ val b = Binding.name common_name;
+ val internal_b = Binding.prefix true common_name b;
+ fun qualify_bs internal = map2 (Binding.prefix internal) b_names bs;
+ val internal_bs = qualify_bs true;
+ val external_bs = qualify_bs false;
(* TODO: check if m, n, etc., are sane *)
@@ -291,7 +296,7 @@
(* coalgebra *)
- val coalg_bind = Binding.suffix_name ("_" ^ coN ^ algN) b;
+ val coalg_bind = Binding.suffix_name ("_" ^ coN ^ algN) internal_b;
val coalg_name = Binding.name_of coalg_bind;
val coalg_def_bind = (Thm.def_binding coalg_bind, []);
@@ -367,7 +372,7 @@
(* morphism *)
- val mor_bind = Binding.suffix_name ("_" ^ morN) b;
+ val mor_bind = Binding.suffix_name ("_" ^ morN) internal_b;
val mor_name = Binding.name_of mor_bind;
val mor_def_bind = (Thm.def_binding mor_bind, []);
@@ -512,8 +517,8 @@
val timer = time (timer "Morphism definition & thms");
- fun hset_rec_bind j = Binding.suffix_name ("_" ^ hset_recN ^ (if m = 1 then "" else
- string_of_int j)) b;
+ fun hset_rec_bind j = internal_b
+ |> Binding.suffix_name ("_" ^ hset_recN ^ (if m = 1 then "" else string_of_int j)) ;
val hset_rec_name = Binding.name_of o hset_rec_bind;
val hset_rec_def_bind = rpair [] o Thm.def_binding o hset_rec_bind;
@@ -567,8 +572,8 @@
val hset_rec_0ss' = transpose hset_rec_0ss;
val hset_rec_Sucss' = transpose hset_rec_Sucss;
- fun hset_bind i j = Binding.suffix_name ("_" ^ hsetN ^
- (if m = 1 then "" else string_of_int j)) (nth bs (i - 1));
+ fun hset_bind i j = nth internal_bs (i - 1)
+ |> Binding.suffix_name ("_" ^ hsetN ^ (if m = 1 then "" else string_of_int j));
val hset_name = Binding.name_of oo hset_bind;
val hset_def_bind = rpair [] o Thm.def_binding oo hset_bind;
@@ -735,7 +740,7 @@
(* bisimulation *)
- val bis_bind = Binding.suffix_name ("_" ^ bisN) b;
+ val bis_bind = Binding.suffix_name ("_" ^ bisN) internal_b;
val bis_name = Binding.name_of bis_bind;
val bis_def_bind = (Thm.def_binding bis_bind, []);
@@ -879,8 +884,7 @@
(* largest self-bisimulation *)
- fun lsbis_bind i = Binding.suffix_name ("_" ^ lsbisN ^ (if n = 1 then "" else
- string_of_int i)) b;
+ fun lsbis_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ lsbisN);
val lsbis_name = Binding.name_of o lsbis_bind;
val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
@@ -975,7 +979,7 @@
val sbdT = Type (sbdT_name, dead_params');
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
- val sbd_bind = Binding.suffix_name ("_" ^ sum_bdN) b;
+ val sbd_bind = Binding.suffix_name ("_" ^ sum_bdN) internal_b;
val sbd_name = Binding.name_of sbd_bind;
val sbd_def_bind = (Thm.def_binding sbd_bind, []);
@@ -1071,8 +1075,7 @@
(* tree coalgebra *)
- fun isNode_bind i = Binding.suffix_name ("_" ^ isNodeN ^ (if n = 1 then "" else
- string_of_int i)) b;
+ fun isNode_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ isNodeN);
val isNode_name = Binding.name_of o isNode_bind;
val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
@@ -1131,8 +1134,7 @@
Library.foldr1 HOLogic.mk_conj [empty, Field, prefCl, tree, undef]
end;
- fun carT_bind i = Binding.suffix_name ("_" ^ carTN ^ (if n = 1 then "" else
- string_of_int i)) b;
+ fun carT_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ carTN);
val carT_name = Binding.name_of o carT_bind;
val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
@@ -1164,8 +1166,7 @@
(Const (nth carTs (i - 1),
Library.foldr (op -->) (map fastype_of As, HOLogic.mk_setT treeT)), As);
- fun strT_bind i = Binding.suffix_name ("_" ^ strTN ^ (if n = 1 then "" else
- string_of_int i)) b;
+ fun strT_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ strTN);
val strT_name = Binding.name_of o strT_bind;
val strT_def_bind = rpair [] o Thm.def_binding o strT_bind;
@@ -1226,7 +1227,7 @@
val to_sbd_thmss = mk_to_sbd_thmss @{thm toCard};
val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard};
- val Lev_bind = Binding.suffix_name ("_" ^ LevN) b;
+ val Lev_bind = Binding.suffix_name ("_" ^ LevN) internal_b;
val Lev_name = Binding.name_of Lev_bind;
val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind);
@@ -1280,7 +1281,7 @@
val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0} [Lev_def]);
val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc} [Lev_def]);
- val rv_bind = Binding.suffix_name ("_" ^ rvN) b;
+ val rv_bind = Binding.suffix_name ("_" ^ rvN) internal_b;
val rv_name = Binding.name_of rv_bind;
val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
@@ -1326,8 +1327,7 @@
val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil} [rv_def]);
val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons} [rv_def]);
- fun beh_bind i = Binding.suffix_name ("_" ^ behN ^ (if n = 1 then "" else
- string_of_int i)) b;
+ fun beh_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ behN);
val beh_name = Binding.name_of o beh_bind;
val beh_def_bind = rpair [] o Thm.def_binding o beh_bind;
@@ -1689,7 +1689,7 @@
||>> mk_Frees "s" corec_sTs
||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
- fun dtor_bind i = Binding.suffix_name ("_" ^ dtorN) (nth bs (i - 1));
+ fun dtor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtorN);
val dtor_name = Binding.name_of o dtor_bind;
val dtor_def_bind = rpair [] o Thm.def_binding o dtor_bind;
@@ -1741,7 +1741,7 @@
val timer = time (timer "dtor definitions & thms");
- fun unfold_bind i = Binding.suffix_name ("_" ^ dtor_unfoldN) (nth bs (i - 1));
+ fun unfold_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtor_unfoldN);
val unfold_name = Binding.name_of o unfold_bind;
val unfold_def_bind = rpair [] o Thm.def_binding o unfold_bind;
@@ -1862,7 +1862,7 @@
Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
- fun ctor_bind i = Binding.suffix_name ("_" ^ ctorN) (nth bs (i - 1));
+ fun ctor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctorN);
val ctor_name = Binding.name_of o ctor_bind;
val ctor_def_bind = rpair [] o Thm.def_binding o ctor_bind;
@@ -1933,7 +1933,7 @@
trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
end;
- fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1));
+ fun corec_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtor_corecN);
val corec_name = Binding.name_of o corec_bind;
val corec_def_bind = rpair [] o Thm.def_binding o corec_bind;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 23:21:48 2013 +0200
@@ -36,7 +36,12 @@
val ks = 1 upto n;
val m = live - n; (*passive, if 0 don't generate a new BNF*)
val b_names = map Binding.name_of bs;
- val b = Binding.name (mk_common_name b_names);
+ val common_name = mk_common_name b_names;
+ val b = Binding.name common_name;
+ val internal_b = Binding.prefix true common_name b;
+ fun qualify_bs internal = map2 (Binding.prefix internal) b_names bs;
+ val internal_bs = qualify_bs true;
+ val external_bs = qualify_bs false;
(* TODO: check if m, n, etc., are sane *)
@@ -232,7 +237,7 @@
(* algebra *)
- val alg_bind = Binding.suffix_name ("_" ^ algN) b;
+ val alg_bind = Binding.suffix_name ("_" ^ algN) internal_b;
val alg_name = Binding.name_of alg_bind;
val alg_def_bind = (Thm.def_binding alg_bind, []);
@@ -319,7 +324,7 @@
(* morphism *)
- val mor_bind = Binding.suffix_name ("_" ^ morN) b;
+ val mor_bind = Binding.suffix_name ("_" ^ morN) internal_b;
val mor_name = Binding.name_of mor_bind;
val mor_def_bind = (Thm.def_binding mor_bind, []);
@@ -707,8 +712,7 @@
val timer = time (timer "min_algs definition & thms");
- fun min_alg_bind i = Binding.suffix_name
- ("_" ^ min_algN ^ (if n = 1 then "" else string_of_int i)) b;
+ fun min_alg_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ min_algN);
val min_alg_name = Binding.name_of o min_alg_bind;
val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
@@ -787,7 +791,7 @@
val timer = time (timer "Minimal algebra definition & thms");
val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs);
- val IIT_bind = Binding.qualify false (Binding.name_of b) (Binding.suffix_name ("_" ^ IITN) b);
+ val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
typedef (IIT_bind, params, NoSyn)
@@ -820,8 +824,7 @@
val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
- fun str_init_bind i = Binding.suffix_name ("_" ^ str_initN ^ (if n = 1 then "" else
- string_of_int i)) b;
+ fun str_init_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ str_initN);
val str_init_name = Binding.name_of o str_init_bind;
val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
@@ -1011,7 +1014,7 @@
val phis = map2 retype_free (map mk_pred1T Ts) init_phis;
val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
- fun ctor_bind i = Binding.suffix_name ("_" ^ ctorN) (nth bs (i - 1));
+ fun ctor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctorN);
val ctor_name = Binding.name_of o ctor_bind;
val ctor_def_bind = rpair [] o Thm.def_binding o ctor_bind;
@@ -1070,7 +1073,7 @@
(mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
val foldx = HOLogic.choice_const foldT $ fold_fun;
- fun fold_bind i = Binding.suffix_name ("_" ^ ctor_foldN) (nth bs (i - 1));
+ fun fold_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctor_foldN);
val fold_name = Binding.name_of o fold_bind;
val fold_def_bind = rpair [] o Thm.def_binding o fold_bind;
@@ -1160,7 +1163,7 @@
Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
- fun dtor_bind i = Binding.suffix_name ("_" ^ dtorN) (nth bs (i - 1));
+ fun dtor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtorN);
val dtor_name = Binding.name_of o dtor_bind;
val dtor_def_bind = rpair [] o Thm.def_binding o dtor_bind;
@@ -1233,7 +1236,7 @@
trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
end;
- fun rec_bind i = Binding.suffix_name ("_" ^ ctor_recN) (nth bs (i - 1));
+ fun rec_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctor_recN);
val rec_name = Binding.name_of o rec_bind;
val rec_def_bind = rpair [] o Thm.def_binding o rec_bind;