src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

 Recursor sugar ("primrec").
 *)
 
 signature BNF_LFP_REC_SUGAR =
 sig
+  datatype primrec_option = Nonexhaustive_Option
+
   type basic_lfp_sugar =
     {T: typ,
      fp_res_index: int,
      C: typ,
      fun_arg_Tsss : typ list list list,

 
   val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory
 
   val add_primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
-  val add_primrec_cmd: (binding * string option * mixfix) list ->
+  val add_primrec_cmd: primrec_option list -> (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory
   val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->

 val simp_attrs = @{attributes [simp]};
 val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
 
 exception OLD_PRIMREC of unit;
 exception PRIMREC of string * term list;
+
+datatype primrec_option = Nonexhaustive_Option;
 
 datatype rec_call =
   No_Rec of int * typ |
   Mutual_Rec of (int * typ) * (int * typ) |
   Nested_Rec of int * typ;

       t
       |> subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls
       |> fold_rev lambda (args @ left_args @ right_args)
     end);
 
-fun build_defs lthy bs mxs (funs_data : eqn_data list list) (rec_specs : rec_spec list) has_call =
+fun build_defs lthy nonexhaustive bs mxs (funs_data : eqn_data list list)
+    (rec_specs : rec_spec list) has_call =
   let
     val n_funs = length funs_data;
 
     val ctr_spec_eqn_data_list' =
       (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data
       |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y))
           ##> (fn x => null x orelse
             raise PRIMREC ("excess equations in definition", map #rhs_term x)) #> fst);
-    val _ = ctr_spec_eqn_data_list' |> map (fn (_, x) => length x <= 1 orelse
-      raise PRIMREC ("multiple equations for constructor", map #user_eqn x));
+    val _ = ctr_spec_eqn_data_list' |> map (fn ({ctr, ...}, x) =>
+        if length x > 1 then raise PRIMREC ("multiple equations for constructor", map #user_eqn x)
+        else if length x = 1 orelse nonexhaustive then ()
+        else warning ("no equation for constructor " ^ Syntax.string_of_term lthy ctr));
 
     val ctr_spec_eqn_data_list =
       ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
 
     val recs = take n_funs rec_specs |> map #recx;

   unfold_thms_tac ctxt fun_defs THEN
   HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
   unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN
   HEADGOAL (rtac refl);
 
-fun prepare_primrec fixes specs lthy0 =
+fun prepare_primrec nonexhaustive fixes specs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val (bs, mxs) = map_split (apfst fst) fixes;
     val fun_names = map Binding.name_of bs;

     val _ =
       map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
         raise PRIMREC ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
           " is not a constructor in left-hand side", [user_eqn])) eqns_data;
 
-    val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
+    val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
 
     fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
         (fun_data : eqn_data list) =
       let
         val js =

       fn lthy => fn defs =>
         split_list (map2 (prove lthy defs) (take actual_nn rec_specs) funs_data)),
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;
 
-fun add_primrec_simple fixes ts lthy =
-  let
-    val (((names, defs), prove), lthy') = prepare_primrec fixes ts lthy
+fun add_primrec_simple' opts fixes ts lthy =
+  let
+    val nonexhaustive = member (op =) opts Nonexhaustive_Option;
+    val (((names, defs), prove), lthy') = prepare_primrec nonexhaustive fixes ts lthy
       handle ERROR str => raise PRIMREC (str, []);
   in
     lthy'
     |> fold_map Local_Theory.define defs
     |-> (fn defs => `(fn lthy => (names, (map fst defs, prove lthy defs))))

            error ("primrec error:\n  " ^ str)
          else
            error ("primrec error:\n  " ^ str ^ "\nin\n  " ^
              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
 
-fun gen_primrec old_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec
-    lthy =
+val add_primrec_simple = add_primrec_simple' [];
+
+fun gen_primrec old_primrec prep_spec opts
+    (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
   let
     val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
     val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
 
     val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy);

         in
           ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
         end);
   in
     lthy
-    |> add_primrec_simple fixes (map snd specs)
+    |> add_primrec_simple' opts fixes (map snd specs)
     |-> (fn (names, (ts, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names simpss)
       #>> pair ts o map snd)
   end
   handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single;
 
-val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec;
+val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
 val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
 
 fun add_primrec_global fixes specs =
   Named_Target.theory_init
   #> add_primrec fixes specs

 fun add_primrec_overloaded ops fixes specs =
   Overloading.overloading ops
   #> add_primrec fixes specs
   ##> Local_Theory.exit_global;
 
+val primrec_option_parser = Parse.group (fn () => "option")
+  (Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option)
+
 val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   "define primitive recursive functions"
-  (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd));
+  ((Scan.optional (@{keyword "("} |--
+      Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
+    (Parse.fixes -- Parse_Spec.where_alt_specs)
+    >> (fn (opts, (fixes, spec)) => snd o add_primrec_cmd opts fixes spec));
 
 end;