Introduce RVrs to BMV Monads

Author: jvanbruegge

Tools/binder_induction.ML

@@ -448,7 +448,7 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
                     REPEAT_DETERM o rtac ctxt @{thm induct_forallI},
                     rtac ctxt inner_prem ORELSE'
                     EVERY' [
-                      Method.insert_tac ctxt [inner_prem],
+                      Method.insert_tac ctxt inner_prems,
                       let
                         val simpset = Simplifier.add_cong @{thm imp_cong} (
                           (BNF_Util.ss_only @{thms

Tools/binder_inductive.ML

@@ -119,7 +119,8 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt: (string * string lis
           val intro = unvarify_global (Term.subst_TVars subst (Thm.prop_of intro));
           val binderss = map (distinct (op=)) (collect_binders intro);
           val xs_binders = map (fn binders => fold_rev (fn t => fn (a, b) => case t of
-            Const (@{const_name insert}, _) $ x $ Const (@{const_name bot}, _) => (x::a, b)
+            Const (@{const_name insert}, _) $ x $ Const (@{const_name bot}, _) => (case x of
+              Bound _ => (a, b) | _ => (x::a, b))
             | _ => (a, t::b)
           ) binders ([], [])) binderss;
           val binders = map (fn (xs, binders) =>

Tools/bmv_monad_def.ML

@@ -154,7 +154,7 @@ fun note_mrsbnf_thms fact_policy qualify name_opt mrsbnf lthy =
 fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs bmv axioms' lthy =
   let
     val names = map (fst o dest_Free);
-    val facts' = @{map 7} (fn axioms => fn mrbnf => fn bmv_axioms => fn bmv_facts => fn Sb => fn Injs => fn SSupps =>
+    val facts' = @{map 8} (fn axioms => fn mrbnf => fn bmv_axioms => fn bmv_facts => fn Sb => fn Injs => fn RVrs => fn SSupps =>
       let
         val mapx = MRBNF_Def.map_of_mrbnf mrbnf;
         val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf;
@@ -168,8 +168,11 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
         ) fs var_types));
         val (live_fs, bound_fs, free_fs) = MRBNF_Def.deinterlace fs var_types;
 
-        val (((gs, aa), x), _) = lthy
-          |> mk_Frees "g" (map fastype_of Injs)
+        val RVrs_aTs = map (HOLogic.dest_setT o body_type o fastype_of) RVrs;
+
+        val ((((hs, gs), aa), x), _) = lthy
+          |> mk_Frees "h" (map (fn a => a --> a) RVrs_aTs)
+          ||>> mk_Frees "g" (map fastype_of Injs)
           ||>> mk_Frees "a" (map (domain_type o fastype_of) Injs)
           ||>> apfst hd o mk_Frees "x" [T];
         val frees = inter (op=) Fs (MRBNF_Def.frees_of_mrbnf mrbnf);
@@ -182,20 +185,23 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
         )) SSupps gs;
         fun find_f T = List.find (fn f => T = domain_type (fastype_of f)) fs;
 
