# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277272488 -3600
# Node ID 9038c9549073218f3223a318f0b7c04dbd5dbcc1
# Parent  99706604c573ae6a6b6392d0427bf4f167a48da0
deleted compose-lemmas in Abs (not needed anymore)

diff -r 99706604c573 -r 9038c9549073 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Jun 23 06:45:03 2010 +0100
+++ b/Nominal/Abs.thy	Wed Jun 23 06:54:48 2010 +0100
@@ -536,7 +536,8 @@
 apply(simp add: atom_image_cong)
 done
 
-lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+lemma swap_atom_image_fresh: 
+  "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
   apply (simp add: fresh_def)
   apply (simp add: supp_atom_image)
   apply (fold fresh_def)
@@ -578,291 +579,6 @@
      R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
 by (simp add: alphas)
 
-lemma alpha_gen_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(clarify)
-  apply(simp)
-  apply(rule a)
-  apply assumption
-  done
-
-lemma alpha_res_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>res R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(rule a)
-  apply assumption
-  done
-
-lemma alpha_lst_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>lst R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(clarify)
-  apply(simp)
-  apply(rule a)
-  apply assumption
-  done
-
-lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym
-
-lemma alpha_gen_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
-  using a
-  apply(simp add: alphas)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rule conjI)
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp_all
-  done
-
-lemma alpha_res_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>res (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>res (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
-  using a
-  apply(simp add: alphas)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp
-  done
-
-lemma alpha_lst_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>lst (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>lst (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
-  using a
-  apply(simp add: alphas)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rule conjI)
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp_all
-  done
-
-lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2
-
-lemma alpha_gen_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 7)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemma alpha_res_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>res R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>res R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemma alpha_lst_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>lst R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>lst R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 7)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans
-
-lemma alpha_gen_compose_trans2:
-  fixes pi pia
-  assumes b: "(aa, (t1, t2)) \<approx>gen
-    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
-    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
-  and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    pia (ac, (sa1, sa2))"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    (pia + pi) (ac, (sa1, sa2))"
-  using b c apply -
-  apply(simp add: alphas2)
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa1" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in r1)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r1)
-  apply(simp)
-  apply(drule_tac x="- pia \<bullet> sa2" in spec)
-  apply(drule mp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="- pia" in r2)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r2)
-  apply(simp)
-  done
-
-lemma alpha_res_compose_trans2:
-  fixes pi pia
-  assumes b: "(aa, (t1, t2)) \<approx>res
-    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
-    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
-  and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    pia (ac, (sa1, sa2))"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    (pia + pi) (ac, (sa1, sa2))"
-  using b c apply -
-  apply(simp add: alphas2)
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa1" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in r1)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r1)
-  apply(simp)
-  apply(drule_tac x="- pia \<bullet> sa2" in spec)
-  apply(drule mp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="- pia" in r2)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r2)
-  apply(simp)
-  done
-
-lemma alpha_lst_compose_trans2:
-  fixes pi pia
-  assumes b: "(aa, (t1, t2)) \<approx>lst
-    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
-    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
-  and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    pia (ac, (sa1, sa2))"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
-    (pia + pi) (ac, (sa1, sa2))"
-  using b c apply -
-  apply(simp add: alphas2)
-  apply(simp add: alphas)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa1" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in r1)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r1)
-  apply(simp)
-  apply(drule_tac x="- pia \<bullet> sa2" in spec)
-  apply(drule mp)
-  apply(rotate_tac 6)
-  apply(drule_tac pi="- pia" in r2)
-  apply(simp)
-  apply(rotate_tac -1)
-  apply(drule_tac pi="pia" in r2)
-  apply(simp)
-  done
-
-lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
-
-
-
 lemma alpha_gen_simpler:
   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
   and fin_fv: "finite (f x)"
diff -r 99706604c573 -r 9038c9549073 Nominal/Equivp.thy
--- a/Nominal/Equivp.thy	Wed Jun 23 06:45:03 2010 +0100
+++ b/Nominal/Equivp.thy	Wed Jun 23 06:54:48 2010 +0100
@@ -2,166 +2,6 @@
 imports "Abs" "Perm" "Tacs" "Rsp"
 begin
 
