diff -r bfa48c000aa7 -r 478c5648e73f Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Wed Dec 22 23:12:51 2010 +0000
+++ b/Nominal/nominal_library.ML	Thu Dec 23 00:22:41 2010 +0000
@@ -11,8 +11,8 @@
   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
@@ -94,9 +94,18 @@
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
+  (* functions for de-Bruijn open terms *)
+  val mk_binop_env: typ list -> string -> term * term -> term
+  val mk_union_env: typ list -> term * term -> term
+  val fold_union_env: typ list -> term list -> term
+
   (* fresh arguments for a term *)
   val fresh_args: Proof.context -> term -> term list
 
+  (* some logic operations *)
+  val strip_full_horn: term -> (string * typ) list * term list * term
+  val mk_full_horn: (string * typ) list -> term list -> term -> term
+
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
@@ -117,6 +126,8 @@
   (* transformation into the object logic *)
   val atomize: thm -> thm
 
+  (* applies a tactic to a formula composed of conjunctions *)
+  val conj_tac: (int -> tactic) -> int -> tactic
 end
 
 
@@ -152,6 +163,12 @@
         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 
@@ -343,6 +360,24 @@
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
 
+(* functions for de-Bruijn open terms *)
+
+fun mk_binop_env tys c (t, u) =
+  let 
+    val ty = fastype_of1 (tys, t) 
+  in
+    Const (c, [ty, ty] ---> ty) $ t $ u
+  end
+
+fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1
+  | mk_union_env tys (@{term "{}::atom set"}, t2) = t2
+  | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1
+  | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2
+  | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)  
+
+fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} 
+
+
 (* produces fresh arguments for a term *)
 
 fun fresh_args ctxt f =
@@ -353,6 +388,24 @@
       |> map Free
 
 
+(** some logic operations **)
+
+(* decompses a formula into params, premises and a conclusion *)
+fun strip_full_horn trm =
+  let
+    fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+    | strip_outer_params B = ([], B)
+
+    val (params, body) = strip_outer_params trm
+    val (prems, concl) = Logic.strip_horn body
+  in
+    (params, prems, concl)
+  end
+
+(* composes a formula out of params, premises and a conclusion *)
+fun mk_full_horn params prems concl =
+  Logic.list_implies (prems, concl)
+  |> fold_rev mk_all params
 
 (** datatypes **)
 
@@ -532,6 +585,19 @@
 (* transformes a theorem into one of the object logic *)
 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
 
+(* applies a tactic to a formula composed of conjunctions *)
+fun conj_tac tac i =
+  let
+     fun select (trm, i) =
+       case trm of
+         @{term "Trueprop"} $ t' => select (t', i)
+       | @{term "op &"} $ _ $ _ => EVERY' [rtac @{thm conjI}, RANGE [conj_tac tac, conj_tac tac]] i
+       | _ => tac i
+  in
+    SUBGOAL select i
+  end
+
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file