--- a/Nominal/Term5.thy	Mon Mar 01 14:26:14 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 01 16:04:03 2010 +0100
@@ -22,8 +22,13 @@
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
 print_theorems
 
+
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [
-  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
+  [ [],
+    [],
+    [(SOME @{term rbv5}, 0, 1)] ],
+  [ [],
+    []]  ] *}
 print_theorems
 
 (* Alternate version with additional binding of name in rlts in rLcons *)
@@ -57,17 +62,12 @@
   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
   apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
   apply (simp_all add: alpha5_inj)
-  apply (tactic {* 
-    ALLGOALS (
-      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt})
-    ) *})
-  apply (simp_all only: eqvts atom_eqvt)
-  done
+sorry
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
-  (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}
-thm alpha5_equivp
+lemma alpha5_equivp:
+  "equivp alpha_rtrm5"
+  "equivp alpha_rlts"
+  sorry
 
 quotient_type
   trm5 = rtrm5 / alpha_rtrm5
@@ -92,13 +92,20 @@
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
   "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
-  apply(simp_all add: alpha_gen)
+  apply(simp_all)
+  apply(simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(erule exE)
+  apply(erule conjE)+
+  apply(simp_all)
   done
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
   apply(simp_all)
+  apply(clarify)
+  apply simp
   done
 
 lemma [quot_respect]:
@@ -112,8 +119,7 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
-  apply (clarify) apply (rule conjI)
-  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (clarify)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   done
 
@@ -149,49 +155,24 @@
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
+apply (simp add: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-done
-
-lemma lets_ok2:
-  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
-   (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp only: alpha_gen)
+apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
 done
 
 lemma lets_ok3:
-  assumes a: "distinct [x, y]"
-  shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
-         (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (simp add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
+  "x \<noteq> y \<Longrightarrow>
+   (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
 done
 
+
 lemma lets_not_ok1:
   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
              (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: alpha5_INJ(3) alpha_gen)
+apply (simp add: alpha5_INJ alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))
 done
 
@@ -214,5 +195,4 @@
 apply (simp add: distinct_helper2)
 done
 
-
 end