src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52302 867d5d16158c
parent 52301 7935e82a4ae4
child 52303 16d7708aba40
equal deleted inserted replaced
52301:7935e82a4ae4 52302:867d5d16158c
    29   val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
    29   val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
    30   val exists_subtype_in: typ list -> typ -> bool
    30   val exists_subtype_in: typ list -> typ -> bool
    31   val flat_rec: 'a list list -> 'a list
    31   val flat_rec: 'a list list -> 'a list
    32   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
    32   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
    33   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
    33   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
    34   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
       
    35   val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
    34   val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
    36     int list list -> term list -> term list -> Proof.context ->
    35     int list list -> term list -> term list -> Proof.context ->
    37     (term list * term list
    36     (term list * term list
    38        * ((typ list list * typ list list list list * term list list * term list list list list)
    37        * ((typ list list * typ list list list list * term list list * term list list list list)
    39           * (typ list list * typ list list list list * term list list
    38           * (typ list list * typ list list list list * term list list
   431   in snd oo add end;
   430   in snd oo add end;
   432 
   431 
   433 fun nesty_bnfs ctxt ctr_Tsss Us =
   432 fun nesty_bnfs ctxt ctr_Tsss Us =
   434   map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
   433   map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
   435 
   434 
   436 fun indexify_fst xs f (x, y) = f (find_index (curry (op =) x) xs) (x, y);
   435 fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
   437 
   436 
   438 fun build_map lthy build_simple =
   437 fun build_map lthy build_simple =
   439   let
   438   let
   440     fun build (TU as (T, U)) =
   439     fun build (TU as (T, U)) =
   441       if T = U then
   440       if T = U then
   672 
   671 
   673         fun mk_goal fss fiter xctr f xs fxs =
   672         fun mk_goal fss fiter xctr f xs fxs =
   674           fold_rev (fold_rev Logic.all) (xs :: fss)
   673           fold_rev (fold_rev Logic.all) (xs :: fss)
   675             (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs)));
   674             (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs)));
   676 
   675 
   677         fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
   676         fun maybe_tick (T, U) u f =
   678 
   677           if try (fst o HOLogic.dest_prodT) U = SOME T then
   679         fun unzip_iters fiters maybe_tick (x as Free (_, T)) Us =
   678             Term.lambda u (HOLogic.mk_prod (u, f $ u))
       
   679           else
       
   680             f;
       
   681 
       
   682         fun unzip_iters tick fiters (x as Free (_, T)) =
   680           map (fn U => if U = T then x else
   683           map (fn U => if U = T then x else
   681             build_map lthy (indexify_fst fpTs (fn kk => fn _ =>
   684             build_map lthy (indexify fst fpTs (fn kk => fn TU =>
   682               nth fiters kk |> length Us = 1 ? maybe_tick (nth us kk))) (T, U) $ x) Us;
   685               nth fiters kk |> maybe_tick TU (nth us kk))) (T, U) $ x);
   683 
   686 
   684         val gxsss = map2 (map2 (flat_rec oo map2 (unzip_iters gfolds (K I)))) xsss y_Tssss;
   687         val gxsss = map2 (map2 (flat_rec oo map2 (unzip_iters false gfolds))) xsss y_Tssss;
   685         val hxsss = map2 (map2 (flat_rec oo map2 (unzip_iters hrecs tick))) xsss z_Tssss;
   688         val hxsss = map2 (map2 (flat_rec oo map2 (unzip_iters true hrecs))) xsss z_Tssss;
   686 
   689 
   687         val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
   690         val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
   688         val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
   691         val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
   689 
   692 
   690         val fold_tacss =
   693         val fold_tacss =
   851         val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs);
   854         val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs);
   852 
   855 
   853         fun intr_coiters fcoiters [] [cf] =
   856         fun intr_coiters fcoiters [] [cf] =
   854             let val T = fastype_of cf in
   857             let val T = fastype_of cf in
   855               if exists_subtype_in Cs T then
   858               if exists_subtype_in Cs T then
   856                 build_map lthy (indexify_fst Cs (K o nth fcoiters)) (T, mk_U T) $ cf
   859                 build_map lthy (indexify fst Cs (K o nth fcoiters)) (T, mk_U T) $ cf
   857               else
   860               else
   858                 cf
   861                 cf
   859             end
   862             end
   860           | intr_coiters fcoiters [cq] [cf, cf'] =
   863           | intr_coiters fcoiters [cq] [cf, cf'] =
   861             mk_If cq (intr_coiters fcoiters [] [cf]) (intr_coiters fcoiters [] [cf']);
   864             mk_If cq (intr_coiters fcoiters [] [cf]) (intr_coiters fcoiters [] [cf']);