# HG changeset patch # User traytel # Date 1378996302 -7200 # Node ID 5ff3a2d112d735c0de5dff12567b91fee66ac0e3 # Parent 1e5314b990098ea9fa992bf17d241028aea52718 conceal internal bindings diff -r 1e5314b99009 -r 5ff3a2d112d7 src/HOL/BNF/Tools/bnf_fp_util.ML --- 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)) diff -r 1e5314b99009 -r 5ff3a2d112d7 src/HOL/BNF/Tools/bnf_gfp.ML --- 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 => diff -r 1e5314b99009 -r 5ff3a2d112d7 src/HOL/BNF/Tools/bnf_lfp.ML --- 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 =>