bnf_decl -> bnf_axiomatization
authortraytel
Tue May 13 09:21:22 2014 +0200 (2014-05-13)
changeset 569425fff4dc31d34
parent 56941 952833323c99
child 56943 a3abb5222fce
bnf_decl -> bnf_axiomatization
NEWS
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Examples/Stream_Processor.thy
src/HOL/Library/BNF_Axiomatization.thy
src/HOL/Library/BNF_Decl.thy
src/HOL/Library/Library.thy
src/HOL/Library/bnf_axiomatization.ML
src/HOL/Library/bnf_decl.ML
     1.1 --- a/NEWS	Mon May 12 17:17:32 2014 +0200
     1.2 +++ b/NEWS	Tue May 13 09:21:22 2014 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4    New theories:
     1.5      Wellorder_Extension.thy (split from Zorn.thy)
     1.6      Library/Cardinal_Notations.thy
     1.7 -    Library/BNF_Decl.thy
     1.8 +    Library/BNF_Axomatization.thy
     1.9      BNF_Examples/Misc_Primcorec.thy
    1.10      BNF_Examples/Stream_Processor.thy
    1.11    Discontinued theories:
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon May 12 17:17:32 2014 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue May 13 09:21:22 2014 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  theory Datatypes
     2.5  imports
     2.6    Setup
     2.7 -  "~~/src/HOL/Library/BNF_Decl"
     2.8 +  "~~/src/HOL/Library/BNF_Axiomatization"
     2.9    "~~/src/HOL/Library/Cardinal_Notations"
    2.10    "~~/src/HOL/Library/FSet"
    2.11    "~~/src/HOL/Library/Simps_Case_Conv"
    2.12 @@ -80,7 +80,7 @@
    2.13  infinite branching.
    2.14  
    2.15  The package is part of @{theory Main}. Additional functionality is provided by
    2.16 -the theory @{theory BNF_Decl}, located in the directory
    2.17 +the theory @{theory BNF_Axiomatization}, located in the directory
    2.18  \verb|~~/src/HOL/Library|.
    2.19  
    2.20  The package, like its predecessor, fully adheres to the LCF philosophy
    2.21 @@ -2477,7 +2477,7 @@
    2.22  for further examples of BNF registration, some of which feature custom
    2.23  witnesses.
    2.24  
    2.25 -The next example declares a BNF axiomatically. The @{command bnf_decl} command
    2.26 +The next example declares a BNF axiomatically. The @{command bnf_axiomatization} command
    2.27  introduces a type @{text "('a, 'b, 'c) F"}, three set constants, a map
    2.28  function, a relator, and a nonemptiness witness that depends only on
    2.29  @{typ 'a}. (The type @{text "'a \<Rightarrow> ('a, 'b, 'c) F"} of
    2.30 @@ -2486,7 +2486,7 @@
    2.31  properties are postulated as axioms.
    2.32  *}
    2.33  
    2.34 -    bnf_decl (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
    2.35 +    bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
    2.36  
    2.37  text {* \blankline *}
    2.38  
    2.39 @@ -2533,11 +2533,11 @@
    2.40  
    2.41  text {*
    2.42  \begin{matharray}{rcl}
    2.43 -  @{command_def "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
    2.44 +  @{command_def "bnf_axiomatization"} & : & @{text "local_theory \<rightarrow> local_theory"}
    2.45  \end{matharray}
    2.46  
    2.47  @{rail \<open>
    2.48 -  @@{command bnf_decl} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
    2.49 +  @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
    2.50      @{syntax wit_types}? mixfix?
    2.51    ;
    2.52    @{syntax_def wit_types}: '[' 'wits' ':' types ']'
    2.53 @@ -2546,7 +2546,7 @@
    2.54  \medskip
    2.55  
    2.56  \noindent
    2.57 -The @{command bnf_decl} command declares a new type and associated constants
    2.58 +The @{command bnf_axiomatization} command declares a new type and associated constants
    2.59  (map, set, relator, and cardinal bound) and asserts the BNF properties for
    2.60  these constants as axioms.
    2.61  
    2.62 @@ -2558,12 +2558,12 @@
    2.63  Type arguments are live by default; they can be marked as dead by entering
    2.64  ``-'' (hyphen) instead of an identifier for the corresponding set function.
    2.65  Witnesses can be specified by their types. Otherwise, the syntax of
    2.66 -@{command bnf_decl} is identical to the left-hand side of a
    2.67 +@{command bnf_axiomatization} is identical to the left-hand side of a
    2.68  @{command datatype_new} or @{command codatatype} definition.
    2.69  
    2.70  The command is useful to reason abstractly about BNFs. The axioms are safe
    2.71  because there exists BNFs of arbitrary large arities. Applications must import
    2.72 -the theory @{theory BNF_Decl}, located in the directory
    2.73 +the theory @{theory BNF_Axiomatization}, located in the directory
    2.74  \verb|~~/src/HOL/Library|, to use this functionality.
    2.75  *}
    2.76  
     3.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Mon May 12 17:17:32 2014 +0200
     3.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Tue May 13 09:21:22 2014 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  header {* Stream Processors *}
     3.5  
     3.6  theory Stream_Processor
     3.7 -imports Stream "~~/src/HOL/Library/BNF_Decl"
     3.8 +imports Stream "~~/src/HOL/Library/BNF_Axiomatization"
     3.9  begin
    3.10  
    3.11  section {* Continuous Functions on Streams *}
    3.12 @@ -150,7 +150,7 @@
    3.13  
    3.14  section {* Generalization to an Arbitrary BNF as Codomain *}
    3.15  
    3.16 -bnf_decl ('a, 'b) F (map: F)
    3.17 +bnf_axiomatization ('a, 'b) F (map: F)
    3.18  
    3.19  notation BNF_Def.convol ("<_ , _>")
    3.20  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/BNF_Axiomatization.thy	Tue May 13 09:21:22 2014 +0200
     4.3 @@ -0,0 +1,18 @@
     4.4 +(*  Title:      HOL/Library/BNF_Axiomatization.thy
     4.5 +    Author:     Dmitriy Traytel, TU Muenchen
     4.6 +    Copyright   2013
     4.7 +
     4.8 +Axiomatic declaration of bounded natural functors.
     4.9 +*)
    4.10 +
    4.11 +header {* Axiomatic declaration of Bounded Natural Functors *}
    4.12 +
    4.13 +theory BNF_Axiomatization
    4.14 +imports Main
    4.15 +keywords
    4.16 +  "bnf_axiomatization" :: thy_decl
    4.17 +begin
    4.18 +
    4.19 +ML_file "bnf_axiomatization.ML"
    4.20 +
    4.21 +end
     5.1 --- a/src/HOL/Library/BNF_Decl.thy	Mon May 12 17:17:32 2014 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,18 +0,0 @@
     5.4 -(*  Title:      HOL/Library/BNF_Decl.thy
     5.5 -    Author:     Dmitriy Traytel, TU Muenchen
     5.6 -    Copyright   2013
     5.7 -
     5.8 -Axiomatic declaration of bounded natural functors.
     5.9 -*)
    5.10 -
    5.11 -header {* Axiomatic declaration of Bounded Natural Functors *}
    5.12 -
    5.13 -theory BNF_Decl
    5.14 -imports Main
    5.15 -keywords
    5.16 -  "bnf_decl" :: thy_decl
    5.17 -begin
    5.18 -
    5.19 -ML_file "bnf_decl.ML"
    5.20 -
    5.21 -end
     6.1 --- a/src/HOL/Library/Library.thy	Mon May 12 17:17:32 2014 +0200
     6.2 +++ b/src/HOL/Library/Library.thy	Tue May 13 09:21:22 2014 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4    AList
     6.5    BigO
     6.6    Bit
     6.7 -  BNF_Decl
     6.8 +  BNF_Axiomatization
     6.9    Boolean_Algebra
    6.10    Char_ord
    6.11    ContNotDenum
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/bnf_axiomatization.ML	Tue May 13 09:21:22 2014 +0200
     7.3 @@ -0,0 +1,120 @@
     7.4 +(*  Title:      HOL/Library/bnf_axiomatization.ML
     7.5 +    Author:     Dmitriy Traytel, TU Muenchen
     7.6 +    Copyright   2013
     7.7 +
     7.8 +Axiomatic declaration of bounded natural functors.
     7.9 +*)
    7.10 +
    7.11 +signature BNF_AXIOMATIZATION =
    7.12 +sig
    7.13 +  val bnf_axiomatization: (binding option * (typ * sort)) list -> binding -> mixfix -> binding ->
    7.14 +    binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory
    7.15 +end
    7.16 +
    7.17 +structure BNF_Axiomatization : BNF_AXIOMATIZATION =
    7.18 +struct
    7.19 +
    7.20 +open BNF_Util
    7.21 +open BNF_Def
    7.22 +
    7.23 +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
    7.24 +  let
    7.25 +   fun prepare_type_arg (set_opt, (ty, c)) =
    7.26 +      let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    7.27 +        (set_opt, (s, prepare_constraint lthy c))
    7.28 +      end;
    7.29 +    val ((user_setbs, vars), raw_vars') =
    7.30 +      map prepare_type_arg raw_vars
    7.31 +      |> `split_list
    7.32 +      |>> apfst (map_filter I);
    7.33 +    val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
    7.34 +
    7.35 +    fun mk_b name user_b =
    7.36 +      (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
    7.37 +      |> Binding.qualify false (Binding.name_of b);
    7.38 +    val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
    7.39 +    val (bd_type_Tname, lthy) =
    7.40 +      Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
    7.41 +    val T = Type (Tname, map TFree vars);
    7.42 +    val bd_type_T = Type (bd_type_Tname, map TFree deads);
    7.43 +    val lives = map TFree (filter_out (member (op =) deads) vars);
    7.44 +    val live = length lives;
    7.45 +    val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
    7.46 +    val (lives', _) = BNF_Util.mk_TFrees (length lives)
    7.47 +      (fold Variable.declare_typ (map TFree vars) lthy);
    7.48 +    val T' = Term.typ_subst_atomic (lives ~~ lives') T;
    7.49 +    val mapT = map2 (curry op -->) lives lives' ---> T --> T';
    7.50 +    val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
    7.51 +    val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
    7.52 +    val mapb = mk_b BNF_Def.mapN user_mapb;
    7.53 +    val bdb = mk_b "bd" Binding.empty;
    7.54 +    val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
    7.55 +      (if live = 1 then [0] else 1 upto live);
    7.56 +
    7.57 +    val witTs = map (prepare_typ lthy) user_witTs;
    7.58 +    val nwits = length witTs;
    7.59 +    val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
    7.60 +      (if nwits = 1 then [0] else 1 upto nwits);
    7.61 +
    7.62 +    val lthy = Local_Theory.background_theory
    7.63 +      (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    7.64 +        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    7.65 +        map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    7.66 +      lthy;
    7.67 +    val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
    7.68 +    val Fsets = map2 (fn setb => fn setT =>
    7.69 +      Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
    7.70 +    val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
    7.71 +    val Fwits = map2 (fn witb => fn witT =>
    7.72 +      Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
    7.73 +    val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
    7.74 +      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
    7.75 +      user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
    7.76 +      lthy;
    7.77 +
    7.78 +    fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
    7.79 +    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    7.80 +    val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    7.81 +
    7.82 +    val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
    7.83 +      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
    7.84 +      ||> `Local_Theory.restore;
    7.85 +
    7.86 +    fun mk_wit_thms set_maps =
    7.87 +      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    7.88 +        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
    7.89 +      |> Conjunction.elim_balanced (length wit_goals)
    7.90 +      |> map2 (Conjunction.elim_balanced o length) wit_goalss
    7.91 +      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
    7.92 +    val phi = Proof_Context.export_morphism lthy_old lthy;
    7.93 +    val thms = unflat all_goalss (Morphism.fact phi raw_thms);
    7.94 +
    7.95 +    val (bnf, lthy') = after_qed mk_wit_thms thms lthy
    7.96 +  in
    7.97 +    (bnf, BNF_Def.register_bnf key bnf lthy')
    7.98 +  end;
    7.99 +
   7.100 +val bnf_axiomatization = prepare_decl (K I) (K I);
   7.101 +
   7.102 +fun read_constraint _ NONE = @{sort type}
   7.103 +  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
   7.104 +
   7.105 +val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ;
   7.106 +
   7.107 +val parse_witTs =
   7.108 +  @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
   7.109 +    >> (fn ("wits", Ts) => Ts
   7.110 +         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   7.111 +  @{keyword "]"} || Scan.succeed [];
   7.112 +
   7.113 +val parse_bnf_axiomatization =
   7.114 +  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   7.115 +    parse_witTs -- Parse.opt_mixfix;
   7.116 +
   7.117 +val _ =
   7.118 +  Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
   7.119 +    (parse_bnf_axiomatization >> 
   7.120 +      (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
   7.121 +         bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd));
   7.122 +
   7.123 +end;
     8.1 --- a/src/HOL/Library/bnf_decl.ML	Mon May 12 17:17:32 2014 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,120 +0,0 @@
     8.4 -(*  Title:      HOL/Library/bnf_decl.ML
     8.5 -    Author:     Dmitriy Traytel, TU Muenchen
     8.6 -    Copyright   2013
     8.7 -
     8.8 -Axiomatic declaration of bounded natural functors.
     8.9 -*)
    8.10 -
    8.11 -signature BNF_DECL =
    8.12 -sig
    8.13 -  val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding ->
    8.14 -    typ list -> local_theory -> BNF_Def.bnf * local_theory
    8.15 -end
    8.16 -
    8.17 -structure BNF_Decl : BNF_DECL =
    8.18 -struct
    8.19 -
    8.20 -open BNF_Util
    8.21 -open BNF_Def
    8.22 -
    8.23 -fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
    8.24 -  let
    8.25 -   fun prepare_type_arg (set_opt, (ty, c)) =
    8.26 -      let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    8.27 -        (set_opt, (s, prepare_constraint lthy c))
    8.28 -      end;
    8.29 -    val ((user_setbs, vars), raw_vars') =
    8.30 -      map prepare_type_arg raw_vars
    8.31 -      |> `split_list
    8.32 -      |>> apfst (map_filter I);
    8.33 -    val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
    8.34 -
    8.35 -    fun mk_b name user_b =
    8.36 -      (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
    8.37 -      |> Binding.qualify false (Binding.name_of b);
    8.38 -    val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
    8.39 -    val (bd_type_Tname, lthy) =
    8.40 -      Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
    8.41 -    val T = Type (Tname, map TFree vars);
    8.42 -    val bd_type_T = Type (bd_type_Tname, map TFree deads);
    8.43 -    val lives = map TFree (filter_out (member (op =) deads) vars);
    8.44 -    val live = length lives;
    8.45 -    val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
    8.46 -    val (lives', _) = BNF_Util.mk_TFrees (length lives)
    8.47 -      (fold Variable.declare_typ (map TFree vars) lthy);
    8.48 -    val T' = Term.typ_subst_atomic (lives ~~ lives') T;
    8.49 -    val mapT = map2 (curry op -->) lives lives' ---> T --> T';
    8.50 -    val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
    8.51 -    val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
    8.52 -    val mapb = mk_b BNF_Def.mapN user_mapb;
    8.53 -    val bdb = mk_b "bd" Binding.empty;
    8.54 -    val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
    8.55 -      (if live = 1 then [0] else 1 upto live);
    8.56 -
    8.57 -    val witTs = map (prepare_typ lthy) user_witTs;
    8.58 -    val nwits = length witTs;
    8.59 -    val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
    8.60 -      (if nwits = 1 then [0] else 1 upto nwits);
    8.61 -
    8.62 -    val lthy = Local_Theory.background_theory
    8.63 -      (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    8.64 -        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    8.65 -        map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    8.66 -      lthy;
    8.67 -    val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
    8.68 -    val Fsets = map2 (fn setb => fn setT =>
    8.69 -      Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
    8.70 -    val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
    8.71 -    val Fwits = map2 (fn witb => fn witT =>
    8.72 -      Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
    8.73 -    val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
    8.74 -      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
    8.75 -      user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
    8.76 -      lthy;
    8.77 -
    8.78 -    fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
    8.79 -    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    8.80 -    val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    8.81 -
    8.82 -    val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
    8.83 -      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
    8.84 -      ||> `Local_Theory.restore;
    8.85 -
    8.86 -    fun mk_wit_thms set_maps =
    8.87 -      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    8.88 -        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
    8.89 -      |> Conjunction.elim_balanced (length wit_goals)
    8.90 -      |> map2 (Conjunction.elim_balanced o length) wit_goalss
    8.91 -      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
    8.92 -    val phi = Proof_Context.export_morphism lthy_old lthy;
    8.93 -    val thms = unflat all_goalss (Morphism.fact phi raw_thms);
    8.94 -
    8.95 -    val (bnf, lthy') = after_qed mk_wit_thms thms lthy
    8.96 -  in
    8.97 -    (bnf, BNF_Def.register_bnf key bnf lthy')
    8.98 -  end;
    8.99 -
   8.100 -val bnf_decl = prepare_decl (K I) (K I);
   8.101 -
   8.102 -fun read_constraint _ NONE = @{sort type}
   8.103 -  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
   8.104 -
   8.105 -val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
   8.106 -
   8.107 -val parse_witTs =
   8.108 -  @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
   8.109 -    >> (fn ("wits", Ts) => Ts
   8.110 -         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   8.111 -  @{keyword "]"} || Scan.succeed [];
   8.112 -
   8.113 -val parse_bnf_decl =
   8.114 -  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   8.115 -    parse_witTs -- Parse.opt_mixfix;
   8.116 -
   8.117 -val _ =
   8.118 -  Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration"
   8.119 -    (parse_bnf_decl >> 
   8.120 -      (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
   8.121 -         bnf_decl_cmd bsTs b mx mapb relb witTs #> snd));
   8.122 -
   8.123 -end;