# HG changeset patch # User krauss # Date 1285670081 -7200 # Node ID 6c8e83d9453663dbf99270b58af05dbde9cd2d76 # Parent 93a10347e356fae67bc844955703bc38208594eb consolidated tupled_lambda; moved to structure HOLogic diff -r 93a10347e356 -r 6c8e83d94536 src/HOL/Tools/Function/function_lib.ML --- 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 diff -r 93a10347e356 -r 6c8e83d94536 src/HOL/Tools/Function/induction_schema.ML --- 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 diff -r 93a10347e356 -r 6c8e83d94536 src/HOL/Tools/Function/mutual.ML --- 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 diff -r 93a10347e356 -r 6c8e83d94536 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 93a10347e356 -r 6c8e83d94536 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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 diff -r 93a10347e356 -r 6c8e83d94536 src/HOL/Tools/hologic.ML --- 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 *)