Allow to change the names of all the constants

Tools/mrbnf_sugar.ML

@@ -9,8 +9,9 @@ type spec = {
   ctors: ((string * mixfix) * typ list) list,
   map_b: binding,
   tvsubst_b: binding,
+  rel_b: binding,
   permute_b: binding option,
-  FVars_bs: binding option list
+  set_bs: binding option list
 };
 
 type mr_bnf = (MRBNF_Def.mrbnf, (BNF_Def.bnf, MRBNF_FP_Def_Sugar.quotient_result MRBNF_FP_Def_Sugar.fp_result_T) MRBNF_Util.either) MRBNF_Util.either
@@ -43,8 +44,9 @@ type spec = {
   ctors: ((string * mixfix) * typ list) list,
   map_b: binding,
   tvsubst_b: binding,
+  rel_b: binding,
   permute_b: binding option,
-  FVars_bs: binding option list
+  set_bs: binding option list
 };
 
 fun add_nesting_mrbnf_names Us =
@@ -80,13 +82,19 @@ fun create_binder_type (fp : MRBNF_Util.fp_kind) (spec : spec) lthy =
 
     val mrbnf = hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf);
 
+    val FVars_names = case #set_bs spec of
+      [x] => [SOME (the_default ("set_" ^ name) (Option.map Binding.name_of x))]
+      | _ => map_index (fn (i, b_opt) =>
+        SOME (the_default ("set" ^ string_of_int i ^ "_" ^ name) (Option.map Binding.name_of b_opt))
+      ) (take (length (#binding_rel spec)) (#set_bs spec));
+
     val (bnf, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf lthy
     val (res, lthy) = MRBNF_FP.construct_binder_fp fp [{
       T_name = name,
       pre_mrbnf = mrbnf,
       nrecs = #rec_vars spec,
       permute = Option.map Binding.name_of (#permute_b spec),
-      FVars = map (Option.map Binding.name_of) (take (length (#binding_rel spec)) (#FVars_bs spec))
+      FVars = FVars_names
     }] (map single (#binding_rel spec)) lthy;
   in ((res, fp_pre_T, mrsbnf, absinfo), lthy) end
 
@@ -207,7 +215,11 @@ fun create_binder_datatype co (spec : spec) lthy =
 
         val _ = clean_message lthy quiet_mode "  Creating renaming function and proving MRBNF axioms ...";
 
-        val ([(rec_mrbnf, vvsubst_res)], lthy) = MRBNF_VVSubst.mrbnf_of_quotient_fixpoint [#map_b spec] I res (#QREC_fixed recursor_result) lthy;
+        val ((rec_mrbnf, vvsubst_res), lthy) = apfst hd (MRBNF_VVSubst.mrbnf_of_quotient_fixpoint [{
+          vvsubst = SOME (#map_b spec),
+          rel = SOME (#rel_b spec),
+          psets = drop (length (#binding_rel spec)) (#set_bs spec)
+        }] I res (#QREC_fixed recursor_result) lthy);
         val lthy = MRBNF_Def.register_mrbnf_raw (fst (dest_Type (#T (hd (#quotient_fps res))))) rec_mrbnf lthy;
       in (SOME {
         recursor_result = recursor_result,

Tools/mrbnf_vvsubst.ML

@@ -7,10 +7,16 @@ sig
     pset_ctors: thm list
   };
 
+  type vvsubst_bs = {
+    vvsubst: binding option,
+    rel: binding option,
+    psets: binding option list
+  };
+
   val vvsubst_result_of: local_theory -> string -> vvsubst_result option
   val register_vvsubst_result: string -> vvsubst_result -> local_theory -> local_theory
 
-  val mrbnf_of_quotient_fixpoint: binding list -> (binding -> binding) -> MRBNF_FP_Def_Sugar.fp_result
+  val mrbnf_of_quotient_fixpoint: vvsubst_bs list -> (binding -> binding) -> MRBNF_FP_Def_Sugar.fp_result
     -> string -> local_theory -> (MRBNF_Def.mrbnf * vvsubst_result) list * local_theory
 end
 
@@ -29,6 +35,12 @@ type vvsubst_result = {
   pset_ctors: thm list
 };
 
+type vvsubst_bs = {
+  vvsubst: binding option,
+  rel: binding option,
+  psets: binding option list
+};
+
 fun morph_vvsubst_result phi { vvsubst_ctor, vvsubst_permute, psets, pset_ctors } = {
   vvsubst_ctor = Morphism.thm phi vvsubst_ctor,
   vvsubst_permute = Morphism.thm phi vvsubst_permute,
@@ -55,7 +67,7 @@ val vvsubst_result_of = vvsubst_result_of_generic o Context.Proof;
 fun mk_supp_bound f = mk_ordLess (mk_card_of (mk_supp f))
   (mk_card_of (HOLogic.mk_UNIV (fst (dest_funT (fastype_of f)))));
 
-fun define_vvsubst_consts qualify names (fp_res : MRBNF_FP_Def_Sugar.fp_result) vars deadss (plives, plives', pbounds, pfrees) old_lthy =
+fun define_vvsubst_consts qualify vvsubst_bss (fp_res : MRBNF_FP_Def_Sugar.fp_result) vars deadss (plives, plives', pbounds, pfrees) old_lthy =
   let
     val subst = Term.typ_subst_atomic (plives ~~ plives');
 
@@ -78,9 +90,13 @@ fun define_vvsubst_consts qualify names (fp_res : MRBNF_FP_Def_Sugar.fp_result)
     val Ts = map #T (#quotient_fps fp_res);
     fun replicate_rec xs = flat (map2 replicate (#rec_vars fp_res) xs);
 
-    fun mk_pset_names (fps:'a MRBNF_FP_Def_Sugar.fp_result_T list) = map (fn raw => map (fn i =>
-      "set" ^ string_of_int (i + nvars) ^ "_" ^ short_type_name (fst (dest_Type (#T raw)))
-    ) (1 upto npassive)) fps;
+    fun mk_pset_names public (fps:'a MRBNF_FP_Def_Sugar.fp_result_T list) = map2 (fn raw => fn vvsubst_bs => map2 (fn i => fn b =>
+      let val def = "set" ^ string_of_int (i + nvars) ^ "_" ^ short_type_name (fst (dest_Type (#T raw)));
+      in if public then case b of
+        SOME b => Binding.name_of b
+        | NONE => def
+      else def end
+    ) (1 upto npassive) (#psets vvsubst_bs)) fps vvsubst_bss;
     val ms = map (fn mrbnf => MRBNF_Def.free_of_mrbnf mrbnf + MRBNF_Def.bound_of_mrbnf mrbnf + MRBNF_Def.live_of_mrbnf mrbnf) mrbnfs;
     val mrbnf_setss = @{map 3} (fn m => fn deads =>
       MRBNF_Def.mk_sets_of_mrbnf (replicate m deads)
@@ -97,7 +113,7 @@ fun define_vvsubst_consts qualify names (fp_res : MRBNF_FP_Def_Sugar.fp_result)
 
     val (raw_psetss, lthy) =
       let
-        val namess = mk_pset_names (#raw_fps fp_res);
+        val namess = mk_pset_names false (#raw_fps fp_res);
         val setss = map2 (fn raw => map2 (fn var => fn n =>
           Free (n, #T raw --> HOLogic.mk_setT var)
         ) (pfrees @ plives @ pbounds)) (#raw_fps fp_res) namess;
@@ -137,7 +153,7 @@ fun define_vvsubst_consts qualify names (fp_res : MRBNF_FP_Def_Sugar.fp_result)
       mk_def_t false Binding.empty qualify name 1 (Term.absfree (dest_Free v) (
         fst raw_pset $ (#rep (#inner quot) $ v)
       ))
-    )) (#quotient_fps fp_res) vs (mk_pset_names (#quotient_fps fp_res)) raw_psetss lthy;
+    )) (#quotient_fps fp_res) vs (mk_pset_names true (#quotient_fps fp_res)) raw_psetss lthy;
 
     val (rels_opt, lthy) = if length plives = 0 then (NONE, lthy) else
       let
@@ -163,10 +179,12 @@ fun define_vvsubst_consts qualify names (fp_res : MRBNF_FP_Def_Sugar.fp_result)
           ||>> apply2 transpose o chop (length (#bfree_vars fp_res));
         val bfree_setss = if null bfree_setss then replicate (length mrbnfs) [] else bfree_setss;
 
-        val rels = map (fn quot => Free ("rel_" ^ short_type_name (fst (dest_Type (#T quot))),
+        val rels = map2 (fn quot => fn vvsubst_bs =>
+          let val def = "rel_" ^ short_type_name (fst (dest_Type (#T quot)));
+          in Free (the_default def (Option.map Binding.name_of (#rel vvsubst_bs)),
           fold_rev (curry (op-->)) (map2 (fn a => fn b => a --> b --> @{typ bool}) plives plives')
-            (#T quot --> subst (#T quot) --> @{typ bool})
-        )) (#quotient_fps fp_res);
+            (#T quot --> subst (#T quot) --> @{typ bool})) end
+        ) (#quotient_fps fp_res) vvsubst_bss;
 
         val f_premss = @{map 4} (fn rec_sets => fn x => fn bfree_sets =>
           flat o @{map 5} (fn i => fn FVarss => fn f => fn rel => fn bset =>
@@ -237,7 +255,7 @@ fun define_vvsubst_consts qualify names (fp_res : MRBNF_FP_Def_Sugar.fp_result)
     lthy
   ) end;
 
-fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Sugar.fp_result) QREC_fixed_name lthy =
+fun mrbnf_of_quotient_fixpoint vvsubst_bss qualify (fp_result : MRBNF_FP_Def_Sugar.fp_result) QREC_fixed_name lthy =
   let
     val mrbnfs = #pre_mrbnfs fp_result;
 
@@ -266,7 +284,7 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga
       in map (Envir.subst_type tyenv) (MRBNF_Def.deads_of_mrbnf mrbnf) end
     ) (#pre_mrbnfs fp_res) (#raw_fps fp_res);
 
-    val ((raw_psetss, psetss, rels_opt), lthy) = define_vvsubst_consts qualify names fp_res vars deadss passives lthy;
+    val ((raw_psetss, psetss, rels_opt), lthy) = define_vvsubst_consts qualify vvsubst_bss fp_res vars deadss passives lthy;
 
     val live = MRBNF_Def.live_of_mrbnf (hd mrbnfs);
     val frees = vars @ pfrees;
@@ -405,9 +423,9 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga
       ])) ctxt
     ])), Position.no_range), NONE) state;
 
-    val (vvsubsts, lthy) = @{fold_map 2} (fn b =>
-      mk_def_t true Binding.empty qualify (Binding.name_of b) 0
-    ) vvsubst_bs (MRBNF_Recursor.get_RECs true "vvsubst" lthy) lthy;
+    val (vvsubsts, lthy) = @{fold_map 3} (fn b => fn T =>
+      mk_def_t true Binding.empty qualify (the_default ("map_" ^ short_type_name (fst (dest_Type T))) (Option.map Binding.name_of b)) 0
+    ) (map #vvsubst vvsubst_bss) (map #T (#quotient_fps fp_res)) (MRBNF_Recursor.get_RECs true "vvsubst" lthy) lthy;
 
     val vvsubst_cctors = @{map 6} (fn vvsubst => fn quot => fn bsets => fn mrbnf => fn x => fn deads =>
       let
@@ -451,7 +469,7 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga
       let
         val (_, lthy) = Local_Theory.begin_nested lthy;
         val (picks, lthy) =
-          @{fold_map 4} (fn quot => fn psets => fn vvsubst => fn b => fn lthy =>
+          @{fold_map 3} (fn quot => fn psets => fn vvsubst => fn lthy =>
             let
               fun mk_Eps f =
                 let val f_T = fastype_of f;
@@ -487,8 +505,8 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga
                   ))
                 )
               );
-            in mk_def_t false b qualify "pick" (length fs + 1) rhs lthy end
-          ) (#quotient_fps fp_res) psetss vvsubsts vvsubst_bs lthy;
+            in mk_def_t false (Binding.name ("vvsubst_" ^ short_type_name (fst (dest_Type (#T quot))))) qualify "pick" (length fs + 1) rhs lthy end
+          ) (#quotient_fps fp_res) psetss vvsubsts lthy;
 
         val (lthy, old_lthy) = `Local_Theory.end_nested lthy;
         val phi = Proof_Context.export_morphism old_lthy lthy;

Tools/parser.ML

@@ -36,15 +36,16 @@ val parse_type_args_named_constrained =
 
 val parse_subst_binding = Parse.name --| \<^keyword>\<open>:\<close> -- Parse.binding;
 
-fun extract_map_rel_pred ("vvsubst", m) = (fn (_, r, p) => (m, r, p))
-  | extract_map_rel_pred ("tvsubst", r) = (fn (m, _, p) => (m, r, p))
-  | extract_map_rel_pred ("permute", p) = (fn (m, r, _) => (m, r, p))
+fun extract_map_rel_pred ("map", m) = (fn (_, r, p, rel) => (m, r, p, rel))
+  | extract_map_rel_pred ("subst", r) = (fn (m, _, p, rel) => (m, r, p, rel))
+  | extract_map_rel_pred ("permute", p) = (fn (m, r, _, rel) => (m, r, p, rel))
+  | extract_map_rel_pred ("rel", rel) = (fn (m, r, p, _) => (m, r, p, rel))
   | extract_map_rel_pred (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"vvsubst\" or \"tvsubst\")");
 
 val parse_subst_bindings =
   @{keyword for} |-- Scan.repeat parse_subst_binding
-    >> (fn ps => fold extract_map_rel_pred ps (Binding.empty, Binding.empty, Binding.empty))
-  || Scan.succeed (Binding.empty, Binding.empty, Binding.empty);
+    >> (fn ps => fold extract_map_rel_pred ps (Binding.empty, Binding.empty, Binding.empty, Binding.empty))
+  || Scan.succeed (Binding.empty, Binding.empty, Binding.empty, Binding.empty);
 
 val parse_binder_datatype = Parse.and_list1 (
   parse_type_args_named_constrained -- Parse.binding -- Parse.opt_mixfix --
@@ -149,7 +150,7 @@ fun create_ctor_spec T_names ((((sel, name), xs), mixfix), binds) (lthy, params)
     val spec = ((Binding.name_of name, mixfix), Ts)
    in (spec, (lthy, params)) end
 
-fun create_binder_spec T_names ((((params, b), mixfix), ctors), (vvsubst_b, tvsubst_b, permute_b)) lthy =
+fun create_binder_spec T_names ((((params, b), mixfix), ctors), (vvsubst_b, tvsubst_b, permute_b, rel_b)) lthy =
   let
     fun prepare_type_arg (T, sort) =
       let val TFree (s, _) = Syntax.parse_typ lthy T
@@ -161,7 +162,7 @@ fun create_binder_spec T_names ((((params, b), mixfix), ctors), (vvsubst_b, tvsu
 
     val lthy = fold (Variable.declare_typ o snd) Ts lthy;
 
-    val FVars_bs = map (snd o fst) Ts;
+    val set_bs = map (snd o fst) Ts;
     val params = fold (fn ((ann, _), T) => Symtab.map_entry (case ann of
       NONE => "plive" | SOME MRBNF_Def.Free_Var => "pfree"
       | SOME MRBNF_Def.Bound_Var => "pbound" | _ => "dead"
@@ -211,10 +212,11 @@ fun create_binder_spec T_names ((((params, b), mixfix), ctors), (vvsubst_b, tvsu
         in (bfree, (0 upto length brecs - 1)) end
       ) frees,
       rec_vars = length brecs + length recs,
-      map_b = with_def vvsubst_b @{binding vvsubst},
-      tvsubst_b = with_def tvsubst_b @{binding tvsubst},
+      map_b = with_def vvsubst_b @{binding map},
+      tvsubst_b = with_def tvsubst_b @{binding subst},
+      rel_b = with_def rel_b @{binding rel},
       permute_b = without_def permute_b,
-      FVars_bs = map without_def FVars_bs
+      set_bs = map without_def set_bs
     } : MRBNF_Sugar.spec;
   in (spec, lthy) end
 

case_studies/Infinitary_FOL/InfFOL.thy

@@ -219,7 +219,7 @@ type_synonym var = k
 type_synonym ifol = "var ifol'"
 
 abbreviation (input) subst :: "ifol \<Rightarrow> (var \<Rightarrow> var) \<Rightarrow> ifol" ("_\<lbrakk>_\<rbrakk>" [600, 600] 400) where
-  "subst t \<rho> \<equiv> vvsubst_ifol' \<rho> t"
+  "subst t \<rho> \<equiv> map_ifol' \<rho> t"
 
 lift_definition kmember :: "'a \<Rightarrow> 'a set\<^sub>k \<Rightarrow> bool" (infix "\<in>\<^sub>k" 200) is "bmember" .
 lift_definition k1member :: "'a \<Rightarrow> 'a set\<^sub>k\<^sub>1 \<Rightarrow> bool" (infix "\<in>\<^sub>k\<^sub>1" 200) is "bmember" .
@@ -310,13 +310,13 @@ inductive deduct :: "ifol set\<^sub>k \<Rightarrow> ifol \<Rightarrow> bool" (in
 | ConjE: "\<lbrakk> \<Delta> \<turnstile> Conj F ; f \<in>\<^sub>k\<^sub>1 F \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f"
 | NegI: "\<Delta>,f \<turnstile> \<bottom> \<Longrightarrow> \<Delta> \<turnstile> Neg f"
 | NegE: "\<lbrakk> \<Delta> \<turnstile> Neg f ; \<Delta> \<turnstile> f \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> \<bottom>"
-| AllI: "\<lbrakk> \<Delta> \<turnstile> f ; set\<^sub>k\<^sub>2 V \<inter> \<Union>(FVars_ifol' ` set\<^sub>k \<Delta>) = {} \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> All V f"
+| AllI: "\<lbrakk> \<Delta> \<turnstile> f ; set\<^sub>k\<^sub>2 V \<inter> \<Union>(set_ifol' ` set\<^sub>k \<Delta>) = {} \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> All V f"
 | AllE: "\<lbrakk> \<Delta> \<turnstile> All V f ; supp \<rho> \<subseteq> set\<^sub>k\<^sub>2 V \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f\<lbrakk>\<rho>\<rbrakk>"
 
 lemma permute_vvsubst[equiv]:
   fixes f \<rho>::"k \<Rightarrow> k"
   assumes "bij f" "|supp f| <o |UNIV::k set|" "|supp \<rho>| <o |UNIV::k set|"
-  shows "permute_ifol' f (vvsubst_ifol' \<rho> x) = vvsubst_ifol' (\<lambda>x. f (\<rho> (inv f x))) (permute_ifol' f x)"
+  shows "permute_ifol' f (map_ifol' \<rho> x) = map_ifol' (\<lambda>x. f (\<rho> (inv f x))) (permute_ifol' f x)"
 proof -
   have "|supp (f \<circ> \<rho> \<circ> inv f)| <o |UNIV::k set|"
     using assms by (meson ifol'_pre.supp_comp_bound supp_inv_bound)
@@ -363,7 +363,7 @@ binder_inductive deduct
      apply (elim exE conjE)
     apply simp
     subgoal for \<Delta> f V
-      apply (rule exE[OF refresh[of V "\<Union>(FVars_ifol' ` set\<^sub>k \<Delta>) \<union> FVars_ifol' (All V f)", unfolded ifol'.set
+      apply (rule exE[OF refresh[of V "\<Union>(set_ifol' ` set\<^sub>k \<Delta>) \<union> set_ifol' (All V f)", unfolded ifol'.set
               Un_Diff Diff_idemp
               ]])
         apply blast
@@ -432,7 +432,7 @@ binder_inductive deduct
     subgoal premises prems for V f \<rho>
     proof -
       define X where "X \<equiv> set\<^sub>k\<^sub>2 V"
-      let ?O = "\<Union> (FVars_ifol' ` set\<^sub>k \<Delta>) \<union> \<rho> ` FVars_ifol' f \<union> imsupp \<rho> \<union> X \<union> (FVars_ifol' f - set\<^sub>k\<^sub>2 V)"
+      let ?O = "\<Union> (set_ifol' ` set\<^sub>k \<Delta>) \<union> \<rho> ` set_ifol' f \<union> imsupp \<rho> \<union> X \<union> (set_ifol' f - set\<^sub>k\<^sub>2 V)"
       have osmall: "|?O| <o |UNIV::var set|"
         apply (intro infinite_class.Un_bound)
         apply (meson ifol'.set_bd_UNIV set\<^sub>k.set_bd var_class.UN_bound)
@@ -475,7 +475,7 @@ binder_inductive deduct
       moreover have "supp \<sigma> \<subseteq> X \<union> W'" using \<sigma>(2) unfolding id_on_def by (meson UnI1 UnI2 \<sigma>_def not_in_supp_alt subsetI)
       ultimately have \<sigma>_small: "|supp \<sigma>| <o |UNIV::var set|" using card_of_subset_bound by blast
 
-      define \<rho>' where "\<rho>' \<equiv> \<lambda>x. if x \<in> \<sigma> ` FVars_ifol' f then (\<rho> \<circ> \<sigma>) x else x"
+      define \<rho>' where "\<rho>' \<equiv> \<lambda>x. if x \<in> \<sigma> ` set_ifol' f then (\<rho> \<circ> \<sigma>) x else x"
       have "supp \<rho>' \<subseteq> supp (\<rho> \<circ> \<sigma>)" unfolding \<rho>'_def supp_def by auto
       then have \<rho>'_small: "|supp \<rho>'| <o |UNIV::var set|"
         by (meson \<sigma>_small card_of_subset_bound ifol'_pre.supp_comp_bound prems(3) ordLess_ordLeq_trans[OF set\<^sub>k\<^sub>2.set_bd] var_set\<^sub>k\<^sub>2_class.large')
@@ -527,7 +527,7 @@ binder_inductive deduct
             apply (rule refl)
 
            apply (unfold set\<^sub>k\<^sub>2.set_map)
-           apply (subgoal_tac "supp (\<rho> \<circ> \<sigma>) \<inter> \<sigma> ` FVars_ifol' f \<subseteq> \<sigma> ` set\<^sub>k\<^sub>2 V")
+           apply (subgoal_tac "supp (\<rho> \<circ> \<sigma>) \<inter> \<sigma> ` set_ifol' f \<subseteq> \<sigma> ` set\<^sub>k\<^sub>2 V")
             apply (smt (verit, best) IntI \<rho>'_def not_in_supp_alt subset_iff)
            apply (unfold supp_def imsupp_def)
         using X_def \<sigma>_def apply auto[1]

case_studies/Infinitary_Lambda_Calculus/ILC.thy

@@ -49,8 +49,8 @@ binder_datatype (FFVars: 'a) iterm
   | iApp "'a iterm" "'a iterm stream"
   | iLam "(xs::'a) dstream" t::"'a iterm" binds xs in t
 for
-  vvsubst: ivvsubst
-  tvsubst: itvsubst
+  map: ivvsubst
+  subst: itvsubst
 
 lemma ex_inj_infinite_regular_var_iterm:
   "\<exists>f :: 'a :: countable \<Rightarrow> 'b :: var_iterm. inj f"

case_studies/POPLmark/POPLmark_2B.thy

@@ -15,7 +15,7 @@ print_theorems
 
 thm trm.subst
 
-abbreviation "tvsubst f1 f2 \<equiv> tvsubst_trm f2 f1"
+abbreviation "tvsubst f1 f2 \<equiv> subst_trm f2 f1"
 
 inductive "value" where
   "value (Abs x T t)"

case_studies/POPLmark/SystemFSub.thy

@@ -11,12 +11,15 @@ declare supp_id_bound[simp]
 type_synonym label = string
 
 declare [[mrbnf_internals]]
-binder_datatype 'a "typ" =
+binder_datatype (FVars_typ: 'a) "typ" =
     TyVar 'a
   | Top
   | Fun "'a typ" "'a typ"
   | Forall \<alpha>::'a "'a typ" t::"'a typ" binds \<alpha> in t
   | TRec "(label, 'a typ) lfset"
+    for
+      map: vvsubst_typ
+      subst: tvsubst_typ
 
 declare supp_swap_bound[OF cinfinite_imp_infinite[OF typ.UNIV_cinfinite], simp]
 declare typ.permute_id[simp] typ.permute_id0[simp]

case_studies/Pi_Calculus/Commitment.thy

@@ -2,7 +2,7 @@ theory Commitment
 imports Pi
 begin
 
-binder_datatype 'var commit =
+binder_datatype (FVars_commit: 'var) commit =
     Finp 'var 'var "'var term"
   | Fout 'var 'var "'var term"
   | Bout 'var x::'var "(t::'var) term" binds x in t

case_studies/Pi_Calculus/Pi.thy

@@ -7,7 +7,7 @@ begin
 (* DATATYPE DECLARTION  *)
 
 declare [[mrbnf_internals]]
-binder_datatype 'a "term" =
+binder_datatype (FVars_term: 'a) "term" =
   Zero
 | Sum "'a term" "'a term"
 | Par "'a term" "'a term" (infixl "\<parallel>" 300)
@@ -17,8 +17,8 @@ binder_datatype 'a "term" =
 | Inp 'a x::'a t::"'a term" binds x in t
 | Res x::'a t::"'a term" binds x in t
 for
-  vvsubst: vvsubst
-  tvsubst: tvsubst
+  map: vvsubst
+  subst: tvsubst
 
 (****************************)
 (* DATATYPE-SPECIFIC CUSTOMIZATION  *)

case_studies/STLC/STLC.thy

@@ -6,13 +6,13 @@ datatype \<tau> = Unit | Arrow \<tau> \<tau> (infixr "\<rightarrow>" 40)
 
 declare [[mrbnf_internals]]
 
-binder_datatype 'a terms =
+binder_datatype (FVars_terms: 'a) terms =
   Var 'a
 | App "'a terms" "'a terms"
 | Abs x::'a \<tau> t::"'a terms" binds x in t
 for
-  vvsubst: vvsubst
-  tvsubst: tvsubst
+  map: vvsubst
+  subst: tvsubst
 
 print_theorems