# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273591017 -7200
# Node ID 2205b572bc9b81512533f2a4c1138b38772d0ad8
# Parent  e08e3c29dbc0d5d3d235cf676c671bd8322ec8a1
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'

diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Abs.thy	Tue May 11 17:16:57 2010 +0200
@@ -760,7 +760,7 @@
   by (simp_all add: fresh_plus_perm)
 
 
-lemma alpha_gen_eqvt(*[eqvt]*):
+lemma alpha_gen_eqvt[eqvt]:
   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/Classical.thy	Tue May 11 17:16:57 2010 +0200
@@ -69,7 +69,6 @@
 thm alpha.intros
 
 declare permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha
 equivariance alpha_trm_raw
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Tue May 11 17:16:57 2010 +0200
@@ -203,9 +203,9 @@
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
   apply (simp add: perm_bv2[symmetric])
-  apply (simp add: eqvts[symmetric])
   apply (simp add: supp_abs)
   apply (simp add: fv_supp)
+  apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
   apply (rule finite_Diff)
@@ -395,18 +395,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a08)
@@ -435,18 +433,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
                 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a15)
@@ -476,18 +472,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a29)
@@ -516,18 +510,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a30)
@@ -557,18 +549,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a32)
@@ -598,18 +588,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
                 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a34)
@@ -659,13 +647,12 @@
 (* for the moment, we force it to be       *)
 
 (*declare permute_pure[eqvt]*)
-(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *)
+(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *)
 
 thm eqvts
 thm eqvts_raw
 
 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_tkind_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/Ex1rec.thy
--- a/Nominal/Ex/Ex1rec.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/Ex1rec.thy	Tue May 11 17:16:57 2010 +0200
@@ -31,7 +31,6 @@
 thm lam_bp.fv[simplified lam_bp.supp(1-2)]
 
 declare permute_lam_raw_permute_bp_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_lam_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/Ex2.thy
--- a/Nominal/Ex/Ex2.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/Ex2.thy	Tue May 11 17:16:57 2010 +0200
@@ -28,7 +28,6 @@
 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
 declare permute_trm_raw_permute_pat_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/Ex3.thy
--- a/Nominal/Ex/Ex3.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/Ex3.thy	Tue May 11 17:16:57 2010 +0200
@@ -32,7 +32,6 @@
 
 
 declare permute_trm_raw_permute_pat_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExLet.thy
--- a/Nominal/Ex/ExLet.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExLet.thy	Tue May 11 17:16:57 2010 +0200
@@ -36,7 +36,6 @@
 
 
 declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExLetMult.thy
--- a/Nominal/Ex/ExLetMult.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExLetMult.thy	Tue May 11 17:16:57 2010 +0200
@@ -23,7 +23,6 @@
 thm trm_lts.fv[simplified trm_lts.supp]
 
 declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExLetRec.thy	Tue May 11 17:16:57 2010 +0200
@@ -33,7 +33,6 @@
 thm trm_lts.fv[simplified trm_lts.supp]
 
 declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExPS3.thy
--- a/Nominal/Ex/ExPS3.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExPS3.thy	Tue May 11 17:16:57 2010 +0200
@@ -36,7 +36,6 @@
 thm exp_pat.supp(1-2)
 
 declare permute_exp_raw_permute_pat_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_exp_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExPS6.thy
--- a/Nominal/Ex/ExPS6.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExPS6.thy	Tue May 11 17:16:57 2010 +0200
@@ -33,7 +33,6 @@
 thm exp_pat.supp
 
 declare permute_exp_raw_permute_pat_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_exp_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExPS7.thy
--- a/Nominal/Ex/ExPS7.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExPS7.thy	Tue May 11 17:16:57 2010 +0200
@@ -29,7 +29,6 @@
 thm exp_lrb_lrbs.supp
 
 declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_exp_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/ExPS8.thy	Tue May 11 17:16:57 2010 +0200
@@ -50,7 +50,6 @@
 
 
 declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_exp_raw
 end
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/LF.thy
--- a/Nominal/Ex/LF.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/LF.thy	Tue May 11 17:16:57 2010 +0200
@@ -21,7 +21,6 @@
 thm kind_ty_trm.supp
 
 declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue May 11 17:16:57 2010 +0200
@@ -16,7 +16,6 @@
 declare lam.perm[eqvt]
 
 declare permute_lam_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 equivariance alpha_lam_raw
 
 section {* Strong Induction Principles*}
@@ -261,7 +260,6 @@
    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
 declare permute_lam_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 equivariance alpha_lam_raw'
 
 thm eqvts_raw
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/Modules.thy
--- a/Nominal/Ex/Modules.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/Modules.thy	Tue May 11 17:16:57 2010 +0200
@@ -69,7 +69,6 @@
 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
 
 declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Tue May 11 17:16:57 2010 +0200
@@ -28,7 +28,6 @@
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
 
 declare permute_trm_raw_permute_assg_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_trm_raw
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/TestMorePerm.thy
--- a/Nominal/Ex/TestMorePerm.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/TestMorePerm.thy	Tue May 11 17:16:57 2010 +0200
@@ -27,7 +27,6 @@
 thm fv_weird_raw.simps[no_vars]
 
 declare permute_weird_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 equivariance alpha_weird_raw
 
 
diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 11 17:16:57 2010 +0200
@@ -15,7 +15,6 @@
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
 declare permute_ty_raw_permute_tys_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 equivariance alpha_ty_raw