--- a/Nominal/nominal_dt_alpha.ML	Tue Jul 27 23:34:30 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jul 29 10:16:33 2010 +0100
@@ -14,13 +14,16 @@
   val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> 
     term list -> term list -> bn_info -> thm list * thm list
 
-  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
+  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
+    thm list -> (thm list * thm list)
 
   val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
   val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> 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
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -333,7 +336,7 @@
   val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
 in
   Variable.export ctxt' ctxt thms
-  |> map mk_simp_rule
+  |> `(map mk_simp_rule)
 end
 
 
@@ -637,5 +640,78 @@
   |> filter_out (is_true o concl_of)
 end
 
+
+(* helper lemmas for respectfulness for fv_raw / bn_raw *)
+
+fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
+let
+  val arg_tys = 
+    alpha_trms 
+    |> map fastype_of
+    |> map domain_type
+
+  val fv_bn_tys1 =
+    (bns @ fvs)
+    |> map fastype_of
+    |> map domain_type
+
+  val (arg_names1, (arg_names2, ctxt')) =
+    ctxt
+    |> Variable.variant_fixes (replicate (length arg_tys) "x") 
+    ||> Variable.variant_fixes (replicate (length arg_tys) "y")
+  
+  val args1 = map Free (arg_names1 ~~ arg_tys)
+  val args2 = map Free (arg_names2 ~~ arg_tys)
+
+  val fv_bn_args1a = map (lookup (arg_tys ~~ args1)) fv_bn_tys1
+  val fv_bn_args1b = map (lookup (arg_tys ~~ args2)) fv_bn_tys1   
+  val fv_bn_eqs1 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) 
+    (bns @ fvs) (fv_bn_args1a ~~ fv_bn_args1b)
+
+  val arg_bn_tys = 
+    alpha_bn_trms 
+    |> map fastype_of
+    |> map domain_type
+
+  val fv_bn_tys2 =
+    fv_bns
+    |> map fastype_of
+    |> map domain_type
+ 
+  val (arg_bn_names1, (arg_bn_names2, ctxt'')) =
+    ctxt'
+    |> Variable.variant_fixes (replicate (length arg_bn_tys) "x") 
+    ||> Variable.variant_fixes (replicate (length arg_bn_tys) "y")
+  
+  val args_bn1 = map Free (arg_bn_names1 ~~ fv_bn_tys2)
+  val args_bn2 = map Free (arg_bn_names2 ~~ fv_bn_tys2)
+  val fv_bn_eqs2 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) 
+    fv_bns (args_bn1 ~~ args_bn2)
+
+  val goal_rhs = 
+    group (fv_bn_tys1 ~~ fv_bn_eqs1) 
+    |> map snd 
+    |> map (foldr1 HOLogic.mk_conj)
+
+  val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) 
+    (alpha_trms @ alpha_bn_trms) ((args1 ~~ args2) @ (args_bn1 ~~ args_bn2)) 
+             
+  val goal =
+    map2 (curry HOLogic.mk_imp) goal_lhs (goal_rhs @ fv_bn_eqs2)
+    |> foldr1 HOLogic.mk_conj
+    |> HOLogic.mk_Trueprop
+
+  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}) 
+in
+  Goal.prove ctxt'' [] [] goal (fn {context, ...} => 
+    HEADGOAL (DETERM o (rtac alpha_induct) THEN_ALL_NEW (asm_full_simp_tac ss)))
+  |> singleton (ProofContext.export ctxt'' ctxt)
+  |> Datatype_Aux.split_conj_thm 
+  |> map (fn th => zero_var_indexes (th RS mp))
+  |> map Datatype_Aux.split_conj_thm 
+  |> flat
+end
+
 end (* structure *)