--- 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 *)