--- a/LamEx.thy	Fri Oct 30 15:35:42 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 15:52:47 2009 +0100
@@ -20,7 +20,7 @@
 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}"
 sorry
 
-termination rfv sorry 
+termination rfv sorry
 
 inductive 
   alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
@@ -156,19 +156,38 @@
   apply(simp add: abs_fresh)
   done
 
+lemma rfv_rsp: "(alpha ===> op =) rfv rfv"
+  sorry
 
 ML {* val qty = @{typ "lam"} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *}
+ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
 
 ML {* lift_thm_lam @{context} @{thm pi_var_com} *}
 ML {* lift_thm_lam @{context} @{thm pi_app_com} *}
 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *}
 
+ML {* lift_thm_lam @{context} @{thm rfv_var} *}
+ML {* lift_thm_lam @{context} @{thm rfv_app} *}
+ML {* lift_thm_lam @{context} @{thm rfv_lam} *}
+
+ML {* lift_thm_lam @{context} @{thm a3} *}
+
+
+
+
+
+
+
+
+
+
+
+
 fun
   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
 where
@@ -241,8 +260,12 @@
 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *}
 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *}
 
-ML {* val t_a = atomize_thm t_u *}
+(* T_U *)
+
+ML {* val t_a = atomize_thm @{thm rfv_var} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
+ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+
 ML {* fun r_mk_comb_tac_lam ctxt =
   r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms
 *}