# HG changeset patch
# User traytel
# Date 1377811308 -7200
# Node ID e414487da3f8e03146d54713a624a6a966309ecc
# Parent  d0153a0a9b2bb7d042bd999b8696a953c2efe526
qualify internal and external constants in {l,g}fp properly

diff -r d0153a0a9b2b -r e414487da3f8 src/HOL/BNF/Tools/bnf_gfp.ML
--- 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;
 
diff -r d0153a0a9b2b -r e414487da3f8 src/HOL/BNF/Tools/bnf_lfp.ML
--- 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;