Fix lingering issues of mrsbnf composition

jvanbruegge · jvanbruegge · commit d374a169373b · 2025-08-08T16:34:32.000+01:00
diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML
@@ -603,6 +603,14 @@ fun create_binder_datatype (spec : spec) lthy =
       ])] end
     ) ctors_tys) ctors_tys));
 
+    fun find_bnfs lthy (Type (n, Ts)) xs =
+      let
+        val insert = case BNF_Def.bnf_of lthy n of
+          SOME bnf => insert ((op=) o apply2 fst) (n, bnf) | NONE => I
+      in insert (fold (find_bnfs lthy) Ts xs) end
+      | find_bnfs _ _ xs = xs
+    val bnfs = fold (find_bnfs lthy) (maps (map (Term.typ_subst_atomic replace) o snd) ctors_tys) [];
+
     val injects = @{map_filter 2} (fn ((ctor, ctor_def), tys) => fn setss => if null tys then NONE else
       let
         val bound_tys = inter (op=) bounds (rev (map TFree (fold Term.add_tfreesT tys [])));
@@ -677,6 +685,7 @@ fun create_binder_datatype (spec : spec) lthy =
           K (Local_Defs.unfold0_tac ctxt (
             @{thms map_sum.simps map_prod_simp sum.inject prod.inject id_apply}
             @ set_simp_thms
+            @ map (BNF_Def.map_id_of_bnf o snd) bnfs
             @ maps MRBNF_Def.set_map_of_mrbnf fp_nesting_mrbnfs
             @ map MRBNF_Def.map_id_of_mrbnf fp_nesting_mrbnfs
             @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
@@ -1052,7 +1061,8 @@ fun create_binder_datatype (spec : spec) lthy =
         ) (MRBNF_Def.map_of_mrbnf rec_mrbnf);
         fun tac ctxt prems = EVERY1 [
           rtac ctxt (trans OF [#vvsubst_ctor vvsubst_res]),
-          K (Local_Defs.unfold0_tac ctxt (thms @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf @ [
+          K (Local_Defs.unfold0_tac ctxt (thms @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
+            @ map (BNF_Def.map_id_of_bnf o snd) bnfs @ [
             MRBNF_Def.map_def_of_mrbnf pre_mrbnf,
             #Abs_inverse (snd info) OF @{thms UNIV_I},
             snd (#noclash (hd (#quotient_fps res)))
@@ -1086,13 +1096,14 @@ fun create_binder_datatype (spec : spec) lthy =
         val mapx = Term.subst_atomic_types (Ts' ~~ (vars @ passives)) (#permute quotient);
         fun tac ctxt prems = EVERY1 [
           rtac ctxt (trans OF [#permute_ctor quotient]),
-          K (Local_Defs.unfold0_tac ctxt (thms @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf @ [
+          K (Local_Defs.unfold0_tac ctxt (thms @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
+            @ map (BNF_Def.map_id_of_bnf o snd) bnfs @ [
             MRBNF_Def.map_def_of_mrbnf pre_mrbnf,
             #Abs_inverse (snd info) OF @{thms UNIV_I}
           ])),
           REPEAT_DETERM o resolve_tac ctxt prems,
           REPEAT_DETERM o EVERY' [
-            EqSubst.eqsubst_tac ctxt [0] (map #map_permute nesting_binder_sugars),
+            EqSubst.eqsubst_tac ctxt [0] (@{print}(map #map_permute nesting_binder_sugars)),
             REPEAT_DETERM o resolve_tac ctxt prems
           ],
           K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
@@ -1139,6 +1150,7 @@ fun create_binder_datatype (spec : spec) lthy =
                 REPEAT_DETERM o resolve_tac ctxt prems,
                 K (Local_Defs.unfold0_tac ctxt (thms
                   @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
+                  @ map (BNF_Def.map_id_of_bnf o snd) bnfs
                   @ #isVVrs tvsubst_res @ map snd (#VVrs tvsubst_res)
                   @ [#Abs_inverse (snd info) OF @{thms UNIV_I}, snd (#noclash quotient)]
                 )),
@@ -1162,7 +1174,9 @@ fun create_binder_datatype (spec : spec) lthy =
                   ])),
                   eresolve_tac ctxt @{thms sum.distinct[THEN notE]}
                 ],
-                K (Local_Defs.unfold0_tac ctxt (map MRBNF_Def.map_id0_of_mrbnf fp_nesting_mrbnfs)),
+                K (Local_Defs.unfold0_tac ctxt (map MRBNF_Def.map_id0_of_mrbnf fp_nesting_mrbnfs
+                  @ map (BNF_Def.map_id_of_bnf o snd) bnfs
+                )),
                 K (Local_Defs.unfold0_tac ctxt @{thms id_def}),
                 rtac ctxt refl
               ]
diff --git a/Tools/mrsbnf_comp.ML b/Tools/mrsbnf_comp.ML
@@ -51,16 +51,17 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
     val bmv = MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf;
     val mrbnf' = nth (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf) (BMV_Monad_Def.leader_of_bmv_monad bmv);
 
-    val (_, _, (mrbnfs', (_, lthy))) = MRBNF_Comp.normalize_mrbnfs (K I) [] [map dest_TFree (snd tys)]
+    val ((_, _, new_tys), _, (mrbnfs', (_, lthy))) = MRBNF_Comp.normalize_mrbnfs (K I) [] [map dest_TFree (snd tys)]
       [] Xs (K (map fst Xs)) NONE [mrbnf'] ((MRBNF_Comp.empty_comp_cache, mrbnf_unfolds), lthy);
     val mrbnf' = hd mrbnfs';
     val ((mrbnf, info, (Ds, absT_info)), lthy) = MRBNF_Comp.seal_mrbnf qualify mrbnf_unfolds name true Ds Ds mrbnf' info_opt lthy;
 
     val var_class = MRBNF_Def.class_of_mrbnf mrbnf;
     val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf';
-    val (lives, bounds, frees) = MRBNF_Def.deinterlace (snd tys) var_types;
+    val (lives, bounds, frees) = MRBNF_Def.deinterlace (map TFree new_tys) var_types;
     val bounds = map (resort_tfree_or_tvar var_class) bounds;
     val frees = map (resort_tfree_or_tvar var_class) frees;
+
     val rep_T = MRBNF_Def.mk_T_of_mrbnf Ds lives bounds frees mrbnf';
 
     val (lives', _) = lthy
@@ -137,7 +138,8 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
           rtac ctxt copy,
           rtac ctxt copy,
           K (Local_Defs.unfold0_tac ctxt (comp_assocs @ [@{thm type_copy_Rep_o_Abs_o} OF [copy]])),
-          rtac ctxt (unfold_defs thm) THEN_ALL_NEW assume_tac ctxt
+          rtac ctxt (unfold_defs thm),
+          REPEAT_DETERM o assume_tac ctxt
         ]) (#map_Sb axioms),  
         map_Injs = Option.map (map (fn thm => fn ctxt => EVERY1 [
           K (Local_Defs.unfold0_tac ctxt defs),
@@ -153,7 +155,8 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
             rtac ctxt copy,
             K (Local_Defs.unfold0_tac ctxt (comp_assocs @ [@{thm type_copy_Rep_o_Abs_o} OF [copy]]))
           ],
-          rtac ctxt (unfold_defs (#map_is_Sb axioms)) THEN_ALL_NEW assume_tac ctxt
+          rtac ctxt (unfold_defs (#map_is_Sb axioms)),
+          REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id})
         ],
         set_Sb = map (fn _ => fn ctxt => EVERY1 [
           K (Local_Defs.unfold0_tac ctxt (defs @ [@{thm SSupp_type_copy} OF [copy]])),
@@ -163,15 +166,17 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
           REPEAT_DETERM o assume_tac ctxt,
           K (Local_Defs.unfold0_tac ctxt @{thms comp_def}),
           rtac ctxt refl
-        ]) (#set_Sb axioms),
-        set_Vrs = map (fn thm => fn ctxt => EVERY1 [
+        ]) (bounds @ lives),
+        set_Vrs = map (K (fn ctxt => EVERY1 [
           K (Local_Defs.unfold_tac ctxt (defs @ [@{thm SSupp_type_copy} OF [copy]])),
           rtac ctxt @{thm trans[OF comp_apply]},
-          rtac ctxt trans,
-          rtac ctxt (unfold_defs thm),
-          K (Local_Defs.unfold0_tac ctxt @{thms comp_def}),
-          rtac ctxt refl
-        ]) (#set_Vrs axioms)
+          rtac ctxt refl ORELSE' EVERY' [
+            rtac ctxt trans,
+            resolve_tac ctxt (map unfold_defs (#set_Vrs axioms)),
+            K (Local_Defs.unfold0_tac ctxt @{thms comp_def}),
+            rtac ctxt refl
+          ]
+        ])) (#set_Vrs axioms)
       }
     ) (MRSBNF_Def.axioms_of_mrsbnf mrsbnf)) lthy;
   in ((mrsbnf, (snd (dest_Type T), absT_info)), lthy) end
@@ -216,8 +221,10 @@ fun compose_mrsbnfs inline_policy fact_policy qualify outer inners oDs Dss oAs A
     val outer_mrbnf = nth (MRSBNF_Def.mrbnfs_of_mrsbnf outer) leader;
     val inner_mrbnfs = map (fn mrsbnf => nth (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf) leader) inners;
 
+    val _ = @{print} "wat"
     val ((mrbnf, tys), (mrbnf_unfolds, lthy)) = MRBNF_Comp.compose_mrbnf MRBNF_Def.Smart_Inline
       qualify flatten_tyargs outer_mrbnf inner_mrbnfs oDs Dss oAs Ass Xs (accum, lthy);
+    val _ = @{print} (tys, MRBNF_Def.T_of_mrbnf mrbnf)
 
     val mrbnf =
       let
diff --git a/Tools/mrsbnf_def.ML b/Tools/mrsbnf_def.ML
@@ -860,18 +860,27 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
     val (fs, names_lthy) = names_lthy
       |> mk_Frees "f" (MRBNF_Def.interlace (map2 (curry (op-->)) As As') (map (fn a => a --> a) Bs) (map (fn a => a --> a) Fs) (MRBNF_Def.var_types_of_mrbnf lmrbnf));
 
+    val subst =
+      (MRBNF_Def.frees_of_mrbnf lmrbnf ~~ Fs)
+      @ (MRBNF_Def.bounds_of_mrbnf lmrbnf ~~ Bs)
+      @ (MRBNF_Def.lives_of_mrbnf lmrbnf ~~ As)
+      @ (MRBNF_Def.lives'_of_mrbnf lmrbnf ~~ As')
+      @ (ldeads ~~ deads)
+    val subst_phi = MRBNF_Util.subst_typ_morphism subst;
+    val mrbnfs = map (MRBNF_Def.morph_mrbnf subst_phi) mrbnfs;
+
     local
-      val subst =
-        (MRBNF_Def.frees_of_mrbnf lmrbnf ~~ Fs)
-        @ (MRBNF_Def.bounds_of_mrbnf lmrbnf ~~ Bs)
-        @ (MRBNF_Def.lives_of_mrbnf lmrbnf ~~ As)
-        @ (MRBNF_Def.lives'_of_mrbnf lmrbnf ~~ As')
-        @ (ldeads ~~ deads)
-      val phi = MRBNF_Util.subst_typ_morphism subst;
+      val T = fastype_of (MRBNF_Def.map_of_mrbnf (hd mrbnfs));
+      val T' = case BMV_Monad_Def.leader BMV_Monad_Def.Maps_of_bmv_monad bmv of
+        SOME Map => fastype_of Map
+        | NONE => fastype_of (BMV_Monad_Def.leader BMV_Monad_Def.Sbs_of_bmv_monad bmv)
+      val tyenv = try (Sign.typ_match (Proof_Context.theory_of lthy)
+        (snd (split_last (binder_types T')) --> body_type T', snd (split_last (binder_types T)) --> body_type T)
+      ) Vartab.empty;
+      val phi = Option.map (fn tyenv => MRBNF_Util.subst_typ_morphism (map (fn (n, (s, T)) => (TVar (n, s), T)) (Vartab.dest tyenv))) tyenv;
     in
-      val mrbnfs = map (MRBNF_Def.morph_mrbnf phi) mrbnfs;
-      val bmv = BMV_Monad_Def.morph_bmv_monad phi bmv;
-    end;
+      val bmv = BMV_Monad_Def.morph_bmv_monad (the_default subst_phi phi) bmv;
+    end
 
     val axioms = @{map 7} (fn mrbnf => fn Sb => fn Injs => fn RVrs => fn Vrs => fn Map_opt => fn lives =>
       let
@@ -888,14 +897,15 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
         val free = length frees;
         val free_fs = take free free_fs';
 
+        val free_prems' = map (HOLogic.mk_Trueprop o mk_supp_bound) free_fs';
         val free_prems = map (HOLogic.mk_Trueprop o mk_supp_bound) free_fs;
         val live_fs' = filter (member (op=) lives o domain_type o fastype_of) live_fs;
 
-        val map_is_Sb = fold_rev Logic.all (free_fs @ live_fs') (fold_rev (curry Logic.mk_implies) free_prems (mk_Trueprop_eq (
+        val map_is_Sb = fold_rev Logic.all (free_fs' @ live_fs') (fold_rev (curry Logic.mk_implies) free_prems' (mk_Trueprop_eq (
           Term.list_comb (Term.subst_atomic_types (filter_out (member (op=) lives o snd) (As' ~~ As)) mapx, MRBNF_Def.interlace
             (map (fn a => the_default (HOLogic.id_const a) (
               List.find (curry (op=) a o domain_type o fastype_of) live_fs'
-            )) As) (map HOLogic.id_const Bs) (free_fs @ map HOLogic.id_const (drop (length frees) Fs))
+            )) As) (map HOLogic.id_const Bs) free_fs'
             (MRBNF_Def.var_types_of_mrbnf mrbnf)
           ),
           let val add_Map = case Map_opt of
@@ -905,9 +915,11 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
                 the (List.find (curry (op=) T o fastype_of) live_fs')
               ) (fst (split_last (binder_types (fastype_of Map)))))
             )
-          in add_Map (Term.list_comb (Sb, map (fn RVr => the (List.find (fn f =>
-              HOLogic.dest_setT (body_type (fastype_of RVr)) = domain_type (fastype_of f)
-            ) fs)) RVrs @ map (fn Inj =>
+          in add_Map (Term.list_comb (Sb, map (fn RVr =>
+            let val T = HOLogic.dest_setT (body_type (fastype_of RVr));
+            in the_default (HOLogic.id_const T) (List.find (fn f =>
+              T = domain_type (fastype_of f)
+            ) free_fs') end) RVrs @ map (fn Inj =>
               HOLogic.mk_comp (Inj, the (List.find (fn f => (op=) (apply2 (domain_type o fastype_of) (Inj, f))) fs))
             ) Injs)
           ) end
@@ -921,14 +933,13 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
           ||>> apfst hd o mk_Frees "x" [body_type (fastype_of Sb)];
 
         val live = MRBNF_Def.live_of_mrbnf mrbnf;
-        val pfree_fs = drop free free_fs';
         val other_prems = flat (MRBNF_Def.interlace (replicate live [])
           (map (fn f => map HOLogic.mk_Trueprop [mk_bij f, mk_supp_bound f]) bound_fs)
-          (replicate free [] @ map (fn f => [HOLogic.mk_Trueprop (mk_supp_bound f)]) pfree_fs)
+          (replicate (length free_fs') [])
           var_types
         );
         val other_fs = flat (MRBNF_Def.interlace (map single live_fs) (map single bound_fs)
-          (replicate free [] @ map single pfree_fs) var_types);
+          (replicate (length free_fs') []) var_types);
 
         val g_prems = map2 (fn Inj => fn g => HOLogic.mk_Trueprop (uncurry mk_ordLess (
           mk_card_of (mk_SSupp Inj $ g), mk_card_of (HOLogic.mk_UNIV (domain_type (fastype_of g)))
@@ -938,7 +949,7 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
         val count = live + MRBNF_Def.free_of_mrbnf mrbnf + MRBNF_Def.bound_of_mrbnf mrbnf;
         val map_Sb = if count - free = 0 then NONE else
           let
-            val map_t = Term.list_comb (mapx, MRBNF_Def.interlace live_fs bound_fs (map HOLogic.id_const frees @ pfree_fs) var_types);
+            val map_t = Term.list_comb (mapx, MRBNF_Def.interlace live_fs bound_fs (map (HOLogic.id_const o domain_type o fastype_of) free_fs') var_types);
             val Sb_t = Term.list_comb (Sb, hs @ gs);
           in SOME (fold_rev Logic.all (other_fs @ hs @ gs) (fold_rev (curry Logic.mk_implies) (other_prems @ h_prems @ g_prems) (mk_Trueprop_eq (
             HOLogic.mk_comp (map_t, Sb_t),
@@ -966,7 +977,7 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
         val set_Sbs =
           let
             val sets' = flat (MRBNF_Def.interlace (map single live_sets) (map single bound_sets)
-              (replicate free [] @ map single (drop free free_sets)) var_types);
+              (replicate (length free_fs') []) var_types);
           in map (fn set => fold_rev Logic.all (hs @ gs @ [x]) (fold_rev (curry Logic.mk_implies) (h_prems @ g_prems) (
             mk_Trueprop_eq (set $ (Term.list_comb (Sb, hs @ gs) $ x), foldl1 mk_Un ((set $ x) ::
               @{map_filter 2} (fn Vrs => fn g => Option.mapPartial (fn mrbnf => Option.map (fn set =>
diff --git a/case_studies/POPLmark/POPLmark_2B.thy b/case_studies/POPLmark/POPLmark_2B.thy
@@ -2,6 +2,7 @@ theory POPLmark_2B
   imports Pattern "HOL-Library.List_Lexorder" "HOL-Library.Char_ord"
 begin
 
+declare [[ML_print_depth=1000]]
 binder_datatype (FTVars: 'tv, FVars: 'v) trm =
     Var 'v
   | Abs x::'v "'tv typ" t::"('tv, 'v) trm" binds x in t
diff --git a/operations/BMV_Composition.thy b/operations/BMV_Composition.thy
@@ -49,12 +49,7 @@ consts Inj_2_T4 :: "'b \<Rightarrow> ('a::var, 'b::var) T4"
 
 ML_file \<open>../Tools/bmv_monad_def.ML\<close>
 
-ML \<open>
-Multithreading.parallel_proofs := 0
-\<close>
-
 declare [[goals_limit=1000]]
-
 declare [[ML_print_depth=1000]]
 
 pbmv_monad "('a, 'b, 'c, 'd, 'e, 'f, 'g) T1"
@@ -800,4 +795,4 @@ let
 in lthy end
 \<close>
 
-end
+end
diff --git a/operations/BMV_Fixpoint.thy b/operations/BMV_Fixpoint.thy
@@ -12,10 +12,6 @@ type_synonym ('tv, 'v, 'btv, 'bv, 'c, 'd) FTerm_pre' =
 
 ML_file \<open>../Tools/mrsbnf_comp.ML\<close>
 
-ML \<open>
-Multithreading.parallel_proofs := 0
-\<close>
-
 local_setup \<open>fn lthy =>
 let
   val T = @{typ "('tv, 'v, 'btv, 'bv, 'c, 'd) FTerm_pre'"};
@@ -1570,4 +1566,4 @@ val x = TVSubst.create_tvsubst_of_mrsbnf
 
 in lthy end\<close>
 
-end
+end
diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy
@@ -170,10 +170,6 @@ axiomatization Sb_LM :: "('a::var \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarr
   and Sb_LM_simp3[simp]: "Sb_LM f1 f2 (App t1 t2) = App (Sb_LM f1 f2 t1) (Sb_LM f1 f2 t2)"
   and Sb_LM_simp4[simp]: "x \<notin> imsupp f1 \<Longrightarrow> x \<notin> IImsupp_LM f2 \<Longrightarrow> Sb_LM f1 f2 (Lam x t) = Lam x (Sb_LM f1 f2 t)"
 
-ML \<open>
-Multithreading.parallel_proofs := 0
-\<close>
-
 lemma Vrs_Un: "FVars_LM t = Vrs_1 t \<union> Vrs_2 t"
   apply (induction t rule: LM.induct)
      apply auto
diff --git a/tests/Regression_Tests.thy b/tests/Regression_Tests.thy
@@ -14,6 +14,7 @@ binder_datatype 'a LLC =
   | Abs x::'a t::"'a LLC" binds x in t
   | Let "(x::'a, t::'a LLC) alist" u::"'a LLC" binds x in t u
 
+declare [[ML_print_depth=1000]]
 (* #70 *)
 datatype ('tv, 'ev, 'rv) type = Type 'tv 'ev 'rv
 binder_datatype ('tv, 'ev, 'rv) type_scheme =
