--- a/LamEx.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/LamEx.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -119,37 +119,35 @@
   shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
   sorry
 
+
+
 lemma real_alpha:
-  assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
+  assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
   shows "Lam a t = Lam b s"
+using a
+unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp: 
+lemma perm_rsp[quot_rsp]:
   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
   sorry
 
-lemma fresh_rsp: 
-  "(op = ===> alpha ===> op =) fresh fresh" 
+lemma fresh_rsp:
+  "(op = ===> alpha ===> op =) fresh fresh"
   apply(auto)
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rVar_rsp: "(op = ===> alpha) rVar rVar"
-  apply(auto)
-  apply(rule a1)
-  apply(simp)
-  done
+lemma rVar_rsp[quot_rsp]:
+  "(op = ===> alpha) rVar rVar"
+by (auto intro:a1)
 
-lemma rApp_rsp: "(alpha ===> alpha ===> alpha) rApp rApp"
-  apply(auto)
-  apply(rule a2)
-  apply (assumption)
-  apply (assumption)
-  done
+lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+by (auto intro:a2)
 
-lemma rLam_rsp: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -162,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -179,7 +177,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
@@ -236,6 +234,11 @@
 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
 done
 
+lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+              \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
+apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *})
+done
+
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
   apply(simp add: supp_def)