# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293057043 0
# Node ID 2d2e610a0de3c4677d03bfce98d11f5b5910d8fa
# Parent  e6e6a3da81aaf35c7f073c32e6881da5a3494454
slight tuning

diff -r e6e6a3da81aa -r 2d2e610a0de3 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Dec 22 21:13:44 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 22 22:30:43 2010 +0000
@@ -63,10 +63,9 @@
 *}
 
 
-
-
 ML {*
-fun process_ecase lthy c (params, prems, concl) bclauses =
+(* adds a freshness condition to the assumptions *)
+fun mk_ecase_prems lthy c (params, prems, concl) bclauses =
   let
     val tys = map snd params
     val binders = get_all_binders bclauses
@@ -80,17 +79,16 @@
         | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   
       end 
 
-    val fresh_prem = 
+    val prems' = 
       case binders of
-        [] => []                        (* case: no binders *)
-      | _ => binders                    (* case: binders *) 
+        [] => prems                        (* case: no binders *)
+      | _ => binders                       (* case: binders *) 
           |> map prep_binder
           |> fold_union_env tys
           |> (fn t => mk_fresh_star t c)
-          |> HOLogic.mk_Trueprop
-          |> single 
+          |> (fn t => HOLogic.mk_Trueprop t :: prems)
   in
-    list_params_prems_concl params (fresh_prem @ prems) concl
+    list_params_prems_concl params prems' concl
   end  
 *}
 
@@ -130,7 +128,11 @@
 *} 
 
 ML {*
-(* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *)
+(* derives an abs_eq theorem of the form 
+
+   Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 
+   Exists q. [as].x = [q o as].(q o x)  for recursive binders
+*)
 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
   (bclause as (BC (bmode, binders, bodies))) =
   case binders of
@@ -141,16 +143,18 @@
         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) = 
+        fun mk_abs cnst_name ty1 ty2 =
+          Const (cnst_name, [ty1, body_ty] ---> Type (ty2, [body_ty]))
+
+        val abs_const = 
           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})
+            Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst}
+          | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"}  @{type_name abs_set}
+          | Res => mk_abs @{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 $ mk_perm (Bound 0) body_trm
-        val abs_rhs' = abs $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
+        val abs_lhs = abs_const $ binder_trm $ body_trm
+        val abs_rhs = abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
+        val abs_rhs' = abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
         val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
         val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs')
         val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
@@ -310,7 +314,7 @@
       |> split_list
       |>> (map o map) strip_params_prems_concl     
 
-    val premss = (map2 o map2) (process_ecase lthy'' c) ecases bclausesss
+    val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases bclausesss
    
     fun tac bclausess exhaust {prems, context} =
       case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas