--- a/Nominal/nominal_dt_supp.ML	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Dec 06 14:24:17 2010 +0000
@@ -17,7 +17,8 @@
     thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
 
   val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
-
+  val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+    Proof.context -> thm list
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -150,12 +151,6 @@
 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
   prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
 
-fun p_tac msg i = 
-  if false then print_tac ("ptest: " ^ msg) else all_tac
-
-fun q_tac msg i = 
-  if true then print_tac ("qtest: " ^ msg) else all_tac
-
 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
   fv_bn_eqvts qinduct bclausess ctxt =
   let
@@ -206,7 +201,29 @@
     val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
       @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
   in
-    induct_prove qtys props qinduct (K (ss_tac ORELSE' (K no_tac))) ctxt
+    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 ctxt =
+  let 
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+    val p = Free (p, @{typ perm})
+
+    fun mk_goal qperm_bn alpha_bn =
+      let
+        val arg_ty = domain_type (fastype_of alpha_bn)
+      in
+        (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
+      end
+
+    val props = map2 mk_goal qperm_bns alpha_bns
+    val ss_tac = (K (print_tac "test")) THEN' 
+      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs))
+  in
+    @{thms TrueI}
+    (*induct_prove qtys props qinduct (K ss_tac) ctxt'
+    |> ProofContext.export ctxt' ctxt
+    |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*)
   end