--- a/Nominal/Ex/Foo2.thy	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Tue Dec 14 14:23:40 2010 +0000
@@ -24,12 +24,6 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
-thm foo.exhaust
-
-ML {* 
-  Variable.import;
-  Variable.import true @{thms foo.exhaust} @{context}
-*}
 
 thm foo.bn_defs
 thm foo.permute_bn
@@ -53,6 +47,26 @@
 thm foo.supp
 thm foo.fresh
 
+(*
+lemma ex_prop:
+  shows "\<exists>n::nat. Suc n = n"
+sorry
+
+lemma test:
+  shows "True"
+apply -
+ML_prf {*
+  val (x, ctxt') = Obtain.result (K (
+  EVERY [print_tac "test", 
+         etac exE 1,
+         print_tac "end"])) 
+  @{thms ex_prop} @{context};
+  ProofContext.verbose := true;
+  ProofContext.pretty_context ctxt'
+  |> Pretty.block
+  |> Pretty.writeln
+*}
+*)
 
 
 text {* *}
@@ -103,7 +117,7 @@
   and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
   shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
+apply(rule_tac foo.exhaust(1))
 apply(rule assms(1))
 apply(rule exI)+
 apply(assumption)
@@ -111,14 +125,7 @@
 apply(rule exI)+
 apply(assumption)
 (* lam case *)
-(*
-apply(rule Let1_rename)
-apply(rule assms(3))
-apply(assumption)
-apply(simp)
-*)
-
-apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
+apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
 apply(erule exE)
 apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
@@ -126,7 +133,7 @@
 apply(drule_tac x="trm" in meta_spec)
 apply(simp only: fresh_star_Pair set.simps)
 apply(drule meta_mp)
-apply(simp)
+apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base)
 apply(erule exE)
 apply(rule assms(3))
 apply(perm_simp)

