Add var class and bound to bmv monad

Tools/binder_induction.ML

@@ -124,14 +124,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
@@ -150,8 +142,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

Tools/bmv_monad_def.ML

@@ -5,7 +5,7 @@ signature BMV_MONAD_DEF = sig
   type 'a bmv_monad_axioms = {
     Sb_Inj: 'a,
     Sb_comp_Injs: 'a list,
-    Sb_comp: 'a,  (* require typeclass on free vars to bound *)
+    Sb_comp: 'a,
     Sb_cong: 'a,
     (* TODO: Add Vrs_bd axiom *)
     Vrs_Injs: 'a list, (* TODO: One per Inj AND var kind *)
@@ -15,6 +15,8 @@ signature BMV_MONAD_DEF = sig
 
   type bmv_monad_model = {
     ops: typ list,
+    bd: term,
+    var_class: class,
     bmv_ops: bmv_monad list,
     frees: typ list,
     lives: typ list,
@@ -27,6 +29,8 @@ signature BMV_MONAD_DEF = sig
   }
 
   val ops_of_bmv_monad: bmv_monad -> typ list;
+  val bd_of_bmv_monad: bmv_monad -> term;
+  val var_class_of_bmv_monad: bmv_monad -> class;
   val leader_of_bmv_monad: bmv_monad -> int;
   val frees_of_bmv_monad: bmv_monad -> typ list;
   val lives_of_bmv_monad: bmv_monad -> typ list;
@@ -38,9 +42,9 @@ signature BMV_MONAD_DEF = sig
   val morph_bmv_monad: morphism -> bmv_monad -> bmv_monad;
 
   val bmv_monad_def: BNF_Def.inline_policy -> (Proof.context -> BNF_Def.fact_policy)
-    -> (binding -> binding) -> bmv_monad_model -> local_theory -> bmv_monad
+    -> (binding -> binding) -> bmv_monad_model -> local_theory -> bmv_monad * local_theory
 
-  val compose_bmv_monad: (binding -> binding) -> bmv_monad -> bmv_monad list -> local_theory -> bmv_monad
+  val compose_bmv_monad: (binding -> binding) -> bmv_monad -> bmv_monad list -> local_theory -> bmv_monad * local_theory
 end
 
 structure BMV_Monad_Def : BMV_MONAD_DEF = struct
@@ -67,9 +71,10 @@ fun morph_bmv_axioms phi {
   Vrs_Sbs = map (Morphism.thm phi) Vrs_Sbs
 } : thm bmv_monad_axioms
 
