First working integration of bmv-based substitution

Author: jvanbruegge

Tools/binder_inductive.ML

@@ -61,7 +61,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt: (string * string lis
 
     (* TODO: Nested sugars? *)
     val param_sugars = map (fn T => Option.mapPartial (fn s =>
-      MRBNF_Sugar.binder_sugar_of no_defs_lthy s
+      Binder_Sugar.binder_sugar_of no_defs_lthy s
     ) (try (fn () => fst (dest_Type T)) ())) param_Ts;
 
     val param_frees = map_filter (fn T => Option.map MRBNF_Def.frees_of_mrbnf (
@@ -82,7 +82,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt: (string * string lis
       | collect_binders (Abs (_, _, t)) = collect_binders t
       | collect_binders (t as (t1 $ t2)) = case try (dest_Type o Term.body_type o fastype_of) t of
         NONE => map2 (curry (op@)) (collect_binders t1) (collect_binders t2)
-        | SOME (s, _) => (case MRBNF_Sugar.binder_sugar_of no_defs_lthy s of
+        | SOME (s, _) => (case Binder_Sugar.binder_sugar_of no_defs_lthy s of
             NONE => map2 (curry (op@)) (collect_binders t1) (collect_binders t2)
             | SOME sugar =>
               let
@@ -544,7 +544,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt: (string * string lis
           map_filter (try dest_Type o snd) (fold Term.add_frees (flat bind_ts) [])
         );
 
-        val bset_bounds = maps (fn Type (s, _) => (case MRBNF_Sugar.binder_sugar_of lthy s of
+        val bset_bounds = maps (fn Type (s, _) => (case Binder_Sugar.binder_sugar_of lthy s of
           SOME sugar => #bset_bounds sugar
           | NONE => [])
         | _ => []) param_Ts;

Tools/binder_sugar.ML

@@ -0,0 +1,81 @@
+signature BINDER_SUGAR = sig
+
+type binder_sugar = {
+  map_simps: thm list,
+  set_simpss: thm list list,
+  permute_simps: thm list,
+  map_permute: thm,
+  subst_simps: thm list option,
+  IImsupp_permute_commutes: thm list option,
+  IImsupp_Diffs: thm list option,
+  bsetss: term option list list,
+  bset_bounds: thm list,
+  mrbnf: MRBNF_Def.mrbnf,
+  strong_induct: thm option,
+  distinct: thm list,
+  inject: thm list,
+  ctors: (term * thm) list
+};
+
+val morph_binder_sugar: morphism -> binder_sugar -> binder_sugar;
+
+
+val binder_sugar_of: local_theory -> string -> binder_sugar option
+val register_binder_sugar: string -> binder_sugar -> local_theory -> local_theory
+
+end
+
+structure Binder_Sugar : BINDER_SUGAR = struct
+
+type binder_sugar = {
+  map_simps: thm list,
+  set_simpss: thm list list,
+  permute_simps: thm list,
+  map_permute: thm,
+  subst_simps: thm list option,
+  IImsupp_permute_commutes: thm list option,
+  IImsupp_Diffs: thm list option,
+  bsetss: term option list list,
+  bset_bounds: thm list,
+  mrbnf: MRBNF_Def.mrbnf,
+  strong_induct: thm option,
+  distinct: thm list,
+  inject: thm list,
+  ctors: (term * thm) list
+};
+
+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 } = {
+  map_simps = map (Morphism.thm phi) map_simps,
+  permute_simps = map (Morphism.thm phi) permute_simps,
+  map_permute = Morphism.thm phi map_permute,
+  set_simpss = map (map (Morphism.thm phi)) set_simpss,
+  subst_simps = Option.map (map (Morphism.thm phi)) subst_simps,
+  IImsupp_permute_commutes = Option.map (map (Morphism.thm phi)) IImsupp_permute_commutes,
+  IImsupp_Diffs = Option.map (map (Morphism.thm phi)) IImsupp_Diffs,
+  bsetss = map (map (Option.map (Morphism.term phi))) bsetss,
+  bset_bounds = map (Morphism.thm phi) bset_bounds,
+  mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf,
+  strong_induct = Option.map (Morphism.thm phi) strong_induct,
+  distinct = map (Morphism.thm phi) distinct,
+  inject = map (Morphism.thm phi) inject,
+  ctors = map (MRBNF_Util.map_prod (Morphism.term phi) (Morphism.thm phi)) ctors
+} : binder_sugar;
+
+structure Data = Generic_Data (
+  type T = binder_sugar Symtab.table;
+  val empty = Symtab.empty;
+  fun merge data : T = Symtab.merge (K true) data;
+);
+
+fun register_binder_sugar name sugar =
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.none}
+    (fn phi => Data.map (Symtab.update (name, morph_binder_sugar phi sugar)));
+
+fun binder_sugar_of_generic context =
+  Option.map (morph_binder_sugar (Morphism.transfer_morphism (Context.theory_of context)))
+  o Symtab.lookup (Data.get context);
+
+val binder_sugar_of = binder_sugar_of_generic o Context.Proof;
+
+end

Tools/bmv_monad_def.ML

@@ -2329,8 +2329,18 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
       }]
     } : (Proof.context -> tactic) bmv_monad_model;
 
+    fun set_unfolds thms (BMV {
+      ops, var_class, leader: int, frees, lives, lives', deads, consts, params, bd_infinite_regular_card_order,
+      axioms, facts, ...
+    }) = BMV {
+      ops = ops, var_class = var_class, leader = leader, frees = frees, lives = lives, lives' = lives',
+      deads = deads, consts = consts, params = params, bd_infinite_regular_card_order = bd_infinite_regular_card_order,
+      axioms = axioms, facts = facts, unfolds = thms
+    }
+
     val ((bmv, _), lthy) = bmv_monad_def BNF_Def.Hardly_Inline (K BNF_Def.Note_Some) qualify NONE model lthy;
-    val new_unfolds = map (Local_Defs.unfold0 lthy unfolds) defs;
+    val new_unfolds = map (Local_Defs.unfold lthy unfolds) defs;
+    val bmv = set_unfolds new_unfolds bmv;
 
   in ((bmv, new_unfolds, defs, (T_name, info)), lthy) end