--- a/LamEx.thy	Tue Nov 03 17:30:43 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 17:51:10 2009 +0100
@@ -23,7 +23,7 @@
 
 termination rfv sorry
 
-inductive 
+inductive
   alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
 where
   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
@@ -32,6 +32,10 @@
 
 print_theorems
 
+lemma alpha_refl:
+  shows "x \<approx> x"
+sorry
+
 quotient lam = rlam / alpha
 sorry
 
@@ -117,12 +121,6 @@
   shows "Lam a t = Lam b s"
 sorry
 
-
-
-
-
-(* Construction Site code *)
-
 lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
@@ -163,11 +161,10 @@
   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 fv_def} *}
-ML {* val consts = lookup_quot_consts defs *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-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 {* 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 pi_var = lift_thm_lam @{context} @{thm pi_var_com} *}
@@ -183,6 +180,7 @@
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
+ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
 
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
@@ -191,19 +189,26 @@
   Quotient.note (@{binding "a1"}, a1) #> snd #>
   Quotient.note (@{binding "a2"}, a2) #> snd #>
   Quotient.note (@{binding "a3"}, a3) #> snd #>
-  Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd
+  Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #>
+  Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd
 *}
 
 thm alpha.cases
 thm alpha_cases
+thm alpha.induct
+thm alpha_induct
 
-thm rlam.inject
-thm pi_var
- 
+lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
+apply (auto)
+apply (erule alpha.cases)
+apply (simp_all add: rlam.inject alpha_refl)
+done
 
-lemma var_inject:
-  shows "(Var a = Var b) = (a = b)"
-sorry
+ML {* val var_inject = Toplevel.program (fn () => lift_thm_lam @{context} @{thm rvar_inject}) *}
+
+local_setup {*
+  Quotient.note (@{binding "var_inject"}, var_inject) #> snd
+*}
 
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
@@ -225,6 +230,17 @@
 
 
 
+
+
+
+
+
+(* 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.induct} *}
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
 ML_prf {*  fun tac ctxt =
@@ -300,38 +316,20 @@
 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 {*
+(*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 (erule alpha.cases)
-apply (simp add: rlam.inject)
-apply (simp)
-apply (simp)
-done
+
+
 
 
-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: "(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