src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
changeset 62692 0701f25fac39
child 64558 63c76802ab5e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,481 @@
     1.4 +(*  Title:      HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
     1.5 +    Author:     Aymeric Bouzy, Ecole polytechnique
     1.6 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.7 +    Copyright   2015, 2016
     1.8 +
     1.9 +Library for generalized corecursor sugar.
    1.10 +*)
    1.11 +
    1.12 +signature BNF_GFP_GREC_SUGAR_UTIL =
    1.13 +sig
    1.14 +  type s_parse_info =
    1.15 +    {outer_buffer: BNF_GFP_Grec.buffer,
    1.16 +     ctr_guards: term Symtab.table,
    1.17 +     inner_buffer: BNF_GFP_Grec.buffer}
    1.18 +
    1.19 +  type rho_parse_info =
    1.20 +    {pattern_ctrs: (term * term list) Symtab.table,
    1.21 +     discs: term Symtab.table,
    1.22 +     sels: term Symtab.table,
    1.23 +     it: term,
    1.24 +     mk_case: typ -> term}
    1.25 +
    1.26 +  exception UNNATURAL of unit
    1.27 +
    1.28 +  val generalize_types: int -> typ -> typ -> typ
    1.29 +  val mk_curry_uncurryN_balanced: Proof.context -> int -> thm
    1.30 +  val mk_const_transfer_goal: Proof.context -> string * typ -> term
    1.31 +  val mk_abs_transfer: Proof.context -> string -> thm
    1.32 +  val mk_rep_transfer: Proof.context -> string -> thm
    1.33 +  val mk_pointful_natural_from_transfer: Proof.context -> thm -> thm
    1.34 +
    1.35 +  val corec_parse_info_of: Proof.context -> typ list -> typ -> BNF_GFP_Grec.buffer -> s_parse_info
    1.36 +  val friend_parse_info_of: Proof.context -> typ list -> typ -> BNF_GFP_Grec.buffer ->
    1.37 +    s_parse_info * rho_parse_info
    1.38 +end;
    1.39 +
    1.40 +structure BNF_GFP_Grec_Sugar_Util : BNF_GFP_GREC_SUGAR_UTIL =
    1.41 +struct
    1.42 +
    1.43 +open Ctr_Sugar
    1.44 +open BNF_Util
    1.45 +open BNF_Tactics
    1.46 +open BNF_Def
    1.47 +open BNF_Comp
    1.48 +open BNF_FP_Util
    1.49 +open BNF_FP_Def_Sugar
    1.50 +open BNF_GFP_Grec
    1.51 +open BNF_GFP_Grec_Tactics
    1.52 +
    1.53 +val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum;
    1.54 +
    1.55 +fun not_codatatype ctxt T =
    1.56 +  error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
    1.57 +
    1.58 +fun generalize_types max_j T U =
    1.59 +  let
    1.60 +    val vars = Unsynchronized.ref [];
    1.61 +
    1.62 +    fun var_of T U =
    1.63 +      (case AList.lookup (op =) (!vars) (T, U) of
    1.64 +        SOME V => V
    1.65 +      | NONE =>
    1.66 +        let val V = TVar ((Name.aT, length (!vars) + max_j), @{sort type}) in
    1.67 +          vars := ((T, U), V) :: !vars; V
    1.68 +        end);
    1.69 +
    1.70 +    fun gen (T as Type (s, Ts)) (U as Type (s', Us)) =
    1.71 +        if s = s' then Type (s, map2 gen Ts Us) else var_of T U
    1.72 +      | gen T U = if T = U then T else var_of T U;
    1.73 +  in
    1.74 +    gen T U
    1.75 +  end;
    1.76 +
    1.77 +fun mk_curry_uncurryN_balanced_raw ctxt n =
    1.78 +  let
    1.79 +    val ((As, B), names_ctxt) = ctxt
    1.80 +      |> mk_TFrees (n + 1)
    1.81 +      |>> split_last;
    1.82 +
    1.83 +    val tupled_As = mk_tupleT_balanced As;
    1.84 +
    1.85 +    val f_T = As ---> B;
    1.86 +    val g_T = tupled_As --> B;
    1.87 +
    1.88 +    val (((f, g), xs), _) = names_ctxt
    1.89 +      |> yield_singleton (mk_Frees "f") f_T
    1.90 +      ||>> yield_singleton (mk_Frees "g") g_T
    1.91 +      ||>> mk_Frees "x" As;
    1.92 +
    1.93 +    val tupled_xs = mk_tuple1_balanced As xs;
    1.94 +
    1.95 +    val uncurried_f = mk_tupled_fun f tupled_xs xs;
    1.96 +    val curried_g = abs_curried_balanced As g;
    1.97 +
    1.98 +    val lhs = HOLogic.mk_eq (uncurried_f, g);
    1.99 +    val rhs =  HOLogic.mk_eq (f, curried_g);
   1.100 +    val goal = fold_rev Logic.all [f, g] (mk_Trueprop_eq (lhs, rhs));
   1.101 +
   1.102 +    fun mk_tac ctxt =
   1.103 +      HEADGOAL (rtac ctxt iffI THEN' dtac ctxt sym THEN' hyp_subst_tac ctxt) THEN
   1.104 +      unfold_thms_tac ctxt @{thms prod.case} THEN
   1.105 +      HEADGOAL (rtac ctxt refl THEN' hyp_subst_tac ctxt THEN'
   1.106 +        REPEAT_DETERM o subst_tac ctxt NONE @{thms unit_abs_eta_conv case_prod_eta} THEN'
   1.107 +        rtac ctxt refl);
   1.108 +  in
   1.109 +    Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, ...} => mk_tac ctxt)
   1.110 +    |> Thm.close_derivation
   1.111 +  end;
   1.112 +
   1.113 +val num_curry_uncurryN_balanced_precomp = 8;
   1.114 +val curry_uncurryN_balanced_precomp =
   1.115 +  map (mk_curry_uncurryN_balanced_raw @{context}) (0 upto num_curry_uncurryN_balanced_precomp);
   1.116 +
   1.117 +fun mk_curry_uncurryN_balanced ctxt n =
   1.118 +  if n <= num_curry_uncurryN_balanced_precomp then nth curry_uncurryN_balanced_precomp n
   1.119 +  else mk_curry_uncurryN_balanced_raw ctxt n;
   1.120 +
   1.121 +fun mk_const_transfer_goal ctxt (s, var_T) =
   1.122 +  let
   1.123 +    val var_As = Term.add_tvarsT var_T [];
   1.124 +
   1.125 +    val ((As, Bs), names_ctxt) = ctxt
   1.126 +      |> Variable.declare_typ var_T
   1.127 +      |> mk_TFrees' (map snd var_As)
   1.128 +      ||>> mk_TFrees' (map snd var_As);
   1.129 +
   1.130 +    val (Rs, _) = names_ctxt
   1.131 +      |> mk_Frees "R" (map2 mk_pred2T As Bs);
   1.132 +
   1.133 +    val T = Term.typ_subst_TVars (map fst var_As ~~ As) var_T;
   1.134 +    val U = Term.typ_subst_TVars (map fst var_As ~~ Bs) var_T;
   1.135 +  in
   1.136 +    mk_parametricity_goal ctxt Rs (Const (s, T)) (Const (s, U))
   1.137 +    |> tap (fn goal => can type_of goal orelse
   1.138 +      error ("Cannot transfer constant " ^ quote (Syntax.string_of_term ctxt (Const (s, T))) ^
   1.139 +        " from type " ^ quote (Syntax.string_of_typ ctxt T) ^ " to " ^
   1.140 +        quote (Syntax.string_of_typ ctxt U)))
   1.141 +  end;
   1.142 +
   1.143 +fun mk_abs_transfer ctxt fpT_name =
   1.144 +  let
   1.145 +    val SOME {pre_bnf, absT_info = {absT, repT, abs, type_definition, ...}, ...} =
   1.146 +      fp_sugar_of ctxt fpT_name;
   1.147 +  in
   1.148 +    if absT = repT then
   1.149 +      raise Fail "no abs/rep"
   1.150 +    else
   1.151 +      let
   1.152 +        val rel_def = rel_def_of_bnf pre_bnf;
   1.153 +
   1.154 +        val absT = T_of_bnf pre_bnf
   1.155 +          |> singleton (freeze_types ctxt (map dest_TVar (lives_of_bnf pre_bnf)));
   1.156 +
   1.157 +        val goal = mk_const_transfer_goal ctxt (dest_Const (mk_abs absT abs))
   1.158 +      in
   1.159 +        Variable.add_free_names ctxt goal []
   1.160 +        |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.161 +          unfold_thms_tac ctxt [rel_def] THEN
   1.162 +          HEADGOAL (rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
   1.163 +      end
   1.164 +  end;
   1.165 +
   1.166 +fun mk_rep_transfer ctxt fpT_name =
   1.167 +  let
   1.168 +    val SOME {pre_bnf, absT_info = {absT, repT, rep, ...}, ...} = fp_sugar_of ctxt fpT_name;
   1.169 +  in
   1.170 +    if absT = repT then
   1.171 +      raise Fail "no abs/rep"
   1.172 +    else
   1.173 +      let
   1.174 +        val rel_def = rel_def_of_bnf pre_bnf;
   1.175 +
   1.176 +        val absT = T_of_bnf pre_bnf
   1.177 +          |> singleton (freeze_types ctxt (map dest_TVar (lives_of_bnf pre_bnf)));
   1.178 +
   1.179 +        val goal = mk_const_transfer_goal ctxt (dest_Const (mk_rep absT rep))
   1.180 +      in
   1.181 +        Variable.add_free_names ctxt goal []
   1.182 +        |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.183 +          unfold_thms_tac ctxt [rel_def] THEN
   1.184 +          HEADGOAL (rtac ctxt @{thm vimage2p_rel_fun})))
   1.185 +      end
   1.186 +  end;
   1.187 +
   1.188 +exception UNNATURAL of unit;
   1.189 +
   1.190 +fun mk_pointful_natural_from_transfer ctxt transfer =
   1.191 +  let
   1.192 +    val _ $ (_ $ Const (s, T0) $ Const (_, U0)) = Thm.prop_of transfer;
   1.193 +    val [T, U] = freeze_types ctxt [] [T0, U0];
   1.194 +    val var_T = generalize_types 0 T U;
   1.195 +
   1.196 +    val var_As = map TVar (rev (Term.add_tvarsT var_T []));
   1.197 +
   1.198 +    val ((As, Bs), names_ctxt) = ctxt
   1.199 +      |> mk_TFrees' (map Type.sort_of_atyp var_As)
   1.200 +      ||>> mk_TFrees' (map Type.sort_of_atyp var_As);
   1.201 +
   1.202 +    val TA = typ_subst_atomic (var_As ~~ As) var_T;
   1.203 +
   1.204 +    val ((xs, fs), _) = names_ctxt
   1.205 +      |> mk_Frees "x" (binder_types TA)
   1.206 +      ||>> mk_Frees "f" (map2 (curry (op -->)) As Bs);
   1.207 +
   1.208 +    val AB_fs = (As ~~ Bs) ~~ fs;
   1.209 +
   1.210 +    fun build_applied_map TU t =
   1.211 +      if op = TU then
   1.212 +        t
   1.213 +      else
   1.214 +        (case try (build_map ctxt [] (the o AList.lookup (op =) AB_fs)) TU of
   1.215 +          SOME mapx => mapx $ t
   1.216 +        | NONE => raise UNNATURAL ());
   1.217 +
   1.218 +    fun unextensionalize (f $ (x as Free _), rhs) = unextensionalize (f, lambda x rhs)
   1.219 +      | unextensionalize tu = tu;
   1.220 +
   1.221 +    val TB = typ_subst_atomic (var_As ~~ Bs) var_T;
   1.222 +
   1.223 +    val (binder_TAs, body_TA) = strip_type TA;
   1.224 +    val (binder_TBs, body_TB) = strip_type TB;
   1.225 +
   1.226 +    val n = length var_As;
   1.227 +    val m = length binder_TAs;
   1.228 +
   1.229 +    val A_nesting_bnfs = nesting_bnfs ctxt [[body_TA :: binder_TAs]] As;
   1.230 +    val A_nesting_map_ids = map map_id_of_bnf A_nesting_bnfs;
   1.231 +    val A_nesting_rel_Grps = map rel_Grp_of_bnf A_nesting_bnfs;
   1.232 +
   1.233 +    val ta = Const (s, TA);
   1.234 +    val tb = Const (s, TB);
   1.235 +    val xfs = @{map 3} (curry build_applied_map) binder_TAs binder_TBs xs;
   1.236 +
   1.237 +    val goal = (list_comb (tb, xfs), build_applied_map (body_TA, body_TB) (list_comb (ta, xs)))
   1.238 +      |> unextensionalize |> mk_Trueprop_eq;
   1.239 +
   1.240 +    val _ = if can type_of goal then () else raise UNNATURAL ();
   1.241 +
   1.242 +    val vars = map (fst o dest_Free) (xs @ fs);
   1.243 +  in
   1.244 +    Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
   1.245 +      mk_natural_from_transfer_tac ctxt m (replicate n true) transfer A_nesting_map_ids
   1.246 +        A_nesting_rel_Grps [])
   1.247 +    |> Thm.close_derivation
   1.248 +  end;
   1.249 +
   1.250 +type s_parse_info =
   1.251 +  {outer_buffer: BNF_GFP_Grec.buffer,
   1.252 +   ctr_guards: term Symtab.table,
   1.253 +   inner_buffer: BNF_GFP_Grec.buffer};
   1.254 +
   1.255 +type rho_parse_info =
   1.256 +  {pattern_ctrs: (term * term list) Symtab.table,
   1.257 +   discs: term Symtab.table,
   1.258 +   sels: term Symtab.table,
   1.259 +   it: term,
   1.260 +   mk_case: typ -> term};
   1.261 +
   1.262 +fun curry_friend (T, t) =
   1.263 +  let
   1.264 +    val prod_T = domain_type (fastype_of t);
   1.265 +    val Ts = dest_tupleT_balanced (num_binder_types T) prod_T;
   1.266 +    val xs = map_index (fn (i, T) => Free ("x" ^ string_of_int i, T)) Ts;
   1.267 +    val body = mk_tuple_balanced xs;
   1.268 +  in
   1.269 +    (T, fold_rev Term.lambda xs (t $ body))
   1.270 +  end;
   1.271 +
   1.272 +fun curry_friends ({Oper, VLeaf, CLeaf, ctr_wrapper, friends} : buffer) =
   1.273 +  {Oper = Oper, VLeaf = VLeaf, CLeaf = CLeaf, ctr_wrapper = ctr_wrapper,
   1.274 +   friends = Symtab.map (K curry_friend) friends};
   1.275 +
   1.276 +fun checked_gfp_sugar_of lthy (T as Type (T_name, _)) =
   1.277 +    (case fp_sugar_of lthy T_name of
   1.278 +      SOME (sugar as {fp = Greatest_FP, ...}) => sugar
   1.279 +    | _ => not_codatatype lthy T)
   1.280 +  | checked_gfp_sugar_of lthy T = not_codatatype lthy T;
   1.281 +
   1.282 +fun generic_spec_of friend ctxt arg_Ts res_T (raw_buffer0 as {VLeaf = VLeaf0, ...}) =
   1.283 +  let
   1.284 +    val thy = Proof_Context.theory_of ctxt;
   1.285 +
   1.286 +    val tupled_arg_T = mk_tupleT_balanced arg_Ts;
   1.287 +
   1.288 +    val {T = fpT, X, fp_res_index, fp_res = {ctors = ctors0, ...},
   1.289 +         absT_info = {abs = abs0, rep = rep0, ...},
   1.290 +         fp_ctr_sugar = {ctrXs_Tss, ctr_sugar = {ctrs = ctrs0, casex = case0, discs = discs0,
   1.291 +           selss = selss0, sel_defs, ...}, ...}, ...} =
   1.292 +      checked_gfp_sugar_of ctxt res_T;
   1.293 +
   1.294 +    val VLeaf0_T = fastype_of VLeaf0;
   1.295 +    val Y = domain_type VLeaf0_T;
   1.296 +
   1.297 +    val raw_buffer = specialize_buffer_types raw_buffer0;
   1.298 +
   1.299 +    val As_rho = tvar_subst thy [fpT] [res_T];
   1.300 +
   1.301 +    val substAT = Term.typ_subst_TVars As_rho;
   1.302 +    val substA = Term.subst_TVars As_rho;
   1.303 +    val substYT = Tsubst Y tupled_arg_T;
   1.304 +    val substY = substT Y tupled_arg_T;
   1.305 +
   1.306 +    val Ys_rho_inner = if friend then [] else [(Y, tupled_arg_T)];
   1.307 +    val substYT_inner = substAT o Term.typ_subst_atomic Ys_rho_inner;
   1.308 +    val substY_inner = substA o Term.subst_atomic_types Ys_rho_inner;
   1.309 +
   1.310 +    val mid_T = substYT_inner (range_type VLeaf0_T);
   1.311 +
   1.312 +    val substXT_mid = Tsubst X mid_T;
   1.313 +
   1.314 +    val XifyT = typ_subst_nonatomic [(res_T, X)];
   1.315 +    val YifyT = typ_subst_nonatomic [(res_T, Y)];
   1.316 +
   1.317 +    val substXYT = Tsubst X Y;
   1.318 +
   1.319 +    val ctor0 = nth ctors0 fp_res_index;
   1.320 +    val ctor = enforce_type ctxt range_type res_T ctor0;
   1.321 +    val preT = YifyT (domain_type (fastype_of ctor));
   1.322 +
   1.323 +    val n = length ctrs0;
   1.324 +    val ks = 1 upto n;
   1.325 +
   1.326 +    fun mk_ctr_guards () =
   1.327 +      let
   1.328 +        val ctr_Tss = map (map (substXT_mid o substAT)) ctrXs_Tss;
   1.329 +        val preT = XifyT (domain_type (fastype_of ctor));
   1.330 +        val mid_preT = substXT_mid preT;
   1.331 +        val abs = enforce_type ctxt range_type mid_preT abs0;
   1.332 +        val absT = range_type (fastype_of abs);
   1.333 +
   1.334 +        fun mk_ctr_guard k ctr_Ts (Const (s, _)) =
   1.335 +          let
   1.336 +            val xs = map_index (fn (i, T) => Free ("x" ^ string_of_int i, T)) ctr_Ts;
   1.337 +            val body = mk_absumprod absT abs n k xs;
   1.338 +          in
   1.339 +            (s, fold_rev Term.lambda xs body)
   1.340 +          end;
   1.341 +      in
   1.342 +        Symtab.make (@{map 3} mk_ctr_guard ks ctr_Tss ctrs0)
   1.343 +      end;
   1.344 +
   1.345 +    val substYT_mid = substYT o Tsubst Y mid_T;
   1.346 +
   1.347 +    val outer_T = substYT_mid preT;
   1.348 +
   1.349 +    val substY_outer = substY o substT Y outer_T;
   1.350 +
   1.351 +    val outer_buffer = curry_friends (map_buffer substY_outer raw_buffer);
   1.352 +    val ctr_guards = mk_ctr_guards ();
   1.353 +    val inner_buffer = curry_friends (map_buffer substY_inner raw_buffer);
   1.354 +
   1.355 +    val s_parse_info =
   1.356 +      {outer_buffer = outer_buffer, ctr_guards = ctr_guards, inner_buffer = inner_buffer};
   1.357 +
   1.358 +    fun mk_friend_spec () =
   1.359 +      let
   1.360 +        fun encapsulate_nested U T free =
   1.361 +          betapply (build_map ctxt [] (fn (T, _) =>
   1.362 +              if T = domain_type VLeaf0_T then Abs (Name.uu, T, VLeaf0 $ Bound 0)
   1.363 +              else Abs (Name.uu, T, Bound 0)) (T, U),
   1.364 +            free);
   1.365 +
   1.366 +        val preT = YifyT (domain_type (fastype_of ctor));
   1.367 +        val YpreT = HOLogic.mk_prodT (Y, preT);
   1.368 +
   1.369 +        val rep = rep0 |> enforce_type ctxt domain_type (substXT_mid (XifyT preT));
   1.370 +
   1.371 +        fun mk_disc k =
   1.372 +          ctrXs_Tss
   1.373 +          |> map_index (fn (i, Ts) =>
   1.374 +            Abs (Name.uu, mk_tupleT_balanced Ts,
   1.375 +              if i + 1 = k then @{const HOL.True} else @{const HOL.False}))
   1.376 +          |> mk_case_sumN_balanced
   1.377 +          |> map_types substXYT
   1.378 +          |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
   1.379 +          |> map_types substAT;
   1.380 +
   1.381 +        val all_discs = map mk_disc ks;
   1.382 +
   1.383 +        fun mk_pair (Const (disc_name, _)) disc = SOME (disc_name, disc)
   1.384 +          | mk_pair _ _ = NONE;
   1.385 +
   1.386 +        val discs = @{map 2} mk_pair discs0 all_discs
   1.387 +          |> map_filter I |> Symtab.make;
   1.388 +
   1.389 +        fun mk_sel sel_def =
   1.390 +          let
   1.391 +            val (sel_name, case_functions) =
   1.392 +              sel_def
   1.393 +              |> Object_Logic.rulify ctxt
   1.394 +              |> Thm.concl_of
   1.395 +              |> perhaps (try drop_all)
   1.396 +              |> perhaps (try HOLogic.dest_Trueprop)
   1.397 +              |> HOLogic.dest_eq
   1.398 +              |>> fst o strip_comb
   1.399 +              |>> fst o dest_Const
   1.400 +              ||> fst o dest_comb
   1.401 +              ||> snd o strip_comb
   1.402 +              ||> map (map_types (XifyT o substAT));
   1.403 +
   1.404 +            fun encapsulate_case_function case_function =
   1.405 +              let
   1.406 +                fun encapsulate bound_Ts [] case_function =
   1.407 +                    let val T = fastype_of1 (bound_Ts, case_function) in
   1.408 +                      encapsulate_nested (substXT_mid T) (substXYT T) case_function
   1.409 +                    end
   1.410 +                  | encapsulate bound_Ts (T :: Ts) case_function =
   1.411 +                    Abs (Name.uu, T,
   1.412 +                      encapsulate (T :: bound_Ts) Ts
   1.413 +                        (betapply (incr_boundvars 1 case_function, Bound 0)));
   1.414 +              in
   1.415 +                encapsulate [] (binder_types (fastype_of case_function)) case_function
   1.416 +              end;
   1.417 +          in
   1.418 +            (sel_name, ctrXs_Tss
   1.419 +              |> map (map_index (fn (i, T) => Free ("x" ^ string_of_int (i + 1), T)))
   1.420 +              |> `(map mk_tuple_balanced)
   1.421 +              |> uncurry (@{map 3} mk_tupled_fun (map encapsulate_case_function case_functions))
   1.422 +              |> mk_case_sumN_balanced
   1.423 +              |> map_types substXYT
   1.424 +              |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
   1.425 +              |> map_types substAT)
   1.426 +          end;
   1.427 +
   1.428 +        val sels = Symtab.make (map mk_sel sel_defs);
   1.429 +
   1.430 +        fun mk_disc_sels_pair disc sels =
   1.431 +          if forall is_some sels then SOME (disc, map the sels) else NONE;
   1.432 +
   1.433 +        val pattern_ctrs = (ctrs0, selss0)
   1.434 +          ||> map (map (try dest_Const #> Option.mapPartial (fst #> Symtab.lookup sels)))
   1.435 +          ||> @{map 2} mk_disc_sels_pair all_discs
   1.436 +          |>> map (dest_Const #> fst)
   1.437 +          |> op ~~
   1.438 +          |> map_filter (fn (s, opt) => if is_some opt then SOME (s, the opt) else NONE)
   1.439 +          |> Symtab.make;
   1.440 +
   1.441 +        val it = HOLogic.mk_comp (VLeaf0, fst_const YpreT);
   1.442 +
   1.443 +        val mk_case =
   1.444 +          let
   1.445 +            val abs_fun_tms = case0
   1.446 +              |> fastype_of
   1.447 +              |> substAT
   1.448 +              |> XifyT
   1.449 +              |> binder_fun_types
   1.450 +              |> map_index (fn (i, T) => Free ("f" ^ string_of_int (i + 1), T));
   1.451 +            val arg_Uss = abs_fun_tms
   1.452 +              |> map fastype_of
   1.453 +              |> map binder_types;
   1.454 +            val arg_Tss = arg_Uss
   1.455 +              |> map (map substXYT);
   1.456 +            val case0 =
   1.457 +              arg_Tss
   1.458 +              |> map (map_index (fn (i, T) => Free ("x" ^ string_of_int (i + 1), T)))
   1.459 +              |> `(map mk_tuple_balanced)
   1.460 +              ||> @{map 3} (@{map 3} encapsulate_nested) arg_Uss arg_Tss
   1.461 +              |> uncurry (@{map 3} mk_tupled_fun abs_fun_tms)
   1.462 +              |> mk_case_sumN_balanced
   1.463 +              |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
   1.464 +              |> fold_rev lambda abs_fun_tms
   1.465 +              |> map_types (substAT o substXT_mid);
   1.466 +          in
   1.467 +            fn U => case0
   1.468 +              |> substT (body_type (fastype_of case0)) U
   1.469 +              |> Syntax.check_term ctxt
   1.470 +          end;
   1.471 +      in
   1.472 +        {pattern_ctrs = pattern_ctrs, discs = discs, sels = sels, it = it, mk_case = mk_case}
   1.473 +      end;
   1.474 +  in
   1.475 +    (s_parse_info, mk_friend_spec)
   1.476 +  end;
   1.477 +
   1.478 +fun corec_parse_info_of ctxt =
   1.479 +  fst ooo generic_spec_of false ctxt;
   1.480 +
   1.481 +fun friend_parse_info_of ctxt =
   1.482 +  apsnd (fn f => f ()) ooo generic_spec_of true ctxt;
   1.483 +
   1.484 +end;