--- a/Nominal/Ex/SingleLet.thy	Tue Jul 27 23:34:30 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Thu Jul 29 10:16:33 2010 +0100
@@ -24,6 +24,7 @@
 thm alpha_bn_imps
 thm distinct
 thm eq_iff
+thm eq_iff_simps
 thm fv_defs
 thm perm_simps
 thm perm_laws
@@ -39,13 +40,13 @@
 term alpha_bn
 
 
-
 lemma a2:
   shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
+apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps 
+  alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
 done
 
 lemma [quot_respect]: 
@@ -59,24 +60,17 @@
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
 apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(assumption)
+apply(simp only: eq_iff)
+apply(simp only: simp_thms)
 apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(assumption)
-apply(assumption)
+apply(simp only: eq_iff)
+apply(tactic {* asm_full_simp_tac HOL_ss 1*})
 apply(simp only: fun_rel_def)
+apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2)
 apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
+apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2)
+apply(simp add: a2)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
 apply(simp only: fun_rel_def)
 apply(rule allI | rule impI)+

--- a/Nominal/NewParser.thy	Tue Jul 27 23:34:30 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Jul 29 10:16:33 2010 +0100
@@ -362,7 +362,7 @@
   (* definition of alpha_eq_iff  lemmas *)
   (* they have a funny shape for the simplifier *)
   val _ = warning "Eq-iff theorems";
-  val alpha_eq_iff = 
+  val (alpha_eq_iff_simps, alpha_eq_iff) = 
     if get_STEPS lthy > 5
     then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
     else raise TEST lthy4
@@ -426,7 +426,9 @@
   (* auxiliary lemmas for respectfulness proofs *)
   (* HERE *)
   
-
+  val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns
+    alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+  val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test))
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -481,7 +483,8 @@
 
   val (_, lthy8') = lthy8
      |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
-     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) 
+     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
+     ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) 
      ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 

--- 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 *)