44 (* Given [fv1, fv2, fv3]

    45    produces %(x, y, z). fv1 x u fv2 y u fv3 z *)

    46 ML {*

    47 fun mk_compound_fv fvs =

    48 let

    49   val nos = (length fvs - 1) downto 0;

    50   val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);

    51   val fvs_union = mk_union fvs_applied;

    52   val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);

    53   fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))

    54 in

    55   fold fold_fun tys (Abs ("", tyh, fvs_union))

    56 end;

    57 *}

    58 

    59 (* Given [R1, R2, R3]

    60    produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)

    61 ML {*

    62 fun mk_compound_alpha Rs =

    63 let

    64   val nos = (length Rs - 1) downto 0;

    65   val nos2 = (2 * length Rs - 1) downto length Rs;

    66   val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)

    67     (Rs ~~ (nos2 ~~ nos));

    68   val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;

    69   val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);

    70   fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))

    71   val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))

    72 in

    73   fold fold_fun tys (Abs ("", tyh, abs_rhs))

    74 end;

    75 *}