--- a/Nominal/Nominal2.thy	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 14 14:23:40 2010 +0000
@@ -18,20 +18,13 @@
 text {* TEST *}
 
 ML {*
-fun list_implies_rev concl trms = Logic.list_implies (trms, concl)
-
-fun mk_all (a, T) t = Const ("all", (T --> propT) --> propT) $ Abs (a, T, t)
-
-fun strip_prems_concl (Const("==>", _) $ A $ B) = strip_prems_concl B |>> cons A
-  | strip_prems_concl B = ([], B) 
-
 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
   | strip_outer_params B = ([], B)
 
 fun strip_params_prems_concl trm =
   let
     val (params, body) = strip_outer_params trm
-    val (prems, concl) = strip_prems_concl body
+    val (prems, concl) = Logic.strip_horn body
   in
     (params, prems, concl)
   end
@@ -40,7 +33,6 @@
   Logic.list_implies (prems, concl)
   |> fold_rev mk_all params
 
-
 fun mk_binop_env tys c (t, u) =
   let val ty = fastype_of1 (tys, t) in
     Const (c, [ty, ty] ---> ty) $ t $ u
@@ -58,9 +50,11 @@
 
 
 ML {*
-fun process_ecase lthy c (params, prems, concl) bclauses =
+fun process_ecase lthy c (params, prems, concl) binders =
   let
-    fun binder tys (opt, i) = 
+    val tys = map snd params
+   
+    fun prep_binder (opt, i) = 
       let
         val t = Bound (length tys - i - 1)
       in
@@ -69,14 +63,12 @@
         | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   
       end 
 
-    val param_tys = map snd params
-       
     val fresh_prem = 
-      case (get_all_binders bclauses) of
+      case binders of
         [] => []                              (* case: no binders *)
       | binders => binders                    (* case: binders *) 
-          |> map (binder param_tys)
-          |> fold_union_env param_tys
+          |> map prep_binder
+          |> fold_union_env tys
           |> (fn t => mk_fresh_star t c)
           |> HOLogic.mk_Trueprop
           |> single 
@@ -85,40 +77,78 @@
   end  
 *}
 
+ML {*
+fun fresh_thm ctxt c params binders bn_finite_thms =
+  let
+    fun prep_binder (opt, i) = 
+      case opt of
+        NONE => setify ctxt (nth params i) 
+      | SOME bn => to_set (bn $ (nth params i))    
+
+    val rhs = HOLogic.mk_tuple (c :: params)
+    val lhs = binders
+      |> map prep_binder
+      |> fold_union
+      |> mk_perm (Bound 0)
+
+    val goal = mk_fresh_star lhs rhs
+      |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
+      |> HOLogic.mk_Trueprop   
+    val ss = @{thms finite.emptyI finite.insertI finite_supp supp_Pair finite_Un finite_fset finite_set} 
+      @ bn_finite_thms  
+  in
+    Goal.prove ctxt [] [] goal
+      (K (HEADGOAL (rtac @{thm at_set_avoiding1}
+          THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
+  end
+*}
+
 
 ML {*
-fun mk_strong_exhausts_goal lthy qexhausts bclausesss =
+fun case_tac ctxt c bn_finite_thms binderss thm =
+  let
+    fun aux_tac (binders : (term option * int) list)=
+      Subgoal.FOCUS (fn {params, context, ...} =>  
+        let
+          val prms = map (term_of o snd) params
+          val fthm = fresh_thm ctxt c prms binders bn_finite_thms
+          val _ = tracing ("params" ^ @{make_string} params) 
+          val _ = tracing ("binders" ^ @{make_string} binders) 
+        in
+          Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
+        end) ctxt
+  in
+    rtac thm THEN' RANGE (map aux_tac binderss)
+  end
+
+fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms =
   let
     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 (ecases, main_concls) = qexhausts'
+    val binderss = map (map get_all_binders) bclausesss
+
+    val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *)
       |> map prop_of
-      |> map strip_prems_concl
+      |> map Logic.strip_horn
       |> split_list
-      |>> map (map strip_params_prems_concl)            
-  in
-    map2 (map2 (process_ecase lthy'' c)) ecases bclausesss
-    |> map2 list_implies_rev main_concls
-    |> rpair lthy''
-  end
+      |>> map (map strip_params_prems_concl)     
 
-fun prove_strong_exhausts lthy qexhausts qtrms bclausesss =
-  let
-    val (goal, lthy') = mk_strong_exhausts_goal lthy qexhausts bclausesss
+    val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss)
 
-    val _ = goal
-      |> map (Syntax.check_term lthy')
-      |> map (Syntax.string_of_term lthy')
-      |> cat_lines
-      |> tracing
+    val _ = tracing ("binderss: " ^ @{make_string} binderss)     
   in
-    @{thms TrueI}
+    Goal.prove_multi lthy'' [] prems main_concls
+     (fn {prems, context} => 
+        EVERY1 [Goal.conjunction_tac,
+                RANGE (map2 (case_tac context c bn_finite_thms) binderss qexhausts')])
   end
 *}
 
+
+
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
@@ -631,7 +661,7 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
-  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses
+  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms
 
   (* noting the theorems *)  
 

--- a/Nominal/Nominal2_Base.thy	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Tue Dec 14 14:23:40 2010 +0000
@@ -1835,6 +1835,12 @@
   shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
   unfolding fresh_def by (simp add: supp_at_base)
 
+lemma fresh_atom_at_base: 
+  fixes b::"'a::at_base"
+  shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
+  by (simp add: fresh_def supp_at_base supp_atom)
+
+
 instance at_base < fs
 proof qed (simp add: supp_at_base)
 

--- a/Nominal/nominal_library.ML	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/nominal_library.ML	Tue Dec 14 14:23:40 2010 +0000
@@ -16,6 +16,7 @@
   val dest_fsetT: typ -> typ
 
   val mk_id: term -> term
+  val mk_all: (string * typ) -> term -> term
 
   val size_const: typ -> term 
 
@@ -154,6 +155,8 @@
     Const (@{const_name id}, ty --> ty) $ trm
   end
 
+fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
+
 
 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})