src/HOL/Tools/BNF/bnf_lift.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (19 months ago)
changeset 67091 1393c2340eec
parent 66272 c6714a9562ae
child 69593 3dda49e08b9d
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/BNF/bnf_lift.ML
     2     Author:     Julian Biendarra, TU Muenchen
     3     Author:     Dmitriy Traytel, ETH Zurich
     4     Copyright   2015
     5 
     6 Lifting of BNFs through typedefs.
     7 *)
     8 
     9 signature BNF_LIFT =
    10 sig
    11   datatype lift_bnf_option =
    12     Plugins_Option of Proof.context -> Plugin_Name.filter
    13   | No_Warn_Wits
    14   val copy_bnf:
    15     (((lift_bnf_option list * (binding option * (string * sort option)) list) *
    16       string) * thm option) * (binding * binding * binding) ->
    17       local_theory -> local_theory
    18   val copy_bnf_cmd:
    19     (((lift_bnf_option list * (binding option * (string * string option)) list) *
    20       string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) ->
    21       local_theory -> local_theory
    22   val lift_bnf:
    23     ((((lift_bnf_option list * (binding option * (string * sort option)) list) *
    24       string) * term list option) * thm option) * (binding * binding * binding) ->
    25       ({context: Proof.context, prems: thm list} -> tactic) list ->
    26       local_theory -> local_theory
    27   val lift_bnf_cmd:
    28      ((((lift_bnf_option list * (binding option * (string * string option)) list) *
    29        string) * string list) * (Facts.ref * Token.src list) option) *
    30        (binding * binding * binding) -> local_theory -> Proof.state
    31 end
    32 
    33 structure BNF_Lift : BNF_LIFT =
    34 struct
    35 
    36 open Ctr_Sugar_Tactics
    37 open BNF_Util
    38 open BNF_Comp
    39 open BNF_Def
    40 
    41 
    42 (* typedef_bnf *)
    43 
    44 datatype lift_bnf_option =
    45   Plugins_Option of Proof.context -> Plugin_Name.filter
    46 | No_Warn_Wits;
    47 
    48 fun typedef_bnf thm wits specs map_b rel_b pred_b opts lthy =
    49   let
    50     val plugins =
    51       get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
    52       |> the_default Plugin_Name.default_filter;
    53     val no_warn_wits = exists (fn No_Warn_Wits => true | _ => false) opts;
    54 
    55     (* extract Rep Abs F RepT AbsT *)
    56     val (_, [Rep_G, Abs_G, F]) = Term.strip_comb (HOLogic.dest_Trueprop (Thm.prop_of thm));
    57     val typ_Abs_G = dest_funT (fastype_of Abs_G);
    58     val RepT = fst typ_Abs_G; (* F *)
    59     val AbsT = snd typ_Abs_G; (* G *)
    60     val AbsT_name = fst (dest_Type AbsT);
    61     val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar);
    62     val alpha0s = map (TFree o snd) specs;
    63 
    64     val _ = length tvs = length alpha0s orelse
    65       error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name);
    66 
    67     (* instantiate the new type variables newtvs to oldtvs *)
    68     val subst = subst_TVars (tvs ~~ alpha0s);
    69     val typ_subst = typ_subst_TVars (tvs ~~ alpha0s);
    70 
    71     val Rep_G = subst Rep_G;
    72     val Abs_G = subst Abs_G;
    73     val F = subst F;
    74     val RepT = typ_subst RepT;
    75     val AbsT = typ_subst AbsT;
    76 
    77     fun flatten_tyargs Ass =
    78       map dest_TFree alpha0s
    79       |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);
    80 
    81     val Ds0 = filter (is_none o fst) specs |> map snd;
    82 
    83     (* get the bnf for RepT *)
    84     val ((bnf, (deads, alphas)),((_, unfolds), lthy)) =
    85       bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
    86         Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);
    87 
    88     val set_bs =
    89       map (fn T => find_index (fn U => T = U) alpha0s) alphas
    90       |> map (the_default Binding.empty o fst o nth specs);
    91 
    92     val _ = (case alphas of [] => error "No live variables" | _ => ());
    93 
    94     val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds;
    95 
    96     (* number of live variables *)
    97     val lives = length alphas;
    98 
    99     (* state the three required properties *)
   100     val sorts = map Type.sort_of_atyp alphas;
   101     val names_lthy = fold Variable.declare_typ (alphas @ deads) lthy;
   102     val (alphas', names_lthy) = mk_TFrees' sorts names_lthy;
   103     val (betas, names_lthy) = mk_TFrees' sorts names_lthy;
   104 
   105     val map_F = mk_map_of_bnf deads alphas betas bnf;
   106 
   107     val (typ_fs, typ_aF) = fastype_of map_F |> strip_typeN lives ||> domain_type;
   108     val typ_pairs = map HOLogic.mk_prodT (alphas ~~ alphas');
   109     val typ_subst_pair = typ_subst_atomic (alphas ~~ typ_pairs);
   110     val typ_pair = typ_subst_pair RepT;
   111 
   112     val subst_b = subst_atomic_types (alphas ~~ betas);
   113     val subst_a' = subst_atomic_types (alphas ~~ alphas');
   114     val subst_pair = subst_atomic_types (alphas ~~ typ_pairs);
   115     val aF_set = F;
   116     val bF_set = subst_b F;
   117     val aF_set' = subst_a' F;
   118     val pairF_set = subst_pair F;
   119     val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf;
   120     val map_F_snd = mk_map_of_bnf deads typ_pairs alphas' bnf;
   121     val wits_F = mk_wits_of_bnf
   122       (replicate (nwits_of_bnf bnf) deads)
   123       (replicate (nwits_of_bnf bnf) alphas) bnf;
   124 
   125     (* val map_closed_F = @{term "\<And>f x. x \<in> F \<Longrightarrow> map_F f x \<in> F"}; *)
   126     val (var_fs, names_lthy) = mk_Frees "f" typ_fs names_lthy;
   127     val (var_x, names_lthy) = mk_Frees "x" [typ_aF] names_lthy |>> the_single;
   128     val mem_x = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_x, aF_set));
   129     val map_f = list_comb (map_F, var_fs);
   130     val mem_map = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_f $ var_x, bF_set));
   131     val imp_map = Logic.mk_implies (mem_x, mem_map);
   132     val map_closed_F = fold_rev Logic.all var_fs (Logic.all var_x imp_map);
   133 
   134     (* val zip_closed_F = @{term "\<And>z. map_F fst z \<in> F \<Longrightarrow> map_F snd z \<in> F \<Longrightarrow> z \<in> F"}; *)
   135     val (var_zs, names_lthy) = mk_Frees "z" [typ_pair] names_lthy;
   136     val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy;
   137     val var_z = hd var_zs;
   138     val fsts = map (fst o Term.strip_comb o HOLogic.mk_fst) pairs;
   139     val snds = map (fst o Term.strip_comb o HOLogic.mk_snd) pairs;
   140     val map_fst = list_comb (list_comb (map_F_fst, fsts), var_zs);
   141     val mem_map_fst = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_fst, aF_set));
   142     val map_snd = list_comb (list_comb (map_F_snd, snds), var_zs);
   143     val mem_map_snd = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_snd, aF_set'));
   144     val mem_z = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_z, pairF_set));
   145     val imp_zip = Logic.mk_implies (mem_map_fst, Logic.mk_implies (mem_map_snd, mem_z));
   146     val zip_closed_F = Logic.all var_z imp_zip;
   147 
   148     (* val wit_closed_F = @{term "wit_F a \<in> F"}; *)
   149     val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy;
   150     val (var_bs, _) = mk_Frees "a" alphas names_lthy;
   151     fun binder_types_until_eq V T =
   152       let
   153         fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U
   154           | strip T = if V = T then [] else
   155               error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T));
   156       in strip T end;
   157     val Iwits = the_default wits_F (Option.map (map (`(map (fn T =>
   158       find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits);
   159     val wit_closed_Fs =
   160       Iwits |> map (fn (I, wit_F) =>
   161         let
   162           val vars = map (nth var_as) I;
   163           val wit_a = list_comb (wit_F, vars);
   164         in fold_rev Logic.all vars (HOLogic.mk_Trueprop (HOLogic.mk_mem (wit_a, aF_set))) end);
   165 
   166     val mk_wit_goals = mk_wit_goals var_as var_bs
   167       (mk_sets_of_bnf (replicate lives deads)  (replicate lives alphas) bnf);
   168 
   169     val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @
   170       (case wits of NONE => [] | _ => maps mk_wit_goals Iwits);
   171 
   172     val lost_wits = filter_out (fn (J, _) => exists (fn (I, _) => I = J) Iwits) wits_F;
   173     val _ =
   174       if null lost_wits orelse no_warn_wits then ()
   175       else
   176         lost_wits
   177         |> map (Syntax.pretty_typ lthy o fastype_of o snd)
   178         |> Pretty.big_list
   179           "The following types of nonemptiness witnesses of the raw type's BNF were lost:"
   180         |> (fn pt => Pretty.chunks [pt,
   181           Pretty.para "You can specify a liftable witness (e.g., a term of one of the above types\
   182             \ that satisfies the typedef's invariant)\
   183             \ using the annotation [wits: <term>]."])
   184         |> Pretty.string_of
   185         |> warning;
   186 
   187     fun after_qed ([map_closed_thm] :: [zip_closed_thm] :: wit_thmss) lthy =
   188           let
   189             val (wit_closed_thms, wit_thms) =
   190               (case wits of
   191                 NONE => (map the_single wit_thmss, wit_thms_of_bnf bnf)
   192               | _ => chop (length wit_closed_Fs) (map the_single wit_thmss))
   193 
   194             (*  construct map set bd rel wit *)
   195             (* val map_G = @{term "\<lambda>f. Abs_G o map_F f o Rep_G"}; *)
   196             val Abs_Gb = subst_b Abs_G;
   197             val map_G =
   198               fold_rev HOLogic.tupled_lambda var_fs
   199                 (HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), Rep_G));
   200 
   201             (* val sets_G = [@{term "set_F o Rep_G"}]; *)
   202             val sets_F = mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf;
   203             val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F;
   204 
   205             (* val bd_G = @{term "bd_F"}; *)
   206             val bd_F = mk_bd_of_bnf deads alphas bnf;
   207             val bd_G = bd_F;
   208 
   209             (* val rel_G = @{term "\<lambda>R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *)
   210             val rel_F = mk_rel_of_bnf deads alphas betas bnf;
   211             val (typ_Rs, _) = strip_typeN lives (fastype_of rel_F);
   212 
   213             val (var_Rs, names_lthy) = mk_Frees "R" typ_Rs lthy;
   214             val Rep_Gb = subst_b Rep_G;
   215             val rel_G = fold_rev absfree (map dest_Free var_Rs)
   216               (mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs));
   217 
   218             (* val pred_G = @{term "\<lambda>P. pred_F P o Rep_G"}; *)
   219             val pred_F = mk_pred_of_bnf deads alphas bnf;
   220             val (typ_Ps, _) = strip_typeN lives (fastype_of pred_F);
   221 
   222             val (var_Ps, names_lthy) = mk_Frees "P" typ_Ps names_lthy;
   223             val pred_G = fold_rev absfree (map dest_Free var_Ps)
   224               (HOLogic.mk_comp (list_comb (pred_F, var_Ps), Rep_G));
   225 
   226             (* val wits_G = [@{term "Abs_G o wit_F"}]; *)
   227             val (var_as, _) = mk_Frees "a" alphas names_lthy;
   228             val wits_G =
   229               map (fn (I, wit_F) =>
   230                 let
   231                   val vs = map (nth var_as) I;
   232                 in fold_rev absfree (map dest_Free vs) (Abs_G $ (list_comb (wit_F, vs))) end)
   233               Iwits;
   234 
   235             (* tactics *)
   236             val Rep_thm = thm RS @{thm type_definition.Rep};
   237             val Abs_inverse_thm = thm RS @{thm type_definition.Abs_inverse};
   238             val Abs_inject_thm = thm RS @{thm type_definition.Abs_inject};
   239             val Rep_cases_thm = thm RS @{thm type_definition.Rep_cases};
   240             val Rep_inverse_thm = thm RS @{thm type_definition.Rep_inverse};
   241 
   242             fun map_id0_tac ctxt =
   243               HEADGOAL (EVERY' [rtac ctxt ext,
   244                 SELECT_GOAL (unfold_thms_tac ctxt [map_id0_of_bnf bnf, id_apply, o_apply,
   245                   Rep_inverse_thm]),
   246                 rtac ctxt refl]);
   247 
   248             fun map_comp0_tac ctxt =
   249               HEADGOAL (EVERY' [rtac ctxt ext,
   250                 SELECT_GOAL (unfold_thms_tac ctxt [map_comp0_of_bnf bnf, o_apply,
   251                   Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]),
   252                 rtac ctxt refl]);
   253 
   254             fun map_cong0_tac ctxt =
   255               HEADGOAL (EVERY' ([SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
   256                 rtac ctxt (([Rep_thm RS map_closed_thm, Rep_thm RS map_closed_thm] MRS
   257                   Abs_inject_thm) RS iffD2),
   258                 rtac ctxt (map_cong0_of_bnf bnf)] @ replicate lives (Goal.assume_rule_tac ctxt)));
   259 
   260             val set_map0s_tac =
   261               map (fn set_map => fn ctxt =>
   262                 HEADGOAL (EVERY' [rtac ctxt ext,
   263                   SELECT_GOAL (unfold_thms_tac ctxt [set_map, o_apply,
   264                     Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]),
   265                   rtac ctxt refl]))
   266              (set_map_of_bnf bnf);
   267 
   268             fun card_order_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_card_order_of_bnf bnf));
   269 
   270             fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf));
   271 
   272             val set_bds_tac =
   273               map (fn set_bd => fn ctxt =>
   274                 HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), rtac ctxt set_bd]))
   275               (set_bd_of_bnf bnf);
   276 
   277             fun le_rel_OO_tac ctxt =
   278               HEADGOAL (EVERY' [rtac ctxt @{thm vimage2p_relcompp_mono},
   279                 rtac ctxt ((rel_OO_of_bnf bnf RS sym) RS @{thm ord_eq_le_trans}),
   280                 rtac ctxt @{thm order_refl}]);
   281 
   282             fun rel_OO_Grp_tac ctxt =
   283               HEADGOAL (EVERY' ([SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt ext))),
   284                 SELECT_GOAL (unfold_thms_tac ctxt [@{thm OO_Grp_alt}, mem_Collect_eq,
   285                   o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf, Bex_def, mem_Collect_eq]),
   286                 rtac ctxt iffI,
   287                 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve0_tac [exE,conjE]))),
   288                 rtac ctxt (zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem}))) RS
   289                   Rep_cases_thm),
   290                 assume_tac ctxt,
   291                 assume_tac ctxt,
   292                 hyp_subst_tac ctxt,
   293                 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))),
   294                 rtac ctxt conjI] @
   295                 replicate (lives - 1) (rtac ctxt conjI THEN' assume_tac ctxt) @
   296                 [assume_tac ctxt,
   297                 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt conjI))),
   298                 REPEAT_DETERM_N 2 o
   299                   etac ctxt (trans OF [iffD2 OF [Abs_inject_thm OF
   300                     [map_closed_thm OF [Rep_thm], Rep_thm]], Rep_inverse_thm]),
   301                 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve0_tac [exE,conjE]))),
   302                 rtac ctxt exI,
   303                 rtac ctxt conjI] @
   304                 replicate (lives - 1) (rtac ctxt conjI THEN' assume_tac ctxt) @
   305                 [assume_tac ctxt,
   306                 rtac ctxt conjI,
   307                 REPEAT_DETERM_N 2 o EVERY'
   308                   [rtac ctxt (iffD1 OF [Abs_inject_thm OF [map_closed_thm OF [Rep_thm], Rep_thm]]),
   309                   etac ctxt (Rep_inverse_thm RS sym RSN (2, trans))]]));
   310 
   311             fun pred_set_tac ctxt =
   312               HEADGOAL (EVERY'
   313                 [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans),
   314                 SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})),
   315                 rtac ctxt refl]);
   316 
   317             fun wit_tac ctxt =
   318               HEADGOAL (EVERY'
   319                 (map (fn thm => (EVERY'
   320                   [SELECT_GOAL (unfold_thms_tac ctxt (o_apply ::
   321                     (wit_closed_thms RL [Abs_inverse_thm]))),
   322                   dtac ctxt thm, assume_tac ctxt]))
   323                 wit_thms));
   324 
   325             val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @
   326               [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @
   327               [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
   328 
   329             val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
   330               tactics wit_tac NONE map_b rel_b pred_b set_bs
   331               (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
   332               lthy;
   333 
   334             val (bnf, lthy) =
   335               morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf
   336               |> (fn bnf => note_bnf_defs bnf lthy);
   337           in
   338             lthy |> BNF_Def.register_bnf plugins AbsT_name bnf
   339           end
   340       | after_qed _ _ = raise Match;
   341   in
   342     (goals, after_qed, defs, lthy)
   343   end;
   344 
   345 
   346 (* main commands *)
   347 
   348 local
   349 
   350 fun prepare_common prepare_name prepare_sort prepare_term prepare_thm
   351     (((((plugins, raw_specs), raw_Tname), raw_wits), xthm_opt), (map_b, rel_b, pred_b)) lthy =
   352   let
   353     val Tname = prepare_name lthy raw_Tname;
   354     val input_thm =
   355       (case xthm_opt of
   356         SOME xthm => prepare_thm lthy xthm
   357       | NONE => Typedef.get_info lthy Tname |> hd |> snd |> #type_definition);
   358     val wits = (Option.map o map) (prepare_term lthy) raw_wits;
   359     val specs =
   360       map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs;
   361 
   362     val _ =
   363       (case HOLogic.dest_Trueprop (Thm.prop_of input_thm) of
   364         Const (@{const_name type_definition}, _) $ _ $ _ $ _ => ()
   365       | _ => error "Unsupported type of a theorem: only type_definition is supported");
   366   in
   367     typedef_bnf input_thm wits specs map_b rel_b pred_b plugins lthy
   368   end;
   369 
   370 fun prepare_lift_bnf prepare_name prepare_sort prepare_term prepare_thm =
   371   (fn (goals, after_qed, definitions, lthy) =>
   372     lthy
   373     |> Proof.theorem NONE after_qed (map (single o rpair []) goals)
   374     |> Proof.refine_singleton
   375         (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
   376     |> Proof.refine_singleton (Method.primitive_text (K I))) oo
   377   prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME));
   378 
   379 fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs =
   380   (fn (goals, after_qed, definitions, lthy) =>
   381     lthy
   382     |> after_qed (map2 (fn goal => fn tac => [Goal.prove lthy [] [] goal
   383         (fn (ctxtprems as {context = ctxt, prems = _}) =>
   384           unfold_thms_tac ctxt definitions THEN tac ctxtprems)])
   385       goals (tacs (length goals)))) oo
   386   prepare_common prepare_name prepare_typ prepare_sort prepare_thm;
   387 
   388 in
   389 
   390 val lift_bnf_cmd =
   391   prepare_lift_bnf
   392     (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
   393     Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms);
   394 
   395 fun lift_bnf args tacs =
   396   prepare_solve (K I) (K I) (K I) (K I) (K tacs) args;
   397 
   398 val copy_bnf =
   399   apfst (apfst (rpair NONE))
   400   #> prepare_solve (K I) (K I) (K I) (K I)
   401     (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1));
   402 
   403 val copy_bnf_cmd =
   404   apfst (apfst (rpair NONE))
   405   #> prepare_solve
   406     (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
   407     Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms)
   408     (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1));
   409 
   410 end;
   411 
   412 
   413 (* outer syntax *)
   414 
   415 local
   416 
   417 val parse_wits =
   418   @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.term >>
   419     (fn ("wits", Ts) => Ts
   420       | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   421   @{keyword "]"} || Scan.succeed [];
   422 
   423 val parse_options =
   424   Scan.optional (@{keyword "("} |--
   425     Parse.list1 (Parse.group (K "option")
   426       (Plugin_Name.parse_filter >> Plugins_Option
   427       || Parse.reserved "no_warn_wits" >> K No_Warn_Wits))
   428     --| @{keyword ")"}) [];
   429 
   430 val parse_plugins =
   431   Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"})
   432     (K Plugin_Name.default_filter) >> Plugins_Option >> single;
   433 
   434 val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm);
   435 
   436 in
   437 
   438 val _ =
   439   Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf}
   440     "register a subtype of a bounded natural functor (BNF) as a BNF"
   441     ((parse_options -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits --
   442       parse_typedef_thm -- parse_map_rel_pred_bindings) >> lift_bnf_cmd);
   443 
   444 val _ =
   445   Outer_Syntax.local_theory @{command_keyword copy_bnf}
   446     "register a type copy of a bounded natural functor (BNF) as a BNF"
   447     ((parse_plugins -- parse_type_args_named_constrained -- Parse.type_const --
   448       parse_typedef_thm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd);
   449 
   450 end;
   451 
   452 end;