src/HOL/Tools/Function/function_lib.ML

+(*  Title:      HOL/Tools/Function/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 Function_Lib =
+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 (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) 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 = subtract (op =) is (0 upto (length xs) - 1)
+   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 Lattices.sup}
+  (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
+                                     @{thms Un_empty_right} @
+                                     @{thms Un_empty_left})) t
+
+
+end