Add mutual recursion and passive positions to tvsubst

ROOT

@@ -32,6 +32,7 @@ session Binders in "thys" = Prelim +
     "../Tools"
   theories
     MRBNF_Composition
+    MRBNF_FP
     MRBNF_Recursor
     Generic_Barendregt_Enhanced_Rule_Induction
     General_Customization
@@ -43,6 +44,7 @@ session Operations in "operations" = Binders +
     Recursor
     VVSubst
     TVSubst
+    Sugar
 
 session Untyped_Lambda_Calculus in "thys/Untyped_Lambda_Calculus" = Binders +
   theories

Tools/binder_induction.ML

@@ -482,7 +482,7 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
             ]) ctxt
           ] end);
 
-          val rule_thm = Local_Defs.unfold0 ctxt @{thms MRBNF_Recursor.prod_sets_simps triv_forall_equality} rule_thm;
+          val rule_thm = Local_Defs.unfold0 ctxt @{thms MRBNF_FP.prod_sets_simps triv_forall_equality} rule_thm;
           val names = map (fst o dest_Free) (
             fst (BNF_Util.mk_Frees "Bound" (map (K HOLogic.unitT) bound_prems) ctxt)
           );

Tools/mrbnf_recursor.ML

@@ -195,7 +195,7 @@ fun mk_quotient_model quot substitution qmodel =
     binding = #binding qmodel,
     UFVarss = map (Term.abs ("t", #T quot) o subst) (#FVars quot),
     Umap = fold_rev Term.abs (map (pair "f") Ts) (
-      Term.abs ("t", #T quot) (Term.list_comb (#rename quot, map Bound (length Ts downto 1)))
+      Term.abs ("t", #T quot) (Term.list_comb (subst (#rename quot), map Bound (length Ts downto 1)))
     ),
     Uctor = #Uctor qmodel,
     validity = Option.map (fn v => {

Tools/mrbnf_sugar.ML

@@ -429,7 +429,7 @@ fun create_binder_datatype (spec : spec) lthy =
       eta_natural = eta_natural_tac
     };
     val tvsubst_model = {
-      fp_result = res,
+      binding = #tvsubst_b spec,
       etas = map (fn a => Option.map (rpair tvsubst_axioms) (
         List.find (fn t => domain_type (fastype_of t) = a) etas
       )) vars
@@ -586,7 +586,8 @@ fun create_binder_datatype (spec : spec) lthy =
 
     val (lthy, tvsubst_opt) = if not (null (map_filter I (#etas tvsubst_model))) then
       let
-        val (tvsubst_res, lthy) = MRBNF_TVSubst.create_tvsubst_of_mrbnf (#tvsubst_b spec) (Binding.prefix_name "tv") tvsubst_model lthy;
+        val (tvsubst_ress, lthy) = MRBNF_TVSubst.create_tvsubst_of_mrbnf (Binding.prefix_name "tv") res [tvsubst_model] lthy;
+        val tvsubst_res = hd tvsubst_ress;
         val tvsubst_simps =
           let
             val (fs, _) = lthy

Tools/mrbnf_vvsubst.ML

@@ -2046,17 +2046,18 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga
 
     val lthy = fold (fn (mrbnf, quot) => MRBNF_Def.register_mrbnf_raw (fst (dest_Type (#T quot))) mrbnf) (xs ~~ #quotient_fps fp_res) lthy;
 
-    val (notess, lthy) = @{fold_map 3} (fn quot => fn vvsubst_cctor => fn vvsubst_rrename => fn lthy =>
+    val (notess, lthy) = @{fold_map 4} (fn quot => fn vvsubst_cctor => fn vvsubst_rrename => fn pset_simps => fn lthy =>
       let
         val vname = short_type_name (fst (dest_Type (#T quot)));
         val notes =
           [(vname ^ "_cctor", [vvsubst_cctor]),
-           (vname ^ "_vvsubst_rrename", [vvsubst_rrename])
+           (vname ^ "_vvsubst_rrename", [vvsubst_rrename]),
+           (vname ^ "_set_simps", pset_simps)
           ] |> (map (fn (thmN, thms) =>
             ((Binding.name thmN, []), [(thms, [])])
           ));
       in Local_Theory.notes notes lthy end
-    ) (#quotient_fps fp_res) vvsubst_cctors vvsubst_rrenames lthy;
+    ) (#quotient_fps fp_res) vvsubst_cctors vvsubst_rrenames pset_simpss lthy;
 
     val ress = map2 (fn t1 => fn t2 => {
       vvsubst_ctor = t1,

operations/Fixpoint.thy

@@ -1,17 +1,34 @@
 theory Fixpoint
-  imports "Binders.MRBNF_Recursor"
+  imports "Binders.MRBNF_FP"
 begin
 
 (* TODO: Show proofs as apply script *)
+ML \<open>
+val ctor_T1_Ts = [
+  [@{typ 'var}],
+  [@{typ unit}],
+  [@{typ 'tyvar}],
+  [@{typ 'rec}, @{typ 'rec2}],
+  [@{typ 'bvar}, @{typ 'brec}],
+  [@{typ 'btyvar}, @{typ 'brec}],
+  [@{typ 'a}]
+]
+val ctor_T2_Ts = [
+  [@{typ 'var}],
+  [@{typ 'tyvar}],
+  [@{typ 'rec}, @{typ 'rec2}],
+  [@{typ 'bvar}, @{typ "'brec list"}],
+  [@{typ 'btyvar}, @{typ 'brec2}],
+  [@{typ 'b}, @{typ 'rec}]
+]
+\<close>
 
 ML \<open>
-val T1 = @{typ "(('var + unit) + 'tyvar + 'rec * 'rec2) + ('bvar * 'brec + 'btyvar * 'brec2) + 'a"}
-val T2 = @{typ "('var + 'tyvar + 'rec * 'rec2) + 'bvar * 'brec + 'btyvar * 'brec2 + 'b * 'rec"};
+val T1 = BNF_FP_Util.mk_sumprodT_balanced ctor_T1_Ts
+val T2 = BNF_FP_Util.mk_sumprodT_balanced ctor_T2_Ts
 val name1 = "T1";
 val name2 = "T2";
 val rel = [[1,3], [1]];
-(*val T1 = @{typ "'var + unit + 'tyvar + 'rec * 'rec2 + 'bvar * 'brec + 'btyvar * 'brec2 + 'a"}
-val T2 = @{typ "'var + 'tyvar + 'rec * 'rec2 + 'bvar * 'brec + 'btyvar * 'brec2 + 'b * 'rec"};*)
 Multithreading.parallel_proofs := 4
 \<close>