--- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 19 18:02:49 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 19 18:25:34 2006 +0200
@@ -9,11 +9,12 @@
fun mk_forall (var as Free (v,T)) t =
all T $ Abs (v,T, abstract_over (var,t))
- | mk_forall _ _ = raise Match
+ | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end
(* Builds a quantification with a new name for the variable. *)
-fun mk_forall_rename ((v,T),newname) t =
- all T $ Abs (newname,T, abstract_over (Free (v,T),t))
+fun mk_forall_rename (v as Free (_,T),newname) t =
+ all T $ Abs (newname, T, abstract_over (v, t))
+ | mk_forall_rename (v, _) _ = let val _ = print v in sys_error "mk_forall_rename" end
(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
fun tupled_lambda vars t =
@@ -44,6 +45,24 @@
end
| dest_all_all t = ([],t)
+
+fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
+ let
+ val [(n', _)] = Variable.rename_wrt ctx [] [(n,T)]
+ val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
+
+ val (n'', body) = Term.dest_abs (n', T, b)
+ val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
+
+ val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
+ in
+ (ctx'', (n', T) :: vs, bd)
+ end
+ | dest_all_all_ctx ctx t =
+ (ctx, [], t)
+
+
+
(* unfold *)
fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
@@ -56,11 +75,15 @@
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
| map3 _ _ _ _ = raise Library.UnequalLengths;
+fun map6 _ [] [] [] [] [] [] = []
+ | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
+ | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
+
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
-fun upairs [] = []
- | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
+fun unordered_pairs [] = []
+ | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
fun the_single [x] = x