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