--- a/LamEx.thy	Mon Nov 02 11:51:50 2009 +0100
+++ b/LamEx.thy	Mon Nov 02 14:57:56 2009 +0100
@@ -11,6 +11,7 @@
 | rApp "rlam" "rlam"
 | rLam "name" "rlam"
 
+print_theorems
 
 function
   rfv :: "rlam \<Rightarrow> name set"
@@ -29,6 +30,8 @@
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
+print_theorems
+
 quotient lam = rlam / alpha
 sorry
 
@@ -176,7 +179,7 @@
 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *}
 
 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
-ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
+ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
@@ -240,6 +243,7 @@
  *}
   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);
@@ -279,39 +283,60 @@
 
 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 {*
-
-
-*}
-
 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
+ML {* val thm = 
+  @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *}
+ML {* val t_a = simp_allex_prs quot [thm] 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_app_prs_thms @ simp_lam_prs_thms) t_t *}
-ML {* val t_a = simp_allex_prs @{context} quot t_l *}
-ML {* val thm = 
-  @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]], symmetric]} *}
-ML {* val t_a1 = eqsubst_thm @{context} [thm] t_a *}
+
+ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @  simp_lam_prs_thms) t_a *}
 ML {* val defs_sym = add_lower_defs @{context} defs; *}
-ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a1 *}
+ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *}
+ML t_l
+ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *}
+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 = repeat_eqsubst_thm @{context} @{thms QUOT_TYPE_I_lam.thm10} t_r1 *}
-ML {* val t_r3 = repeat_eqsubst_thm @{context} @{thms id_apply} t_r2 *}
-
+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
+
+lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)"
+apply (rule alpha.cases)
+apply (assumption)
+apply (assumption)
+apply (simp_all)
+apply (cases "a = b")
+apply (simp_all)
+apply (cases "ba = b")
+apply (simp_all)
+
+
+lemma var_inject_test:
+  fixes a b
+  assumes a: "Var a = Var b"
+  shows "(a = b)"
+  using a   apply (cases "a = b")
+  apply (simp_all)
+  apply (rule_tac x="Var a" and xa = "Var b" in alpha_cases)
+  apply (rule a)
+
+
 lemma
-  assumes a: "(a::lam) = b"
-  shows "False"
-  using a
-  apply (rule alpha_induct)
-
+  assumes a: "(x::lam) = y"
+  shows "P x y"
+  apply (induct rule: alpha_induct)
+  apply (rule a)
+thm alpha.induct
+thm alpha_induct
 fun
   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
 where