src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51794 a1ffbc36323a
parent 51793 22f22172a361
child 51795 096b96281e34
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 14:14:52 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 14:14:54 2013 +0200
     1.3 @@ -76,10 +76,14 @@
     1.4  fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
     1.5  fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
     1.6  
     1.7 -(* This order is for compatibility with the old datatype package. *)
     1.8 -fun unzip_rec curryf xs =
     1.9 -  let val ps = map curryf xs in
    1.10 -    map fst ps @ map_filter snd ps
    1.11 +fun flat_rec unzipf xs =
    1.12 +  let val ps = map unzipf xs in
    1.13 +    (* The first line below gives the preferred order. The second line is for compatibility with the
    1.14 +       old datatype package: *)
    1.15 +    maps (op @) ps
    1.16 +(*
    1.17 +    maps fst ps @ maps snd ps
    1.18 +*)
    1.19    end;
    1.20  
    1.21  fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
    1.22 @@ -364,14 +368,14 @@
    1.23              | proj_recT proj (Type (s, Ts)) = Type (s, map (proj_recT proj) Ts)
    1.24              | proj_recT _ T = T;
    1.25  
    1.26 -          fun curry_recT T =
    1.27 -            if exists_fp_subtype T then (proj_recT fst T, SOME (proj_recT snd T)) else (T, NONE);
    1.28 +          fun unzip_recT T =
    1.29 +            if exists_fp_subtype T then ([proj_recT fst T], [proj_recT snd T]) else ([T], []);
    1.30  
    1.31            val z_Tsss =
    1.32              map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
    1.33                ns mss fp_rec_fun_Ts;
    1.34 -          val z_Tssss = map (map (unzip_rec curry_recT)) z_Tsss;
    1.35 -          val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css;
    1.36 +          val z_Tsss' = map (map (flat_rec unzip_recT)) z_Tsss;
    1.37 +          val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
    1.38  
    1.39            val hss = map2 (map2 retype_free) h_Tss gss;
    1.40            val zsss = map2 (map2 (map2 retype_free)) z_Tsss ysss;
    1.41 @@ -642,15 +646,15 @@
    1.42                | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
    1.43                | mk_U _ T = T;
    1.44  
    1.45 -            fun curry_rec (x as Free (_, T)) =
    1.46 +            fun unzip_rec (x as Free (_, T)) =
    1.47                if exists_fp_subtype T then
    1.48 -                (build_prod_proj fst_const (T, mk_U fst T) $ x,
    1.49 -                 SOME (build_prod_proj snd_const (T, mk_U snd T) $ x))
    1.50 +                ([build_prod_proj fst_const (T, mk_U fst T) $ x],
    1.51 +                 [build_prod_proj snd_const (T, mk_U snd T) $ x])
    1.52                else
    1.53 -                (x, NONE);
    1.54 +                ([x], []);
    1.55  
    1.56              fun mk_rec_like_arg f xs =
    1.57 -              mk_tupled_fun (HOLogic.mk_tuple xs) f (flat (unzip_rec curry_rec xs));
    1.58 +              mk_tupled_fun (HOLogic.mk_tuple xs) f (flat_rec unzip_rec xs);
    1.59  
    1.60              fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xsss)) =
    1.61                let
    1.62 @@ -869,14 +873,14 @@
    1.63  
    1.64              val mk_U = typ_subst (map2 pair fpTs Cs);
    1.65  
    1.66 -            fun intr_rec_likes frec_likes maybe_cons (x as Free (_, T)) =
    1.67 +            fun unzip_rec_likes frec_likes combine (x as Free (_, T)) =
    1.68                if exists_fp_subtype T then
    1.69 -                maybe_cons x [build_rec_like frec_likes (T, mk_U T) $ x]
    1.70 +                combine (x, build_rec_like frec_likes (T, mk_U T) $ x)
    1.71                else
    1.72 -                [x];
    1.73 +                ([x], []);
    1.74  
    1.75 -            val gxsss = map (map (maps (intr_rec_likes gfolds (K I)))) xsss;
    1.76 -            val hxsss = map (map (maps (intr_rec_likes hrecs cons))) xsss;
    1.77 +            val gxsss = map (map (flat_rec (unzip_rec_likes gfolds (fn (_, t) => ([t], []))))) xsss;
    1.78 +            val hxsss = map (map (flat_rec (unzip_rec_likes hrecs (pairself single)))) xsss;
    1.79  
    1.80              val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
    1.81              val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;