--- a/Nominal/nominal_dt_alpha.ML	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sat Aug 14 16:54:41 2010 +0800
@@ -30,7 +30,8 @@
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
   val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
 
-  val resolve_fun_rel: thm -> thm
+  val mk_funs_rsp: thm -> thm
+  val mk_alpha_permute_rsp: thm -> thm 
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -559,21 +560,21 @@
 
 (** proves the equivp predicate for all alphas **)
 
-val equivp_intro = 
-  @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R"
-    by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)}
+val transp_def' =
+  @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" 
+    by (rule eq_reflection, auto simp add: transp_def)}
 
 fun raw_prove_equivp alphas refl symm trans ctxt = 
 let
-  val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
-  val refl' = map atomize refl
-  val symm' = map atomize symm
-  val trans' = map atomize trans
+  val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
+  val symm' = map (fold_rule @{thms symp_def} o atomize) symm
+  val trans' = map (fold_rule [transp_def'] o atomize) trans
+
   fun prep_goal t = 
     HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) 
 in    
   Goal.prove_multi ctxt [] [] (map prep_goal alphas)
-  (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' 
+  (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' 
      RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
 end
 
@@ -613,10 +614,11 @@
 let
   val arg_ty = domain_type o fastype_of 
   val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+  fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 
-  val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs
-  val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns
-  val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns
+  val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
+  val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
+  val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
   
   val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
     @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
@@ -690,17 +692,28 @@
 end
 
 
-(* resolve with @{thm fun_relI} *)
+(* transformation of the natural rsp-lemmas into the standard form *)
+
+val fun_rsp = @{lemma
+  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}
+
+fun mk_funs_rsp thm = 
+ thm
+ |> atomize
+ |> single
+ |> curry (op OF) fun_rsp
 
-fun resolve_fun_rel thm =
-let 
-  val fun_rel = @{thm fun_relI}
-  val thm' = forall_intr_vars thm
-  val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm')
-  val fun_rel' = Thm.instantiate cinsts fun_rel
-in
-  thm' COMP fun_rel'
-end 
+
+val permute_rsp = @{lemma 
+  "(!x y p. R x y --> R (permute p x) (permute p y)) 
+     ==> ((op =) ===> R ===> R) permute permute"  by simp}
+
+fun mk_alpha_permute_rsp thm = 
+ thm
+ |> atomize
+ |> single
+ |> curry (op OF) permute_rsp
+
 
 
 end (* structure *)