--- a/Nominal/Ex/Foo2.thy	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Dec 12 00:10:40 2010 +0000
@@ -24,9 +24,10 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
-term "bn"
-
-
+ML {* 
+  Variable.import;
+  Variable.import true @{thms foo.exhaust} @{context}
+*}
 
 thm foo.bn_defs
 thm foo.permute_bn
@@ -42,7 +43,7 @@
 thm foo.fv_defs
 thm foo.bn_defs
 thm foo.perm_simps
-thm foo.eq_iff(5)
+thm foo.eq_iff
 thm foo.fv_bn_eqvt
 thm foo.size_eqvt
 thm foo.supports
@@ -52,6 +53,7 @@
 
 
 
+text {* *}
 
 
 

--- a/Nominal/Nominal2.thy	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 12 00:10:40 2010 +0000
@@ -15,6 +15,8 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+text {* TEST *}
+
 ML {*
 fun strip_prems_concl trm =
   (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
@@ -23,10 +25,29 @@
   | strip_outer_params B = ([], B)
 *}
 
+
+ML {*
+fun binders bclauses = 
+  let
+    fun aux1 (NONE, i) = Bound i 
+      | aux1 (SOME bn, i) = bn $ Bound i         
+  in
+    bclauses
+    |> map (fn (BC (_, x, _)) => x)
+    |> flat
+    |> map aux1
+  end
+*}
+
 ML {*
 fun prove_strong_exhausts lthy qexhausts qtrms bclausess =
   let
-    val (cses, main_concls) = qexhausts
+    val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy 
+
+    val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
+    val c = Free (c, TFree (a, @{sort fs}))
+
+    val (cses, main_concls) = qexhausts'
       |> map prop_of
       |> map strip_prems_concl
       |> split_list
@@ -36,12 +57,15 @@
         val (params, (body, concl)) = cse
           |> strip_outer_params
           ||> Logic.dest_implies
+        
+        (*val bnds = HOLogic.mk_tuple (binders bclauses)*)
+        val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (c, c))
       in
-        Logic.mk_implies (body, concl) 
+        Logic.mk_implies (prem, Logic.mk_implies (body, concl)) 
       end  
   
     val cses' = map2 (map2 process_case) cses bclausess
-      |> map (map (Syntax.string_of_term lthy))
+      |> map (map (Syntax.string_of_term lthy''))
       |> map commas
       |> cat_lines
 

--- a/Nominal/nominal_dt_rawfuns.ML	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Dec 12 00:10:40 2010 +0000
@@ -18,21 +18,10 @@
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
 
-  val is_atom: Proof.context -> typ -> bool
-  val is_atom_set: Proof.context -> typ -> bool
-  val is_atom_fset: Proof.context -> typ -> bool
-  val is_atom_list: Proof.context -> typ -> bool
-  val mk_atom_set: term -> term
-  val mk_atom_fset: term -> term
-
-  val setify: Proof.context -> term -> term
-  val listify: Proof.context -> term -> term
-
   val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
     (term list * thm list * bn_info list * thm list * local_theory) 
 
-
   val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> 
     thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
 
@@ -71,83 +60,6 @@
 fun lookup xs x = the (AList.lookup (op=) xs x)
 
 
-(* testing for concrete atom types *)
-fun is_atom ctxt ty =
-  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
-
-fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
-  | is_atom_set _ _ = false;
-
-fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
-  | is_atom_fset _ _ = false;
-
-fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
-  | is_atom_list _ _ = false
-
-
-(* functions for producing sets, fsets and lists of general atom type
-   out from concrete atom types *)
-fun mk_atom_set t =
-  let
-    val ty = fastype_of t;
-    val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
-    val img_ty = atom_ty --> ty --> @{typ "atom set"};
-  in
-    Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
-  end
-
-
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
-  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-
-fun mk_atom_fset t =
-  let
-    val ty = fastype_of t;
-    val atom_ty = dest_fsetT ty
-    val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
-    val fset = @{term "fset :: atom fset => atom set"}
-  in
-    fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)
-  end
-
-  fun mk_atom_list t =
-  let
-    val ty = fastype_of t
-    val atom_ty = dest_listT ty
-    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}
-  in
-    Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
-  end
-
-(* functions that coerces singletons, sets and fsets of concrete atoms
-   into sets of general atoms *)
-fun setify ctxt t =
-  let
-    val ty = fastype_of t;
-  in
-    if is_atom ctxt ty
-      then  HOLogic.mk_set @{typ atom} [mk_atom t]
-    else if is_atom_set ctxt ty
-      then mk_atom_set t
-    else if is_atom_fset ctxt ty
-      then mk_atom_fset t
-    else raise TERM ("setify", [t])
-  end
-
-(* functions that coerces singletons and lists of concrete atoms
-   into lists of general atoms  *)
-fun listify ctxt t =
-  let
-    val ty = fastype_of t;
-  in
-    if is_atom ctxt ty
-      then HOLogic.mk_list @{typ atom} [mk_atom t]
-    else if is_atom_list ctxt ty
-      then mk_atom_list t
-    else raise TERM ("listify", [t])
-  end
-
-
 (** functions that define the raw binding functions **)
 
 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or

