Fix errors from rebase

Author: jvanbruegge

Tools/binder_sugar.ML

@@ -4,7 +4,7 @@ type binder_sugar = {
   map_simps: thm list,
   set_simpss: thm list list,
   permute_simps: thm list,
-  map_permute: thm,
+  map_permute: thm option,
   subst_simps: thm list option,
   IImsupp_permute_commutes: thm list option,
   IImsupp_Diffs: thm list option,
@@ -20,7 +20,6 @@ type binder_sugar = {
 
 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
 
@@ -32,7 +31,7 @@ type binder_sugar = {
   map_simps: thm list,
   set_simpss: thm list list,
   permute_simps: thm list,
-  map_permute: thm,
+  map_permute: thm option,
   subst_simps: thm list option,
   IImsupp_permute_commutes: thm list option,
   IImsupp_Diffs: thm list option,
@@ -52,7 +51,7 @@ fun morph_binder_sugar phi { map_simps, permute_simps, map_permute, set_simpss,
 } = {
   map_simps = map (Morphism.thm phi) map_simps,
   permute_simps = map (Morphism.thm phi) permute_simps,
-  map_permute = Morphism.thm phi map_permute,
+  map_permute = Option.map (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,

Tools/bmv_monad_def.ML

@@ -796,6 +796,7 @@ 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

@@ -13,25 +13,6 @@ type spec = {
   FVars_bs: binding option list
 };
 
-type binder_sugar = {
-  map_simps: thm list,
-  set_simpss: thm list list,
-  permute_simps: thm list,
-  map_permute: thm option,
-  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;
-
 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
 
 val mr_bnf_of: local_theory -> bool -> string -> mr_bnf option;
@@ -41,7 +22,7 @@ val build_permute_for: Proof.context -> term list -> typ list -> typ -> (string
 val create_binder_type : MRBNF_Util.fp_kind -> spec -> local_theory
   -> (MRBNF_FP_Def_Sugar.fp_result * typ * MRSBNF_Def.mrsbnf * MRBNF_Comp.absT_info) * local_theory
 
-val create_binder_datatype : bool -> spec -> local_theory -> binder_sugar * local_theory
+val create_binder_datatype : bool -> spec -> local_theory -> Binder_Sugar.binder_sugar * local_theory
 end
 
 structure MRBNF_Sugar : MRBNF_SUGAR =
@@ -66,57 +47,6 @@ type spec = {
   FVars_bs: binding option list
 };
 
-type binder_sugar = {
-  map_simps: thm list,
-  set_simpss: thm list list,
-  permute_simps: thm list,
-  map_permute: thm option,
-  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 = Option.map (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 (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;
-
 fun add_nesting_mrbnf_names Us =
   let
     fun add (Type (s, Ts)) ss =
@@ -963,9 +893,12 @@ fun create_binder_datatype co (spec : spec) lthy =
       eta_compl_free = eta_compl_free_tac,
       eta_natural = eta_natural_tac
     };
-    val eta_models = map (fn a => Option.map (fn { eta, Inj } => { eta = eta, Inj = Inj, tacs = tvsubst_axioms }) (
-      List.find (fn { eta, ...} => domain_type (fastype_of eta) = a) etas
-    )) vars;
+    val tvsubst_model = {
+      binding = #tvsubst_b spec,
+      etas = map (fn a => Option.map (fn { Inj, eta } => { Inj = Inj, eta = eta, tacs = tvsubst_axioms }) (
+        List.find (fn t => domain_type (fastype_of (#eta t)) = a) etas
+      )) vars
+    };
 
     val thms = @{thms prod.set_map sum.set_map prod_set_simps sum_set_simps UN_empty UN_empty2
       Un_empty_left Un_empty_right UN_singleton comp_def map_sum.simps map_prod_simp
@@ -1177,7 +1110,7 @@ fun create_binder_datatype co (spec : spec) lthy =
           REPEAT_DETERM o resolve_tac ctxt prems,
           REPEAT_DETERM o EVERY' [
             EqSubst.eqsubst_tac ctxt [0] (map (the o #map_permute) nesting_binder_sugars),
-            REPEAT_DETERM o resolve_tac ctxt prems
+            REPEAT_DETERM o resolve_tac ctxt prems                        
           ],
           K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
           rtac ctxt refl
@@ -1189,8 +1122,12 @@ 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 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) eta_models (#QREC_fixed recursor_result) lthy;
+          rec_mrbnf (#vvsubst_ctor vvsubst_res) (#vvsubst_permute vvsubst_res) (#tvsubst_b spec)
+          (#etas tvsubst_model) (#QREC_fixed recursor_result) lthy;
 
         val lthy = BMV_Monad_Def.register_pbmv_monad (fst (dest_Type qT))
           (MRSBNF_Def.bmv_monad_of_mrsbnf (#mrsbnf tvsubst_res)) lthy;
@@ -1240,7 +1177,7 @@ fun create_binder_datatype co (spec : spec) lthy =
 
             val bmv_unfolds = maps BMV_Monad_Def.unfolds_of_bmv_monad bmvs;
             fun tac ctxt prems = EVERY1 [
-              K (Local_Defs.unfold0_tac ctxt (map (Thm.symmetric o snd) (map_filter (Option.map #Inj) eta_models))),
+              K (Local_Defs.unfold0_tac ctxt (map (Thm.symmetric o snd) (map_filter (Option.map #Inj) (#etas tvsubst_model)))),
               EVERY' [
                 resolve_tac ctxt (#tvsubst_Injs tvsubst_res),
                 REPEAT_DETERM o resolve_tac ctxt prems
@@ -1297,18 +1234,17 @@ fun create_binder_datatype co (spec : spec) lthy =
     val induct_attrib = Attrib.internal Position.none (K (Induct.induct_type (fst (dest_Type qT))))
     val equiv = @{attributes [simp, equiv]}
 
-    (*fun unfold_tvsubst res = map_filter (Option.map (
+    val unfold_tvsubst = map (
       Local_Defs.unfold lthy (
         @{thms SSupp_def[symmetric, THEN meta_eq_to_obj_eq, THEN fun_cong]}
         @ map (Thm.symmetric o snd) ctors
         @ [@{lemma "\<Union>((Vrs \<circ> \<rho>) ` SSupp Inj \<rho>) = IImsupp Inj Vrs \<rho>"
             by (auto simp: IImsupp_def)}]
       )
-    ));*)
-<<<<<<< HEAD
+    );
 
-    val IImsupp_permute_commutes = Option.map (fn (res, _) => unfold_tvsubst res (#IImsupp_permute_commutes res)) tvsubst_opt;
-    val IImsupp_Diffs = Option.map (fn (res, _) => unfold_tvsubst res (#IImsupp_Diffs res)) tvsubst_opt;
+    val IImsupp_permute_commutes = Option.map (fn (res, _) => unfold_tvsubst (#IImsupp_permute_commutes res)) tvsubst_opt;
+    val IImsupp_Diffs = Option.map (fn (res, _) => unfold_tvsubst (#IImsupp_Diffs res)) tvsubst_opt;
 
     val (sugar, lthy) = if co then
       let
@@ -1329,7 +1265,7 @@ fun create_binder_datatype co (spec : spec) lthy =
           distinct = [],
           inject = [],
           ctors = []
-        } : binder_sugar;
+        } : Binder_Sugar.binder_sugar;
       in (sugar, lthy) end
     else
       let
@@ -1349,7 +1285,7 @@ fun create_binder_datatype co (spec : spec) lthy =
           distinct = distinct,
           inject = injects,
           ctors = ctors
-        } : binder_sugar;
+        } : Binder_Sugar.binder_sugar;
       in (sugar, lthy) end
 
     val lthy = Binder_Sugar.register_binder_sugar (fst (dest_Type qT)) sugar lthy;

Tools/tvsubst.ML

@@ -603,7 +603,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
         val ((((fs, rhos), hs), x), _) = lthy
           |> mk_Frees "f" (map ((fn a => a --> a) o HOLogic.dest_setT o body_type o fastype_of) (BMV_Monad_Def.leader BMV_Monad_Def.RVrs_of_bmv_monad bmv))
           ||>> mk_Frees "\<rho>" (map fastype_of (BMV_Monad_Def.leader BMV_Monad_Def.Injs_of_bmv_monad bmv))
-          ||>> mk_Frees "h" (replicate 2 (#T quot --> #T quot))
+          ||>> mk_Frees "h" (replicate nrecs (#T quot --> #T quot))
           ||>> apfst hd o mk_Frees "x" [domain_type (fastype_of (#ctor quot))];
 
         val prems = flat (BMV_Monad_Def.mk_small_prems_of_bmv_monad bmv
@@ -671,8 +671,11 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
 
     val rho_prems = Proof_Context.get_thms lthy "f_prems";
 
-    val avoiding_sets = map (foldl1 mk_Un o map_filter I) (transpose IImsuppss);
+    val avoiding_sets = map2 (fn free =>
+      the_default (mk_bot free) o try (foldl1 mk_Un) o map_filter I
+    ) frees (transpose (filter_out null IImsuppss));
 
+    val _ = @{print} "3"
     val Uctor =
       let
         val ctor = #ctor quot;
@@ -793,7 +796,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
         rtac ctxt @{thm trans[OF comp_apply]},
         K (Local_Defs.unfold0_tac ctxt @{thms inv_simp1}),
         rtac ctxt @{thm trans[OF comp_apply]},
-        EqSubst.eqsubst_tac ctxt [0] (map #map_permute sugars),
+        EqSubst.eqsubst_tac ctxt [0] (map (the o #map_permute) sugars),
         REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
         resolve_tac ctxt (map (fn thm => Local_Defs.unfold ctxt @{thms comp_def} (thm RS fun_cong))
           (maps (the_default [] o #IImsupp_permute_commutes) sugars)
@@ -855,9 +858,9 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
         ],
         REPEAT_DETERM o rtac ctxt @{thm Un_mono'},
         SELECT_GOAL (Local_Defs.unfold0_tac ctxt (no_reflexive (#set_Vrs mrsbnf_axioms))),
-        EqSubst.eqsubst_tac ctxt [0] (#Vrs_Sbs bmv_axioms),
+        EqSubst.eqsubst_tac ctxt [0] (#Sb_Inj bmv_axioms :: #Vrs_Sbs bmv_axioms),
         REPEAT_DETERM o resolve_tac ctxt (@{thms supp_id_bound} @ rho_prems),
-        K (Local_Defs.unfold0_tac ctxt @{thms image_id}),
+        K (Local_Defs.unfold0_tac ctxt @{thms image_id id_apply}),
         rtac ctxt @{thm Un_upper1} ORELSE' EVERY' [
           rtac ctxt @{thm subsetI},
           etac ctxt @{thm UN_E},
@@ -893,14 +896,15 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
           rtac ctxt @{thm UN_mono[OF subset_refl]},
           resolve_tac ctxt prems,
           SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms prod.collapse}),
-          eresolve_tac ctxt @{thms UnI1 UnI2}
+          eresolve_tac ctxt @{thms UnI1 UnI2} ORELSE' assume_tac ctxt
         ]
       ]) ctxt
     ])), Position.no_range), NONE) state;
 
     val (tvsubst, lthy) = mk_def_t true Binding.empty I (Binding.name_of tvsubst_b) 0
       (hd (MRBNF_Recursor.get_RECs true "tvsubst" lthy)) lthy;
 
+    val _ = @{print} "4"
     val tvsubst_not_isInj =
       let
         val x = Free ("x", domain_type (fastype_of (#ctor quot)));
@@ -1143,6 +1147,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
       | _ => error "only works for datatypes"
     val fresh_induct = #fresh_induct fp_thms;
 
+    (* needs to account for vars that are not injections on RHS *)
     val FVars_tvsubsts = map (fn FVars =>
       let
         val t = Free ("t", domain_type (fastype_of FVars));
@@ -1159,6 +1164,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
           FVars $ (Term.list_comb (fst tvsubst, map_filter I rhos) $ t),
           foldl1 mk_Un rhss
         );
+        val _ = @{print} (Thm.cterm_of lthy goal)
       in Goal.prove_sorry lthy (names (map_filter I rhos @ [t])) rho_prems' goal (fn {context=ctxt, prems} => EVERY1 [
         DETERM o rtac ctxt (infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) avoiding_sets) fresh_induct),
         REPEAT_DETERM_N nvars o SELECT_GOAL (REPEAT_DETERM (FIRST1 [
@@ -1184,25 +1190,42 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
           EqSubst.eqsubst_tac ctxt [0] (#Vrs_Sbs bmv_axioms),
           REPEAT_DETERM o resolve_tac ctxt (@{thms supp_id_bound} @ prems)
         ],
-        K (Local_Defs.unfold0_tac ctxt (@{thms image_id UN_Un} @ #Vrs_Map (the (BMV_Monad_Def.leader BMV_Monad_Def.params_of_bmv_monad bmv)))),
+        K (Local_Defs.unfold0_tac ctxt (@{thms image_id UN_Un id_apply}
+          @ #Vrs_Map (the (BMV_Monad_Def.leader BMV_Monad_Def.params_of_bmv_monad bmv))
+          @ [#Sb_Inj bmv_axioms]
+        )),
+        K (print_tac ctxt "1"),
         rtac ctxt (mk_Un_cong (nrecs + 1) (length rhss)),
         REPEAT_DETERM o EVERY' [
-          EqSubst.eqsubst_tac ctxt [0] (map_filter (Option.map (#eta_compl_free o #axioms)) defs),
+          EqSubst.eqsubst_tac ctxt [0] (@{print}(map_filter (Option.map (#eta_compl_free o #axioms)) defs)),
+          K (print_tac ctxt "1.1"),
           SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map_filter (Option.map (snd o #isInj)) defs)),
           rotate_tac ~1,
           etac ctxt @{thm contrapos_np},
+          K (print_tac ctxt "1.2"),
           SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{thms not_all not_not comp_def} @ map_filter (Option.map (snd o #Inj)) defs)),
           etac ctxt exE,
           hyp_subst_tac ctxt,
+          K (print_tac ctxt "1.3"),
           rtac ctxt exI,
-          rtac ctxt refl
+          rtac ctxt refl,
+          K (print_tac ctxt "1.35")
+        ],
+        K (Local_Defs.unfold0_tac ctxt (@{thms UN_empty Un_empty_left Un_empty_right image_id}
+          @ the_default [] (Option.map single (#Map_map mrsbnf_facts))
+        )),
+        TRY o EVERY' [
+          EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf),
+          REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
         ],
-        K (Local_Defs.unfold0_tac ctxt @{thms UN_empty Un_empty_left Un_empty_right}),
+        K (Local_Defs.unfold0_tac ctxt (@{thms image_id})),
+        K (print_tac ctxt "1.4"),
         rtac ctxt refl,
         rtac ctxt trans,
         rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "minus"]},
         rtac ctxt @{thm UN_cong},
         Goal.assume_rule_tac ctxt,
+        K (print_tac ctxt "2"),
         REPEAT_DETERM o EVERY' [
           EqSubst.eqsubst_tac ctxt [0] (maps (the_default []) IImsupp_Diffs @ maps (the_default [] o #IImsupp_Diffs) sugars),
           REPEAT_DETERM o (assume_tac ctxt ORELSE' EVERY' [
@@ -1218,12 +1241,16 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
             ])
           ])
         ],
+        K (print_tac ctxt "3"),
         K (Local_Defs.unfold0_tac ctxt @{thms Un_Diff[symmetric]}),
         rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "minus"]},
         K (Local_Defs.unfold0_tac ctxt @{thms UN_UN_flatten UN_Un_distrib[symmetric]}),
         rtac ctxt refl,
-        rtac ctxt @{thm UN_cong},
-        Goal.assume_rule_tac ctxt,
+        TRY o EVERY' [
+          rtac ctxt @{thm UN_cong},
+          Goal.assume_rule_tac ctxt
+        ],
+        K (print_tac ctxt "4"),
         EVERY' (map_filter (Option.map (fn def => EVERY' [
           K (Local_Defs.unfold0_tac ctxt [snd (#isInj def)]),
           etac ctxt exE,
@@ -1234,8 +1261,10 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
           K (Local_Defs.unfold0_tac ctxt (@{thms UN_single UN_empty Un_empty_left Un_empty_right}
             @ maps (the_default []) FVars_Injs
           )),
+          K (print_tac ctxt "5"),
           rtac ctxt refl
-        ])) (rev defs))
+        ])) (rev defs)),
+        K (print_tac ctxt "end")
       ]) end
     ) (#FVarss quot);
 
@@ -1752,7 +1781,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
         );
       in Goal.prove_sorry lthy (names (fs @ map_filter I rhos)) (f_prems @ rho_prems') goal (fn {context=ctxt, prems} => EVERY1 [
         REPEAT_DETERM o EVERY' [
-          EqSubst.eqsubst_tac ctxt [0] (map (fn thm => thm RS sym) (map_permute :: map #map_permute sugars)),
+          EqSubst.eqsubst_tac ctxt [0] (map (fn thm => thm RS sym) (map_permute :: map (the o #map_permute) sugars)),
           REPEAT_DETERM o resolve_tac ctxt prems
         ],
         rtac ctxt (#map_Sb_strong (hd (MRSBNF_Def.facts_of_mrsbnf rec_mrsbnf))),