--- a/src/HOL/Tools/Function/function_lib.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Tue Sep 28 12:34:41 2010 +0200
@@ -18,17 +18,6 @@
fun plural sg pl [x] = sg
| plural sg pl _ = pl
-(* lambda-abstracts over an arbitrarily nested tuple
- ==> hologic.ML? *)
-fun tupled_lambda vars t =
- case vars of
- (Free v) => lambda (Free v) t
- | (Var v) => lambda (Var v) t
- | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
- (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
- | _ => raise Match
-
-
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
let
val (n, body) = Term.dest_abs a
--- a/src/HOL/Tools/Function/induction_schema.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Tue Sep 28 12:34:41 2010 +0200
@@ -196,7 +196,7 @@
|> fold_rev (Logic.all o Free) ws
|> term_conv thy ind_atomize
|> Object_Logic.drop_judgment thy
- |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+ |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
in
SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
end
--- a/src/HOL/Tools/Function/mutual.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Tue Sep 28 12:34:41 2010 +0200
@@ -221,7 +221,7 @@
val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
val atup = foldr1 HOLogic.mk_prod avars
in
- tupled_lambda atup (list_comb (P, avars))
+ HOLogic.tupled_lambda atup (list_comb (P, avars))
end
val Ps = map2 mk_P parts newPs
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 12:34:41 2010 +0200
@@ -1999,12 +1999,6 @@
(fn NONE => "X" | SOME k' => string_of_int k')
(ks @ [SOME k]))) arities));
-fun split_lambda (x as Free _) t = lambda x t
- | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
- HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
- | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
- | split_lambda t _ = raise (TERM ("split_lambda", [t]))
-
fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
@@ -2029,7 +2023,7 @@
val x = Name.variant names "x"
val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
- val t = fold_rev split_lambda args (PredicateCompFuns.mk_Eval
+ val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
(list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
in
(if is_eval then t else Free (x, funT), x :: names)
@@ -2120,8 +2114,8 @@
val (r, _) = PredicateCompFuns.dest_Eval t'
in (SOME (fst (strip_comb r)), NONE) end
val (inargs, outargs) = split_map_mode strip_eval mode args
- val predterm = fold_rev split_lambda inargs
- (PredicateCompFuns.mk_Enum (split_lambda (HOLogic.mk_tuple outargs)
+ val predterm = fold_rev HOLogic.tupled_lambda inargs
+ (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
(list_comb (Const (name, T), args))))
val lhs = Const (mode_cname, funT)
val def = Logic.mk_equals (lhs, predterm)
@@ -3224,7 +3218,7 @@
val t_pred = compile_expr comp_modifiers ctxt
(body, deriv) [] additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
- val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
+ val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output_tuple
in
if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Sep 28 12:34:41 2010 +0200
@@ -177,15 +177,7 @@
val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
-fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
- | mk_split_lambda [x] t = lambda x t
- | mk_split_lambda xs t =
- let
- fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
- | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
- in
- mk_split_lambda' xs t
- end;
+val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
fun cpu_time description f =
let
--- a/src/HOL/Tools/hologic.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Sep 28 12:34:41 2010 +0200
@@ -67,6 +67,7 @@
val split_const: typ * typ * typ -> term
val mk_split: term -> term
val flatten_tupleT: typ -> typ list
+ val tupled_lambda: term -> term -> term
val mk_tupleT: typ list -> typ
val strip_tupleT: typ -> typ list
val mk_tuple: term list -> term
@@ -327,6 +328,15 @@
fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
| flatten_tupleT T = [T];
+(*abstraction over nested tuples*)
+fun tupled_lambda (x as Free _) b = lambda x b
+ | tupled_lambda (x as Var _) b = lambda x b
+ | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
+ mk_split (tupled_lambda u (tupled_lambda v b))
+ | tupled_lambda (Const ("Product_Type.Unity", _)) b =
+ Abs ("x", unitT, b)
+ | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
+
(* tuples with right-fold structure *)