src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52300 4a4da43e855a
parent 52299 085771de5720
child 52301 7935e82a4ae4
equal deleted inserted replaced
52299:085771de5720 52300:4a4da43e855a
   251     map (Term.subst_TVars rho) ts0
   251     map (Term.subst_TVars rho) ts0
   252   end;
   252   end;
   253 
   253 
   254 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
   254 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
   255 
   255 
   256 fun meta_unzip_rec getT left right nested fpTs y =
       
   257   let val T = getT y in
       
   258     if member (op =) fpTs T then [left y, right y]
       
   259     else if exists_subtype_in fpTs T then [nested y]
       
   260     else [y]
       
   261   end;
       
   262 
       
   263 fun project_co_recT special_Tname Cs proj =
   256 fun project_co_recT special_Tname Cs proj =
   264   let
   257   let
   265     fun project (Type (s, Ts as [T, U])) =
   258     fun project (Type (s, Ts as [T, U])) =
   266         if s = special_Tname andalso member (op =) Cs U then proj (T, U)
   259         if s = special_Tname andalso member (op =) Cs U then proj (T, U)
   267         else Type (s, map project Ts)
   260         else Type (s, map project Ts)
   681         val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
   674         val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
   682 
   675 
   683         fun mk_nested_U maybe_mk_prodT =
   676         fun mk_nested_U maybe_mk_prodT =
   684           typ_subst_nonatomic (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
   677           typ_subst_nonatomic (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
   685 
   678 
   686         fun unzip_iters fiters maybe_tick maybe_mk_prodT =
   679         fun unzip_iters fiters maybe_tick maybe_mk_prodT x =
   687           meta_unzip_rec (snd o dest_Free) I
   680           let val Free (_, T) = x in
   688             (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (K o nth fiters))
   681             if member (op =) fpTs T then
   689               (T, mk_U T) $ x)
   682               [x, build_map lthy (indexify_fst fpTs (K o nth fiters)) (T, mk_U T) $ x]
   690             (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (fn kk => fn _ =>
   683             else if exists_subtype_in fpTs T then
   691               maybe_tick (nth us kk) (nth fiters kk))) (T, mk_nested_U maybe_mk_prodT T) $ x)
   684               [build_map lthy (indexify_fst fpTs (fn kk => fn _ =>
   692             fpTs;
   685                  maybe_tick (nth us kk) (nth fiters kk))) (T, mk_nested_U maybe_mk_prodT T) $ x]
       
   686             else
       
   687               [x]
       
   688           end;
   693 
   689 
   694         fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
   690         fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
   695 
   691 
   696         val gxsss = map (map (flat_rec (single o List.last o unzip_iters gfolds (K I) (K I)))) xsss;
   692         val gxsss = map (map (flat_rec (single o List.last o unzip_iters gfolds (K I) (K I)))) xsss;
   697         val hxsss = map (map (flat_rec (unzip_iters hrecs tick (curry HOLogic.mk_prodT)))) xsss;
   693         val hxsss = map (map (flat_rec (unzip_iters hrecs tick (curry HOLogic.mk_prodT)))) xsss;