+        val h_fs = map (the o find_f o domain_type o fastype_of) hs;
+        val h_prems = map (HOLogic.mk_Trueprop o mk_supp_bound) hs;
+
         val Sb_comp_right =
           let
             val fs' = map (the o find_f o domain_type o fastype_of) gs;
             val f'_prems = map (HOLogic.mk_Trueprop o mk_supp_bound) fs';
             val goal = Term.subst_atomic_types (As' ~~ As) (mk_Trueprop_eq (
-              Term.list_comb (Sb, map2 (curry HOLogic.mk_comp) gs fs'),
+              Term.list_comb (Sb, map2 (curry HOLogic.mk_comp) (hs @ gs) (h_fs @ fs')),
               HOLogic.mk_comp (
-                Term.list_comb (Sb, gs),
+                Term.list_comb (Sb, hs @ gs),
                 Term.list_comb (mapx, map (fn T => case List.find (fn f => (domain_type T) = domain_type (fastype_of f)) fs' of
                   SOME f => f | NONE => HOLogic.id_const (domain_type T)
                 ) (fst (split_last (binder_types (fastype_of mapx)))))
               )
             ));
-          in Goal.prove_sorry lthy (names (fs' @ gs)) (f'_prems @ g_prems) goal (fn {context=ctxt, prems} => EVERY1 [
+          in Goal.prove_sorry lthy (names (fs' @ hs @ gs)) (f'_prems @ h_prems @ g_prems) goal (fn {context=ctxt, prems} => EVERY1 [
             EqSubst.eqsubst_tac ctxt [0] [#map_is_Sb axioms],
             REPEAT_DETERM o resolve_tac ctxt prems,
             rtac ctxt sym,
@@ -276,9 +282,9 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
         } end
     ) axioms' mrbnfs (BMV_Monad_Def.axioms_of_bmv_monad bmv) (BMV_Monad_Def.facts_of_bmv_monad bmv)
       (BMV_Monad_Def.Sbs_of_bmv_monad bmv) (BMV_Monad_Def.Injs_of_bmv_monad bmv)
-      (BMV_Monad_Def.SSupps_of_bmv_monad bmv);
+      (BMV_Monad_Def.RVrs_of_bmv_monad bmv) (BMV_Monad_Def.SSupps_of_bmv_monad bmv);
 
-    val facts' = @{map 8} (fn axioms => fn facts => fn mrbnf => fn bmv_axioms => fn bmv_facts => fn Sb => fn Injs => fn SSupps =>
+    val facts' = @{map 9} (fn axioms => fn facts => fn mrbnf => fn bmv_axioms => fn bmv_facts => fn Sb => fn RVrs => fn Injs => fn SSupps =>
       let
         val mapx = MRBNF_Def.map_of_mrbnf mrbnf;
         val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf;
@@ -288,8 +294,11 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
         val fs = map (fn T => the (List.find (curry (op=) T o fastype_of) fs)) (fst (split_last (binder_types (fastype_of mapx))));
         val (live_fs, bound_fs, free_fs) = MRBNF_Def.deinterlace fs var_types;
 
-        val (((gs, aa), x), _) = lthy
-          |> mk_Frees "g" (map fastype_of Injs)
+        val RVrs_aTs = map (HOLogic.dest_setT o body_type o fastype_of) RVrs;
+
+        val ((((hs, gs), aa), x), _) = lthy
+          |> mk_Frees "h" (map (fn a => a --> a) RVrs_aTs)
+          ||>> mk_Frees "g" (map fastype_of Injs)
           ||>> mk_Frees "a" (map (domain_type o fastype_of) Injs)
           ||>> apfst hd o mk_Frees "x" [T];
         val frees = inter (op=) Fs (MRBNF_Def.frees_of_mrbnf mrbnf);
@@ -299,16 +308,23 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
           mk_ordLess (mk_card_of (SSupp $ g)) (mk_card_of (HOLogic.mk_UNIV (domain_type (fastype_of g))))
         )) SSupps gs;
 
+        fun find_f T = List.find (curry (op=) T o domain_type o fastype_of) fs;
+        val h_prems = map (HOLogic.mk_Trueprop o mk_supp_bound) hs;
+        val h_fs = map (the o find_f o domain_type o fastype_of) hs;
+
+        val infinite_UNIV = @{thm cinfinite_imp_infinite} OF [MRBNF_Def.UNIV_cinfinite_of_mrbnf (hd mrbnfs)];
+
         val map_Sb_strong =
           let
             val map_t = Term.list_comb (mapx, fs);
             val mrbnfs = map (fn Inj =>
               the (List.find (fn mrbnf => body_type (fastype_of (MRBNF_Def.map_of_mrbnf mrbnf)) = body_type (fastype_of Inj)) mrbnfs)
             ) Injs;
-            fun find_f T = List.find (curry (op=) T o domain_type o fastype_of) fs;
             val goal = mk_Trueprop_eq (
-              HOLogic.mk_comp (map_t, Term.list_comb (Sb, gs)),
-              HOLogic.mk_comp (Term.list_comb (Term.subst_atomic_types (As ~~ As') Sb, map2 (fn g => fn mrbnf =>
+              HOLogic.mk_comp (map_t, Term.list_comb (Sb, hs @ gs)),
+              HOLogic.mk_comp (Term.list_comb (Term.subst_atomic_types (As ~~ As') Sb,
+                map2 (fn h => fn f => HOLogic.mk_comp (HOLogic.mk_comp (f, h), mk_inv f)) hs fs @
+                map2 (fn g => fn mrbnf =>
                 let val mapx = MRBNF_Def.map_of_mrbnf mrbnf;
                 in HOLogic.mk_comp (HOLogic.mk_comp (
                   Term.list_comb (mapx,
@@ -324,7 +340,7 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
               (map (fn f => map HOLogic.mk_Trueprop [mk_bij f, mk_supp_bound f]) free_fs) var_types);
             val id_of_f = HOLogic.id_const o domain_type o fastype_of
             val count = live + MRBNF_Def.bound_of_mrbnf mrbnf + MRBNF_Def.free_of_mrbnf mrbnf - length frees;
-          in Goal.prove_sorry lthy (names (fs @ gs)) (f_prems @ g_prems) goal (fn {context=ctxt, prems} => EVERY1 [
+          in Goal.prove_sorry lthy (names (fs @ hs @ gs)) (f_prems @ h_prems @ g_prems) goal (fn {context=ctxt, prems} => EVERY1 [
             if count = 0 then K all_tac else EVERY' [
               rtac ctxt trans,
               rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "(\<circ>)"]},
@@ -365,7 +381,8 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
               rtac ctxt trans,
               rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "(\<circ>)"]},
               rtac ctxt (#Sb_comp_right facts),
-              REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound}
+              REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound supp_comp_bound}
+                @ [infinite_UNIV]
                 @ maps (map_filter I o #SSupp_map_bound) facts' @ prems @ #SSupp_comp_bound bmv_facts
               ),
               K (Local_Defs.unfold0_tac ctxt @{thms comp_assoc}),
@@ -387,8 +404,8 @@ fun mk_mrsbnf fact_policy qualify (deads, As, As', Bs, Fs, fs) name_opt mrbnfs b
         map_Sb_strong = map_Sb_strong
       }: mrsbnf_facts end
     ) axioms' facts' mrbnfs (BMV_Monad_Def.axioms_of_bmv_monad bmv) (BMV_Monad_Def.facts_of_bmv_monad bmv)
-      (BMV_Monad_Def.Sbs_of_bmv_monad bmv) (BMV_Monad_Def.Injs_of_bmv_monad bmv)
-      (BMV_Monad_Def.SSupps_of_bmv_monad bmv);
+      (BMV_Monad_Def.Sbs_of_bmv_monad bmv) (BMV_Monad_Def.RVrs_of_bmv_monad bmv)
+      (BMV_Monad_Def.Injs_of_bmv_monad bmv) (BMV_Monad_Def.SSupps_of_bmv_monad bmv);
 
     val mrsbnf = MRSBNF {
       mrbnfs = mrbnfs,
@@ -447,7 +464,7 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
       ) mrbnfs (BMV_Monad_Def.Sbs_of_bmv_monad bmv) (BMV_Monad_Def.Maps_of_bmv_monad bmv);
     end;
 
-    val axioms = @{map 6} (fn mrbnf => fn Sb => fn Injs => fn SSupps => fn Vrs => fn bmv_frees =>
+    val axioms = @{map 7} (fn mrbnf => fn Sb => fn Injs => fn SSupps => fn RVrs => fn Vrs => fn bmv_frees =>
       let
         val mapx = MRBNF_Def.map_of_mrbnf mrbnf;
         val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf;
@@ -468,7 +485,9 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
             (map HOLogic.id_const As) (map HOLogic.id_const Bs) (free_fs @ map HOLogic.id_const (drop (length frees) Fs))
             (MRBNF_Def.var_types_of_mrbnf mrbnf)
           ),
-          Term.list_comb (Sb, map (fn Inj =>
+          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 =>
             HOLogic.mk_comp (Inj, the (List.find (fn f => (op=) (apply2 (domain_type o fastype_of) (Inj, f))) fs))
           ) Injs)
         )));
@@ -512,12 +531,11 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
             mk_Trueprop_eq (set $ (Term.list_comb (Sb, gs) $ x), set $ x)
           ))) sets' end;
 
-        val Vrs' = bmv_frees ~~ transpose Vrs;
         val set_Vrs = map (fn set =>
           let
             val aT = HOLogic.dest_setT (fastype_of (set $ x));
-            val Vrs = the (AList.lookup (op=) Vrs' aT);
-            val Vrs' = map_filter (Option.map (fn Vrs => Vrs $ x)) Vrs;
+            val Vrs = filter (curry (op=) aT o HOLogic.dest_setT o body_type o fastype_of) (RVrs @ Vrs);
+            val Vrs' = map (fn Vrs => Vrs $ x) Vrs;
           in Logic.all x (mk_Trueprop_eq (set $ x, case Vrs' of
             [] => mk_bot aT
             | _ => foldl1 mk_Un Vrs'
@@ -530,8 +548,8 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
         set_Sb = set_Sbs
       }: term mrsbnf_axioms end
     ) mrbnfs (BMV_Monad_Def.Sbs_of_bmv_monad bmv) (BMV_Monad_Def.Injs_of_bmv_monad bmv)
-      (BMV_Monad_Def.SSupps_of_bmv_monad bmv) (BMV_Monad_Def.Vrs_of_bmv_monad bmv)
-      (BMV_Monad_Def.frees_of_bmv_monad bmv);
+      (BMV_Monad_Def.SSupps_of_bmv_monad bmv) (BMV_Monad_Def.RVrs_of_bmv_monad bmv)
+      (BMV_Monad_Def.Vrs_of_bmv_monad bmv) (BMV_Monad_Def.frees_of_bmv_monad bmv);
 
   in (axioms, (deads, As, As', Bs, Fs, fs), mrbnfs, bmv) end
 

Tools/mrsbnf_def.ML

@@ -9,8 +9,7 @@ type_synonym ('tv, 'v, 'btv, 'bv, 'c, 'd) FTerm_pre' =
   + 'bv * 'tv FType * 'c \<comment>\<open>Lam x::'v \<open>'tv FType\<close> t::\<open>('tv, 'v) FTerm\<close> binds x in t\<close>
   + 'btv * 'c            \<comment>\<open>TyLam a::'tv t::\<open>('tv, 'v) FTerm\<close> binds a in t\<close>"
 
-ML_file \<open>../Tools/mrsbnf_comp.ML\<close>
-
+(*ML_file \<open>../Tools/mrsbnf_comp.ML\<close>*)