--- a/Nominal/nominal_dt_alpha.ML	Sat Jul 31 02:10:42 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Sun Aug 08 10:12:38 2010 +0800
@@ -27,6 +27,7 @@
   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
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -621,5 +622,24 @@
     (K (asm_full_simp_tac ss)) ctxt
 end
 
+(* helper lemmas for respectfulness for size *)
+
+fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
+let
+  val arg_tys = map (domain_type o fastype_of) all_alpha_trms
+
+  fun mk_prop ty (x, y) = HOLogic.mk_eq 
+    (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
+
+  val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys 
+  
+  val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps 
+    permute_prod_def prod.cases prod.recs})
+
+  val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
+in
+  alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
+end
+
 end (* structure *)