-(* TODO: Add bound *)
 datatype bmv_monad = BMV of {
   ops: typ list,
+  bd: term,
+  var_class: class,
   leader: int,
   frees: typ list,
   lives: typ list,
@@ -80,11 +85,29 @@ datatype bmv_monad = BMV of {
   axioms: thm bmv_monad_axioms list
 }
 
+fun morph_bmv_monad phi (BMV {
+  ops, bd, var_class, leader, frees, lives, Injs, Sbs, Maps, Vrs, axioms
+}) = BMV {
+  ops = map (Morphism.typ phi) ops,
+  bd = Morphism.term phi bd,
+  leader = leader,
+  var_class = var_class,
+  frees = map (Morphism.typ phi) frees,
+  lives = map (Morphism.typ phi) lives,
+  Injs = map (map (Morphism.term phi)) Injs,
+  Sbs = map (Morphism.term phi) Sbs,
+  Maps = map (Option.map (Morphism.term phi)) Maps,
+  Vrs = map (map (Morphism.term phi)) Vrs,
+  axioms = map (morph_bmv_axioms phi) axioms
+}
+
 datatype supported_functor = Supported_Functor (* TODO *)
 
 fun Rep_bmv (BMV x) = x
 
 val ops_of_bmv_monad = #ops o Rep_bmv
+val bd_of_bmv_monad = #bd o Rep_bmv
+val var_class_of_bmv_monad = #var_class o Rep_bmv;
 val leader_of_bmv_monad = #leader o Rep_bmv
 val frees_of_bmv_monad = #frees o Rep_bmv
 val lives_of_bmv_monad = #lives o Rep_bmv
@@ -95,6 +118,8 @@ val Vrs_of_bmv_monad = #Vrs o Rep_bmv
 
 type bmv_monad_model = {
   ops: typ list,
+  bd: term,
+  var_class: class,
   frees: typ list,
   lives: typ list,
   bmv_ops: bmv_monad list,
@@ -106,19 +131,20 @@ type bmv_monad_model = {
   tacs: (Proof.context -> tactic) bmv_monad_axioms list
 }
 
-fun morph_bmv_monad phi (BMV {
-  ops, leader, frees, lives, Injs, Sbs, Maps, Vrs, axioms
-}) = BMV {
+fun morph_bmv_monad_model phi { ops, bd, var_class, frees, lives, bmv_ops, leader, Injs, Sbs, Maps, Vrs, tacs } = {
   ops = map (Morphism.typ phi) ops,
-  leader = leader,
+  bd = Morphism.term phi bd,
+  var_class = var_class,
   frees = map (Morphism.typ phi) frees,
   lives = map (Morphism.typ phi) lives,
+  bmv_ops = map (morph_bmv_monad phi) bmv_ops,
+  leader = leader,
   Injs = map (map (Morphism.term phi)) Injs,
   Sbs = map (Morphism.term phi) Sbs,
   Maps = map (Option.map (Morphism.term phi)) Maps,
   Vrs = map (map (Morphism.term phi)) Vrs,
-  axioms = map (morph_bmv_axioms phi) axioms
-}
+  tacs = tacs
+} : bmv_monad_model;
 
 fun prove_axioms (model: bmv_monad_model) lthy =
   let
@@ -215,10 +241,23 @@ fun prove_axioms (model: bmv_monad_model) lthy =
 
 fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lthy =
   let
+    val _ = let
+      val var_large = MRBNF_Def.get_class_assumption [#var_class model] "large" lthy;
+      val bd' = snd (dest_comb (dest_card_of (
+        fst (dest_ordLeq (HOLogic.dest_Trueprop (Thm.prop_of var_large)))
+      )));
+      in if bd' <> #bd model then error "var_class does not match bound" else () end
+    val frees = map (fn T => TFree (apsnd (
+      Sign.minimize_sort (Proof_Context.theory_of lthy) o cons (#var_class model)
+    ) (dest_TFree T))) (#frees model);
+    val model = morph_bmv_monad_model (MRBNF_Util.subst_typ_morphism (#frees model ~~ frees)) model;
+
     val axioms = prove_axioms model lthy;
 
     val bmv = BMV {
       ops = #ops model @ maps (#ops o Rep_bmv) (#bmv_ops model),
+      bd = #bd model,
+      var_class = #var_class model,
       leader = #leader model,
       frees = #frees model,
       lives = #lives model,
@@ -228,7 +267,7 @@ fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lth
       Maps = #Maps model @ maps (#Maps o Rep_bmv) (#bmv_ops model),
       axioms = axioms @ maps (#axioms o Rep_bmv) (#bmv_ops model)
     } : bmv_monad;
-  in bmv end
+  in (bmv, lthy) end
 
 (* Cleanup: Throw away op iff any:
 - not the leader

Tools/mrbnf_def.ML

@@ -255,6 +255,8 @@ sig
   val mrbnf_cmd: ((((((((binding * string) * string) * (var_type * string) list) * string)
       * string list) * string option) * string option) * string option) * (Proof.context -> Plugin_Name.filter) ->
     Proof.context -> Proof.state
+
+  val get_class_assumption: string list -> string -> Proof.context -> thm;
 end;
 
 structure MRBNF_Def : MRBNF_DEF =
@@ -1655,14 +1657,13 @@ fun define_mrbnf_consts const_policy fact_policy internal Ds_opt classes_opt map
       in bs ~~ set_rhss end;
     val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs);
 
-    val ((((mrbnf_map_term, raw_map_def),
+    val (((mrbnf_map_term, raw_map_def),
       (mrbnf_set_terms, raw_set_defs)),
-      _ (* (mrbnf_bd_term, raw_bd_def) *)), (lthy, lthy_old)) =
+      (lthy, lthy_old)) =
         no_defs_lthy
         |> Local_Theory.begin_nested |> snd
         |> maybe_define true map_bind_def
         ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
-        ||>> (fn lthy => ((bd_rhs, Drule.reflexive_thm), lthy)) (* maybe_define true bd_bind_def*)
         ||> `Local_Theory.end_nested;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;

Tools/mrbnf_util.ML

@@ -35,6 +35,10 @@ sig
   val mk_ex: string * typ -> term -> term;
   val mk_insert: term -> term -> term;
 
+  val dest_ordLess: term -> term * term;
+  val dest_ordLeq: term -> term * term;
+  val dest_card_of: term -> term;
+
   val strip_ex: term -> (string * typ) list * term
 
   val mk_conj_thms: int -> local_theory -> thm * thm
@@ -99,6 +103,19 @@ fun subst_typ_morphism subst = Morphism.morphism "subst_typ" {
   typ = [K (Term.typ_subst_atomic subst)]
 };
 
+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_ordLeq t =
+  let val t' = case HOLogic.dest_mem t of
+    (t', Const (@{const_name ordLeq}, _)) => t'
+    | _ => raise TERM ("dest_ordLeq", [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 mk_def_t_syn syn public b qualify name n rhs lthy =
   let
     val b' = qualify (Binding.name name);

operations/BMV_Monad.thy

@@ -99,6 +99,8 @@ Multithreading.parallel_proofs := 0
 ML \<open>
 val model_FType = {
   ops = [@{typ "'a::var FType"}],
+  bd = @{term natLeq},
+  var_class = @{class var},
   leader = 0,
   frees = [@{typ "'a::var"}],
   lives = [],
@@ -136,7 +138,7 @@ val model_FType = {
 \<close>
 
 ML \<open>
-val FType_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_FType @{context}
+val FType_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_FType @{context})
 \<close>
 
 
@@ -234,6 +236,8 @@ declare [[ML_print_depth=10000]]
 ML \<open>
 val model_ID = {
   ops = [@{typ "'a"}],
+  bd = @{term natLeq},
+  var_class = @{class var},
   leader = 0,
   frees = [@{typ "'a"}],
   lives = [],
@@ -271,12 +275,14 @@ val model_ID = {
 } : BMV_Monad_Def.bmv_monad_model;
 \<close>
 ML \<open>
-val id_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_ID @{context}
+val id_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_ID @{context})
 \<close>
 
 ML \<open>
 val model_L = {
   ops = [@{typ "'a1 * 'a1 * ('c1 + 'c2)"}],
+  bd = @{term natLeq},
+  var_class = @{class var},
   leader = 0,
   frees = [@{typ "'a1"}, @{typ "'a2"}],
   lives = [@{typ "'c1"}, @{typ "'c2"}],
@@ -335,12 +341,14 @@ val model_L = {
 } : BMV_Monad_Def.bmv_monad_model;
 \<close>
 ML \<open>
-val L_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L @{context}
+val L_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L @{context})
 \<close>
 
 ML \<open>
 val model_L1 = {
   ops = [@{typ "'a1 * 'a2"}],
+  bd = @{term natLeq},
+  var_class = @{class var},
   leader = 0,
   frees = [@{typ "'a1"}, @{typ "'a2"}],
   lives = [],
@@ -405,7 +413,7 @@ val model_L1 = {
 } : BMV_Monad_Def.bmv_monad_model;
 \<close>
 ML \<open>
-val L1_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L1 @{context}
+val L1_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L1 @{context})
 \<close>
 
 (* ML \<open>
@@ -484,6 +492,8 @@ val L2_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_No
 ML \<open>
 val model_L2 = {
   ops = [@{typ "'a1 * 'a2::var FType"}],
+  bd = @{term natLeq},
+  var_class = @{class var},
   leader = 0,
   frees = [@{typ 'a1}, @{typ "'a2::var"}],
   lives = [],
@@ -552,11 +562,9 @@ val model_L2 = {
 } : BMV_Monad_Def.bmv_monad_model;
 \<close>
 ML \<open>
-val L2_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L2 @{context}
+val L2_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L2 @{context})
 \<close>
 
-ML \<open>
-val x = BMV_Monad_Def.compose_bmv_monad I L_bmv [L1_bmv, L2_bmv] @{context}
-\<close>
+local_setup \<open>snd o BMV_Monad_Def.compose_bmv_monad I L_bmv [L1_bmv, L2_bmv]\<close>
 
 end