--- a/Nominal/nominal_library.ML	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/nominal_library.ML	Sun Dec 12 00:10:40 2010 +0000
@@ -12,6 +12,7 @@
   val is_true: term -> bool
  
   val dest_listT: typ -> typ
+  val dest_fsetT: typ -> typ
 
   val mk_id: term -> term
 
@@ -34,6 +35,28 @@
   val mk_atom_ty: typ -> term -> term
   val mk_atom: term -> term
 
+  val mk_atom_set_ty: typ -> term -> term
+  val mk_atom_set: term -> term
+  val mk_atom_fset_ty: typ -> term -> term
+  val mk_atom_fset: term -> term
+  val mk_atom_list_ty: typ -> term -> term
+  val mk_atom_list: term -> term
+
+  val is_atom: Proof.context -> typ -> bool
+  val is_atom_set: Proof.context -> typ -> bool
+  val is_atom_fset: Proof.context -> typ -> bool
+  val is_atom_list: Proof.context -> typ -> bool
+
+  val setify_ty: Proof.context -> typ -> term -> term
+  val setify: Proof.context -> term -> term
+  val listify_ty: Proof.context -> typ -> term -> term
+  val listify: Proof.context -> term -> term
+
+  val fresh_ty: typ -> typ -> typ
+  val fresh_star_const: typ -> typ -> term
+  val mk_fresh_star_ty: typ -> typ -> term -> term -> term
+  val mk_fresh_star: term -> term -> term
+
   val supp_ty: typ -> typ
   val supp_const: typ -> term
   val mk_supp_ty: typ -> term -> term
@@ -110,6 +133,10 @@
 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 =
   let 
     val ty = fastype_of trm
@@ -150,6 +177,79 @@
 fun mk_atom_ty ty t = atom_const ty $ t;
 fun mk_atom t = mk_atom_ty (fastype_of t) t;
 
+fun mk_atom_set_ty ty t =
+  let
+    val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
+    val img_ty = atom_ty --> ty --> @{typ "atom set"};
+  in
+    Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+  end
+
+fun mk_atom_fset_ty ty t =
+  let
+    val atom_ty = dest_fsetT ty
+    val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
+    val fset = @{term "fset :: atom fset => atom set"}
+  in
+    fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)
+  end
+
+fun mk_atom_list_ty ty t =
+  let
+    val atom_ty = dest_listT ty
+    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}
+  in
+    Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
+  end
+
+fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t
+fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t
+fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t
+
+
+
+(* testing for concrete atom types *)
+fun is_atom ctxt ty =
+  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
+
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
+  | is_atom_set _ _ = false;
+
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
+  | is_atom_fset _ _ = false;
+
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+  | is_atom_list _ _ = false
+
+
+(* functions that coerces singletons, sets and fsets of concrete atoms
+   into sets of general atoms *)
+fun setify_ty ctxt ty t =
+  if is_atom ctxt ty
+    then  HOLogic.mk_set @{typ atom} [mk_atom_ty ty t]
+  else if is_atom_set ctxt ty
+    then mk_atom_set_ty ty t
+  else if is_atom_fset ctxt ty
+    then mk_atom_fset_ty ty t
+  else raise TERM ("setify", [t])
+
+(* functions that coerces singletons and lists of concrete atoms
+   into lists of general atoms  *)
+fun listify_ty ctxt ty t =
+  if is_atom ctxt ty
+    then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t]
+  else if is_atom_list ctxt ty
+    then mk_atom_list_ty ty t
+  else raise TERM ("listify", [t])
+
+fun setify ctxt t = setify_ty ctxt (fastype_of t) t
+fun listify ctxt t = listify_ty ctxt (fastype_of t) t
+
+fun fresh_ty ty1 ty2 = [ty1, ty2] ---> @{typ bool}
+fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2)
+fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2
+fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (fastype_of t2) t1 t2
+
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
 fun mk_supp_ty ty t = supp_const ty $ t