diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -6,6 +6,7 @@
      ("nominal_dt_quot.ML")
 begin
 
+
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
@@ -50,9 +51,10 @@
 
 
 ML {*
-fun process_ecase lthy c (params, prems, concl) binders =
+fun process_ecase lthy c (params, prems, concl) bclauses =
   let
     val tys = map snd params
+    val binders = get_all_binders bclauses
    
     fun prep_binder (opt, i) = 
       let
@@ -77,15 +79,21 @@
   end  
 *}
 
+
 ML {*
-fun fresh_thm ctxt c params binders bn_finite_thms =
+fun fresh_thm ctxt c parms 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))    
+        NONE => setify ctxt (nth parms i) 
+      | SOME bn => to_set (bn $ (nth parms i))  
 
-    val rhs = HOLogic.mk_tuple (c :: params)
+    fun prep_binder2 (opt, i) = 
+      case opt of
+        NONE => atomify ctxt (nth parms i)
+      | SOME bn => bn $ (nth parms i) 
+
+    val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
     val lhs = binders
       |> map prep_binder
       |> fold_union
@@ -94,33 +102,99 @@
     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  
+ 
+    val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} 
+      @ @{thms finite.intros finite_Un finite_set finite_fset}  
   in
     Goal.prove ctxt [] [] goal
       (K (HEADGOAL (rtac @{thm at_set_avoiding1}
           THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
   end
+
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) =
+  case binders of
+    [] => [] 
+  | binders =>
+      let
+        val binder_trm = Nominal_Dt_Alpha.comb_binders ctxt bmode parms binders
+        val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
+        val body_ty = fastype_of body_trm
+
+        val (abs_name, binder_ty, abs_ty) = 
+          case bmode of
+            Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
+          | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})
+          | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})
+
+        val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty]))
+        val abs_lhs = abs $ binder_trm $ body_trm
+        val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0
+        val goal = HOLogic.mk_eq (abs_lhs, abs_rhs)
+          |> (fn t => HOLogic.mk_exists ("y", body_ty, t))
+          |> HOLogic.mk_Trueprop  
+ 
+        val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
+          @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
+          fresh_star_set} @ @{thms finite.intros finite_fset}  
+     in
+       [Goal.prove ctxt [] [] goal
+          (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
+              THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] 
+     end
+*}
+
+ML {* 
+fun partitions [] [] = []
+  | partitions xs (i :: js) = 
+      let
+        val (head, tail) = chop i xs
+      in
+        head :: partitions tail js
+      end
+*}
+
+
+ML {*
+fun mk_cperm ctxt p ctrm =
+  mk_perm (term_of p) (term_of ctrm)
+  |> cterm_of (ProofContext.theory_of ctxt)
+*}
+
+
+ML {*
+fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm =
+  let
+    fun aux_tac prem bclauses =
+      case (get_all_binders bclauses) of
+        [] => EVERY' [rtac prem, atac]
+      | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} =>  
+          let
+            val parms = map (term_of o snd) params
+            val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
+  
+            val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
+            val (([(_, fperm)], fprops), ctxt') = Obtain.result
+              (K (EVERY1 [etac exE, 
+                          full_simp_tac (HOL_basic_ss addsimps ss), 
+                          REPEAT o (etac conjE)])) [fthm] ctxt 
+            (*
+            val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops))
+            *)    
+            val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses)
+            (* 
+            val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs))
+            *)
+          in
+            (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*)
+            Skip_Proof.cheat_tac (ProofContext.theory_of ctxt')
+          end) ctxt
+  in
+    rtac thm THEN' RANGE (map2 aux_tac prems bclausess)
+  end
 *}
 
 
 ML {*
-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 
@@ -128,22 +202,22 @@
     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c = Free (c, TFree (a, @{sort fs}))
 
-    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 Logic.strip_horn
       |> split_list
       |>> map (map strip_params_prems_concl)     
 
-    val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss)
-
-    val _ = tracing ("binderss: " ^ @{make_string} binderss)     
+    val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss)
   in
     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')])
+     (fn {prems:thm list, context} =>
+        let
+           val prems' = partitions prems (map length bclausesss)
+        in
+          EVERY1 [Goal.conjunction_tac,
+            RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')]
+        end)
   end
 *}
 
@@ -323,7 +397,7 @@
   val raw_induct_thm = #induct dtinfo
   val raw_induct_thms = #inducts dtinfo
   val raw_exhaust_thms = map #exhaust dtinfos
-  val raw_size_trms = map size_const raw_tys
+  val raw_size_trms = map HOLogic.size_const raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop