--- a/Quot/Examples/LamEx.thy	Fri Jan 15 16:13:49 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 17:09:36 2010 +0100
@@ -29,6 +29,25 @@
 
 end
 
+instance rlam::pt_name
+apply(default)
+apply(induct_tac [!] x rule: rlam.induct)
+apply(simp_all add: pt_name2 pt_name3)
+done
+
+instance rlam::fs_name
+apply(default)
+apply(induct_tac [!] x rule: rlam.induct)
+apply(simp add: supp_def)
+apply(fold supp_def)
+apply(simp add: supp_atm)
+apply(simp add: supp_def Collect_imp_eq Collect_neg_eq)
+apply(simp add: supp_def)
+apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric])
+apply(fold supp_def)
+apply(simp add: supp_atm)
+done
+
 inductive
   alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
 where
@@ -362,6 +381,60 @@
 
 (* lemma hom_reg: *)
 
+lemma rlam_rec_eqvt:
+  fixes pi::"name prm"
+  and   f1::"name \<Rightarrow> ('a::pt_name)"
+  shows "(pi\<bullet>rlam_rec f1 f2 f3 t) = rlam_rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
+apply(induct t)
+apply(simp_all)
+apply(simp add: perm_fun_def)
+apply(perm_simp)
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+back
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+apply(simp)
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+back
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
+apply(simp)
+done
+ 
+
+lemma rlam_rec_respects:
+  assumes f1: "f_var \<in> Respects (op= ===> op=)"
+  and     f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)"
+  and     f3: "f_lam \<in> Respects (op= ===> alpha ===> op= ===> op=)"
+  shows "rlam_rec f_var f_app f_lam \<in> Respects (alpha ===> op =)"
+apply(simp add: mem_def)
+apply(simp add: Respects_def)
+apply(rule allI)
+apply(rule allI)
+apply(rule impI)
+apply(erule alpha.induct)
+apply(simp)
+apply(simp)
+using f2
+apply(simp add: mem_def)
+apply(simp add: Respects_def)
+using f3[simplified mem_def Respects_def]
+apply(simp)
+apply(case_tac "a=b")
+apply(clarify)
+apply(simp)
+apply(subst pt_swap_bij'')
+apply(rule pt_name_inst)
+apply(rule at_name_inst)
+apply(subst pt_swap_bij'')
+apply(rule pt_name_inst)
+apply(rule at_name_inst)
+apply(simp)
+apply(generate_fresh "name")
+(* probably true *)
+sorry
+
 lemma hom: 
   "\<exists>hom\<in>Respects (alpha ===> op =). 
     ((\<forall>x. hom (rVar x) = f_var x) \<and>