--- a/src/HOL/Tools/function_package/fundef_lib.ML Tue Jun 23 12:09:14 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-(* Title: HOL/Tools/function_package/fundef_lib.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Some fairly general functions that should probably go somewhere else...
-*)
-
-structure FundefLib = struct
-
-fun map_option f NONE = NONE
- | map_option f (SOME x) = SOME (f x);
-
-fun fold_option f NONE y = y
- | fold_option f (SOME x) y = f x y;
-
-fun fold_map_option f NONE y = (NONE, y)
- | fold_map_option f (SOME x) y = apfst SOME (f x y);
-
-(* Ex: "The variable" ^ plural " is" "s are" vs *)
-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 ("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
- in
- (Free (n, T), body)
- end
- | dest_all _ = raise Match
-
-
-(* Removes all quantifiers from a term, replacing bound variables by frees. *)
-fun dest_all_all (t as (Const ("all",_) $ _)) =
- let
- val (v,b) = dest_all t
- val (vs, b') = dest_all_all b
- in
- (v :: vs, b')
- end
- | dest_all_all t = ([],t)
-
-
-(* FIXME: similar to Variable.focus *)
-fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
- let
- val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
- val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
-
- val (n'', body) = Term.dest_abs (n', T, b)
- val _ = (n' = n'') orelse error "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)
-
-
-fun map3 _ [] [] [] = []
- | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
- | map3 _ _ _ _ = raise Library.UnequalLengths;
-
-fun map4 _ [] [] [] [] = []
- | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
- | map4 _ _ _ _ _ = 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;
-
-fun map7 _ [] [] [] [] [] [] [] = []
- | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
- | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
-
-
-
-(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
-(* ==> library *)
-fun unordered_pairs [] = []
- | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
-
-
-(* Replaces Frees by name. Works with loose Bounds. *)
-fun replace_frees assoc =
- map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
- | t => t)
-
-
-fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
- | rename_bound n _ = raise Match
-
-fun mk_forall_rename (n, v) =
- rename_bound n o Logic.all v
-
-fun forall_intr_rename (n, cv) thm =
- let
- val allthm = forall_intr cv thm
- val (_ $ abs) = prop_of allthm
- in
- Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
- end
-
-
-(* Returns the frees in a term in canonical order, excluding the fixes from the context *)
-fun frees_in_term ctxt t =
- Term.add_frees t []
- |> filter_out (Variable.is_fixed ctxt o fst)
- |> rev
-
-
-datatype proof_attempt = Solved of thm | Stuck of thm | Fail
-
-fun try_proof cgoal tac =
- case SINGLE tac (Goal.init cgoal) of
- NONE => Fail
- | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
-
-
-fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
- if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
- | dest_binop_list _ t = [ t ]
-
-
-(* separate two parts in a +-expression:
- "a + b + c + d + e" --> "(a + b + d) + (c + e)"
-
- Here, + can be any binary operation that is AC.
-
- cn - The name of the binop-constructor (e.g. @{const_name Un})
- ac - the AC rewrite rules for cn
- is - the list of indices of the expressions that should become the first part
- (e.g. [0,1,3] in the above example)
-*)
-
-fun regroup_conv neu cn ac is ct =
- let
- val mk = HOLogic.mk_binop cn
- val t = term_of ct
- val xs = dest_binop_list cn t
- val js = 0 upto (length xs) - 1 \\ is
- val ty = fastype_of t
- val thy = theory_of_cterm ct
- in
- Goal.prove_internal []
- (cterm_of thy
- (Logic.mk_equals (t,
- if is = []
- then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
- else if js = []
- then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
- else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
- (K (rewrite_goals_tac ac
- THEN rtac Drule.reflexive_thm 1))
- end
-
-(* instance for unions *)
-fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un}
- (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
- @{thms "Un_empty_right"} @
- @{thms "Un_empty_left"})) t
-
-
-end