--- a/Nominal/nominal_dt_alpha.ML	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Sat Nov 13 10:25:03 2010 +0000
@@ -28,13 +28,16 @@
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
   val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> 
     Proof.context -> thm list * thm list
+
   val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
   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 raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
-
+  val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list -> 
+    Proof.context -> thm list
+  
   val mk_funs_rsp: thm -> thm
   val mk_alpha_permute_rsp: thm -> thm 
 end
@@ -582,7 +585,6 @@
   let
     val alpha_names =  map (fst o dest_Const) alpha_trms 
     val props = map prep_trans_goal alpha_trms
-    val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}  
   in
     alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
       (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
@@ -752,6 +754,58 @@
   end
 
 
+(* rsp for permute_bn functions *)
+
+val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
+ by (simp add: fun_rel_def)}
+
+fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt = 
+  SUBPROOF (fn {prems, context, ...} => 
+    let
+      val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+      val prems'' = map (transform_prem1 context pred_names) prems'
+    in
+      HEADGOAL 
+        (simp_tac (HOL_basic_ss addsimps (simps @ prems'))
+         THEN' TRY o REPEAT_ALL_NEW 
+           (FIRST' [ rtac @{thm TrueI}, 
+                     rtac @{thm conjI}, 
+                     rtac @{thm refl},
+                     resolve_tac prems', 
+                     resolve_tac prems'',
+                     resolve_tac alpha_intros ]))
+    end) ctxt
+
+fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt =
+  let
+    val arg_ty = domain_type o fastype_of
+    val perm_bn_ty = range_type o range_type o fastype_of
+    val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt		   
+    val p = Free (p, @{typ perm})
+
+    fun mk_prop t =
+      let
+        val alpha_trm = lookup ty_assoc (perm_bn_ty t)
+      in
+        (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))
+      end
+
+    val goals = map mk_prop perm_bns
+    val alpha_names =  map (fst o dest_Const) alpha_trms       
+    
+  in
+    alpha_prove alpha_trms goals alpha_induct 
+      (raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt
+     |> ProofContext.export ctxt' ctxt
+     |> map atomize
+     |> map single
+     |> map (curry (op OF) perm_bn_rsp)
+  end
+
+
+
 (* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma