--- a/Nominal/Nominal2_Base.thy Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Base.thy Mon Feb 28 15:21:10 2011 +0000
@@ -8,8 +8,12 @@
imports Main
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Quotient_Examples/FSet"
-uses ("nominal_library.ML")
+uses ("nominal_basics.ML")
+ ("nominal_thmdecls.ML")
+ ("nominal_permeq.ML")
+ ("nominal_library.ML")
("nominal_atoms.ML")
+ ("nominal_eqvt.ML")
begin
section {* Atoms and Sorts *}
@@ -437,38 +441,6 @@
end
-lemma Not_eqvt:
- shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
-by (simp add: permute_bool_def)
-
-lemma conj_eqvt:
- shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma imp_eqvt:
- shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma ex_eqvt:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma all_eqvt:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-lemma ex1_eqvt:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
- unfolding Ex1_def
- apply(simp add: ex_eqvt)
- unfolding permute_fun_def
- apply(simp add: conj_eqvt all_eqvt)
- unfolding permute_fun_def
- apply(simp add: imp_eqvt permute_bool_def)
- done
-
lemma permute_boolE:
fixes P::"bool"
shows "p \<bullet> P \<Longrightarrow> P"
@@ -541,11 +513,6 @@
unfolding mem_def permute_fun_def permute_bool_def
by simp
-lemma mem_eqvt:
- shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_def
- by (simp add: permute_fun_app_eq)
-
lemma empty_eqvt:
shows "p \<bullet> {} = {}"
unfolding empty_def Collect_def
@@ -555,22 +522,6 @@
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
unfolding permute_set_eq_image image_insert ..
-lemma Collect_eqvt:
- shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
-
-lemma inter_eqvt:
- shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def
- apply(simp add: Collect_eqvt)
- apply(simp add: permute_fun_def)
- apply(simp add: conj_eqvt)
- apply(simp add: mem_eqvt)
- apply(simp add: permute_fun_def)
- done
-
-
-
subsection {* Permutations for units *}
instantiation unit :: pt
@@ -635,6 +586,8 @@
shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
+
+
subsection {* Permutations for options *}
instantiation option :: (pt) pt
@@ -654,6 +607,8 @@
subsection {* Permutations for fsets *}
+
+
lemma permute_fset_rsp[quot_respect]:
shows "(op = ===> list_eq ===> list_eq) permute permute"
unfolding fun_rel_def
@@ -682,7 +637,9 @@
and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
by (lifting permute_list.simps)
-
+lemma fset_eqvt:
+ shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
+ by (lifting set_eqvt)
subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
@@ -762,6 +719,277 @@
instance int :: pure
proof qed (rule permute_int_def)
+
+
+subsection {* Basic functions about permutations *}
+
+use "nominal_basics.ML"
+
+
+subsection {* Equivariance infrastructure *}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+use "nominal_thmdecls.ML"
+setup "Nominal_ThmDecls.setup"
+
+
+lemmas [eqvt] =
+ (* permutations *)
+ uminus_eqvt add_perm_eqvt swap_eqvt
+
+ (* datatypes *)
+ Pair_eqvt
+ permute_list.simps
+ permute_option.simps
+ permute_sum.simps
+
+ (* sets *)
+ empty_eqvt insert_eqvt set_eqvt
+
+ (* fsets *)
+ permute_fset fset_eqvt
+
+
+
+subsection {* perm_simp infrastructure *}
+
+definition
+ "unpermute p = permute (- p)"
+
+lemma eqvt_apply:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ and x :: "'a::pt"
+ shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+ unfolding permute_fun_def by simp
+
+lemma eqvt_lambda:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+ unfolding permute_fun_def unpermute_def by simp
+
+lemma eqvt_bound:
+ shows "p \<bullet> unpermute p x \<equiv> x"
+ unfolding unpermute_def by simp
+
+text {* provides perm_simp methods *}
+
+use "nominal_permeq.ML"
+setup Nominal_Permeq.setup
+
+method_setup perm_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
+
+method_setup perm_strict_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+
+(* the normal version of this lemma would cause loops *)
+lemma permute_eqvt_raw[eqvt_raw]:
+ shows "p \<bullet> permute \<equiv> permute"
+apply(simp add: fun_eq_iff permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
+subsubsection {* Equivariance of Logical Operators *}
+
+lemma eq_eqvt [eqvt]:
+ shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+ unfolding permute_eq_iff permute_bool_def ..
+
+lemma Not_eqvt [eqvt]:
+ shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
+by (simp add: permute_bool_def)
+
+lemma conj_eqvt [eqvt]:
+ shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma imp_eqvt [eqvt]:
+ shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+declare imp_eqvt[folded induct_implies_def, eqvt]
+
+lemma ex_eqvt [eqvt]:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+lemma all_eqvt [eqvt]:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
+declare all_eqvt[folded induct_forall_def, eqvt]
+
+lemma ex1_eqvt [eqvt]:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ unfolding Ex1_def
+ by (perm_simp) (rule refl)
+
+lemma mem_eqvt [eqvt]:
+ shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ unfolding mem_def
+ by (simp add: permute_fun_app_eq)
+
+lemma Collect_eqvt [eqvt]:
+ shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ unfolding Collect_def permute_fun_def ..
+
+
+
+lemma inter_eqvt [eqvt]:
+ shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ unfolding Int_def
+ by (perm_simp) (rule refl)
+
+lemma image_eqvt [eqvt]:
+ shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ unfolding permute_set_eq_image
+ unfolding permute_fun_def [where f=f]
+ by (simp add: image_image)
+
+lemma if_eqvt [eqvt]:
+ shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+ by (simp add: permute_fun_def permute_bool_def)
+
+lemma True_eqvt [eqvt]:
+ shows "p \<bullet> True = True"
+ unfolding permute_bool_def ..
+
+lemma False_eqvt [eqvt]:
+ shows "p \<bullet> False = False"
+ unfolding permute_bool_def ..
+
+lemma disj_eqvt [eqvt]:
+ shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma all_eqvt2:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex_eqvt2:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex1_eqvt2:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma the_eqvt:
+ assumes unique: "\<exists>!x. P x"
+ shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+ apply(rule the1_equality [symmetric])
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_simp add: permute_minus_cancel)
+ apply(rule unique)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_simp add: permute_minus_cancel)
+ apply(rule theI'[OF unique])
+ done
+
+lemma the_eqvt2:
+ assumes unique: "\<exists>!x. P x"
+ shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+ apply(rule the1_equality [symmetric])
+ apply(simp add: ex1_eqvt2[symmetric])
+ apply(simp add: permute_bool_def unique)
+ apply(simp add: permute_bool_def)
+ apply(rule theI'[OF unique])
+ done
+
+subsubsection {* Equivariance Set Operations *}
+
+lemma Bex_eqvt[eqvt]:
+ shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ unfolding Bex_def
+ by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+ shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ unfolding Ball_def
+ by (perm_simp) (rule refl)
+
+lemma UNIV_eqvt[eqvt]:
+ shows "p \<bullet> UNIV = UNIV"
+ unfolding UNIV_def
+ by (perm_simp) (rule refl)
+
+lemma union_eqvt[eqvt]:
+ shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ unfolding Un_def
+ by (perm_simp) (rule refl)
+
+lemma Diff_eqvt[eqvt]:
+ fixes A B :: "'a::pt set"
+ shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+ unfolding set_diff_eq
+ by (perm_simp) (rule refl)
+
+lemma Compl_eqvt[eqvt]:
+ fixes A :: "'a::pt set"
+ shows "p \<bullet> (- A) = - (p \<bullet> A)"
+ unfolding Compl_eq_Diff_UNIV
+ by (perm_simp) (rule refl)
+
+lemma subset_eqvt[eqvt]:
+ shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
+ unfolding subset_eq
+ by (perm_simp) (rule refl)
+
+lemma psubset_eqvt[eqvt]:
+ shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
+ unfolding psubset_eq
+ by (perm_simp) (rule refl)
+
+lemma vimage_eqvt[eqvt]:
+ shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ unfolding vimage_def
+ by (perm_simp) (rule refl)
+
+lemma Union_eqvt[eqvt]:
+ shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+ unfolding Union_eq
+ by (perm_simp) (rule refl)
+
+lemma Sigma_eqvt:
+ shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
+unfolding Sigma_def
+unfolding UNION_eq_Union_image
+by (perm_simp) (rule refl)
+
+lemma finite_permute_iff:
+ shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+ unfolding permute_set_eq_vimage
+ using bij_permute by (rule finite_vimage_iff)
+
+lemma finite_eqvt[eqvt]:
+ shows "p \<bullet> finite A = finite (p \<bullet> A)"
+ unfolding finite_permute_iff permute_bool_def ..
+
+
+subsubsection {* Product Operations *}
+
+lemma fst_eqvt[eqvt]:
+ "p \<bullet> (fst x) = fst (p \<bullet> x)"
+ by (cases x) simp
+
+lemma snd_eqvt[eqvt]:
+ "p \<bullet> (snd x) = snd (p \<bullet> x)"
+ by (cases x) simp
+
+lemma split_eqvt[eqvt]:
+ shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ unfolding split_def
+ by (perm_simp) (rule refl)
+
+
+
+
subsection {* Supp, Freshness and Supports *}
context pt
@@ -843,12 +1071,12 @@
finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
qed
-lemma fresh_eqvt:
+lemma fresh_eqvt [eqvt]:
shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
unfolding permute_bool_def
by (simp add: fresh_permute_iff)
-lemma supp_eqvt:
+lemma supp_eqvt [eqvt]:
shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
unfolding supp_conv_fresh
unfolding Collect_def
@@ -970,7 +1198,6 @@
"supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
-
section {* Finitely-supported types *}
class fs = pt +
@@ -1246,6 +1473,58 @@
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+subsubsection {* List Operations *}
+
+lemma append_eqvt[eqvt]:
+ shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ by (induct xs) auto
+
+lemma rev_eqvt[eqvt]:
+ shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ by (induct xs) (simp_all add: append_eqvt)
+
+lemma supp_rev:
+ shows "supp (rev xs) = supp xs"
+ by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+
+lemma fresh_rev:
+ shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+ by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+
+lemma map_eqvt[eqvt]:
+ shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+
+lemma removeAll_eqvt[eqvt]:
+ shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+ by (induct xs) (auto)
+
+lemma supp_removeAll:
+ fixes x::"atom"
+ shows "supp (removeAll x xs) = supp xs - {x}"
+ by (induct xs)
+ (auto simp add: supp_Nil supp_Cons supp_atom)
+
+lemma filter_eqvt[eqvt]:
+ shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt[eqvt]:
+ shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
+lemma length_eqvt[eqvt]:
+ shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
+
instance list :: (fs) fs
apply default
apply (induct_tac x)
@@ -1266,13 +1545,6 @@
unfolding fresh_def supp_def
unfolding MOST_iff_cofinite by simp
-lemma supp_subset_fresh:
- assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
- shows "supp y \<subseteq> supp x"
- using a
- unfolding fresh_def
- by blast
-
lemma fresh_fun_app:
assumes "a \<sharp> f" and "a \<sharp> x"
shows "a \<sharp> f x"
@@ -1316,6 +1588,16 @@
using supp_fun_app by auto
qed
+lemma supp_fun_app_eqvt:
+ assumes a: "eqvt f"
+ shows "supp (f x) \<subseteq> supp x"
+proof -
+ from a have "supp f = {}" by (simp add: supp_fun_eqvt)
+ then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast
+qed
+
+
+
text {* equivariance of a function at a given argument *}
definition
@@ -1353,7 +1635,8 @@
using supp_eqvt_at[OF asm fin]
by auto
-text {* helper functions for nominal_functions *}
+
+subsection {* helper functions for nominal_functions *}
lemma the_default_eqvt:
assumes unique: "\<exists>!x. P x"
@@ -1445,27 +1728,6 @@
unfolding fresh_def
by (auto simp add: supp_finite_atom_set assms)
-
-lemma Union_fresh:
- shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
- unfolding Union_image_eq[symmetric]
- apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
- unfolding eqvt_def
- unfolding permute_fun_def
- apply(simp)
- unfolding UNION_def
- unfolding Collect_def
- unfolding Bex_def
- apply(simp add: ex_eqvt)
- unfolding permute_fun_def
- apply(simp add: conj_eqvt)
- apply(simp add: mem_eqvt)
- apply(simp add: supp_eqvt)
- unfolding permute_fun_def
- apply(simp)
- apply(assumption)
- done
-
lemma Union_supports_set:
shows "(\<Union>x \<in> S. supp x) supports S"
proof -
@@ -1489,12 +1751,14 @@
assumes fin: "finite S"
shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
proof -
+ have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)"
+ unfolding eqvt_def
+ by (perm_simp) (simp)
have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
- by (rule supp_finite_atom_set[symmetric])
- (rule Union_of_finite_supp_sets[OF fin])
- also have "\<dots> \<subseteq> supp S"
- by (rule supp_subset_fresh)
- (simp add: Union_fresh)
+ by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
+ also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
+ also have "\<dots> \<subseteq> supp S" using eqvt
+ by (rule supp_fun_app_eqvt)
finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
qed
@@ -1564,10 +1828,6 @@
subsection {* Type @{typ "'a fset"} is finitely supported *}
-lemma fset_eqvt:
- shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
- by (lifting set_eqvt)
-
lemma supp_fset [simp]:
shows "supp (fset S) = supp S"
unfolding supp_def
@@ -1610,6 +1870,30 @@
done
+lemma in_fset_eqvt[eqvt]:
+ shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
+unfolding in_fset
+by (perm_simp) (simp)
+
+lemma union_fset_eqvt[eqvt]:
+ shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
+by (induct S) (simp_all)
+
+lemma supp_union_fset:
+ fixes S T::"'a::fs fset"
+ shows "supp (S |\<union>| T) = supp S \<union> supp T"
+by (induct S) (auto)
+
+lemma fresh_union_fset:
+ fixes S T::"'a::fs fset"
+ shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
+unfolding fresh_def
+by (simp add: supp_union_fset)
+
+lemma map_fset_eqvt[eqvt]:
+ shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+ by (lifting map_eqvt)
+
section {* Freshness and Fresh-Star *}
lemma fresh_Unit_elim:
@@ -1751,15 +2035,10 @@
unfolding fresh_star_def
by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
-lemma fresh_star_eqvt:
+lemma fresh_star_eqvt [eqvt]:
shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
unfolding fresh_star_def
-unfolding Ball_def
-apply(simp add: all_eqvt)
-apply(subst permute_fun_def)
-apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
-done
-
+by (perm_simp) (rule refl)
section {* Induction principle for permutations *}
@@ -2191,6 +2470,8 @@
assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
+declare atom_eqvt[eqvt]
+
class at = at_base +
assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
@@ -2300,6 +2581,7 @@
where
"(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
+
lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
unfolding flip_def by (rule swap_self)
@@ -2318,7 +2600,7 @@
lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
by (simp add: flip_commute)
-lemma flip_eqvt:
+lemma flip_eqvt [eqvt]:
fixes a b c::"'a::at_base"
shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
unfolding flip_def
@@ -2638,5 +2920,10 @@
use "nominal_atoms.ML"
+section {* automatic equivariance procedure for inductive definitions *}
+
+use "nominal_eqvt.ML"
+
+
end