diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/nominal_library.ML	Mon Feb 28 15:21:10 2011 +0000
@@ -1,45 +1,11 @@
 (*  Title:      nominal_library.ML
     Author:     Christian Urban
 
-  Basic functions for nominal.
+  Library functions for nominal.
 *)
 
 signature NOMINAL_LIBRARY =
 sig
-  val trace: bool Unsynchronized.ref
-  val trace_msg: (unit -> string) -> unit
-
-  val last2: 'a list -> 'a * 'a
-  val split_last2: 'a list -> 'a list * 'a * 'a
-  val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
-  val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
-  val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
-  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a
-  
-  val is_true: term -> bool
- 
-  val dest_listT: typ -> typ
-  val dest_fsetT: typ -> typ
-
-  val mk_id: term -> term
-  val mk_all: (string * typ) -> term -> term
-  val mk_All: (string * typ) -> term -> term
-  val mk_exists: (string * typ) -> term -> term
-
-  val sum_case_const: typ -> typ -> typ -> term
-  val mk_sum_case: term -> term -> term
- 
-  val mk_minus: term -> term
-  val mk_plus: term -> term -> term
-
-  val perm_ty: typ -> typ 
-  val perm_const: typ -> term
-  val mk_perm_ty: typ -> term -> term -> term
-  val mk_perm: term -> term -> term
-  val dest_perm: term -> term * term
-
   val mk_sort_of: term -> term
   val atom_ty: typ -> typ
   val atom_const: typ -> term
@@ -91,9 +57,6 @@
   val mk_finite_ty: typ -> term -> term
   val mk_finite: term -> term
 
-  val mk_equiv: thm -> thm
-  val safe_mk_equiv: thm -> thm
-
   val mk_diff: term * term -> term
   val mk_append: term * term -> term
   val mk_union: term * term -> term
@@ -144,101 +107,6 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if ! trace then tracing (msg ()) else ()
-
-
-(* orders an AList according to keys - every key needs to be there *)
-fun order eq keys list = 
-  map (the o AList.lookup eq list) keys
-
-(* orders an AList according to keys - returns default for non-existing keys *)
-fun order_default eq default keys list = 
-  map (the_default default o AList.lookup eq list) keys
-
-(* remove duplicates *)
-fun remove_dups eq [] = []
-  | remove_dups eq (x :: xs) = 
-      if member eq xs x 
-      then remove_dups eq xs 
-      else x :: remove_dups eq xs
-
-fun last2 [] = raise Empty
-  | last2 [_] = raise Empty
-  | last2 [x, y] = (x, y)
-  | last2 (_ :: xs) = last2 xs
-
-fun split_last2 xs = 
-  let
-    val (xs', x) = split_last xs
-    val (xs'', y) = split_last xs'
-  in
-    (xs'', y, x)
-  end
-
-fun map4 _ [] [] [] [] = []
-  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
-
-fun split_filter f [] = ([], [])
-  | split_filter f (x :: xs) =
-      let 
-        val (r, l) = split_filter f xs 
-      in 
-        if f x 
-        then (x :: r, l) 
-        else (r, x :: l) 
-      end
-
-(* to be used with left-infix binop-operations *)
-fun fold_left f [] z = z
-  | fold_left f [x] z = x
-  | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
-
-
-
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
-
-fun dest_listT (Type (@{type_name list}, [T])) = T
-  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
-
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
-  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-
-
-fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
-
-fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
-
-fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)
-
-fun mk_exists (a, T) t =  HOLogic.exists_const T $ Abs (a, T, t)
-
-fun sum_case_const ty1 ty2 ty3 = 
-  Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
-
-fun mk_sum_case trm1 trm2 =
-  let
-    val ([ty1], ty3) = strip_type (fastype_of trm1)
-    val ty2 = domain_type (fastype_of trm2)
-  in
-    sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
-  end 
-
-
-
-fun mk_minus p = @{term "uminus::perm => perm"} $ p
-
-fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
-
-fun perm_ty ty = @{typ "perm"} --> ty --> ty
-fun perm_const ty  = Const (@{const_name "permute"}, perm_ty ty)
-fun mk_perm_ty ty p trm = perm_const ty $ p $ trm
-fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
-
-fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
-  | dest_perm t = raise TERM ("dest_perm", [t]);
-
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
 fun atom_ty ty = ty --> @{typ "atom"};
@@ -358,10 +226,6 @@
 fun mk_finite t = mk_finite_ty (fastype_of t) t
 
 
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
-
 (* functions that construct differences, appends and unions
    but avoid producing empty atom sets or empty atom lists *)