--- a/Nominal/nominal_dt_quot.ML	Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Tue Dec 07 14:27:39 2010 +0000
@@ -35,7 +35,9 @@
  
   val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
     thm list -> Proof.context -> thm list
-  
+
+  val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+    thm list -> Proof.context -> thm list  
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -323,6 +325,7 @@
     induct_prove qtys props qinduct (K ss_tac) ctxt
   end
 
+
 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
   let 
     val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
@@ -344,7 +347,31 @@
     |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
   end
 
+fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
+  let 
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+    val p = Free (p, @{typ perm})
 
+    fun mk_goal qbn qperm_bn =
+      let
+        val arg_ty = domain_type (fastype_of qbn)
+      in
+        (arg_ty, fn x => 
+          (mk_id (Abs ("", arg_ty, 
+             HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x))
+      end
+
+    val props = map2 mk_goal qbns qperm_bns
+    val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
+    val ss_tac = 
+      EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
+              TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [],
+              TRY o asm_full_simp_tac HOL_basic_ss]
+  in
+    induct_prove qtys props qinduct (K ss_tac) ctxt'
+    |> ProofContext.export ctxt' ctxt 
+    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
+  end
 
 end (* structure *)