Add support for passive free variables

Author: jvanbruegge

Tools/binder_sugar.ML

@@ -11,6 +11,7 @@ type binder_sugar = {
   tvsubst_permute: thm option,
   bsetss: term option list list,
   bset_bounds: thm list,
+  pset_ctors: thm list,
   mrbnf: MRBNF_Def.mrbnf,
   strong_induct: thm option,
   distinct: thm list,
@@ -38,6 +39,7 @@ type binder_sugar = {
   tvsubst_permute: thm option,
   bsetss: term option list list,
   bset_bounds: thm list,
+  pset_ctors: thm list,
   mrbnf: MRBNF_Def.mrbnf,
   strong_induct: thm option,
   distinct: thm list,
@@ -47,7 +49,7 @@ type binder_sugar = {
 
 fun morph_binder_sugar phi { map_simps, permute_simps, map_permute, set_simpss, subst_simps, mrbnf,
   strong_induct, distinct, inject, ctors, bsetss, bset_bounds, IImsupp_permute_commutes, IImsupp_Diffs,
-  tvsubst_permute
+  tvsubst_permute, pset_ctors
 } = {
   map_simps = map (Morphism.thm phi) map_simps,
   permute_simps = map (Morphism.thm phi) permute_simps,
@@ -59,6 +61,7 @@ fun morph_binder_sugar phi { map_simps, permute_simps, map_permute, set_simpss,
   tvsubst_permute = Option.map (Morphism.thm phi) tvsubst_permute,
   bsetss = map (map (Option.map (Morphism.term phi))) bsetss,
   bset_bounds = map (Morphism.thm phi) bset_bounds,
+  pset_ctors = map (Morphism.thm phi) pset_ctors,
   mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf,
   strong_induct = Option.map (Morphism.thm phi) strong_induct,
   distinct = map (Morphism.thm phi) distinct,

Tools/bmv_monad_def.ML

@@ -796,7 +796,6 @@ fun note_bmv_monad_thms fact_policy qualify bmv_b_opt bmv lthy =
     val facts = facts_of_bmv_monad bmv;
     val params = params_of_bmv_monad bmv;
     val unfolds = unfolds_of_bmv_monad bmv;
-    val _ = @{print} unfolds
 
     fun note_unless_dont_note (noted, lthy) =
       let val notes =

Tools/mrbnf_sugar.ML

@@ -1121,14 +1121,17 @@ fun create_binder_datatype co (spec : spec) lthy =
 
     val (lthy, tvsubst_opt) = if not (null (map_filter I (#etas tvsubst_model))) andalso not co then
       let
+        val _ = @{print} "before tvsubst"
         val recursor_result = #recursor_result (the vvsubst_res_opt);
         val rec_mrbnf = #rec_mrbnf (the vvsubst_res_opt);
         val vvsubst_res = #vvsubst_res (the vvsubst_res_opt);
 
         val (tvsubst_res, lthy) = TVSubst.create_tvsubst_of_mrsbnf (Binding.prefix_name "tv") res mrsbnf
-          rec_mrbnf (#vvsubst_ctor vvsubst_res) (#vvsubst_permute vvsubst_res) (#tvsubst_b spec)
+          rec_mrbnf (#vvsubst_ctor vvsubst_res) (#vvsubst_permute vvsubst_res) (#pset_ctors (#vvsubst_res (the vvsubst_res_opt))) (#tvsubst_b spec)
           (#etas tvsubst_model) (#QREC_fixed recursor_result) lthy;
 
+        val _ = @{print} "after tvsubst"
+
         val lthy = BMV_Monad_Def.register_pbmv_monad (fst (dest_Type qT))
           (MRSBNF_Def.bmv_monad_of_mrsbnf (#mrsbnf tvsubst_res)) lthy;
         val lthy = MRSBNF_Def.register_mrsbnf (fst (dest_Type qT)) (#mrsbnf tvsubst_res) lthy;
@@ -1261,6 +1264,7 @@ fun create_binder_datatype co (spec : spec) lthy =
           tvsubst_permute = Option.map (#tvsubst_permute o fst) tvsubst_opt,
           bsetss = [],
           bset_bounds = [],
+          pset_ctors = [],
           mrbnf = mrbnf,
           distinct = [],
           inject = [],
@@ -1281,6 +1285,7 @@ fun create_binder_datatype co (spec : spec) lthy =
           tvsubst_permute = Option.map (#tvsubst_permute o fst) tvsubst_opt,
           bsetss = bset_optss,
           bset_bounds = [],
+          pset_ctors = #pset_ctors (#vvsubst_res (the vvsubst_res_opt)),
           mrbnf = mrbnf,
           distinct = distinct,
           inject = injects,