--- a/LamEx.thy	Wed Nov 25 10:52:21 2009 +0100
+++ b/LamEx.thy	Wed Nov 25 11:41:42 2009 +0100
@@ -176,7 +176,6 @@
 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 {* 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" *}
@@ -268,101 +267,6 @@
 
 (* Construction Site code *)
 
-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 {* val t_a = atomize_thm @{thm alpha.cases} *}
-(* prove {* build_regularize_goal t_a rty rel @{context}  *}
-ML_prf {*  fun tac ctxt =
-     (FIRST' [
-      rtac rel_refl,
-      atac,
-      rtac @{thm universal_twice},
-      (rtac @{thm impI} THEN' atac),
-      rtac @{thm implication_twice},
-      EqSubst.eqsubst_tac ctxt [0]
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])],
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
-      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-     ]);
- *}
-  apply (tactic {* tac @{context} 1 *}) *)
-ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
-
-ML {*
-  val rt = build_repabs_term @{context} t_r consts rty qty
-  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
-*}
-prove rg
-apply(atomize(full))
-(*ML_prf {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
-  (FIRST' [
-    rtac trans_thm,
-    LAMBDA_RES_TAC ctxt,
-    res_forall_rsp_tac ctxt,
-    res_exists_rsp_tac ctxt,
-    (
-     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
-     THEN_ALL_NEW (fn _ => no_tac)
-    ),
-    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
-    rtac refl,
-    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
-    Cong_Tac.cong_tac @{thm cong},
-    rtac @{thm ext},
-    rtac reflex_thm,
-    atac,
-    (
-     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-     THEN_ALL_NEW (fn _ => no_tac)
-    ),
-    WEAK_LAMBDA_RES_TAC ctxt
-    ]);
-*}*)
-ML_prf {*
-  fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
-*}
-apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
-
-
-
-
-
-
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-
-
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
-ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS} ) alls *}
-ML {* val exthms = map (make_allex_prs_thm @{context} quot @{thm EXISTS_PRS} ) exs *}
-ML {* val t_a = MetaSimplifier.rewrite_rule allthms t_t *}
-ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
-ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
-ML {* val t_l = repeat_eqsubst_thm @{context} (simp_lam_prs_thms) t_a *}
-ML {* val t_l1 = repeat_eqsubst_thm @{context} simp_app_prs_thms t_l *}
-ML {* val defs_sym = add_lower_defs @{context} defs; *}
-ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *}
-ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l1 *}
-ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *}
-ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
-ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *}
-ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *}
-ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *}
-ML {* val alpha_induct = ObjectLogic.rulify t_r3 *}
-
-(*local_setup {*
-  Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd
-*}*)
-
-thm alpha_induct
-thm alpha.induct
-
 
 
 
@@ -384,6 +288,9 @@
 
 declare [[map noption = (option_map, option_rel)]]
 
+lemma "option_map id = id"
+sorry
+
 lemma OPT_QUOTIENT:
   assumes q: "QUOTIENT R Abs Rep"
   shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)"