--- a/Nominal/Nominal2.thy	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 12 22:09:11 2010 +0000
@@ -18,60 +18,104 @@
 text {* TEST *}
 
 ML {*
-fun strip_prems_concl trm =
-  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
+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
+  in
+    (params, prems, concl)
+  end
+
+fun list_params_prems_concl params prems concl =
+  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
+  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_rev (curry (mk_union_env tys)) trms @{term "{}::atom set"}
+
 *}
 
 
 ML {*
-fun binders bclauses = 
+fun process_ecase lthy c (params, prems, concl) bclauses =
   let
-    fun aux1 (NONE, i) = Bound i 
-      | aux1 (SOME bn, i) = bn $ Bound i         
+    fun binder tys (opt, i) = 
+      let
+        val t = Bound (length tys - i - 1)
+      in
+        case opt of
+          NONE => setify_ty lthy (nth tys i) t 
+        | 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: no binders *)
+      | binders => binders                    (* case: binders *) 
+          |> map (binder param_tys)
+          |> fold_union_env param_tys
+          |> (fn t => mk_fresh_star t c)
+          |> HOLogic.mk_Trueprop
+          |> single 
   in
-    bclauses
-    |> map (fn (BC (_, x, _)) => x)
-    |> flat
-    |> map aux1
-  end
+    list_params_prems_concl params (fresh_prem @ prems) concl
+  end  
 *}
 
+
 ML {*
-fun prove_strong_exhausts lthy qexhausts qtrms bclausess =
+fun mk_strong_exhausts_goal lthy qexhausts bclausesss =
   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 (cses, main_concls) = qexhausts'
+    val (ecases, main_concls) = qexhausts'
       |> map prop_of
       |> map strip_prems_concl
       |> 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
 
-    fun process_case cse bclauses =
-      let
-        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 (prem, Logic.mk_implies (body, concl)) 
-      end  
-  
-    val cses' = map2 (map2 process_case) cses bclausess
-      |> map (map (Syntax.string_of_term lthy''))
-      |> map commas
+fun prove_strong_exhausts lthy qexhausts qtrms bclausesss =
+  let
+    val (goal, lthy') = mk_strong_exhausts_goal lthy qexhausts bclausesss
+
+    val _ = goal
+      |> map (Syntax.check_term lthy')
+      |> map (Syntax.string_of_term lthy')
       |> cat_lines
-
-    val _ = tracing ("cases\n " ^ cses')
+      |> tracing
   in
-    ()
+    @{thms TrueI}
   end
 *}
 
@@ -230,9 +274,6 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val _ = tracing ("bclauses\n" ^ cat_lines (map @{make_string} bclauses))
-  val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses))
-
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo