src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 56152 2a31945b9a58
child 56805 8a87502c7da3
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
     2     Author:     Lorenz Panny, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2013
     5 
     6 Corecursor sugar ("primcorec" and "primcorecursive").
     7 *)
     8 
     9 signature BNF_GFP_REC_SUGAR =
    10 sig
    11   datatype primcorec_option = Sequential_Option | Exhaustive_Option
    12 
    13   val add_primcorecursive_cmd: primcorec_option list ->
    14     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
    15     Proof.context -> Proof.state
    16   val add_primcorec_cmd: primcorec_option list ->
    17     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
    18     local_theory -> local_theory
    19 end;
    20 
    21 structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR =
    22 struct
    23 
    24 open Ctr_Sugar_General_Tactics
    25 open Ctr_Sugar
    26 open BNF_Util
    27 open BNF_Def
    28 open BNF_FP_Util
    29 open BNF_FP_Def_Sugar
    30 open BNF_FP_N2M_Sugar
    31 open BNF_FP_Rec_Sugar_Util
    32 open BNF_GFP_Rec_Sugar_Tactics
    33 
    34 val codeN = "code"
    35 val ctrN = "ctr"
    36 val discN = "disc"
    37 val disc_iffN = "disc_iff"
    38 val excludeN = "exclude"
    39 val selN = "sel"
    40 
    41 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
    42 val simp_attrs = @{attributes [simp]};
    43 val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
    44 
    45 exception PRIMCOREC of string * term list;
    46 
    47 fun primcorec_error str = raise PRIMCOREC (str, []);
    48 fun primcorec_error_eqn str eqn = raise PRIMCOREC (str, [eqn]);
    49 fun primcorec_error_eqns str eqns = raise PRIMCOREC (str, eqns);
    50 
    51 datatype primcorec_option = Sequential_Option | Exhaustive_Option;
    52 
    53 datatype corec_call =
    54   Dummy_No_Corec of int |
    55   No_Corec of int |
    56   Mutual_Corec of int * int * int |
    57   Nested_Corec of int;
    58 
    59 type basic_corec_ctr_spec =
    60   {ctr: term,
    61    disc: term,
    62    sels: term list};
    63 
    64 type corec_ctr_spec =
    65   {ctr: term,
    66    disc: term,
    67    sels: term list,
    68    pred: int option,
    69    calls: corec_call list,
    70    discI: thm,
    71    sel_thms: thm list,
    72    disc_excludess: thm list list,
    73    collapse: thm,
    74    corec_thm: thm,
    75    disc_corec: thm,
    76    sel_corecs: thm list};
    77 
    78 type corec_spec =
    79   {corec: term,
    80    disc_exhausts: thm list,
    81    nested_maps: thm list,
    82    nested_map_idents: thm list,
    83    nested_map_comps: thm list,
    84    ctr_specs: corec_ctr_spec list};
    85 
    86 exception NOT_A_MAP of term;
    87 
    88 fun not_codatatype ctxt T =
    89   error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
    90 fun ill_formed_corec_call ctxt t =
    91   error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
    92 fun invalid_map ctxt t =
    93   error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
    94 fun unexpected_corec_call ctxt t =
    95   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
    96 
    97 fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs);
    98 
    99 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
   100 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
   101 val mk_dnf = mk_disjs o map mk_conjs;
   102 
   103 val conjuncts_s = filter_out (curry (op aconv) @{const True}) o HOLogic.conjuncts;
   104 
   105 fun s_not @{const True} = @{const False}
   106   | s_not @{const False} = @{const True}
   107   | s_not (@{const Not} $ t) = t
   108   | s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u
   109   | s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u
   110   | s_not t = @{const Not} $ t;
   111 
   112 val s_not_conj = conjuncts_s o s_not o mk_conjs;
   113 
   114 fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
   115 
   116 fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
   117 
   118 fun propagate_units css =
   119   (case List.partition (can the_single) css of
   120      ([], _) => css
   121    | ([u] :: uss, css') =>
   122      [u] :: propagate_units (map (propagate_unit_neg (s_not u))
   123        (map (propagate_unit_pos u) (uss @ css'))));
   124 
   125 fun s_conjs cs =
   126   if member (op aconv) cs @{const False} then @{const False}
   127   else mk_conjs (remove (op aconv) @{const True} cs);
   128 
   129 fun s_disjs ds =
   130   if member (op aconv) ds @{const True} then @{const True}
   131   else mk_disjs (remove (op aconv) @{const False} ds);
   132 
   133 fun s_dnf css0 =
   134   let val css = propagate_units css0 in
   135     if null css then
   136       [@{const False}]
   137     else if exists null css then
   138       []
   139     else
   140       map (fn c :: cs => (c, cs)) css
   141       |> AList.coalesce (op =)
   142       |> map (fn (c, css) => c :: s_dnf css)
   143       |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)])
   144   end;
   145 
   146 fun fold_rev_let_if_case ctxt f bound_Ts =
   147   let
   148     val thy = Proof_Context.theory_of ctxt;
   149 
   150     fun fld conds t =
   151       (case Term.strip_comb t of
   152         (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t)
   153       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
   154         fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
   155       | (Const (c, _), args as _ :: _ :: _) =>
   156         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
   157           if n >= 0 andalso n < length args then
   158             (case fastype_of1 (bound_Ts, nth args n) of
   159               Type (s, Ts) =>
   160               (case dest_case ctxt s Ts t of
   161                 SOME ({sel_splits = _ :: _, ...}, conds', branches) =>
   162                 fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches)
   163               | _ => f conds t)
   164             | _ => f conds t)
   165           else
   166             f conds t
   167         end
   168       | _ => f conds t);
   169   in
   170     fld []
   171   end;
   172 
   173 fun case_of ctxt s =
   174   (case ctr_sugar_of ctxt s of
   175     SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
   176   | _ => NONE);
   177 
   178 fun massage_let_if_case ctxt has_call massage_leaf =
   179   let
   180     val thy = Proof_Context.theory_of ctxt;
   181 
   182     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
   183 
   184     fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t
   185       | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t)
   186       | massage_abs bound_Ts m t =
   187         let val T = domain_type (fastype_of1 (bound_Ts, t)) in
   188           Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0))
   189         end
   190     and massage_rec bound_Ts t =
   191       let val typof = curry fastype_of1 bound_Ts in
   192         (case Term.strip_comb t of
   193           (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
   194         | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
   195           let val branches' = map (massage_rec bound_Ts) branches in
   196             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
   197           end
   198         | (c as Const (@{const_name case_prod}, _), arg :: args) =>
   199           massage_rec bound_Ts
   200             (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
   201         | (Const (c, _), args as _ :: _ :: _) =>
   202           (case try strip_fun_type (Sign.the_const_type thy c) of
   203             SOME (gen_branch_Ts, gen_body_fun_T) =>
   204             let
   205               val gen_branch_ms = map num_binder_types gen_branch_Ts;
   206               val n = length gen_branch_ms;
   207             in
   208               if n < length args then
   209                 (case gen_body_fun_T of
   210                   Type (_, [Type (T_name, _), _]) =>
   211                   if case_of ctxt T_name = SOME c then
   212                     let
   213                       val (branches, obj_leftovers) = chop n args;
   214                       val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
   215                       val branch_Ts' = map typof branches';
   216                       val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
   217                       val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
   218                     in
   219                       Term.list_comb (casex',
   220                         branches' @ tap (List.app check_no_call) obj_leftovers)
   221                     end
   222                   else
   223                     massage_leaf bound_Ts t
   224                 | _ => massage_leaf bound_Ts t)
   225               else
   226                 massage_leaf bound_Ts t
   227             end
   228           | NONE => massage_leaf bound_Ts t)
   229         | _ => massage_leaf bound_Ts t)
   230       end;
   231   in
   232     massage_rec
   233   end;
   234 
   235 fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
   236 
   237 fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   238   let
   239     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
   240 
   241     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd);
   242 
   243     fun massage_mutual_call bound_Ts U T t =
   244       if has_call t then
   245         (case try dest_sumT U of
   246           SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t
   247         | NONE => invalid_map ctxt t)
   248       else
   249         build_map_Inl (T, U) $ t;
   250 
   251     fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
   252         (case try (dest_map ctxt s) t of
   253           SOME (map0, fs) =>
   254           let
   255             val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
   256             val map' = mk_map (length fs) dom_Ts Us map0;
   257             val fs' =
   258               map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs;
   259           in
   260             Term.list_comb (map', fs')
   261           end
   262         | NONE => raise NOT_A_MAP t)
   263       | massage_map _ _ _ t = raise NOT_A_MAP t
   264     and massage_map_or_map_arg bound_Ts U T t =
   265       if T = U then
   266         tap check_no_call t
   267       else
   268         massage_map bound_Ts U T t
   269         handle NOT_A_MAP _ => massage_mutual_fun bound_Ts U T t
   270     and massage_mutual_fun bound_Ts U T t =
   271       (case t of
   272         Const (@{const_name comp}, _) $ t1 $ t2 =>
   273         mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
   274       | _ =>
   275         let
   276           val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
   277             domain_type (fastype_of1 (bound_Ts, t)));
   278         in
   279           Term.lambda var (massage_call bound_Ts U T (betapply (t, var)))
   280         end)
   281     and massage_call bound_Ts U T =
   282       massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
   283         if has_call t then
   284           (case U of
   285             Type (s, Us) =>
   286             (case try (dest_ctr ctxt s) t of
   287               SOME (f, args) =>
   288               let
   289                 val typof = curry fastype_of1 bound_Ts;
   290                 val f' = mk_ctr Us f
   291                 val f'_T = typof f';
   292                 val arg_Ts = map typof args;
   293               in
   294                 Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
   295               end
   296             | NONE =>
   297               (case t of
   298                 Const (@{const_name case_prod}, _) $ t' =>
   299                 let
   300                   val U' = curried_type U;
   301                   val T' = curried_type T;
   302                 in
   303                   Const (@{const_name case_prod}, U' --> U) $ massage_call bound_Ts U' T' t'
   304                 end
   305               | t1 $ t2 =>
   306                 (if has_call t2 then
   307                   massage_mutual_call bound_Ts U T t
   308                 else
   309                   massage_map bound_Ts U T t1 $ t2
   310                   handle NOT_A_MAP _ => massage_mutual_call bound_Ts U T t)
   311               | Abs (s, T', t') =>
   312                 Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
   313               | _ => massage_mutual_call bound_Ts U T t))
   314           | _ => ill_formed_corec_call ctxt t)
   315         else
   316           build_map_Inl (T, U) $ t) bound_Ts;
   317 
   318     val T = fastype_of1 (bound_Ts, t);
   319   in
   320     if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
   321   end;
   322 
   323 fun expand_to_ctr_term ctxt s Ts t =
   324   (case ctr_sugar_of ctxt s of
   325     SOME {ctrs, casex, ...} =>
   326     Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
   327   | NONE => raise Fail "expand_to_ctr_term");
   328 
   329 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   330   (case fastype_of1 (bound_Ts, t) of
   331     Type (s, Ts) =>
   332     massage_let_if_case ctxt has_call (fn _ => fn t =>
   333       if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t
   334   | _ => raise Fail "expand_corec_code_rhs");
   335 
   336 fun massage_corec_code_rhs ctxt massage_ctr =
   337   massage_let_if_case ctxt (K false)
   338     (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
   339 
   340 fun fold_rev_corec_code_rhs ctxt f =
   341   fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
   342 
   343 fun case_thms_of_term ctxt t =
   344   let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
   345     (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars,
   346      maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
   347   end;
   348 
   349 fun basic_corec_specs_of ctxt res_T =
   350   (case res_T of
   351     Type (T_name, _) =>
   352     (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
   353       NONE => not_codatatype ctxt res_T
   354     | SOME {ctrs, discs, selss, ...} =>
   355       let
   356         val thy = Proof_Context.theory_of ctxt;
   357 
   358         val gfpT = body_type (fastype_of (hd ctrs));
   359         val As_rho = tvar_subst thy [gfpT] [res_T];
   360         val substA = Term.subst_TVars As_rho;
   361 
   362         fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
   363       in
   364         map3 mk_spec ctrs discs selss
   365         handle ListPair.UnequalLengths => not_codatatype ctxt res_T
   366       end)
   367   | _ => not_codatatype ctxt res_T);
   368 
   369 fun map_thms_of_typ ctxt (Type (s, _)) =
   370     (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
   371   | map_thms_of_typ _ _ = [];
   372 
   373 fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
   374   let
   375     val thy = Proof_Context.theory_of lthy0;
   376 
   377     val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
   378           common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
   379       nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
   380 
   381     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
   382 
   383     val indices = map #fp_res_index fp_sugars;
   384     val perm_indices = map #fp_res_index perm_fp_sugars;
   385 
   386     val perm_gfpTs = map #T perm_fp_sugars;
   387     val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
   388 
   389     val nn0 = length res_Ts;
   390     val nn = length perm_gfpTs;
   391     val kks = 0 upto nn - 1;
   392     val perm_ns' = map length perm_ctrXs_Tsss';
   393 
   394     val perm_Ts = map #T perm_fp_sugars;
   395     val perm_Xs = map #X perm_fp_sugars;
   396     val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
   397     val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
   398 
   399     fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
   400       | zip_corecT U =
   401         (case AList.lookup (op =) Xs_TCs U of
   402           SOME (T, C) => [T, C]
   403         | NONE => [U]);
   404 
   405     val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns';
   406     val perm_f_Tssss =
   407       map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
   408     val perm_q_Tssss =
   409       map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss;
   410 
   411     val (perm_p_hss, h) = indexedd perm_p_Tss 0;
   412     val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
   413     val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
   414 
   415     val fun_arg_hs =
   416       flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
   417 
   418     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
   419     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
   420 
   421     val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
   422 
   423     val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
   424     val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
   425     val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
   426 
   427     val f_Tssss = unpermute perm_f_Tssss;
   428     val gfpTs = unpermute perm_gfpTs;
   429     val Cs = unpermute perm_Cs;
   430 
   431     val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts;
   432     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
   433 
   434     val substA = Term.subst_TVars As_rho;
   435     val substAT = Term.typ_subst_TVars As_rho;
   436     val substCT = Term.typ_subst_TVars Cs_rho;
   437 
   438     val perm_Cs' = map substCT perm_Cs;
   439 
   440     fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
   441         (if exists_subtype_in Cs T then Nested_Corec
   442          else if nullary then Dummy_No_Corec
   443          else No_Corec) g_i
   444       | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
   445 
   446     fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse
   447         corec_thm disc_corec sel_corecs =
   448       let val nullary = not (can dest_funT (fastype_of ctr)) in
   449         {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
   450          calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
   451          disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
   452          disc_corec = disc_corec, sel_corecs = sel_corecs}
   453       end;
   454 
   455     fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
   456         : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
   457       let val p_ios = map SOME p_is @ [NONE] in
   458         map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
   459           disc_excludesss collapses corec_thms disc_corecs sel_corecss
   460       end;
   461 
   462     fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec,
   463         co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
   464         sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
   465       {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec,
   466        disc_exhausts = disc_exhausts,
   467        nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
   468        nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
   469        nested_map_comps = map map_comp_of_bnf nested_bnfs,
   470        ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
   471          sel_corecss};
   472   in
   473     ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
   474       co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
   475       co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy)
   476   end;
   477 
   478 val undef_const = Const (@{const_name undefined}, dummyT);
   479 
   480 val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
   481 
   482 fun abstract vs =
   483   let
   484     fun abs n (t $ u) = abs n t $ abs n u
   485       | abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b)
   486       | abs n t =
   487         let val j = find_index (curry (op =) t) vs in
   488           if j < 0 then t else Bound (n + j)
   489         end;
   490   in abs 0 end;
   491 
   492 type coeqn_data_disc = {
   493   fun_name: string,
   494   fun_T: typ,
   495   fun_args: term list,
   496   ctr: term,
   497   ctr_no: int,
   498   disc: term,
   499   prems: term list,
   500   auto_gen: bool,
   501   ctr_rhs_opt: term option,
   502   code_rhs_opt: term option,
   503   eqn_pos: int,
   504   user_eqn: term
   505 };
   506 
   507 type coeqn_data_sel = {
   508   fun_name: string,
   509   fun_T: typ,
   510   fun_args: term list,
   511   ctr: term,
   512   sel: term,
   513   rhs_term: term,
   514   ctr_rhs_opt: term option,
   515   code_rhs_opt: term option,
   516   eqn_pos: int,
   517   user_eqn: term
   518 };
   519 
   520 datatype coeqn_data =
   521   Disc of coeqn_data_disc |
   522   Sel of coeqn_data_sel;
   523 
   524 fun check_extra_variables lthy vars names eqn =
   525   let val b = fold_aterms (fn x as Free (v, _) =>
   526     if (not (member (op =) vars x) andalso
   527       not (member (op =) names v) andalso
   528       v <> Name.uu_ andalso
   529       not (Variable.is_fixed lthy v)) then cons x else I | _ => I) eqn []
   530   in
   531     null b orelse
   532     primcorec_error_eqn ("extra variable(s) in equation: " ^
   533       commas (map (Syntax.string_of_term lthy) b)) eqn
   534   end;
   535 
   536 fun dissect_coeqn_disc lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
   537     eqn_pos ctr_rhs_opt code_rhs_opt prems' concl matchedsss =
   538   let
   539     fun find_subterm p =
   540       let (* FIXME \<exists>? *)
   541         fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v)
   542           | find t = if p t then SOME t else NONE;
   543       in find end;
   544 
   545     val applied_fun = concl
   546       |> find_subterm (member (op = o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
   547       |> the
   548       handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl;
   549     val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
   550 
   551     val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in
   552         null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds
   553       end;
   554 
   555     val _ =
   556       let
   557         val bad = prems'
   558           |> filter (exists_subterm (fn Free (v, _) => member (op =) fun_names v | _ => false))
   559       in
   560         null bad orelse primcorec_error_eqns "corecursive call(s) in condition(s)" bad
   561       end;
   562 
   563     val _ = forall is_Free fun_args orelse
   564       primcorec_error_eqn ("non-variable function argument \"" ^
   565         Syntax.string_of_term lthy (find_first (not o is_Free) fun_args |> the) ^
   566           "\" (pattern matching is not supported by primcorec(ursive))") applied_fun
   567 
   568     val _ = let val d = duplicates (op =) fun_args in null d orelse
   569       primcorec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ "\"")
   570         applied_fun end;
   571 
   572     val SOME (sequential, basic_ctr_specs) =
   573       AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name;
   574 
   575     val discs = map #disc basic_ctr_specs;
   576     val ctrs = map #ctr basic_ctr_specs;
   577     val not_disc = head_of concl = @{term Not};
   578     val _ = not_disc andalso length ctrs <> 2 andalso
   579       primcorec_error_eqn "negated discriminator for a type with \<noteq> 2 constructors" concl;
   580     val disc' = find_subterm (member (op =) discs o head_of) concl;
   581     val eq_ctr0 = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd)
   582         |> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in
   583           if n >= 0 then SOME n else NONE end | _ => NONE);
   584 
   585     val _ = if is_some disc' andalso perhaps (try HOLogic.dest_not) concl <> the disc'
   586       then primcorec_error_eqn "malformed discriminator formula" concl else ();
   587 
   588 
   589     val _ = is_some disc' orelse is_some eq_ctr0 orelse
   590       primcorec_error_eqn "no discriminator in equation" concl;
   591     val ctr_no' =
   592       if is_none disc' then the eq_ctr0 else find_index (curry (op =) (head_of (the disc'))) discs;
   593     val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
   594     val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
   595 
   596     val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_;
   597     val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
   598     val prems = map (abstract (List.rev fun_args)) prems';
   599     val actual_prems =
   600       (if catch_all orelse sequential then maps s_not_conj matchedss else []) @
   601       (if catch_all then [] else prems);
   602 
   603     val matchedsss' = AList.delete (op =) fun_name matchedsss
   604       |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]);
   605 
   606     val user_eqn =
   607       (actual_prems, concl)
   608       |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args)
   609       |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies;
   610 
   611     val _ = check_extra_variables lthy fun_args fun_names user_eqn;
   612   in
   613     (Disc {
   614       fun_name = fun_name,
   615       fun_T = fun_T,
   616       fun_args = fun_args,
   617       ctr = ctr,
   618       ctr_no = ctr_no,
   619       disc = disc,
   620       prems = actual_prems,
   621       auto_gen = catch_all,
   622       ctr_rhs_opt = ctr_rhs_opt,
   623       code_rhs_opt = code_rhs_opt,
   624       eqn_pos = eqn_pos,
   625       user_eqn = user_eqn
   626     }, matchedsss')
   627   end;
   628 
   629 fun dissect_coeqn_sel lthy fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos
   630     ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn =
   631   let
   632     val (lhs, rhs) = HOLogic.dest_eq eqn
   633       handle TERM _ =>
   634              primcorec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
   635     val sel = head_of lhs;
   636     val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free
   637       handle TERM _ =>
   638              primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
   639 
   640     val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in
   641         null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds
   642       end;
   643 
   644     val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name)
   645       handle Option.Option =>
   646              primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
   647     val {ctr, ...} =
   648       (case of_spec_opt of
   649         SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
   650       | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
   651           handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn);
   652     val user_eqn = drop_all eqn0;
   653 
   654     val _ = check_extra_variables lthy fun_args fun_names user_eqn;
   655   in
   656     Sel {
   657       fun_name = fun_name,
   658       fun_T = fun_T,
   659       fun_args = fun_args,
   660       ctr = ctr,
   661       sel = sel,
   662       rhs_term = rhs,
   663       ctr_rhs_opt = ctr_rhs_opt,
   664       code_rhs_opt = code_rhs_opt,
   665       eqn_pos = eqn_pos,
   666       user_eqn = user_eqn
   667     }
   668   end;
   669 
   670 fun dissect_coeqn_ctr lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
   671     eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
   672   let
   673     val (lhs, rhs) = HOLogic.dest_eq concl;
   674     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
   675 
   676     val _ = check_extra_variables lthy fun_args fun_names (drop_all eqn0);
   677 
   678     val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
   679     val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
   680     val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
   681       handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
   682 
   683     val disc_concl = betapply (disc, lhs);
   684     val (eqn_data_disc_opt, matchedsss') =
   685       if null (tl basic_ctr_specs) then
   686         (NONE, matchedsss)
   687       else
   688         apfst SOME (dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos
   689           (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
   690 
   691     val sel_concls = sels ~~ ctr_args
   692       |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg))
   693         handle UnequalLengths =>
   694           primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
   695 
   696 (*
   697 val _ = tracing ("reduced\n    " ^ Syntax.string_of_term @{context} concl ^ "\nto\n    \<cdot> " ^
   698  (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n    \<cdot> ")) "" ^
   699  space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^
   700  "\nfor premise(s)\n    \<cdot> " ^
   701  space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) prems));
   702 *)
   703 
   704     val eqns_data_sel =
   705       map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos
   706         (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
   707   in
   708     (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss')
   709   end;
   710 
   711 fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss =
   712   let
   713     val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []);
   714     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
   715 
   716     val _ = check_extra_variables lthy fun_args fun_names concl;
   717 
   718     val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
   719 
   720     val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ =>
   721         if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs)
   722         else primcorec_error_eqn "not a constructor" ctr) [] rhs' []
   723       |> AList.group (op =);
   724 
   725     val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs);
   726     val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
   727         binder_types (fastype_of ctr)
   728         |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
   729           if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
   730         |> curry Term.list_comb ctr
   731         |> curry HOLogic.mk_eq lhs);
   732 
   733     val sequentials = replicate (length fun_names) false;
   734   in
   735     fold_map2 (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
   736         (SOME (abstract (List.rev fun_args) rhs)))
   737       ctr_premss ctr_concls matchedsss
   738   end;
   739 
   740 fun dissect_coeqn lthy has_call fun_names sequentials
   741     (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
   742   let
   743     val eqn = drop_all eqn0
   744       handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
   745     val (prems, concl) = Logic.strip_horn eqn
   746       |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop
   747         handle TERM _ => primcorec_error_eqn "malformed function equation" eqn;
   748 
   749     val head = concl
   750       |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
   751       |> head_of;
   752 
   753     val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (snd o HOLogic.dest_eq);
   754 
   755     val discs = maps (map #disc) basic_ctr_specss;
   756     val sels = maps (maps #sels) basic_ctr_specss;
   757     val ctrs = maps (map #ctr) basic_ctr_specss;
   758   in
   759     if member (op =) discs head orelse
   760         is_some rhs_opt andalso
   761           member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
   762       dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
   763         matchedsss
   764       |>> single
   765     else if member (op =) sels head then
   766       ([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
   767        matchedsss)
   768     else if is_some rhs_opt andalso
   769         is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
   770       if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then
   771         dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
   772           (if null prems then
   773              SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
   774            else
   775              NONE)
   776           prems concl matchedsss
   777       else if null prems then
   778         dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
   779         |>> flat
   780       else
   781         primcorec_error_eqn "cannot mix constructor and code views (see manual for details)" eqn
   782     else
   783       primcorec_error_eqn "malformed function equation" eqn
   784   end;
   785 
   786 fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
   787     ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
   788   if is_none (#pred (nth ctr_specs ctr_no)) then I else
   789     s_conjs prems
   790     |> curry subst_bounds (List.rev fun_args)
   791     |> abs_tuple_balanced fun_args
   792     |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
   793 
   794 fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel =
   795   find_first (curry (op =) sel o #sel) sel_eqns
   796   |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term)
   797   |> the_default undef_const
   798   |> K;
   799 
   800 fun build_corec_args_mutual_call lthy has_call (sel_eqns : coeqn_data_sel list) sel =
   801   (case find_first (curry (op =) sel o #sel) sel_eqns of
   802     NONE => (I, I, I)
   803   | SOME {fun_args, rhs_term, ... } =>
   804     let
   805       val bound_Ts = List.rev (map fastype_of fun_args);
   806       fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
   807       fun rewrite_end _ t = if has_call t then undef_const else t;
   808       fun rewrite_cont bound_Ts t =
   809         if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
   810       fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term
   811         |> abs_tuple_balanced fun_args;
   812     in
   813       (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
   814     end);
   815 
   816 fun build_corec_arg_nested_call lthy has_call (sel_eqns : coeqn_data_sel list) sel =
   817   (case find_first (curry (op =) sel o #sel) sel_eqns of
   818     NONE => I
   819   | SOME {fun_args, rhs_term, ...} =>
   820     let
   821       fun massage bound_Ts U T =
   822         let
   823           fun rewrite bound_Ts (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) b)
   824             | rewrite bound_Ts (t as _ $ _) =
   825               let val (u, vs) = strip_comb t in
   826                 if is_Free u andalso has_call u then
   827                   Inr_const U T $ mk_tuple1_balanced bound_Ts vs
   828                 else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
   829                   map (rewrite bound_Ts) vs |> chop 1
   830                   |>> HOLogic.mk_split o the_single
   831                   |> Term.list_comb
   832                 else
   833                   Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
   834               end
   835             | rewrite _ t =
   836               if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
   837           in
   838             rewrite bound_Ts
   839           end;
   840 
   841       val bound_Ts = List.rev (map fastype_of fun_args);
   842 
   843       fun build t =
   844         rhs_term
   845         |> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t))
   846         |> abs_tuple_balanced fun_args;
   847     in
   848       build
   849     end);
   850 
   851 fun build_corec_args_sel lthy has_call (all_sel_eqns : coeqn_data_sel list)
   852     (ctr_spec : corec_ctr_spec) =
   853   (case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of
   854     [] => I
   855   | sel_eqns =>
   856     let
   857       val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
   858       val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
   859       val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
   860       val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
   861     in
   862       I
   863       #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
   864       #> fold (fn (sel, (q, g, h)) =>
   865         let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
   866           nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
   867       #> fold (fn (sel, n) => nth_map n
   868         (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
   869     end);
   870 
   871 fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list)
   872     (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =
   873   let
   874     val corecs = map #corec corec_specs;
   875     val ctr_specss = map #ctr_specs corec_specs;
   876     val corec_args = hd corecs
   877       |> fst o split_last o binder_types o fastype_of
   878       |> map (fn T => if range_type T = HOLogic.boolT
   879           then Abs (Name.uu_, domain_type T, @{term False})
   880           else Const (@{const_name undefined}, T))
   881       |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
   882       |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
   883     fun currys [] t = t
   884       | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
   885           |> fold_rev (Term.abs o pair Name.uu) Ts;
   886 
   887 (*
   888 val _ = tracing ("corecursor arguments:\n    \<cdot> " ^
   889  space_implode "\n    \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
   890 *)
   891 
   892     val excludess' =
   893       disc_eqnss
   894       |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
   895         #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
   896         #> maps (uncurry (map o pair)
   897           #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
   898               ((c, c', a orelse a'), (x, s_not (s_conjs y)))
   899             ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
   900             ||> Logic.list_implies
   901             ||> curry Logic.list_all (map dest_Free fun_args))));
   902   in
   903     map (Term.list_comb o rpair corec_args) corecs
   904     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
   905     |> map2 currys arg_Tss
   906     |> Syntax.check_terms lthy
   907     |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
   908       bs mxs
   909     |> rpair excludess'
   910   end;
   911 
   912 fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec)
   913     (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) =
   914   let val num_disc_eqns = length disc_eqns in
   915     if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> length ctr_specs - 1 then
   916       disc_eqns
   917     else
   918       let
   919         val n = 0 upto length ctr_specs
   920           |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns));
   921         val {ctr, disc, ...} = nth ctr_specs n;
   922         val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
   923           |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
   924         val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
   925         val extra_disc_eqn = {
   926           fun_name = Binding.name_of fun_binding,
   927           fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
   928           fun_args = fun_args,
   929           ctr = ctr,
   930           ctr_no = n,
   931           disc = disc,
   932           prems = maps (s_not_conj o #prems) disc_eqns,
   933           auto_gen = true,
   934           ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
   935           code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
   936           eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *),
   937           user_eqn = undef_const};
   938       in
   939         chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
   940       end
   941   end;
   942 
   943 fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list)
   944     ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
   945   let
   946     val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
   947       |> find_index (curry (op =) sel) o #sels o the;
   948   in
   949     K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else [])
   950     |> nth_map sel_no |> AList.map_entry (op =) ctr
   951   end;
   952 
   953 fun applied_fun_of fun_name fun_T fun_args =
   954   Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
   955 
   956 fun is_trivial_implies thm =
   957   uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
   958 
   959 fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy =
   960   let
   961     val thy = Proof_Context.theory_of lthy;
   962 
   963     val (bs, mxs) = map_split (apfst fst) fixes;
   964     val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
   965 
   966     val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
   967         [] => ()
   968       | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
   969 
   970     val actual_nn = length bs;
   971 
   972     val sequentials = replicate actual_nn (member (op =) opts Sequential_Option);
   973     val exhaustives = replicate actual_nn (member (op =) opts Exhaustive_Option);
   974 
   975     val fun_names = map Binding.name_of bs;
   976     val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
   977     val frees = map (fst #>> Binding.name_of #> Free) fixes;
   978     val has_call = exists_subterm (member (op =) frees);
   979     val eqns_data =
   980       fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
   981         (tag_list 0 (map snd specs)) of_specs_opt []
   982       |> flat o fst;
   983 
   984     val _ =
   985       let
   986         val missing = fun_names
   987           |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data
   988             |> not oo member (op =))
   989       in
   990         null missing
   991           orelse primcorec_error_eqns ("missing equations for function(s): " ^ commas missing) []
   992       end;
   993 
   994     val callssss =
   995       map_filter (try (fn Sel x => x)) eqns_data
   996       |> partition_eq (op = o pairself #fun_name)
   997       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
   998       |> map (flat o snd)
   999       |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
  1000       |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
  1001         (ctr, map (K []) sels))) basic_ctr_specss);
  1002 
  1003 (*
  1004 val _ = tracing ("callssss = " ^ @{make_string} callssss);
  1005 *)
  1006 
  1007     val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
  1008           strong_coinduct_thms), lthy') =
  1009       corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
  1010     val corec_specs = take actual_nn corec_specs';
  1011     val ctr_specss = map #ctr_specs corec_specs;
  1012 
  1013     val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
  1014       |> partition_eq (op = o pairself #fun_name)
  1015       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
  1016       |> map (sort (op < o pairself #ctr_no |> make_ord) o flat o snd);
  1017 
  1018     val _ = disc_eqnss' |> map (fn x =>
  1019       let val d = duplicates (op = o pairself #ctr_no) x in null d orelse
  1020         (if forall (is_some o #ctr_rhs_opt) x then
  1021           primcorec_error_eqns "multiple equations for constructor(s)"
  1022             (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
  1023               |> map (the o #ctr_rhs_opt)) else
  1024           primcorec_error_eqns "excess discriminator formula in definition"
  1025             (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) end);
  1026 
  1027     val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
  1028       |> partition_eq (op = o pairself #fun_name)
  1029       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
  1030       |> map (flat o snd);
  1031 
  1032     val arg_Tss = map (binder_types o snd o fst) fixes;
  1033     val disc_eqnss = map6 mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
  1034       disc_eqnss';
  1035     val (defs, excludess') =
  1036       build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
  1037 
  1038     val tac_opts =
  1039       map (fn {code_rhs_opt, ...} :: _ =>
  1040         if auto orelse is_some code_rhs_opt then SOME (auto_tac o #context) else NONE) disc_eqnss;
  1041 
  1042     fun exclude_tac tac_opt sequential (c, c', a) =
  1043       if a orelse c = c' orelse sequential then
  1044         SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
  1045       else
  1046         tac_opt;
  1047 
  1048 (*
  1049 val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
  1050  space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
  1051 *)
  1052 
  1053     val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
  1054         (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
  1055            (exclude_tac tac_opt sequential j), goal))))
  1056       tac_opts sequentials excludess';
  1057 
  1058     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
  1059     val (goal_idxss, exclude_goalss) = excludess''
  1060       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
  1061       |> split_list o map split_list;
  1062 
  1063     fun list_all_fun_args extras =
  1064       map2 (fn [] => I
  1065           | {fun_args, ...} :: _ => map (curry Logic.list_all (extras @ map dest_Free fun_args)))
  1066         disc_eqnss;
  1067 
  1068     val syntactic_exhaustives =
  1069       map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns
  1070           orelse exists #auto_gen disc_eqns)
  1071         disc_eqnss;
  1072     val de_facto_exhaustives =
  1073       map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives;
  1074 
  1075     val nchotomy_goalss =
  1076       map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
  1077         de_facto_exhaustives disc_eqnss
  1078       |> list_all_fun_args []
  1079     val nchotomy_taut_thmss =
  1080       map5 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} =>
  1081           fn {code_rhs_opt, ...} :: _ => fn [] => K []
  1082             | [goal] => fn true =>
  1083               let
  1084                 val (_, _, arg_disc_exhausts, _, _) =
  1085                   case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
  1086               in
  1087                 [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
  1088                    mk_primcorec_nchotomy_tac ctxt (res_disc_exhausts @ arg_disc_exhausts))
  1089                  |> Thm.close_derivation]
  1090               end
  1091             | false =>
  1092               (case tac_opt of
  1093                 SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation]
  1094               | NONE => []))
  1095         tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives;
  1096 
  1097     val syntactic_exhaustives =
  1098       map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns
  1099           orelse exists #auto_gen disc_eqns)
  1100         disc_eqnss;
  1101 
  1102     val nchotomy_goalss =
  1103       map2 (fn (NONE, false) => map (rpair []) | _ => K []) (tac_opts ~~ syntactic_exhaustives)
  1104         nchotomy_goalss;
  1105 
  1106     val goalss = nchotomy_goalss @ exclude_goalss;
  1107 
  1108     fun prove thmss'' def_infos lthy =
  1109       let
  1110         val def_thms = map (snd o snd) def_infos;
  1111 
  1112         val (nchotomy_thmss, exclude_thmss) =
  1113           (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'');
  1114 
  1115         val ps =
  1116           Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
  1117 
  1118         val exhaust_thmss =
  1119           map2 (fn false => K []
  1120               | true => fn disc_eqns as {fun_args, ...} :: _ =>
  1121                 let
  1122                   val p = Bound (length fun_args);
  1123                   fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
  1124                 in
  1125                   [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)]
  1126                 end)
  1127             de_facto_exhaustives disc_eqnss
  1128           |> list_all_fun_args ps
  1129           |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
  1130               | [nchotomy_thm] => fn [goal] =>
  1131                 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
  1132                    (length disc_eqns) nchotomy_thm
  1133                  |> K |> Goal.prove_sorry lthy [] [] goal
  1134                  |> Thm.close_derivation])
  1135             disc_eqnss nchotomy_thmss;
  1136         val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
  1137 
  1138         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
  1139         fun mk_excludesss excludes n =
  1140           fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])))
  1141             excludes (map (fn k => replicate k [asm_rl] @ replicate (n - k) []) (0 upto n - 1));
  1142         val excludessss =
  1143           map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs)
  1144             (map2 append excludess' taut_thmss) corec_specs;
  1145 
  1146         fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss
  1147             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
  1148           if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then
  1149             []
  1150           else
  1151             let
  1152               val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
  1153               val k = 1 + ctr_no;
  1154               val m = length prems;
  1155               val goal =
  1156                 applied_fun_of fun_name fun_T fun_args
  1157                 |> curry betapply disc
  1158                 |> HOLogic.mk_Trueprop
  1159                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
  1160                 |> curry Logic.list_all (map dest_Free fun_args);
  1161             in
  1162               if prems = [@{term False}] then
  1163                 []
  1164               else
  1165                 mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
  1166                 |> K |> Goal.prove_sorry lthy [] [] goal
  1167                 |> Thm.close_derivation
  1168                 |> pair (#disc (nth ctr_specs ctr_no))
  1169                 |> pair eqn_pos
  1170                 |> single
  1171             end;
  1172 
  1173         fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
  1174               : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
  1175             ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, eqn_pos, ...} : coeqn_data_sel) =
  1176           let
  1177             val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs;
  1178             val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
  1179             val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
  1180               (find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
  1181             val sel_corec = find_index (curry (op =) sel) (#sels ctr_spec)
  1182               |> nth (#sel_corecs ctr_spec);
  1183             val k = 1 + ctr_no;
  1184             val m = length prems;
  1185             val goal =
  1186               applied_fun_of fun_name fun_T fun_args
  1187               |> curry betapply sel
  1188               |> rpair (abstract (List.rev fun_args) rhs_term)
  1189               |> HOLogic.mk_Trueprop o HOLogic.mk_eq
  1190               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
  1191               |> curry Logic.list_all (map dest_Free fun_args);
  1192             val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
  1193           in
  1194             mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
  1195               nested_map_idents nested_map_comps sel_corec k m excludesss
  1196             |> K |> Goal.prove_sorry lthy [] [] goal
  1197             |> Thm.close_derivation
  1198             |> pair sel
  1199             |> pair eqn_pos
  1200           end;
  1201 
  1202         fun prove_ctr disc_alist sel_alist (disc_eqns : coeqn_data_disc list)
  1203             (sel_eqns : coeqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) =
  1204           (* don't try to prove theorems when some sel_eqns are missing *)
  1205           if not (exists (curry (op =) ctr o #ctr) disc_eqns)
  1206               andalso not (exists (curry (op =) ctr o #ctr) sel_eqns)
  1207             orelse
  1208               filter (curry (op =) ctr o #ctr) sel_eqns
  1209               |> fst o finds (op = o apsnd #sel) sels
  1210               |> exists (null o snd) then
  1211             []
  1212           else
  1213             let
  1214               val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) =
  1215                 (find_first (curry (op =) ctr o #ctr) disc_eqns,
  1216                  find_first (curry (op =) ctr o #ctr) sel_eqns)
  1217                 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x,
  1218                   #ctr_rhs_opt x, #eqn_pos x))
  1219                 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #ctr_rhs_opt x,
  1220                   #eqn_pos x))
  1221                 |> the o merge_options;
  1222               val m = length prems;
  1223               val goal =
  1224                 (case rhs_opt of
  1225                   SOME rhs => rhs
  1226                 | NONE =>
  1227                   filter (curry (op =) ctr o #ctr) sel_eqns
  1228                   |> fst o finds (op = o apsnd #sel) sels
  1229                   |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
  1230                   |> curry Term.list_comb ctr)
  1231                 |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
  1232                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
  1233                 |> curry Logic.list_all (map dest_Free fun_args);
  1234               val disc_thm_opt = AList.lookup (op =) disc_alist disc;
  1235               val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);
  1236             in
  1237               if prems = [@{term False}] then [] else
  1238                 mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms
  1239                 |> K |> Goal.prove_sorry lthy [] [] goal
  1240                 |> Thm.close_derivation
  1241                 |> pair ctr
  1242                 |> pair eqn_pos
  1243                 |> single
  1244             end;
  1245 
  1246         fun prove_code exhaustive (disc_eqns : coeqn_data_disc list)
  1247             (sel_eqns : coeqn_data_sel list) nchotomys ctr_alist ctr_specs =
  1248           let
  1249             val fun_data_opt =
  1250               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
  1251                find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
  1252               |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x))
  1253               ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x))
  1254               |> merge_options;
  1255           in
  1256             (case fun_data_opt of
  1257               NONE => []
  1258             | SOME (fun_name, fun_T, fun_args, rhs_opt) =>
  1259               let
  1260                 val bound_Ts = List.rev (map fastype_of fun_args);
  1261 
  1262                 val lhs = applied_fun_of fun_name fun_T fun_args;
  1263                 val rhs_info_opt =
  1264                   (case rhs_opt of
  1265                     SOME rhs =>
  1266                     let
  1267                       val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
  1268                       val cond_ctrs =
  1269                         fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
  1270                       val ctr_thms =
  1271                         map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
  1272                     in SOME (false, rhs, raw_rhs, ctr_thms) end
  1273                   | NONE =>
  1274                     let
  1275                       fun prove_code_ctr ({ctr, sels, ...} : corec_ctr_spec) =
  1276                         if not (exists (curry (op =) ctr o fst) ctr_alist) then NONE else
  1277                           let
  1278                             val prems = find_first (curry (op =) ctr o #ctr) disc_eqns
  1279                               |> Option.map #prems |> the_default [];
  1280                             val t =
  1281                               filter (curry (op =) ctr o #ctr) sel_eqns
  1282                               |> fst o finds (op = o apsnd #sel) sels
  1283                               |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x))
  1284                                 #-> abstract)
  1285                               |> curry Term.list_comb ctr;
  1286                           in
  1287                             SOME (prems, t)
  1288                           end;
  1289                       val ctr_conds_argss_opt = map prove_code_ctr ctr_specs;
  1290                       val exhaustive_code =
  1291                         exhaustive
  1292                         orelse exists (is_some andf (null o fst o the)) ctr_conds_argss_opt
  1293                         orelse forall is_some ctr_conds_argss_opt
  1294                           andalso exists #auto_gen disc_eqns;
  1295                       val rhs =
  1296                         (if exhaustive_code then
  1297                            split_last (map_filter I ctr_conds_argss_opt) ||> snd
  1298                          else
  1299                            Const (@{const_name Code.abort}, @{typ String.literal} -->
  1300                                (HOLogic.unitT --> body_type fun_T) --> body_type fun_T) $
  1301                              HOLogic.mk_literal fun_name $
  1302                              absdummy HOLogic.unitT (incr_boundvars 1 lhs)
  1303                            |> pair (map_filter I ctr_conds_argss_opt))
  1304                          |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
  1305                     in
  1306                       SOME (exhaustive_code, rhs, rhs, map snd ctr_alist)
  1307                     end);
  1308               in
  1309                 (case rhs_info_opt of
  1310                   NONE => []
  1311                 | SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) =>
  1312                   let
  1313                     val ms = map (Logic.count_prems o prop_of) ctr_thms;
  1314                     val (raw_goal, goal) = (raw_rhs, rhs)
  1315                       |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
  1316                         #> curry Logic.list_all (map dest_Free fun_args));
  1317                     val (distincts, discIs, _, sel_splits, sel_split_asms) =
  1318                       case_thms_of_term lthy raw_rhs;
  1319 
  1320                     val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
  1321                         sel_split_asms ms ctr_thms
  1322                         (if exhaustive_code then try the_single nchotomys else NONE)
  1323                       |> K |> Goal.prove_sorry lthy [] [] raw_goal
  1324                       |> Thm.close_derivation;
  1325                   in
  1326                     mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
  1327                     |> K |> Goal.prove_sorry lthy [] [] goal
  1328                     |> Thm.close_derivation
  1329                     |> single
  1330                   end)
  1331               end)
  1332           end;
  1333 
  1334         val disc_alistss = map3 (map oo prove_disc) corec_specs excludessss disc_eqnss;
  1335         val disc_alists = map (map snd o flat) disc_alistss;
  1336         val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
  1337         val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss;
  1338         val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
  1339         val sel_thmss = map (map snd o sort_list_duplicates) sel_alists;
  1340 
  1341         fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
  1342             (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
  1343             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
  1344           if null exhaust_thms orelse null disc_thms then
  1345             []
  1346           else
  1347             let
  1348               val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
  1349               val goal =
  1350                 mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc,
  1351                   mk_conjs prems)
  1352                 |> curry Logic.list_all (map dest_Free fun_args);
  1353             in
  1354               mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
  1355                 (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
  1356               |> K |> Goal.prove_sorry lthy [] [] goal
  1357               |> Thm.close_derivation
  1358               |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
  1359                 @{thms eqTrueE eq_False[THEN iffD1] notnotD}
  1360               |> pair eqn_pos
  1361               |> single
  1362             end;
  1363 
  1364         val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
  1365           disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
  1366           |> map sort_list_duplicates;
  1367 
  1368         val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists)
  1369           disc_eqnss sel_eqnss ctr_specss;
  1370         val ctr_thmss' = map (map snd) ctr_alists;
  1371         val ctr_thmss = map (map snd o order_list) ctr_alists;
  1372 
  1373         val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
  1374           ctr_specss;
  1375 
  1376         val disc_iff_or_disc_thmss =
  1377           map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss;
  1378         val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
  1379 
  1380         val common_name = mk_common_name fun_names;
  1381 
  1382         val anonymous_notes =
  1383           [(flat disc_iff_or_disc_thmss, simp_attrs)]
  1384           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
  1385 
  1386         val notes =
  1387           [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
  1388            (codeN, code_thmss, code_nitpicksimp_attrs),
  1389            (ctrN, ctr_thmss, []),
  1390            (discN, disc_thmss, []),
  1391            (disc_iffN, disc_iff_thmss, []),
  1392            (excludeN, exclude_thmss, []),
  1393            (exhaustN, nontriv_exhaust_thmss, []),
  1394            (selN, sel_thmss, simp_attrs),
  1395            (simpsN, simp_thmss, []),
  1396            (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
  1397           |> maps (fn (thmN, thmss, attrs) =>
  1398             map2 (fn fun_name => fn thms =>
  1399                 ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
  1400               fun_names (take actual_nn thmss))
  1401           |> filter_out (null o fst o hd o snd);
  1402 
  1403         val common_notes =
  1404           [(coinductN, if n2m then [coinduct_thm] else [], []),
  1405            (strong_coinductN, if n2m then [strong_coinduct_thm] else [], [])]
  1406           |> filter_out (null o #2)
  1407           |> map (fn (thmN, thms, attrs) =>
  1408             ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
  1409       in
  1410         lthy
  1411         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
  1412         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
  1413         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
  1414         |> Local_Theory.notes (anonymous_notes @ notes @ common_notes)
  1415         |> snd
  1416       end;
  1417 
  1418     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
  1419   in
  1420     (goalss, after_qed, lthy')
  1421   end;
  1422 
  1423 fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs') lthy =
  1424   let
  1425     val (raw_specs, of_specs_opt) =
  1426       split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
  1427     val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
  1428   in
  1429     add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
  1430     handle ERROR str => primcorec_error str
  1431   end
  1432   handle PRIMCOREC (str, eqns) =>
  1433          if null eqns then
  1434            error ("primcorec error:\n  " ^ str)
  1435          else
  1436            error ("primcorec error:\n  " ^ str ^ "\nin\n  " ^
  1437              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
  1438 
  1439 val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
  1440   lthy
  1441   |> Proof.theorem NONE after_qed goalss
  1442   |> Proof.refine (Method.primitive_text (K I))
  1443   |> Seq.hd) ooo add_primcorec_ursive_cmd false;
  1444 
  1445 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
  1446   lthy
  1447   |> after_qed (map (fn [] => []
  1448       | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
  1449     goalss)) ooo add_primcorec_ursive_cmd true;
  1450 
  1451 val primcorec_option_parser = Parse.group (fn () => "option")
  1452   (Parse.reserved "sequential" >> K Sequential_Option
  1453   || Parse.reserved "exhaustive" >> K Exhaustive_Option)
  1454 
  1455 val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
  1456   (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
  1457 
  1458 val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
  1459   "define primitive corecursive functions"
  1460   ((Scan.optional (@{keyword "("} |--
  1461       Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
  1462     (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
  1463 
  1464 val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
  1465   "define primitive corecursive functions"
  1466   ((Scan.optional (@{keyword "("} |--
  1467       Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
  1468     (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
  1469 
  1470 end;