# 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