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