# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1292547704 0
# Node ID 1803104d76c9caeddd53a9c106cdaa6bf959b390
# Parent  0ee253e66372f0febb9effb4b67b15ee681b90e6
tuned

diff -r 0ee253e66372 -r 1803104d76c9 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri Dec 17 00:39:27 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Dec 17 01:01:44 2010 +0000
@@ -67,8 +67,8 @@
 
     val fresh_prem = 
       case binders of
-        [] => []                              (* case: no binders *)
-      | binders => binders                    (* case: binders *) 
+        [] => []                        (* case: no binders *)
+      | _ => binders                    (* case: binders *) 
           |> map prep_binder
           |> fold_union_env tys
           |> (fn t => mk_fresh_star t c)
@@ -81,6 +81,8 @@
 
 
 ML {*
+(* derives the freshness theorem that there exists a p, such that 
+   (p o as) #* (c, t1,\<dots>, tn) *)
 fun fresh_thm ctxt c parms binders bn_finite_thms =
   let
     fun prep_binder (opt, i) = 
@@ -110,13 +112,16 @@
       (K (HEADGOAL (rtac @{thm at_set_avoiding1}
           THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
   end
+*} 
 
+ML {*
+(* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *)
 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 binder_trm = comb_binders ctxt bmode parms binders
         val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
         val body_ty = fastype_of body_trm
 
@@ -143,17 +148,8 @@
      end
 *}
 
-ML {* 
-fun partitions [] [] = []
-  | partitions xs (i :: js) = 
-      let
-        val (head, tail) = chop i xs
-      in
-        head :: partitions tail js
-      end
-*}
 
-
+(* FIXME: use pure cterm functions *)
 ML {*
 fun mk_cperm ctxt p ctrm =
   mk_perm (term_of p) (term_of ctrm)
@@ -177,10 +173,13 @@
               (K (EVERY1 [etac exE, 
                           full_simp_tac (HOL_basic_ss addsimps ss), 
                           REPEAT o (etac conjE)])) [fthm] ctxt 
+  
+            val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses)
+
+            val _ = tracing ("test")
             (*
             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))
             *)
diff -r 0ee253e66372 -r 1803104d76c9 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri Dec 17 00:39:27 2010 +0000
+++ b/Nominal/nominal_library.ML	Fri Dec 17 01:01:44 2010 +0000
@@ -9,6 +9,7 @@
   val last2: 'a list -> 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
   val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
+  val partitions: 'a list -> int list -> 'a list list
 
   val is_true: term -> bool
  
@@ -136,6 +137,17 @@
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
+(* partitions a set according to the numbers in the int list *)
+fun partitions [] [] = []
+  | partitions xs (i :: js) = 
+      let
+        val (head, tail) = chop i xs
+      in
+        head :: partitions tail js
+      end
+
+
+
 fun is_true @{term "Trueprop True"} = true
   | is_true _ = false