Automatically infer/fix types in pbmv_monad command

Tools/binder_inductive.ML

@@ -547,7 +547,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
             REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
             hyp_subst_tac ctxt,
             REPEAT_DETERM o resolve_tac ctxt (
-              @{thms emp_bound iffD2[OF insert_bound] ordLeq_refl}
+              @{thms 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
@@ -981,4 +981,4 @@ val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>binder_inductive\<close> "derive strengthened induction theorems for inductive predicates"
     (binder_inductive_parser >> binder_inductive_cmd);
 
-end
+end

Tools/bmv_monad_def.ML

@@ -34,6 +34,7 @@ signature BMV_MONAD_DEF = sig
     var_class: class,
     bmv_ops: bmv_monad list,
     frees: typ list,
+    deads: typ list,
     leader: int,
     lives: typ list,
     lives': typ list,
@@ -53,6 +54,7 @@ signature BMV_MONAD_DEF = sig
   val frees_of_bmv_monad: bmv_monad -> typ list;
   val lives_of_bmv_monad: bmv_monad -> typ list;
   val lives'_of_bmv_monad: bmv_monad -> typ list;
+  val deads_of_bmv_monad: bmv_monad -> typ list;
   val Injs_of_bmv_monad: bmv_monad -> term list list;
   val Sbs_of_bmv_monad: bmv_monad -> term list;
   val Maps_of_bmv_monad: bmv_monad -> term option list;
@@ -169,6 +171,7 @@ datatype bmv_monad = BMV of {
   frees: typ list,
   lives: typ list,
   lives': typ list,
+  deads: typ list,
   params: thm bmv_monad_param option list,
   Injs: term list list,
   Sbs: term list,
@@ -178,7 +181,7 @@ datatype bmv_monad = BMV of {
 }
 
 fun morph_bmv_monad phi (BMV {
-  ops, bd, var_class, leader, frees, lives, lives', params, Injs, Sbs, Vrs, axioms,
+  ops, bd, var_class, leader, frees, lives, lives',  deads, params, Injs, Sbs, Vrs, axioms,
   bd_infinite_regular_card_order
 }) = BMV {
   ops = map (Morphism.typ phi) ops,
@@ -188,6 +191,7 @@ fun morph_bmv_monad phi (BMV {
   frees = map (Morphism.typ phi) frees,
   lives = map (Morphism.typ phi) lives,
   lives' = map (Morphism.typ phi) lives',
+  deads = map (Morphism.typ phi) deads,
   params = map (Option.map (morph_bmv_monad_param phi (Morphism.thm phi))) params,
   Injs = map (map (Morphism.term phi)) Injs,
   Sbs = map (Morphism.term phi) Sbs,
@@ -205,6 +209,7 @@ 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
 val lives'_of_bmv_monad = #lives' o Rep_bmv
+val deads_of_bmv_monad = #deads o Rep_bmv
 val Injs_of_bmv_monad = #Injs o Rep_bmv
 val Sbs_of_bmv_monad = #Sbs o Rep_bmv
 val Maps_of_bmv_monad = map (Option.map #Map) o #params o Rep_bmv
@@ -221,6 +226,7 @@ type 'a bmv_monad_model = {
   frees: typ list,
   lives: typ list,
   lives': typ list,
+  deads: typ list,
   params: 'a bmv_monad_param option list,
   bmv_ops: bmv_monad list,
   leader: int,
@@ -232,14 +238,15 @@ type 'a bmv_monad_model = {
 }
 
 fun morph_bmv_monad_model phi f ({ ops, bd, var_class, frees, lives, lives', params, bmv_ops, leader,
-  Injs, Sbs, Vrs, tacs, bd_infinite_regular_card_order }
+  Injs, Sbs, Vrs, tacs, bd_infinite_regular_card_order, deads }
 ) = {
   ops = map (Morphism.typ phi) ops,
   bd = Morphism.term phi bd,
   var_class = var_class,
   frees = map (Morphism.typ phi) frees,
   lives = map (Morphism.typ phi) lives,
   lives' = map (Morphism.typ phi) lives',
+  deads = map (Morphism.typ phi) deads,
   params = map (Option.map (morph_bmv_monad_param phi f)) params,
   bmv_ops = map (morph_bmv_monad phi) bmv_ops,
   leader = leader,
@@ -282,8 +289,8 @@ fun mk_bmv_monad_axioms ops bd Sb Injs Vrs bmv_ops lthy =
 
     val axioms = @{map 4} (fn T => fn Injs => fn Sb => fn Vrs =>
       let
-        val (own_Injs, other_Injs) = partition (fn Inj => member (op=) ops (body_type (fastype_of Inj))) Injs;
-        val is_own_Inj = map (member (op=) ops o body_type o fastype_of) Injs;
+        val (own_Injs, other_Injs) = partition (fn Inj => body_type (fastype_of Inj) = T) Injs;
+        val is_own_Inj = map (curry (op=) T o body_type o fastype_of) Injs;
         val other_idxs = map (fn Inj => find_index (fn T => body_type (fastype_of Inj) = T) Ts) other_Injs;
         val ((((rhos, rhos'), aa), x), _) = lthy
           |> mk_Frees "\<rho>" (map fastype_of Injs)
@@ -539,6 +546,7 @@ fun define_bmv_monad_consts const_policy fact_policy qualify (model: 'a bmv_mona
       frees = #frees model,
       lives = #lives model,
       lives' = #lives' model,
+      deads = #deads model,
       bmv_ops = #bmv_ops model,
       params = params,
       Injs = Injs,
@@ -572,6 +580,7 @@ fun mk_bmv_monad const_policy fact_policy (model: thm bmv_monad_model) lthy =
       frees = #frees model,
       lives = #lives model,
       lives' = #lives' model,
+      deads = #deads model,
       params = #params model @ maps (#params o Rep_bmv) (#bmv_ops model),
       Injs = #Injs model @ maps (#Injs o Rep_bmv) (#bmv_ops model),
       Sbs = #Sbs model @ maps (#Sbs o Rep_bmv) (#bmv_ops model),
@@ -619,6 +628,7 @@ fun mk_thm_model (model: 'a bmv_monad_model) params axioms bd_irco = {
   frees = #frees model,
   lives = #lives model,
   lives' = #lives' model,
+  deads = #deads model,
   bmv_ops = #bmv_ops model,
   params = params,
   Injs = #Injs model,
@@ -666,6 +676,7 @@ fun pbmv_monad_of_bnf bnf lthy =
      frees = [],
      lives = lives,
      lives' = lives',
+     deads = deads,
      bmv_ops = [],
      params = [SOME {
        Map = BNF_Def.mk_map_of_bnf deads lives lives' bnf,
@@ -848,6 +859,7 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
         frees = #frees bmv,
         lives = #lives bmv,
         lives' = #lives' bmv,
+        deads = #deads bmv,
         params = [param],
         Injs = [Injs],
         Sbs = [Sb],
@@ -867,15 +879,19 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
     val frees = distinct (op=) (maps frees_of_bmv_monad (outer :: inners'));
     val outer_Vrs = map (nth (Vrs_of_bmv_monad outer)) idxs;
 
+    val vars = distinct (op=) (map TFree (fold Term.add_tfreesT (ops' @ maps ops_of_bmv_monad inners') []));
+    val lives = distinct (op=) (maps lives_of_bmv_monad inners');
+
     val model = {
       ops = ops',
       bmv_ops = bmv_ops,
       bd = bd_of_bmv_monad outer, (* TODO: compose bounds *)
       bd_infinite_regular_card_order = fn ctxt => rtac ctxt (bd_infinite_regular_card_order_of_bmv_monad outer) 1,
       var_class = var_class_of_bmv_monad outer,
       frees = frees,
-      lives = distinct (op=) (maps lives_of_bmv_monad inners'),
+      lives = lives,
       lives' = distinct (op=) (maps lives'_of_bmv_monad inners'),
+      deads = subtract (op=) (lives @ frees) vars,
       params = replicate (length ops') NONE,
       leader = 0,
       Injs = Injs,
@@ -1014,17 +1030,26 @@ fun pbmv_monad_cmd ((((((b, ops), Sbs), Injs), Vrs), param_opt), bd) lthy =
   let
     val ops = map (Syntax.read_typ lthy) ops;
     val bd = Syntax.read_term lthy bd;
-    val Sbs = map (Syntax.read_term lthy) Sbs;
+    val Sbs = map2 (fn Sb => fn T => Term.subst_atomic_types (
+      map (apply2 TFree) (Term.add_tfreesT (body_type (fastype_of Sb)) [] ~~ Term.add_tfreesT T [])
+      @ map (apply2 TFree) (Term.add_tfreesT (snd (split_last (binder_types (fastype_of Sb)))) [] ~~ Term.add_tfreesT T [])
+    ) Sb) (map (Syntax.read_term lthy) Sbs) ops;
     val frees = distinct (op=) (maps (
       map (fst o dest_funT) o fst o split_last o binder_types o fastype_of
     ) Sbs);
     val Injs = map (map (Syntax.read_term lthy)) Injs;
     val Vrs = map (map (map (fn "_" => NONE | t => SOME (Syntax.read_term lthy t)))) Vrs;
+    val Vrs = map2 (fn T => map (map (Option.map (fn Vrs => Term.subst_atomic_types (
+      map (apply2 TFree) (Term.add_tfreesT (fst (dest_funT (fastype_of Vrs))) [] ~~ Term.add_tfreesT T [])
+    ) Vrs)))) ops Vrs;
 
     val b = if Binding.is_empty b then fst (dest_Type (hd ops)) else Local_Theory.full_name lthy b
 
     val goals = mk_bmv_monad_axioms ops bd Sbs Injs Vrs [] lthy;
 
+    val vars = distinct (op=) (map TFree (fold Term.add_tfreesT ops []));
+    val lives = [];
+
     fun after_qed thmss lthy =
       let
         val thms = map hd thmss;
@@ -1036,6 +1061,7 @@ fun pbmv_monad_cmd ((((((b, ops), Sbs), Injs), Vrs), param_opt), bd) lthy =
           frees = frees,
           lives = [],
           lives' = [],
+          deads = subtract (op=) (lives @ frees) vars,
           bmv_ops = [],
           params = replicate (length ops) NONE,
           Injs = Injs,
@@ -1109,10 +1135,10 @@ val _ =
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword pbmv_monad}
   "register a parametrized bounded multi-variate monad"
-  (parse_opt_binding_colon -- Scan.repeat1 (Scan.unless (Parse.reserved "Sbs") Parse.typ) --|
-    (Parse.reserved "Sbs" -- @{keyword ":"}) -- Scan.repeat1 (Scan.unless (Parse.reserved "Injs") Parse.term) --|
-    (Parse.reserved "Injs" -- @{keyword ":"}) -- Parse.list (Scan.repeat1 (Scan.unless (Parse.reserved "Vrs") Parse.term)) --|
-    (Parse.reserved "Vrs" -- @{keyword ":"}) -- Parse.and_list (Parse.list (
+  (parse_opt_binding_colon -- Parse.and_list1 Parse.typ --|
+    (Parse.reserved "Sbs" -- @{keyword ":"}) -- Parse.and_list1 Parse.term --|
+    (Parse.reserved "Injs" -- @{keyword ":"}) -- Parse.and_list1 (Scan.repeat1 (Scan.unless (Parse.reserved "Vrs") Parse.term)) --|
+    (Parse.reserved "Vrs" -- @{keyword ":"}) -- Parse.and_list1 (Parse.list1 (
       Scan.repeat1 (Scan.unless (Parse.reserved "Map" || Parse.reserved "bd") (Parse.term || Parse.reserved "_"))
     )) --
     Scan.optional (

operations/BMV_Monad.thy

@@ -4,8 +4,6 @@ theory BMV_Monad
    "pbmv_monad" :: thy_goal
 begin
 
-
-
 declare [[mrbnf_internals]]
 binder_datatype 'a FType
   = TyVar 'a
@@ -94,6 +92,8 @@ using assms(3) proof (binder_induction t avoiding: "IImsupp_FType \<rho>''" "IIm
     by (smt (verit, ccfv_threshold) CollectI IImsupp_FType_def SSupp_FType_def Un_iff)
 qed (auto simp: assms(1-2))
 
+declare [[ML_print_depth=1000]]
+
 ML_file \<open>../Tools/bmv_monad_def.ML\<close>
 
 local_setup \<open>fold BMV_Monad_Def.register_bnf_as_pbmv_monad [@{type_name sum}, @{type_name prod}]\<close>
@@ -120,27 +120,34 @@ pbmv_monad "'a::var FType"
   apply (rule Sb_cong_FType[unfolded SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]]; assumption)
   done
 
-typedef ('a1, 'a2, 'c1, 'c2) L = "UNIV :: ('a1 * 'a1 * ('c1 + 'c2)) set"
+typedef ('a1, 'a2, 'c1, 'c2) L' = "UNIV :: ('a1 * 'a1 * ('c1 + 'c2)) set"
   by (rule exI, rule UNIV_I)
 
-(*pbmv_monad "('a1, 'a2, 'c1, 'c2) L"
-  frees: 'a1 'a2
-  Sbs: "\<lambda>f x. Abs_L (map_prod f (map_prod f id) (Rep_L x))"
-  Injs: "id :: 'a1 \<Rightarrow> 'a1"
-  Vrs: "\<lambda>x. case Rep_L x of (x1, x2, _) \<Rightarrow> {x1, x2}"
+declare [[ML_print_depth=1000]]
+pbmv_monad "('a1, 'a2, 'c1, 'c2) L'"                         and 'a1
+  Sbs: "\<lambda>f x. Abs_L' (map_prod f (map_prod f id) (Rep_L' x))" and "id :: ('a1 \<Rightarrow> 'a1) \<Rightarrow> 'a1 \<Rightarrow> 'a1"
+  Injs: "id :: 'a1 \<Rightarrow> 'a1"                                  and "id :: 'a1 \<Rightarrow> 'a1"
+  Vrs: "\<lambda>x. case Rep_L' x of (x1, x2, _) \<Rightarrow> {x1, x2}"        and "\<lambda>x. {x}"
   bd: natLeq
-  lives: 'c1 'c2*)
+              apply (rule infinite_regular_card_order_natLeq)
+             apply (auto simp: Abs_L'_inject Abs_L'_inverse Rep_L'_inverse prod.map_comp comp_def
+      id_def case_prod_beta insert_bound[OF natLeq_Cinfinite]
+      Cinfinite_gt_empty[OF natLeq_Cinfinite]
+      )[4]
+         apply (unfold Abs_L'_inject[OF UNIV_I UNIV_I] case_prod_beta)[1]
+         apply (metis (no_types, lifting) fst_map_prod insertCI prod.collapse snd_map_prod)
+        apply (auto simp: insert_bound[OF natLeq_Cinfinite] Cinfinite_gt_empty[OF natLeq_Cinfinite])
+  done
 
 ML_file \<open>../Tools/pbmv_monad_comp.ML\<close>
 
 ML \<open>
 Multithreading.parallel_proofs := 0
 \<close>
-declare [[ML_print_depth=1000]]
 local_setup \<open>fn lthy =>
   let
     val (bmv, (thms, lthy)) = PBMV_Monad_Comp.pbmv_monad_of_typ true BNF_Def.Smart_Inline (K BNF_Def.Note_Some) I
-      @{typ "'a1 * 'a1 * (('a1 * 'a2) + ('a1 * 'a2 * 'a2 * 'a2 FType))"}
+      @{typ "'a1 * 'a1 * (('a1 * 'a2) + ('a1 * ('a2 * ('a2 * 'a2 FType))))"}
       ([], lthy)
 
     val _ = @{print} (map (map (map (Option.map (Thm.cterm_of lthy o
@@ -250,11 +257,6 @@ typ "('a1, 'a2) L1_M1"
 typ "('a1, 'a2) L1_M2"
 typ "('a1, 'a2) L2_M2"
 
-lemma insert_bound: "Cinfinite r \<Longrightarrow> |A| <o r \<Longrightarrow> |insert x A| <o r"
-  by (metis Card_order_iff_ordLeq_card_of card_of_Field_ordIso card_of_Un_singl_ordLess_infinite1 cinfinite_def insert_is_Un ordLess_ordIso_trans ordLess_ordLeq_trans)
-
-declare [[ML_print_depth=10000]]
-
 ML \<open>
 val id_bmv = the (BMV_Monad_Def.pbmv_monad_of @{context} "BMV_Monad.ID")
 val FType_bmv = the (BMV_Monad_Def.pbmv_monad_of @{context} "BMV_Monad.FType")
@@ -269,6 +271,7 @@ val model_L = {
   frees = [@{typ "'a1"}],
   lives = [@{typ "'c1"}, @{typ "'c2"}],
   lives' = [@{typ "'c1'"}, @{typ "'c2'"}],
+  deads = [],
   bmv_ops = [BMV_Monad_Def.morph_bmv_monad (
     MRBNF_Util.subst_typ_morphism (
       BMV_Monad_Def.frees_of_bmv_monad id_bmv ~~ [@{typ "'a1"}]
@@ -399,6 +402,7 @@ val model_L1 = {
   frees = [@{typ "'a1"}, @{typ "'a2"}],
   lives = [],
   lives' = [],
+  deads = [],
   bmv_ops = [
     BMV_Monad_Def.morph_bmv_monad (
       MRBNF_Util.subst_typ_morphism (
@@ -481,6 +485,7 @@ val model_L2 = {
   frees = [@{typ 'a1}, @{typ "'a2"}],
   lives = [],
   lives' = [],
+  deads = [],
   bmv_ops = [
     BMV_Monad_Def.morph_bmv_monad (
       MRBNF_Util.subst_typ_morphism (

thys/MRBNF_FP.thy

@@ -330,7 +330,7 @@ lemma induct_implies_equal_eq: "HOL.induct_implies (HOL.induct_equal x y) P = (x
 lemma large_imp_infinite: "natLeq \<le>o |UNIV::'a set| \<Longrightarrow> infinite (UNIV::'a set)"
   using infinite_iff_natLeq_ordLeq by blast
 
-lemma insert_bound: "infinite (UNIV::'a set) \<Longrightarrow> |insert x A| <o |UNIV::'a set| \<longleftrightarrow> |A| <o |UNIV::'a set|"
+lemma insert_bound_UNIV: "infinite (UNIV::'a set) \<Longrightarrow> |insert x A| <o |UNIV::'a set| \<longleftrightarrow> |A| <o |UNIV::'a set|"
   by (metis card_of_Un_singl_ordLess_infinite insert_is_Un)
 
 lemma id_on_comp: "id_on A f \<Longrightarrow> id_on A g \<Longrightarrow> id_on A (f \<circ> g)"

thys/POPLmark/SystemFSub.thy

@@ -248,7 +248,7 @@ binder_inductive ty
       [@{term "permute_typ :: (var \<Rightarrow> var) \<Rightarrow> type \<Rightarrow> type"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
       [NONE, NONE, NONE, NONE, SOME [NONE, NONE, NONE, SOME 1, SOME 0, SOME 0]]
       @{thm prems(3)} @{thm prems(2)} @{thms  prems(1)[THEN ty_fresh_extend] id_onD}
-      @{thms emp_bound insert_bound ID.set_bd typ.Un_bound typ.UN_bound typ.set_bd_UNIV infinite_UNIV}
+      @{thms emp_bound insert_bound_UNIV ID.set_bd typ.Un_bound typ.UN_bound typ.set_bd_UNIV infinite_UNIV}
       @{thms typ_inject image_iff} @{thms typ.permute_cong_id context_map_cong_id map_idI}
       @{thms cong[OF cong[OF cong[OF refl[of R]] refl] refl, THEN iffD1, rotated -1] id_onD} @{context}\<close>)
   done

thys/Pi_Calculus/Pi_Transition_Early.thy

@@ -34,7 +34,7 @@ binder_inductive trans
        SOME [SOME 0, NONE, SOME 1, SOME 0, SOME 1],
        SOME [NONE, SOME 2, SOME 0, SOME 0]]
       @{thm prems(3)} @{thm prems(2)} @{thms }
-      @{thms emp_bound singl_bound insert_bound card_of_minus_bound term.Un_bound term.set_bd_UNIV commit.FVars_bd_UNIVs infinite_UNIV bns_bound}
+      @{thms emp_bound singl_bound insert_bound_UNIV card_of_minus_bound term.Un_bound term.set_bd_UNIV commit.FVars_bd_UNIVs infinite_UNIV bns_bound}
       @{thms bij_implies_inject Res_inject Inp_inject Bout_inject FVars_commit_Cmt ns_alt vars_alt Int_Un_distrib}
       @{thms Inp_eq_usub term.permute_cong_id term.permute_cong_id[symmetric] arg_cong2[where f=Cmt, OF _ refl] arg_cong2[where f=Cmt, OF refl]
           action.map_ident_strong cong[OF arg_cong2[OF _ refl] refl, of _ _ Bout] Cmt_rrename_bound_action Cmt_rrename_bound_action_Par}

thys/Pi_Calculus/Pi_Transition_Late.thy

@@ -33,7 +33,7 @@ binder_inductive trans
        SOME [SOME 0, NONE, SOME 1, SOME 0, SOME 1],
        SOME [NONE, SOME 2, SOME 0, SOME 0]]
       @{thm prems(3)} @{thm prems(2)} @{thms }
-      @{thms emp_bound singl_bound insert_bound card_of_minus_bound term.Un_bound term.FVars_bd_UNIVs commit.FVars_bd_UNIVs infinite_UNIV bns_bound}
+      @{thms emp_bound singl_bound insert_bound_UNIV card_of_minus_bound term.Un_bound term.FVars_bd_UNIVs commit.FVars_bd_UNIVs infinite_UNIV bns_bound}
       @{thms bij_implies_inject Res_inject Inp_inject Bout_inject FVars_commit_Cmt ns_alt vars_alt Int_Un_distrib}
       @{thms Inp_eq_usub term.permute_cong term.permute_cong_id term.permute_cong_id[symmetric] arg_cong2[where f=Cmt, OF _ refl] arg_cong2[where f=Cmt, OF refl]
           action.map_ident_strong cong[OF arg_cong2[OF _ refl] refl, of _ _ Bout] Cmt_rrename_bound_action Cmt_rrename_bound_action_Par}
@@ -45,4 +45,4 @@ binder_inductive trans
   done
 print_theorems
 
-end
+end

thys/Prelim/Prelim.thy

@@ -512,6 +512,9 @@ lemma supp_inv_bound:
   unfolding supp_inv[OF b]
   using s card_of_image ordLeq_ordLess_trans by blast
 
+lemma insert_bound: "Cinfinite r \<Longrightarrow> |A| <o r \<Longrightarrow> |insert x A| <o r"
+  by (metis Card_order_iff_ordLeq_card_of card_of_Field_ordIso card_of_Un_singl_ordLess_infinite1 cinfinite_def insert_is_Un ordLess_ordIso_trans ordLess_ordLeq_trans)
+
 lemma Un_Cinfinite_ordLess: "|A| <o r \<Longrightarrow> |B| <o r \<Longrightarrow> Cinfinite r \<Longrightarrow> |A \<union> B| <o r"
   using Un_Cinfinite_bound_strict .
  (* apply (simp add: cinfinite_def) *)