--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Sep 12 15:46:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Sep 12 16:31:42 2013 +0200
@@ -587,13 +587,15 @@
in
Binding.prefix_name rawN
#> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
+ #> Binding.conceal
end;
val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
(fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
(empty_unfolds, lthy));
- fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))));
+ fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
+ #> Binding.conceal;
val Ass = map (map dest_TFree) livess;
val resDs = fold (subtract (op =)) Ass resBs;
@@ -606,7 +608,8 @@
val Dss = map3 (append oo map o nth) livess kill_poss deadss;
- val pre_qualify = Binding.qualify false o Binding.name_of;
+ fun pre_qualify b = Binding.qualify false (Binding.name_of b)
+ #> Config.get lthy' bnf_note_all = false ? Binding.conceal;
val ((pre_bnfs, deadss), lthy'') =
fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Sep 12 15:46:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Sep 12 16:31:42 2013 +0200
@@ -66,13 +66,17 @@
val ks = 1 upto n;
val m = live - n; (*passive, if 0 don't generate a new BNF*)
val ls = 1 upto m;
+
+ val note_all = Config.get lthy bnf_note_all;
val b_names = map Binding.name_of bs;
- 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;
+ val b_name = mk_common_name b_names;
+ val b = Binding.name b_name;
+ val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
+ fun mk_internal_bs name =
+ map (fn b =>
+ Binding.prefix true b_name (Binding.suffix_name ("_" ^ name) b) |> Binding.conceal) bs;
+ val external_bs = map2 (Binding.prefix false) b_names bs
+ |> note_all = false ? map Binding.conceal;
(* TODO: check if m, n, etc., are sane *)
@@ -297,7 +301,7 @@
(* coalgebra *)
- val coalg_bind = Binding.suffix_name ("_" ^ coN ^ algN) internal_b;
+ val coalg_bind = mk_internal_b (coN ^ algN) ;
val coalg_name = Binding.name_of coalg_bind;
val coalg_def_bind = (Thm.def_binding coalg_bind, []);
@@ -373,7 +377,7 @@
(* morphism *)
- val mor_bind = Binding.suffix_name ("_" ^ morN) internal_b;
+ val mor_bind = mk_internal_b morN;
val mor_name = Binding.name_of mor_bind;
val mor_def_bind = (Thm.def_binding mor_bind, []);
@@ -518,8 +522,7 @@
val timer = time (timer "Morphism definition & thms");
- fun hset_rec_bind j = internal_b
- |> Binding.suffix_name ("_" ^ hset_recN ^ (if m = 1 then "" else string_of_int j)) ;
+ fun hset_rec_bind j = mk_internal_b (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;
@@ -573,8 +576,8 @@
val hset_rec_0ss' = transpose hset_rec_0ss;
val hset_rec_Sucss' = transpose hset_rec_Sucss;
- fun hset_bind i j = nth internal_bs (i - 1)
- |> Binding.suffix_name ("_" ^ hsetN ^ (if m = 1 then "" else string_of_int j));
+ fun hset_binds j = mk_internal_bs (hsetN ^ (if m = 1 then "" else string_of_int j))
+ fun hset_bind i j = nth (hset_binds j) (i - 1);
val hset_name = Binding.name_of oo hset_bind;
val hset_def_bind = rpair [] o Thm.def_binding oo hset_bind;
@@ -741,7 +744,7 @@
(* bisimulation *)
- val bis_bind = Binding.suffix_name ("_" ^ bisN) internal_b;
+ val bis_bind = mk_internal_b bisN;
val bis_name = Binding.name_of bis_bind;
val bis_def_bind = (Thm.def_binding bis_bind, []);
@@ -885,7 +888,8 @@
(* largest self-bisimulation *)
- fun lsbis_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ lsbisN);
+ val lsbis_binds = mk_internal_bs lsbisN;
+ fun lsbis_bind i = nth lsbis_binds (i - 1);
val lsbis_name = Binding.name_of o lsbis_bind;
val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
@@ -970,8 +974,7 @@
then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss)
else
let
- val sbdT_bind =
- Binding.qualify false (Binding.name_of b) (Binding.suffix_name ("_" ^ sum_bdTN) b);
+ val sbdT_bind = mk_internal_b sum_bdTN;
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
typedef (sbdT_bind, dead_params, NoSyn)
@@ -980,7 +983,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) internal_b;
+ val sbd_bind = mk_internal_b sum_bdN;
val sbd_name = Binding.name_of sbd_bind;
val sbd_def_bind = (Thm.def_binding sbd_bind, []);
@@ -1076,7 +1079,8 @@
(* tree coalgebra *)
- fun isNode_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ isNodeN);
+ val isNode_binds = mk_internal_bs isNodeN;
+ fun isNode_bind i = nth isNode_binds (i - 1);
val isNode_name = Binding.name_of o isNode_bind;
val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
@@ -1135,7 +1139,8 @@
Library.foldr1 HOLogic.mk_conj [empty, Field, prefCl, tree, undef]
end;
- fun carT_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ carTN);
+ val carT_binds = mk_internal_bs carTN;
+ fun carT_bind i = nth carT_binds (i - 1);
val carT_name = Binding.name_of o carT_bind;
val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
@@ -1167,7 +1172,8 @@
(Const (nth carTs (i - 1),
Library.foldr (op -->) (map fastype_of As, HOLogic.mk_setT treeT)), As);
- fun strT_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ strTN);
+ val strT_binds = mk_internal_bs strTN;
+ fun strT_bind i = nth strT_binds (i - 1);
val strT_name = Binding.name_of o strT_bind;
val strT_def_bind = rpair [] o Thm.def_binding o strT_bind;
@@ -1228,7 +1234,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) internal_b;
+ val Lev_bind = mk_internal_b LevN;
val Lev_name = Binding.name_of Lev_bind;
val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind);
@@ -1282,7 +1288,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) internal_b;
+ val rv_bind = mk_internal_b rvN;
val rv_name = Binding.name_of rv_bind;
val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
@@ -1328,7 +1334,8 @@
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 = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ behN);
+ val beh_binds = mk_internal_bs behN;
+ fun beh_bind i = nth beh_binds (i - 1);
val beh_name = Binding.name_of o beh_bind;
val beh_def_bind = rpair [] o Thm.def_binding o beh_bind;
@@ -1636,7 +1643,7 @@
val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
lthy
|> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
- typedef (b, params, mx) car_final NONE
+ typedef (Binding.conceal b, params, mx) car_final NONE
(EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
|>> apsnd split_list o split_list;
@@ -1692,7 +1699,7 @@
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;
+ val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
fun dtor_spec i rep str map_FT dtorT Jz Jz' =
let
@@ -1744,7 +1751,7 @@
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;
+ val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
fun unfold_spec i T AT abs f z z' =
let
@@ -1865,7 +1872,7 @@
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;
+ val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
fun ctor_spec i ctorT =
let
@@ -1936,7 +1943,7 @@
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;
+ val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
val corec_strs =
map3 (fn dtor => fn sum_s => fn mapx =>
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Sep 12 15:46:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Sep 12 16:31:42 2013 +0200
@@ -36,13 +36,17 @@
val n = length bnfs; (*active*)
val ks = 1 upto n;
val m = live - n; (*passive, if 0 don't generate a new BNF*)
+
+ val note_all = Config.get lthy bnf_note_all;
val b_names = map Binding.name_of bs;
- 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;
+ val b_name = mk_common_name b_names;
+ val b = Binding.name b_name;
+ val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
+ fun mk_internal_bs name =
+ map (fn b =>
+ Binding.prefix true b_name (Binding.suffix_name ("_" ^ name) b) |> Binding.conceal) bs;
+ val external_bs = map2 (Binding.prefix false) b_names bs
+ |> note_all = false ? map Binding.conceal;
(* TODO: check if m, n, etc., are sane *)
@@ -238,7 +242,7 @@
(* algebra *)
- val alg_bind = Binding.suffix_name ("_" ^ algN) internal_b;
+ val alg_bind = mk_internal_b algN;
val alg_name = Binding.name_of alg_bind;
val alg_def_bind = (Thm.def_binding alg_bind, []);
@@ -325,7 +329,7 @@
(* morphism *)
- val mor_bind = Binding.suffix_name ("_" ^ morN) internal_b;
+ val mor_bind = mk_internal_b morN;
val mor_name = Binding.name_of mor_bind;
val mor_def_bind = (Thm.def_binding mor_bind, []);
@@ -712,8 +716,9 @@
val timer = time (timer "min_algs definition & thms");
- 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_binds = mk_internal_bs min_algN;
+ fun min_alg_bind i = nth min_alg_binds (i - 1);
+ fun min_alg_name i = Binding.name_of (min_alg_bind i);
val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
fun min_alg_spec i =
@@ -791,7 +796,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.suffix_name ("_" ^ IITN) b;
+ val IIT_bind = mk_internal_b IITN;
val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
typedef (IIT_bind, params, NoSyn)
@@ -824,7 +829,8 @@
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 = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ str_initN);
+ val str_init_binds = mk_internal_bs str_initN;
+ fun str_init_bind i = nth str_init_binds (i - 1);
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;
@@ -953,7 +959,8 @@
val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
lthy
- |> fold_map3 (fn b => fn mx => fn car_init => typedef (b, params, mx) car_init NONE
+ |> fold_map3 (fn b => fn mx => fn car_init =>
+ typedef (Binding.conceal b, params, mx) car_init NONE
(EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
rtac alg_init_thm] 1)) bs mixfixes car_inits
|>> apsnd split_list o split_list;
@@ -1016,7 +1023,7 @@
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;
+ val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
fun ctor_spec i abs str map_FT_init x x' =
let
@@ -1075,7 +1082,7 @@
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;
+ val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
fun fold_spec i T AT =
let
@@ -1165,7 +1172,7 @@
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;
+ val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
fun dtor_spec i FT T =
let
@@ -1238,7 +1245,7 @@
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;
+ val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
val rec_strs =
map3 (fn ctor => fn prod_s => fn mapx =>