add helper function map_prod
authordesharna
Mon Jul 07 16:06:46 2014 +0200 (2014-07-07)
changeset 575271b07ca054327
parent 57526 7027cf5c1f2c
child 57528 9afc832252a3
add helper function map_prod
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jul 07 16:06:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jul 07 16:06:46 2014 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4          val i = find_index (fn T => x = T) Xs;
     1.5          val TUrec =
     1.6            (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
     1.7 -            NONE => 
     1.8 +            NONE =>
     1.9                force_rec i TU
    1.10                  (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
    1.11            | SOME f => f);
    1.12 @@ -368,7 +368,7 @@
    1.13        fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
    1.14          mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
    1.15        resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
    1.16 -      |>> apfst rev o apsnd rev;
    1.17 +      |>> map_prod rev rev;
    1.18      val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
    1.19        |> mk_recs
    1.20        ||> `Local_Theory.restore;
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
     2.3 @@ -744,7 +744,7 @@
     2.4      val eqn = drop_all eqn0
     2.5        handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
     2.6      val (prems, concl) = Logic.strip_horn eqn
     2.7 -      |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop
     2.8 +      |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop
     2.9          handle TERM _ => primcorec_error_eqn "malformed function equation" eqn;
    2.10  
    2.11      val head = concl
    2.12 @@ -900,7 +900,7 @@
    2.13          #> maps (uncurry (map o pair)
    2.14            #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
    2.15                ((c, c', a orelse a'), (x, s_not (s_conjs y)))
    2.16 -            ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
    2.17 +            ||> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop
    2.18              ||> Logic.list_implies
    2.19              ||> curry Logic.list_all (map dest_Free fun_args))));
    2.20    in
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
     3.3 @@ -342,8 +342,8 @@
     3.4        val fun_name_ctr_pos_list =
     3.5          map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
     3.6        val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
     3.7 -      val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) mutual_calls';
     3.8 -      val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) nested_calls';
     3.9 +      val mutual_calls = map (map_prod (nth ctr_args) (nth args o fst)) mutual_calls';
    3.10 +      val nested_calls = map (map_prod (nth ctr_args) (nth args o fst)) nested_calls';
    3.11      in
    3.12        t
    3.13        |> subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Jul 07 16:06:46 2014 +0200
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Jul 07 16:06:46 2014 +0200
     4.3 @@ -8,6 +8,8 @@
     4.4  
     4.5  signature CTR_SUGAR_UTIL =
     4.6  sig
     4.7 +  val map_prod: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
     4.8 +
     4.9    val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    4.10    val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    4.11    val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
    4.12 @@ -83,6 +85,8 @@
    4.13  structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
    4.14  struct
    4.15  
    4.16 +fun map_prod f g (x, y) = (f x, g y)
    4.17 +
    4.18  fun map3 _ [] [] [] = []
    4.19    | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
    4.20    | map3 _ _ _ _ = raise ListPair.UnequalLengths;