Add BMV monads

ROOT

@@ -22,6 +22,8 @@ session Binders in "thys" = Prelim +
     MRBNF_Composition
     MRBNF_FP
     MRBNF_Recursor
+    Swapping
+    Support
 
 session Operations in "operations" = Untyped_Lambda_Calculus +
   theories
@@ -36,6 +38,8 @@ session Operations in "operations" = Untyped_Lambda_Calculus +
     VVSubst_Corec
     TVSubst
     Sugar
+    BMV_Monad
+    BMV_Fixpoint
 
 session Tests in "tests" = Case_Studies +
   sessions
@@ -116,3 +120,7 @@ session System_Fsub in "case_studies/POPLmark" = Case_Studies +
     Pattern
     POPLmark_1B
     POPLmark_2B
+
+session STLC in "case_studies/STLC" = Binders +
+  theories
+    STLC

Tools/binder_induction.ML

@@ -121,14 +121,6 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
       | NONE => error "Automatic detection of induction rule is not supported yet, please specify with rule:"
       );
 
-      fun dest_ordLess t =
-        let val t' = case HOLogic.dest_mem t of
-          (t', Const (@{const_name ordLess}, _)) => t'
-          | _ => raise TERM ("dest_ordLess", [t])
-        in HOLogic.dest_prod t' end
-      fun dest_card_of (Const (@{const_name card_of}, _) $ t) = t
-        | dest_card_of t = raise TERM ("dest_card_of", [t])
-
       fun strip_all (Const (@{const_name HOL.All}, _) $ t) = (case t of
         Abs (x, T, t) => let val a = Free (x, T)
           in apfst (curry (op::) a) (strip_all (Term.subst_bound (a, t))) end
@@ -153,8 +145,8 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
           val vars_prems = map (try (
             HOLogic.dest_Trueprop
             #> snd o strip_all
-            #> fst o dest_ordLess
-            #> dest_card_of
+            #> fst o MRBNF_Util.dest_ordLess
+            #> MRBNF_Util.dest_card_of
             #> fst o Term.strip_comb
             #> snd o Term.dest_Var
             #> HOLogic.dest_setT o range_type
@@ -463,6 +455,10 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
                     rotate_tac ~1
                   ],
                   SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms de_Morgan_disj singleton_iff Int_Un_distrib Un_empty}),
+                  REPEAT_DETERM o CHANGED o EVERY' [
+                    SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms conj_assoc}),
+                    SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms conj_assoc[symmetric]})
+                  ],
                   REPEAT_DETERM o EVERY' [
                     etac ctxt conjE,
                     rotate_tac ~2
@@ -471,9 +467,9 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
                 Subgoal.FOCUS_PREMS (fn {context=ctxt, prems=inner_prems, ...} => EVERY1 [
                   DETERM o resolve_tac ctxt (IH :: repeat_mp IH),
                   IF_UNSOLVED o EVERY' [
-                    SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms Un_iff de_Morgan_disj singleton_iff Int_Un_distrib Un_empty}),
+                    K (Local_Defs.unfold0_tac ctxt @{thms notin_Un Un_iff de_Morgan_disj singleton_iff Int_Un_distrib Un_empty}),
                     EVERY' (map (fn inner_prem => EVERY' (map (fn tac => DETERM o tac) [
-                      TRY o rtac ctxt conjI,
+                      REPEAT_DETERM o rtac ctxt conjI,
                       let val x = length (fst (Logic.strip_horn (Thm.prop_of inner_prem)));
                       in REPEAT_DETERM_N x o rtac ctxt @{thm induct_impliesI} end,
                       REPEAT_DETERM o rtac ctxt @{thm induct_forallI},
@@ -484,7 +480,7 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking
                           val simpset = Simplifier.add_cong @{thm imp_cong} (
                             (BNF_Util.ss_only @{thms
                               split_paired_All HOL.simp_thms all_simps HOL.induct_forall_def prod.inject induct_implies_equal_eq
-                              disjoint_single trans[OF arg_cong2[OF Int_commute refl, of "(=)"] disjoint_single]
+                              disjoint_single trans[OF arg_cong2[OF Int_commute refl, of "(=)"] disjoint_single] conj_assoc
                             } ctxt)
                             addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}]
                           )

Tools/binder_inductive.ML

@@ -66,6 +66,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt: (string * string lis
           (MRBNF_Util.subst_typ_morphism (snd (dest_Type (MRBNF_Def.T_of_mrbnf mrbnf)) ~~ Ts))
           mrbnf))
       | collect_params _ = [];
+
     val pot_bind_Ts = foldl1 (fn (xs, ys) => if
       subset (op=) (xs, ys) then ys else union (op=) ys xs
     ) (map collect_params param_Ts);
@@ -78,7 +79,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
@@ -115,7 +116,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) =>
@@ -539,7 +541,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;
@@ -550,7 +552,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt: (string * string lis
             REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
             hyp_subst_tac ctxt,
             REPEAT_DETERM o resolve_tac ctxt (
-              @{thms conjI emp_bound iffD2[OF insert_bound] ordLeq_refl}
+              @{thms conjI emp_bound iffD2[OF insert_bound_UNIV] ordLeq_refl}
               @ infinite_UNIVs @ [Un_bound, UN_bound]
               @ maps (fn thm => [thm, @{thm ordLess_ordLeq_trans} OF [thm]]) (
                 maps set_bd_UNIVs_of_mr_bnfs binder_mr_bnfs

Tools/binder_sugar.ML

@@ -0,0 +1,88 @@
+signature BINDER_SUGAR = sig
+
+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,
+  tvsubst_permute: thm option,
+  bsetss: term option list list,
+  bset_bounds: thm list,
+  pset_ctors: 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 option,
+  subst_simps: thm list option,
+  IImsupp_permute_commutes: thm list option,
+  IImsupp_Diffs: thm list option,
+  tvsubst_permute: thm option,
+  bsetss: term option list list,
+  bset_bounds: thm list,
+  pset_ctors: 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,
+  tvsubst_permute, pset_ctors
+} = {
+  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,
+  tvsubst_permute = Option.map (Morphism.thm phi) tvsubst_permute,
+  bsetss = map (map (Option.map (Morphism.term phi))) bsetss,
+  bset_bounds = map (Morphism.thm phi) bset_bounds,
+  pset_ctors = map (Morphism.thm phi) pset_ctors,
+  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