src/HOL/Tools/function_package/fundef_lib.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19770 be5c23ebe1eb
child 19841 f2fa72c13186
permissions -rw-r--r--
adding case theorems for code generator
     1 (*  Title:      HOL/Tools/function_package/lib.ML
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 A package for general recursive function definitions. 
     6 Some fairly general functions that should probably go somewhere else... 
     7 *)
     8 
     9 
    10 fun mk_forall (var as Free (v,T)) t =
    11     all T $ Abs (v,T, abstract_over (var,t))
    12   | mk_forall _ _ = raise Match
    13 
    14 (* Builds a quantification with a new name for the variable. *)
    15 fun mk_forall_rename ((v,T),newname) t =
    16     all T $ Abs (newname,T, abstract_over (Free (v,T),t))
    17 
    18 (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
    19 fun tupled_lambda vars t =
    20     case vars of
    21 	(Free v) => lambda (Free v) t
    22       | (Var v) => lambda (Var v) t
    23       | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
    24 	(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
    25       | _ => raise Match
    26 
    27 
    28 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
    29     let
    30 	val (n, body) = Term.dest_abs a
    31     in
    32 	(Free (n, T), body)
    33     end
    34   | dest_all _ = raise Match
    35 
    36 
    37 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    38 fun dest_all_all (t as (Const ("all",_) $ _)) = 
    39     let
    40 	val (v,b) = dest_all t
    41 	val (vs, b') = dest_all_all b
    42     in
    43 	(v :: vs, b')
    44     end
    45   | dest_all_all t = ([],t)
    46 
    47 (* unfold *)
    48 fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
    49 
    50 val dest_implies_list = 
    51     split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
    52 
    53 fun implies_elim_swp a b = implies_elim b a
    54 
    55 fun map3 _ [] [] [] = []
    56   | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
    57   | map3 _ _ _ _ = raise UnequalLengths;
    58 
    59 
    60 
    61 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
    62 fun upairs [] = []
    63   | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
    64 
    65 
    66 fun the_single [x] = x
    67   | the_single _ = sys_error "the_single"