consolidated tupled_lambda; moved to structure HOLogic
authorkrauss
Tue Sep 28 12:34:41 2010 +0200 (2010-09-28)
changeset 397566c8e83d94536
parent 39755 93a10347e356
child 39759 b4bd83468600
consolidated tupled_lambda; moved to structure HOLogic
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/Tools/Function/function_lib.ML	Tue Sep 28 12:10:37 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Tue Sep 28 12:34:41 2010 +0200
     1.3 @@ -18,17 +18,6 @@
     1.4  fun plural sg pl [x] = sg
     1.5    | plural sg pl _ = pl
     1.6  
     1.7 -(* lambda-abstracts over an arbitrarily nested tuple
     1.8 -  ==> hologic.ML? *)
     1.9 -fun tupled_lambda vars t =
    1.10 -  case vars of
    1.11 -    (Free v) => lambda (Free v) t
    1.12 -  | (Var v) => lambda (Var v) t
    1.13 -  | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
    1.14 -      (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
    1.15 -  | _ => raise Match
    1.16 -
    1.17 -
    1.18  fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
    1.19    let
    1.20      val (n, body) = Term.dest_abs a
     2.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Tue Sep 28 12:10:37 2010 +0200
     2.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Tue Sep 28 12:34:41 2010 +0200
     2.3 @@ -196,7 +196,7 @@
     2.4        |> fold_rev (Logic.all o Free) ws
     2.5        |> term_conv thy ind_atomize
     2.6        |> Object_Logic.drop_judgment thy
     2.7 -      |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
     2.8 +      |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
     2.9    in
    2.10      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
    2.11    end
     3.1 --- a/src/HOL/Tools/Function/mutual.ML	Tue Sep 28 12:10:37 2010 +0200
     3.2 +++ b/src/HOL/Tools/Function/mutual.ML	Tue Sep 28 12:34:41 2010 +0200
     3.3 @@ -221,7 +221,7 @@
     3.4          val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
     3.5          val atup = foldr1 HOLogic.mk_prod avars
     3.6        in
     3.7 -        tupled_lambda atup (list_comb (P, avars))
     3.8 +        HOLogic.tupled_lambda atup (list_comb (P, avars))
     3.9        end
    3.10  
    3.11      val Ps = map2 mk_P parts newPs
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 12:10:37 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 12:34:41 2010 +0200
     4.3 @@ -1999,12 +1999,6 @@
     4.4        (fn NONE => "X" | SOME k' => string_of_int k')
     4.5          (ks @ [SOME k]))) arities));
     4.6  
     4.7 -fun split_lambda (x as Free _) t = lambda x t
     4.8 -  | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
     4.9 -    HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
    4.10 -  | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
    4.11 -  | split_lambda t _ = raise (TERM ("split_lambda", [t]))
    4.12 -
    4.13  fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
    4.14    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
    4.15    | strip_split_abs t = t
    4.16 @@ -2029,7 +2023,7 @@
    4.17        val x = Name.variant names "x"
    4.18        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
    4.19        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
    4.20 -      val t = fold_rev split_lambda args (PredicateCompFuns.mk_Eval
    4.21 +      val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
    4.22          (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
    4.23      in
    4.24        (if is_eval then t else Free (x, funT), x :: names)
    4.25 @@ -2120,8 +2114,8 @@
    4.26              val (r, _) = PredicateCompFuns.dest_Eval t'
    4.27            in (SOME (fst (strip_comb r)), NONE) end
    4.28          val (inargs, outargs) = split_map_mode strip_eval mode args
    4.29 -        val predterm = fold_rev split_lambda inargs
    4.30 -          (PredicateCompFuns.mk_Enum (split_lambda (HOLogic.mk_tuple outargs)
    4.31 +        val predterm = fold_rev HOLogic.tupled_lambda inargs
    4.32 +          (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
    4.33              (list_comb (Const (name, T), args))))
    4.34          val lhs = Const (mode_cname, funT)
    4.35          val def = Logic.mk_equals (lhs, predterm)
    4.36 @@ -3224,7 +3218,7 @@
    4.37          val t_pred = compile_expr comp_modifiers ctxt
    4.38            (body, deriv) [] additional_arguments;
    4.39          val T_pred = dest_predT compfuns (fastype_of t_pred)
    4.40 -        val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
    4.41 +        val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output_tuple
    4.42        in
    4.43          if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
    4.44        end
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Sep 28 12:10:37 2010 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Sep 28 12:34:41 2010 +0200
     5.3 @@ -177,15 +177,7 @@
     5.4  val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
     5.5  val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
     5.6  
     5.7 -fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
     5.8 -  | mk_split_lambda [x] t = lambda x t
     5.9 -  | mk_split_lambda xs t =
    5.10 -  let
    5.11 -    fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
    5.12 -      | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
    5.13 -  in
    5.14 -    mk_split_lambda' xs t
    5.15 -  end;
    5.16 +val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
    5.17  
    5.18  fun cpu_time description f =
    5.19    let
     6.1 --- a/src/HOL/Tools/hologic.ML	Tue Sep 28 12:10:37 2010 +0200
     6.2 +++ b/src/HOL/Tools/hologic.ML	Tue Sep 28 12:34:41 2010 +0200
     6.3 @@ -67,6 +67,7 @@
     6.4    val split_const: typ * typ * typ -> term
     6.5    val mk_split: term -> term
     6.6    val flatten_tupleT: typ -> typ list
     6.7 +  val tupled_lambda: term -> term -> term
     6.8    val mk_tupleT: typ list -> typ
     6.9    val strip_tupleT: typ -> typ list
    6.10    val mk_tuple: term list -> term
    6.11 @@ -327,6 +328,15 @@
    6.12  fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    6.13    | flatten_tupleT T = [T];
    6.14  
    6.15 +(*abstraction over nested tuples*)
    6.16 +fun tupled_lambda (x as Free _) b = lambda x b
    6.17 +  | tupled_lambda (x as Var _) b = lambda x b
    6.18 +  | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
    6.19 +      mk_split (tupled_lambda u (tupled_lambda v b))
    6.20 +  | tupled_lambda (Const ("Product_Type.Unity", _)) b =
    6.21 +      Abs ("x", unitT, b)
    6.22 +  | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
    6.23 +
    6.24  
    6.25  (* tuples with right-fold structure *)
    6.26