-ML {*
-fun build_alpha_sym_trans_gl alphas (x, y, z) =
-let
-  fun build_alpha alpha =
-    let
-      val ty = domain_type (fastype_of alpha);
-      val var = Free(x, ty);
-      val var2 = Free(y, ty);
-      val var3 = Free(z, ty);
-      val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
-      val transp = HOLogic.mk_imp (alpha $ var $ var2,
-        HOLogic.mk_all (z, ty,
-          HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
-    in
-      (symp, transp)
-    end;
-  val eqs = map build_alpha alphas
-  val (sym_eqs, trans_eqs) = split_list eqs
-  fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
-in
-  (conj sym_eqs, conj trans_eqs)
-end
-*}
-
-ML {*
-fun build_alpha_refl_gl fv_alphas_lst alphas =
-let
-  val (fvs_alphas, _) = split_list fv_alphas_lst;
-  val (_, alpha_ts) = split_list fvs_alphas;
-  val tys = map (domain_type o fastype_of) alpha_ts;
-  val names = Datatype_Prop.make_tnames tys;
-  val args = map Free (names ~~ tys);
-  fun find_alphas ty x =
-    domain_type (fastype_of x) = ty;
-  fun refl_eq_arg (ty, arg) =
-    let
-      val rel_alphas = filter (find_alphas ty) alphas;
-    in
-      map (fn x => x $ arg $ arg) rel_alphas
-    end;
-  (* Flattening loses the induction structure *)
-  val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
-in
-  (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
-end
-*}
-
-ML {*
-fun reflp_tac induct eq_iff =
-  rtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
-  split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
-  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
-     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
-       add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps})
-*}
-
-ML {*
-fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
-let
-  val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
-  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
-in
-  HOLogic.conj_elims refl_conj
-end
-*}
-
-lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="-pi" in exI)
-by auto
-
-ML {*
-fun symp_tac induct inj eqvt ctxt =
-  rtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
-  THEN_ALL_NEW
-  REPEAT o etac @{thm exi_neg}
-  THEN_ALL_NEW
-  split_conj_tac THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
-  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-*}
-
-
-lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
-apply (erule exE)+
-apply (rule_tac x="pia + pi" in exI)
-by auto
-
-
-ML {*
-fun eetac rule = 
-  Subgoal.FOCUS_PARAMS (fn focus =>
-    let
-      val concl = #concl focus
-      val prems = Logic.strip_imp_prems (term_of concl)
-      val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
-      val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
-      val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
-    in
-      (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
-    end
-  )
-*}
-
-ML {*
-fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
-  rtac induct THEN_ALL_NEW
-  (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
-  split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
-  THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
-  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
-  TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
-  (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
-*}
-
-lemma transpI:
-  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
-  unfolding transp_def
-  by blast
-
-ML {*
-fun equivp_tac reflps symps transps =
-  (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
-  simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
-  THEN' rtac conjI THEN' rtac allI THEN'
-  resolve_tac reflps THEN'
-  rtac conjI THEN' rtac allI THEN' rtac allI THEN'
-  resolve_tac symps THEN'
-  rtac @{thm transpI} THEN' resolve_tac transps
-*}
-
-ML {*
-fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
-let
-  val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
-  val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
-  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
-  fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
-  val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
-  val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
-  val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
-  val symps = HOLogic.conj_elims symp
-  val transps = HOLogic.conj_elims transp
-  fun equivp alpha =
-    let
-      val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
-      val goal = @{term Trueprop} $ (equivp $ alpha)
-      fun tac _ = equivp_tac reflps symps transps 1
-    in
-      Goal.prove ctxt [] [] goal tac
-    end
-in
-  map equivp alphas
-end
-*}
-
 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
 by auto
 
diff -r 99706604c573 -r 9038c9549073 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed Jun 23 06:45:03 2010 +0100
+++ b/Nominal/NewParser.thy	Wed Jun 23 06:54:48 2010 +0100
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Tacs" "Equivp" "Lift"
+        "Perm" "Tacs" "Lift" "Equivp"
 begin
 
 (* TODO