# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269675727 -3600
# Node ID e8cf0520c82030bca9a8739e5568cc849d1f9f76
# Parent  94b8b70f7bc0533f3a8ba057000bda30bf8b3182
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.

diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -460,12 +460,16 @@
   shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
-lemma alpha_gen2:
+lemma alphas2:
   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
   \<and> pi \<bullet> bs = cs)"
-by (simp add: alpha_gen)
-
+  "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
+  (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
+  "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) =
+  (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
+  \<and> pi \<bullet> bsl = csl)"
+by (simp_all add: alphas)
 
 lemma alpha_gen_compose_sym:
   fixes pi
@@ -473,7 +477,7 @@
   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: alpha_gen)
+  apply(simp add: alphas)
   apply(erule conjE)+
   apply(rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
@@ -485,6 +489,42 @@
   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)"
@@ -492,7 +532,7 @@
   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: alpha_gen)
+  apply(simp add: alphas)
   apply clarify
   apply (rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
@@ -506,6 +546,49 @@
   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)"
@@ -513,7 +596,7 @@
   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: alpha_gen)
+  apply(simp add: alphas)
   apply(erule conjE)+
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
@@ -526,6 +609,47 @@
   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
@@ -538,8 +662,8 @@
   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: alpha_gen2)
-  apply(simp add: alpha_gen)
+  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)
@@ -560,6 +684,76 @@
   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_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
@@ -571,36 +765,22 @@
   by (simp_all add: fresh_zero_perm)
 
 lemma alpha_gen_sym:
-  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
-  and     b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
+  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
   unfolding alphas fresh_star_def
-  apply (erule_tac [1] conjE)+
-  apply (erule_tac [2] conjE)+
-  apply (erule_tac [3] conjE)+
   using a
-  apply (simp_all add: fresh_minus_perm)
-  apply (rotate_tac [!] -1)
-  apply (drule_tac [!] p="-p" in b)
-  apply (simp_all)
-  apply (metis permute_minus_cancel(2))
-  apply (metis permute_minus_cancel(2))
-  done
+  by (auto simp add:  fresh_minus_perm)
+
 lemma alpha_gen_trans:
-  assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)"
-  and b: "R (p \<bullet> x) y"
-  and c: "R (q \<bullet> y) z"
-  and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
+  assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
   shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
-  unfolding alphas
-  unfolding fresh_star_def
-  apply (simp_all add: fresh_plus_perm)
-  apply (metis a c d permute_minus_cancel(2))+
-  done
+  using a
+  unfolding alphas fresh_star_def
+  by (simp_all add: fresh_plus_perm)
 
 lemma alpha_gen_eqvt:
   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/ExTySch.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -36,7 +36,7 @@
   "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
   apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
   apply (simp_all only: t_raw_tyS_raw.size)
-  apply (simp_all only: alpha_gen)
+  apply (simp_all only: alphas)
   apply clarify
   apply (simp_all only: size_eqvt_raw)
   done
@@ -119,7 +119,7 @@
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen)
+  apply(simp add: alphas)
   apply(auto)
   apply(simp add: fresh_star_def fresh_zero_perm)
   done
diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -681,7 +681,7 @@
   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 (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) 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)))
 *}
 
@@ -715,7 +715,7 @@
   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 (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) 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)))
 *}
 
@@ -897,7 +897,7 @@
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -464,11 +464,11 @@
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
-  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff
-  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1
+  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff
+  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1
   val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
-  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
-  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
+  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
+  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -62,7 +62,7 @@
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
@@ -81,7 +81,7 @@
   simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
-   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
      @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
@@ -260,7 +260,7 @@
 
 ML {*
 fun fvbv_rsp_tac' simps ctxt =
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW