src/HOL/Tools/hologic.ML
changeset 39756 6c8e83d94536
parent 39250 548a3e5521ab
child 40627 becf5d5187cc
     1.1 --- a/src/HOL/Tools/hologic.ML	Tue Sep 28 12:10:37 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Tue Sep 28 12:34:41 2010 +0200
     1.3 @@ -67,6 +67,7 @@
     1.4    val split_const: typ * typ * typ -> term
     1.5    val mk_split: term -> term
     1.6    val flatten_tupleT: typ -> typ list
     1.7 +  val tupled_lambda: term -> term -> term
     1.8    val mk_tupleT: typ list -> typ
     1.9    val strip_tupleT: typ -> typ list
    1.10    val mk_tuple: term list -> term
    1.11 @@ -327,6 +328,15 @@
    1.12  fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    1.13    | flatten_tupleT T = [T];
    1.14  
    1.15 +(*abstraction over nested tuples*)
    1.16 +fun tupled_lambda (x as Free _) b = lambda x b
    1.17 +  | tupled_lambda (x as Var _) b = lambda x b
    1.18 +  | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
    1.19 +      mk_split (tupled_lambda u (tupled_lambda v b))
    1.20 +  | tupled_lambda (Const ("Product_Type.Unity", _)) b =
    1.21 +      Abs ("x", unitT, b)
    1.22 +  | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
    1.23 +
    1.24  
    1.25  (* tuples with right-fold structure *)
    1.26