section ‹Permutations›
theory Renaming
imports
"~~/src/HOL/Library/Infinite_Set"
"~~/src/Tools/Adhoc_Overloading"
Util
begin
text ‹A class for all infinite types.›
class infinite =
assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
text ‹This theory is mainly ported from HOL-Nominal2, but using locales instead
of type classes. The intention is to leave the type of atoms arbitrary (such
that it can later be used with polymorphic first-order terms.›
text ‹The set of all permutations of a given type.›
definition perms :: "('a ⇒ 'a) set"
where
"perms = {f. bij f ∧ finite {x. f x ≠ x}}"
typedef 'a perm = "perms :: ('a ⇒ 'a) set"
by standard (auto simp: perms_def)
lemma permsI [Pure.intro]:
assumes "bij f" and "MOST x. f x = x"
shows "f ∈ perms"
using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
lemma perms_imp_bij:
"f ∈ perms ⟹ bij f"
by (simp add: perms_def)
lemma perms_imp_finite_domain:
"f ∈ perms ⟹ finite {x. f x ≠ x}"
by (simp add: perms_def)
lemma perms_imp_MOST_eq:
"f ∈ perms ⟹ MOST x. f x = x"
by (simp add: perms_def) (metis MOST_iff_finiteNeg)
lemma id_perms [simp]:
"id ∈ perms"
"(λx. x) ∈ perms"
by (auto simp: perms_def bij_def)
lemma perms_comp [simp]:
assumes "f ∈ perms" and "g ∈ perms"
shows "(f ∘ g) ∈ perms"
using assms
by (force intro: permsI bij_comp elim: perms_imp_bij MOST_rev_mp [OF perms_imp_MOST_eq])
lemma perms_inv:
assumes "f ∈ perms"
shows "inv f ∈ perms"
using assms
by (force intro: permsI bij_imp_bij_inv MOST_mono [OF perms_imp_MOST_eq]
dest: perms_imp_bij
simp: bij_def inv_f_eq)
lemma bij_Rep_perm:
"bij (Rep_perm p)"
using Rep_perm [of p] by (simp add: perms_def)
lemma finite_Rep_perm:
"finite {x. Rep_perm p x ≠ x}"
using Rep_perm [of p] by (simp add: perms_def)
lemma Rep_perm_ext:
"Rep_perm p1 = Rep_perm p2 ⟹ p1 = p2"
by (simp add: fun_eq_iff Rep_perm_inject [symmetric])
instance perm :: (type) size ..
instantiation perm :: (type) group_add
begin
definition "0 = Abs_perm id"
definition "- p = Abs_perm (inv (Rep_perm p))"
definition "p + q = Abs_perm (Rep_perm p ∘ Rep_perm q)"
definition "(p1::'a perm) - p2 = p1 + - p2"
lemma Rep_perm_0: "Rep_perm 0 = id"
unfolding zero_perm_def by (simp add: Abs_perm_inverse)
lemma Rep_perm_add:
"Rep_perm (p1 + p2) = Rep_perm p1 ∘ Rep_perm p2"
unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
lemma Rep_perm_uminus:
"Rep_perm (- p) = inv (Rep_perm p)"
unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
instance
by standard
(simp_all add: Rep_perm_inject [symmetric] minus_perm_def Rep_perm_add Rep_perm_uminus
Rep_perm_0 o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
end
definition swap :: "'a ⇒ 'a ⇒ 'a perm" ("'(_ ⇌ _')")
where
"(x ⇌ y) = Abs_perm (λz. if z = x then y else if z = y then x else z)"
lemma Rep_perm_swap:
"Rep_perm (x ⇌ y) = (λz. if z = x then y else if z = y then x else z)"
by (auto intro!: Abs_perm_inverse permsI simp: bij_def MOST_eq_imp inj_on_def MOST_conj_distrib swap_def)
lemmas Rep_perm_simps =
Rep_perm_0
Rep_perm_add
Rep_perm_uminus
Rep_perm_swap
lemma swap_cancel:
"(x ⇌ y) + (x ⇌ y) = 0"
"(x ⇌ y) + (y ⇌ x) = 0"
by (rule_tac [!] Rep_perm_ext)
(simp add: Rep_perm_simps fun_eq_iff)+
lemma swap_self [simp]:
"(x ⇌ x) = 0"
by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff)
lemma minus_swap [simp]:
"- (a ⇌ b) = (a ⇌ b)"
by (rule minus_unique [OF swap_cancel(1)])
lemma swap_commute:
"(a ⇌ b) = (b ⇌ a)"
by (rule Rep_perm_ext)
(simp add: Rep_perm_swap fun_eq_iff)
lemma swap_triple:
assumes "a ≠ b" and "c ≠ b"
shows "(a ⇌ c) + (b ⇌ c) + (a ⇌ c) = (a ⇌ b)"
using assms
by (rule_tac Rep_perm_ext)
(auto simp add: Rep_perm_simps fun_eq_iff)
section ‹Permutation Types›
ML ‹
structure Equivariance = Named_Thms (
val name = @{binding "eqvt"}
val description = "equivariance rules"
)
›
setup Equivariance.setup
text ‹Infix syntax for @{text PERMUTE} has higher precedence than
addition, but lower than unary minus.›
consts PERMUTE :: "('a :: infinite) perm ⇒ 'b ⇒ 'b" (infixr "∙" 75)
locale permutation_type =
fixes permute :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
assumes permute_zero [simp]: "permute 0 x = x"
and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
begin
adhoc_overloading
PERMUTE permute
text ‹Equivariance.›
definition eqvt :: "'b ⇒ bool"
where
"eqvt x ⟷ (∀p. p ∙ x = x)"
definition unpermute :: "'a perm ⇒ 'b ⇒ 'b"
where
"unpermute p = permute (- p)"
definition variants :: "('b × 'b) set"
where
"variants = {(x, y). ∃π. π ∙ x = y}"
lemma permute_diff [simp]:
shows "(p - q) ∙ x = p ∙ - q ∙ x"
unfolding diff_conv_add_uminus permute_plus by simp
lemma permute_minus_cancel [simp]:
shows "p ∙ - p ∙ x = x"
and "- p ∙ p ∙ x = x"
unfolding permute_plus [symmetric] by simp_all
lemma permute_swap_cancel [simp]:
shows "(a ⇌ b) ∙ (a ⇌ b) ∙ x = x"
unfolding permute_plus [symmetric]
by (simp add: swap_cancel)
lemma permute_swap_cancel2 [simp]:
shows "(a ⇌ b) ∙ (b ⇌ a) ∙ x = x"
unfolding permute_plus [symmetric]
by (simp add: swap_commute)
lemma inj_permute [simp]:
shows "inj (op ∙ p)"
by (rule inj_on_inverseI) (rule permute_minus_cancel)
lemma surj_permute [simp]:
shows "surj (op ∙ p)"
by (rule surjI) (rule permute_minus_cancel)
lemma bij_permute [simp]:
shows "bij (op ∙ p)"
by (rule bijI [OF inj_permute surj_permute])
lemma inv_permute:
shows "inv (op ∙ p) = op ∙ (- p)"
by (rule inv_equality) (simp_all)
lemma permute_minus:
shows "op ∙ (- p) = inv (op ∙ p)"
by (simp add: inv_permute)
lemma permute_eq_iff [simp]:
shows "p ∙ x = p ∙ y ⟷ x = y"
by (rule inj_permute [THEN inj_eq])
lemma variants_refl:
"(x, x) ∈ variants"
proof -
have "0 ∙ x = x" by simp
then have "∃π. π ∙ x = x" ..
then show ?thesis by (auto simp: variants_def)
qed
lemma variants_sym:
assumes "(x, y) ∈ variants"
shows "(y, x) ∈ variants"
proof -
from assms obtain π where "y = π ∙ x" by (auto simp: variants_def)
then have "-π ∙ y = x" by simp
then show ?thesis by (auto simp: variants_def)
qed
lemma variants_trans:
assumes "(x, y) ∈ variants" and "(y, z) ∈ variants"
shows "(x, z) ∈ variants"
proof -
from assms obtain π⇩1 and π⇩2
where "y = π⇩1 ∙ x" and "z = π⇩2 ∙ y" by (auto simp: variants_def)
then have "(π⇩2 + π⇩1) ∙ x = z" by simp
then have "∃π. π ∙ x = z" ..
then show ?thesis by (auto simp: variants_def)
qed
lemma variants_equiv_on_TRS:
"equiv R (variants ∩ R × R)"
by (rule equivI)
(auto simp: refl_on_def sym_def trans_def variants_refl dest: variants_sym variants_trans)
lemma variants_TRS:
"equiv UNIV variants"
by (rule equivI)
(auto simp: refl_on_def sym_def trans_def variants_refl dest: variants_sym variants_trans)
lemma permute_flip: "x = π ∙ y ⟹ y = -π ∙ x" by auto
end
definition permute_atom :: "'a perm ⇒ 'a ⇒ 'a"
where
"permute_atom p a = (Rep_perm p) a"
adhoc_overloading
PERMUTE permute_atom
interpretation atom_pt: permutation_type permute_atom
by standard (simp add: permute_atom_def Rep_perm_simps)+
lemma swap_atom:
"(a ⇌ b) ∙ c = (if c = a then b else if c = b then a else c)"
by (simp add: permute_atom_def Rep_perm_swap)
lemma swap_atom_simps [simp]:
"(a ⇌ b) ∙ a = b"
"(a ⇌ b) ∙ b = a"
"c ≠ a ⟹ c ≠ b ⟹ (a ⇌ b) ∙ c = c"
by (simp_all add: swap_atom)
lemma perm_eq_iff:
shows "p = q ⟷ (∀a. p ∙ a = q ∙ a)"
unfolding permute_atom_def
by (metis Rep_perm_ext ext)
definition permute_perm :: "'a perm ⇒ 'a perm ⇒ 'a perm"
where
"permute_perm p q = p + q + - p"
adhoc_overloading
PERMUTE permute_perm
interpretation perm_pt: permutation_type permute_perm
by standard
(simp_all add: permute_perm_def minus_add, simp only: diff_conv_add_uminus add.assoc)
lemma permute_self:
shows "p ∙ p = p"
by (simp add: permute_perm_def add.assoc)
lemma pemute_minus_self:
shows "(-p) ∙ p = p"
by (simp add: add.assoc permute_perm_def)
lemma (in permutation_type) permute_eqvt:
fixes x :: "'b"
shows "p ∙ (q ∙ x) = (p ∙ q) ∙ (p ∙ x)"
by (simp add: permute_perm_def)
lemma zero_perm_eqvt [eqvt]:
shows "p ∙ (0 :: ('a :: infinite) perm) = 0"
by (simp add: permute_perm_def)
lemma add_perm_eqvt [eqvt]:
fixes p p1 p2 :: "('a :: infinite) perm"
shows "p ∙ (p1 + p2) = p ∙ p1 + p ∙ p2"
by (simp add: permute_perm_def perm_eq_iff)
locale fun_pt =
dom: permutation_type perm1 + ran: permutation_type perm2
for perm1 :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
and perm2 :: "'a perm ⇒ 'c ⇒ 'c"
begin
adhoc_overloading
PERMUTE perm1 perm2
definition permute_fun :: "'a perm ⇒ ('b ⇒ 'c) ⇒ ('b ⇒ 'c)"
where
"permute_fun p f = (λx. p ∙ (f (-p ∙ x)))"
adhoc_overloading
PERMUTE permute_fun
end
sublocale fun_pt ⊆ permutation_type permute_fun
by standard (auto simp: permute_fun_def, metis dom.permute_plus minus_add)
locale fun_comp_pt =
a: fun_pt pa pb +
b: fun_pt pb pc +
c: fun_pt pa pc
for pa :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
and pb :: "'a perm ⇒ 'c ⇒ 'c"
and pc :: "'a perm ⇒ 'd ⇒ 'd"
begin
adhoc_overloading
PERMUTE pa pb pc a.permute_fun b.permute_fun c.permute_fun
lemma comp_eqvt':
fixes g :: "'b ⇒ 'c" and f :: "'c ⇒ 'd"
shows "p ∙ (λx. f (g x)) = (λx. (p ∙ f) ((p ∙ g) x))"
by (simp add: a.permute_fun_def b.permute_fun_def c.permute_fun_def)
lemma comp_eqvt [eqvt]:
fixes g :: "'b ⇒ 'c" and f :: "'c ⇒ 'd"
shows "p ∙ (f ∘ g) = (p ∙ f) ∘ (p ∙ g)"
by (simp add: comp_def comp_eqvt')
end
context fun_pt
begin
lemma apply_eqvt:
fixes f :: "'b ⇒ 'c" and x :: "'b"
shows "p ∙ (f x) = (p ∙ f) (p ∙ x)"
by (simp add: permute_fun_def)
lemma lambda_eqvt:
fixes p :: "('a::infinite) perm" and f :: "'b ⇒ 'c"
shows "p ∙ f = (λx. p ∙ (f (dom.unpermute p x)))"
by (simp add: permute_fun_def dom.unpermute_def)
lemma unpermute_self:
"p ∙ unpermute p x = x"
by (simp add: unpermute_def)
lemma permute_fun_comp:
fixes p :: "'a perm"
shows "p ∙ f = (op ∙ p) o f o (op ∙ (-p))"
by (simp add: comp_def permute_fun_def)
end
definition permute_bool :: "'a perm ⇒ bool ⇒ bool" where
"permute_bool p b = b"
adhoc_overloading
PERMUTE permute_bool
interpretation bool_pt: permutation_type permute_bool
by standard (simp add: permute_bool_def)+
lemma permute_boolE:
fixes p :: "('a :: infinite) perm"
shows "p ∙ P ⟹ P"
by (simp add: permute_bool_def)
lemma permute_boolI:
fixes p :: "('a :: infinite) perm"
shows "P ⟹ p ∙ P"
by (simp add: permute_bool_def)
lemma Not_eqvt [eqvt]:
"p ∙ (¬ A) ⟷ ¬ (p ∙ A)"
by (simp add: permute_bool_def)
lemma conj_eqvt [eqvt]:
"p ∙ (A ∧ B) ⟷ (p ∙ A) ∧ (p ∙ B)"
by (simp add: permute_bool_def)
lemma imp_eqvt [eqvt]:
"p ∙ (A ⟶ B) ⟷ (p ∙ A) ⟶ (p ∙ B)"
by (simp add: permute_bool_def)
lemmas
True_eqvt [eqvt] = permute_bool_def [of _ True] and
False_eqvt [eqvt] = permute_bool_def [of _ False]
lemma disj_eqvt [eqvt]:
"p ∙ (A ∨ B) ⟷ (p ∙ A) ∨ (p ∙ B)"
by (simp add: permute_bool_def)
locale pred_pt =
arg: permutation_type perm
for perm :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
begin
definition
permute_pred :: "('a::infinite) perm ⇒ ('b ⇒ bool) ⇒ ('b ⇒ bool)"
where
"permute_pred p P = (λx. P (perm (-p) x))"
end
sublocale pred_pt ⊆ fun_pt perm permute_bool
rewrites "permute_fun = permute_pred"
proof -
show *: "fun_pt perm permute_bool" ..
show "fun_pt.permute_fun perm permute_bool = permute_pred"
unfolding fun_pt.permute_fun_def [OF *, abs_def] permute_bool_def permute_pred_def [abs_def]
..
qed
definition permute_atom_pred :: "('a :: infinite) perm ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" where
"permute_atom_pred p P = (λx. P (-p ∙ x))"
adhoc_overloading
PERMUTE permute_atom_pred
interpretation atom_pred_pt: pred_pt permute_atom
rewrites "pred_pt.permute_pred permute_atom = permute_atom_pred"
proof -
show *: "pred_pt permute_atom" ..
show "pred_pt.permute_pred permute_atom = permute_atom_pred"
by (simp add: permute_atom_pred_def [abs_def] pred_pt.permute_pred_def [OF *, abs_def])
qed
context permutation_type
begin
interpretation pred: pred_pt permute ..
adhoc_overloading
PERMUTE pred.permute_pred
lemma eq_eqvt [eqvt]:
fixes x :: "'b"
shows "p ∙ (x = y) ⟷ (p ∙ x) = (p ∙ y)"
unfolding permute_eq_iff permute_bool_def ..
lemma all_eqvt [eqvt]:
fixes P :: "'b ⇒ bool"
shows "p ∙ (∀x. P x) = (∀x. (p ∙ P) x)"
unfolding pred.permute_pred_def permute_bool_def
by (metis permute_plus permute_zero right_minus)
lemma all_eqvt':
fixes P :: "'c ⇒ bool"
shows "p ∙ (∀x. P x) = (∀x. p ∙ (P x))"
by (simp add: permute_bool_def)
lemma ball_eqvt':
fixes P :: "'c ⇒ bool"
shows "p ∙ (∀x∈A. P x) = (∀x∈A. p ∙ (P x))"
by (simp add: permute_bool_def)
lemma ex_eqvt [eqvt]:
fixes P :: "'b ⇒ bool"
shows "p ∙ (∃x. P x) = (∃x. (p ∙ P) x)"
unfolding Ex_def pred.permute_pred_def permute_bool_def
by (simp) (metis permute_minus_cancel(2))
lemma ex1_eqvt [eqvt]:
fixes P :: "'b ⇒ bool"
shows "p ∙ (∃!x. P x) = (∃!x. (p ∙ P) x)"
unfolding Ex1_def pred_pt.permute_pred_def
by (simp add: eqvt pred.permute_pred_def)
(metis permute_minus_cancel(2))
lemma if_eqvt [eqvt]:
fixes x :: "'b"
shows "p ∙ (if b then x else y) = (if p ∙ b then p ∙ x else p ∙ y)"
by (simp add: pred_pt.permute_pred_def permute_bool_def)
lemma all_eqvt2:
fixes P :: "'b ⇒ bool"
shows "p ∙ (∀x. P x) = (∀x. p ∙ P (- p ∙ x))"
by (simp add: eqvt pred.permute_pred_def)
(metis permute_bool_def)
lemma ex_eqvt2:
fixes P :: "'b ⇒ bool"
shows "p ∙ (∃x. P x) = (∃x. p ∙ P (- p ∙ x))"
by (simp add: eqvt pred.permute_pred_def)
(metis permute_bool_def)
lemma ex1_eqvt2:
fixes P :: "'b ⇒ bool"
shows "p ∙ (∃!x. P x) = (∃!x. p ∙ P (- p ∙ x))"
by (simp add: eqvt pred.permute_pred_def)
(metis permute_bool_def)
end
locale set_pt =
elt: permutation_type perm for perm :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
begin
adhoc_overloading
PERMUTE perm
definition permute_set :: "'a perm ⇒ 'b set ⇒ 'b set"
where
"permute_set p A = {p ∙ x | x. x ∈ A}"
adhoc_overloading
PERMUTE permute_set
lemma permute_set_subset:
fixes π :: "('a :: infinite) perm"
and A :: "'b set"
assumes "A ⊆ B"
shows "π ∙ A ⊆ π ∙ B"
using assms by (auto simp: permute_set_def)
lemma subset_imp_ex_perm:
fixes A :: "'b set"
assumes "A ⊆ B"
shows "∀x ∈ A. ∃p. ∃y ∈ B. p ∙ x = y"
using assms by (auto) (metis elt.permute_zero set_rev_mp)
end
sublocale set_pt ⊆ permutation_type permute_set
by standard (auto simp: permute_set_def)
context set_pt
begin
lemma permute_set_eq:
"p ∙ X = {x. - p ∙ x ∈ X}"
by (auto simp: permute_set_def) (metis elt.permute_minus_cancel(1))
lemma permute_set_eq_image:
"p ∙ X = op ∙ p ` X"
by (auto simp: permute_set_def)
lemma permute_set_eq_vimage:
"p ∙ X = op ∙ (- p) -` X"
by (simp add: permute_set_eq vimage_def)
lemma permute_finite [simp]:
"finite (p ∙ X) = finite X"
unfolding permute_set_eq_vimage
using bij_permute by (metis elt.bij_permute finite_vimage_iff)
lemma mem_permute_iff:
fixes p :: "'a perm"
shows "(p ∙ x) ∈ (p ∙ X) ⟷ x ∈ X"
by (auto simp: permute_set_def)
lemma inv_mem_simps [simp]:
fixes p :: "'a perm"
shows "(-p ∙ x) ∈ X ⟷ x ∈ (p ∙ X)"
and "x ∈ (-p ∙ X) ⟷ (p ∙ x) ∈ X"
by (metis permute_minus_cancel(2) mem_permute_iff)+
lemma empty_eqvt [simp]:
"p ∙ {} = {}"
by (simp add: permute_set_def)
lemma permute_set_emptyD [dest]:
"p ∙ A = {} ⟹ A = {}"
by (simp add: permute_set_def)
lemma insert_eqvt [eqvt]:
"p ∙ (insert x A) = insert (p ∙ x) (p ∙ A)"
unfolding permute_set_eq_image image_insert ..
lemma mem_eqvt [eqvt]:
shows "p ∙ (x ∈ A) ⟷ (p ∙ x) ∈ (p ∙ A)"
unfolding permute_bool_def permute_set_def
by (simp add: eqvt)
interpretation elt_pred_pt: pred_pt perm ..
adhoc_overloading
PERMUTE elt_pred_pt.permute_pred
lemma Collect_eqvt [eqvt]:
"p ∙ {x. P x} = {x. (p ∙ P) x}"
by (simp add: permute_set_eq elt_pred_pt.permute_pred_def)
lemma inter_eqvt [eqvt]:
"p ∙ (A ∩ B) = (p ∙ A) ∩ (p ∙ B)"
unfolding Int_def permute_set_eq by simp
lemma Bex_eqvt [eqvt]:
"p ∙ (∃x ∈ S. P x) = (∃x ∈ (p ∙ S). (p ∙ P) x)"
by (simp add: Bex_def pred_pt.permute_pred_def eqvt elt_pred_pt.permute_pred_def permute_set_def)
lemma Ball_eqvt [eqvt]:
"p ∙ (∀x ∈ S. P x) = (∀x ∈ (p ∙ S). (p ∙ P) x)"
by (simp add: Ball_def eqvt permute_set_def elt_pred_pt.permute_pred_def)
lemma UNIV_eqvt [eqvt]:
"p ∙ UNIV = UNIV"
unfolding UNIV_def by (auto simp add: permute_set_def) (metis elt.permute_minus_cancel(1))
lemma union_eqvt [eqvt]:
"p ∙ (A ∪ B) = (p ∙ A) ∪ (p ∙ B)"
by (auto simp: Un_def permute_set_def)
lemma Union_eqvt [eqvt]:
"p ∙ ⋃A = ⋃(op ∙ p ` A)"
by (auto simp: permute_set_def)
lemma UNION_eqvt [eqvt]:
"p ∙ UNION A f = UNION A (λx. p ∙ f x)"
by (auto simp: permute_set_def)
lemma Diff_eqvt [eqvt]:
fixes A B :: "'b set"
shows "p ∙ (A - B) = (p ∙ A) - (p ∙ B)"
by (auto simp: set_diff_eq permute_set_def)
lemma Compl_eqvt [eqvt]:
fixes A :: "'b set"
shows "p ∙ (- A) = - (p ∙ A)"
by (auto simp: permute_set_def Compl_eq_Diff_UNIV)
(metis elt.permute_minus_cancel(1))
lemma subset_eqvt [eqvt]:
"p ∙ (S ⊆ T) ⟷ (p ∙ S) ⊆ (p ∙ T)"
by (simp add: subset_eq eqvt elt_pred_pt.permute_pred_def)
lemma psubset_eqvt [eqvt]:
"p ∙ (S ⊂ T) ⟷ (p ∙ S) ⊂ (p ∙ T)"
by (simp add: psubset_eq eqvt)
end
definition permute_atom_set :: "('a :: infinite) perm ⇒ 'a set ⇒ 'a set"
where
"permute_atom_set p A = {p ∙ x | x. x ∈ A}"
adhoc_overloading
PERMUTE permute_atom_set
interpretation atom_set_pt: set_pt permute_atom
rewrites "set_pt.permute_set permute_atom = permute_atom_set"
and "pred_pt.permute_pred permute_atom = permute_atom_pred"
proof -
show *: "set_pt permute_atom" ..
show "set_pt.permute_set permute_atom = permute_atom_set"
by (simp add: permute_atom_set_def [abs_def] set_pt.permute_set_def [OF *, abs_def])
have **: "pred_pt permute_atom" ..
show "pred_pt.permute_pred permute_atom = permute_atom_pred"
by (simp add: permute_atom_pred_def [abs_def] pred_pt.permute_pred_def [OF **, abs_def])
qed
lemma swap_set_not_in:
assumes "a ∉ S" "b ∉ S"
shows "(a ⇌ b) ∙ S = S"
using assms by (auto simp: permute_atom_set_def swap_atom)
lemma swap_set_in:
assumes "a ∈ S" "b ∉ S"
shows "(a ⇌ b) ∙ S ≠ S"
using assms by (force simp: permute_atom_set_def swap_atom)
lemma swap_set_in_eq:
assumes "a ∈ S" "b ∉ S"
shows "(a ⇌ b) ∙ S = (S - {a}) ∪ {b}"
using assms by (auto simp: permute_atom_set_def swap_atom)
lemma swap_set_both_in:
assumes "a ∈ S" "b ∈ S"
shows "(a ⇌ b) ∙ S = S"
using assms by (auto simp add: permute_atom_set_def swap_atom) metis
definition permute_unit :: "'a perm ⇒ unit ⇒ unit"
where
"permute_unit p (u :: unit) = u"
interpretation unit_pt: permutation_type permute_unit
by standard (simp add: permute_unit_def)+
adhoc_overloading
PERMUTE permute_unit
locale prod_pt =
fst: permutation_type perm1 + snd: permutation_type perm2
for perm1 :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
and perm2 :: "'a perm ⇒ 'c ⇒ 'c"
begin
adhoc_overloading
PERMUTE perm1 perm2
fun permute_prod :: "'a perm ⇒ ('b × 'c) ⇒ ('b × 'c)"
where
permute_prod_eqvt [eqvt]: "permute_prod p (x, y) = (p ∙ x, p ∙ y)"
adhoc_overloading
PERMUTE permute_prod
declare permute_prod.simps [simp del]
end
sublocale prod_pt ⊆ permutation_type permute_prod
by standard (auto simp: eqvt)
locale sum_pt =
l: permutation_type perm1 + r: permutation_type perm2
for perm1 :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
and perm2 :: "'a perm ⇒ 'c ⇒ 'c"
begin
adhoc_overloading
PERMUTE perm1 perm2
fun permute_sum :: "'a perm ⇒ ('b + 'c) ⇒ ('b + 'c)"
where
"permute_sum p (Inl x) = Inl (p ∙ x)" |
"permute_sum p (Inr y) = Inr (p ∙ y)"
adhoc_overloading
PERMUTE permute_sum
end
sublocale sum_pt ⊆ permutation_type permute_sum
by (standard, case_tac [!] x) (simp)+
locale list_pt =
elt: permutation_type perm for perm :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
begin
adhoc_overloading
PERMUTE perm
definition permute_list :: "'a perm ⇒ 'b list ⇒ 'b list"
where
[simp]: "permute_list p = map (λx. p ∙ x)"
adhoc_overloading
PERMUTE permute_list
lemma nth_eqvt:
"i < length xs ⟹ π ∙ (xs ! i) = (π ∙ xs) ! i"
by simp
end
sublocale list_pt ⊆ permutation_type permute_list
by (standard, induct_tac [!] x) (simp)+
locale option_pt =
elt: permutation_type perm for perm :: "('a :: infinite) perm ⇒ 'b ⇒ 'b"
begin
adhoc_overloading
PERMUTE perm
fun permute_option :: "'a perm ⇒ 'b option ⇒ 'b option"
where
"permute_option p None = None" |
"permute_option p (Some x) = Some (p ∙ x)"
adhoc_overloading
PERMUTE permute_option
end
sublocale option_pt ⊆ permutation_type permute_option
by (standard, case_tac [!] x) (simp)+
locale rel_pt =
step: prod_pt perm perm for perm :: "('a :: infinite perm) ⇒ 'b ⇒ 'b"
begin
adhoc_overloading
PERMUTE perm step.permute_prod
interpretation set_pt step.permute_prod
by (standard) (case_tac [!] x, auto simp: step.permute_prod.simps)
adhoc_overloading
PERMUTE permute_set
end
sublocale rel_pt ⊆ set_pt step.permute_prod ..
context rel_pt
begin
lemma relcomp_eqvt:
fixes R S :: "'b rel"
assumes "⋀p. p ∙ R = R" and "⋀p. p ∙ S = S"
shows "p ∙ (R O S) = R O S"
proof -
interpret step_pred: pred_pt step.permute_prod ..
{ fix a b x y z assume "-p ∙ (a, b) = (x, z)" and "(a, y) ∈ R" and "(y, b) ∈ S"
moreover then have "-p ∙ (a, y) ∈ R" and "-p ∙ (y, b) ∈ S"
by (simp_all, auto simp: eqvt assms)
ultimately have "(x, -p ∙ y) ∈ R" and "(-p ∙ y, z) ∈ S" by (auto simp: eqvt)
then have "∃y. (x, y) ∈ R ∧ (y, z) ∈ S" by blast }
moreover
{ fix a b x y z assume "- p ∙ (a, b) = (x, z)" and "(x, y) ∈ R" and "(y, z) ∈ S"
moreover then have "p ∙ (x, y) ∈ R" and "p ∙ (y, z) ∈ S"
by (auto simp: inv_mem_simps [symmetric] assms)
ultimately have "(a, p ∙ y) ∈ R" and "(p ∙ y, b) ∈ S" by (auto simp: eqvt)
then have "∃y. (a, y) ∈ R ∧ (y, b) ∈ S" by blast }
moreover have "R O S = {(x, z). ∃y. (x, y) ∈ R ∧ (y, z) ∈ S}" by auto
ultimately have "p ∙ (R O S) = {(x, z). ∃y. p ∙ ((x, y) ∈ R) ∧ p ∙ ((y, z) ∈ S)}"
using [[show_variants]]
by (auto simp: eqvt step_pred.permute_pred_def mem_permute_iff simp del: step.permute_prod_eqvt)
then show ?thesis by (auto simp: permute_bool_def)
qed
end
section ‹Pure Types›
locale pure =
permutation_type permute for permute :: "('a :: infinite) perm ⇒ 'b ⇒ 'b" +
assumes permute_pure [simp]: "(p :: 'a perm) ∙ (x :: 'b) = x"
interpretation unit_pure: pure permute_unit
by standard (simp add: permute_unit_def)
interpretation bool_pure: pure permute_bool
by standard (simp add: permute_bool_def)
lemma (in fun_pt) eqvt_fun_iff:
"eqvt f ⟷ (∀(p :: 'a perm) x. p ∙ (f x) = f (p ∙ x))"
by (auto simp add: eqvt_def permute_fun_def)
(metis dom.unpermute_def apply_eqvt lambda_eqvt)
lemma bool_pt_eqvt [simp]:
"bool_pt.eqvt TYPE('a :: infinite) x"
by (simp add: bool_pt.eqvt_def permute_bool_def)
lemma swap_eqvt [eqvt]:
fixes p :: "('a :: infinite) perm"
shows "p ∙ (a ⇌ b) = (p ∙ a ⇌ p ∙ b)"
by (auto simp add: permute_perm_def swap_atom perm_eq_iff)
consts
FRESH :: "'a ⇒ 'b ⇒ bool" (infix "♯" 55)
context permutation_type
begin
text ‹The support of @{term x} (aka, the set of free variables, provided we have infinitely many
atoms at our disposal).›
definition supp :: "'b ⇒ 'a set"
where
"supp x = {a. infinite {b. (a ⇌ b) ∙ x ≠ x}}"
definition fresh :: "'a ⇒ 'b ⇒ bool"
where
"fresh a x ⟷ a ∉ supp x"
adhoc_overloading
FRESH fresh
definition fresh_set :: "'a set ⇒ 'b ⇒ bool"
where
"fresh_set A x ⟷ (∀a ∈ A. a ♯ x)"
adhoc_overloading
FRESH fresh_set
definition supports :: "'a set ⇒ 'b ⇒ bool"
where
"supports S x ⟷ (∀a b. (a ∉ S ∧ b ∉ S ⟶ (a ⇌ b) ∙ x = x))"
lemma fresh_set_disjoint:
assumes "A ♯ x"
shows "A ∩ supp x = {}"
using assms unfolding fresh_set_def fresh_def
by (metis disjoint_iff_not_equal)
lemma supp_is_subset:
fixes S :: "'a set"
and x :: "'b"
assumes a1: "supports S x"
and a2: "finite S"
shows "supp x ⊆ S"
proof (rule ccontr)
assume "¬ (supp x ⊆ S)"
then obtain a where b1: "a ∈ supp x" and b2: "a ∉ S" by auto
from a1 b2 have "∀b. b ∉ S ⟶ (a ⇌ b) ∙ x = x" unfolding supports_def by auto
then have "{b. (a ⇌ b) ∙ x ≠ x} ⊆ S" by auto
with a2 have "finite {b. (a ⇌ b) ∙ x ≠ x}" by (simp add: finite_subset)
then have "a ∉ (supp x)" unfolding supp_def by simp
with b1 show False by simp
qed
lemma supp_conv_fresh:
"supp x = {a. ¬ a ♯ x}"
by (simp add: fresh_def)
lemma swap_rel_trans:
fixes a b c :: "'a" and x :: "'b"
assumes "(a ⇌ c) ∙ x = x" and "(b ⇌ c) ∙ x = x"
shows "(a ⇌ b) ∙ x = x"
proof (cases)
assume "a = b ∨ c = b"
with assms show "(a ⇌ b) ∙ x = x" by auto
next
assume *: "¬ (a = b ∨ c = b)"
have "((a ⇌ c) + (b ⇌ c) + (a ⇌ c)) ∙ x = x"
using assms by simp
also have "(a ⇌ c) + (b ⇌ c) + (a ⇌ c) = (a ⇌ b)"
using assms * by (simp add: swap_triple)
finally show "(a ⇌ b) ∙ x = x" .
qed
lemma obtain_atom:
fixes X :: "'a set"
assumes X: "finite X"
obtains a where "a ∉ X"
proof -
from X have "MOST a. a ∉ X"
unfolding MOST_iff_cofinite by simp
then have "INFM a. a ∉ X" using infinite_UNIV and X by (metis Collect_mem_eq INFM_iff_infinite finite_Collect_not)
then obtain a where "a ∉ X"
by (auto elim: INFM_E)
then show ?thesis ..
qed
lemma swap_fresh_fresh:
assumes a: "a ♯ x" and b: "b ♯ x"
shows "(a ⇌ b) ∙ x = x"
proof -
have "finite {c. (a ⇌ c) ∙ x ≠ x}" "finite {c. (b ⇌ c) ∙ x ≠ x}"
using a b unfolding fresh_def supp_def by simp_all
then have "finite ({c. (a ⇌ c) ∙ x ≠ x} ∪ {c. (b ⇌ c) ∙ x ≠ x})" by simp
then obtain c
where "(a ⇌ c) ∙ x = x" "(b ⇌ c) ∙ x = x"
by (rule obtain_atom) (auto)
then show "(a ⇌ b) ∙ x = x" by (rule swap_rel_trans)
qed
text ‹The notion of support does not make sense for a finite set of atoms.›
lemma supp_empty:
assumes "finite (UNIV :: 'a set)"
shows "supp x = {}"
using assms by (auto simp: supp_def) (metis rev_finite_subset top_greatest)
lemma fresh_ex:
assumes "finite (supp x)"
shows "∃a::'a. a ♯ x"
using ex_new_if_finite [OF infinite_UNIV assms] by (simp add: fresh_def)
lemma fresh_set_supp_conv:
shows "supp x ♯ y ⟹ supp y ♯ x"
by (auto simp add: fresh_set_def fresh_def)
lemma supp_supports:
fixes x :: "'b"
shows "supports (supp x) x"
unfolding supports_def
proof (intro strip)
fix a b
assume "a ∉ (supp x) ∧ b ∉ (supp x)"
then have "a ♯ x" and "b ♯ x" by (simp_all add: fresh_def)
then show "(a ⇌ b) ∙ x = x" by (simp add: swap_fresh_fresh)
qed
lemma supp_is_least_supports:
fixes S :: "'a set"
and x :: "'b"
assumes a1: "supports S x"
and a2: "finite S"
and a3: "⋀S'. finite S' ⟹ supports S' x ⟹ S ⊆ S'"
shows "(supp x) = S"
proof (rule equalityI)
show "(supp x) ⊆ S" using a1 a2 by (rule supp_is_subset)
with a2 have fin: "finite (supp x)" by (rule rev_finite_subset)
have "supports (supp x) x" by (rule supp_supports)
with fin a3 show "S ⊆ supp x" by blast
qed
lemma subsetCI:
"(⋀x. x ∈ A ⟹ x ∉ B ⟹ False) ⟹ A ⊆ B" by auto
lemma finite_supp_unique:
assumes a1: "supports S x"
assumes a2: "finite S"
assumes a3: "⋀a b. ⟦a ∈ S; b ∉ S⟧ ⟹ (a ⇌ b) ∙ x ≠ x"
shows "supp x = S"
using a1 a2
proof (rule supp_is_least_supports)
fix S'
assume "finite S'" and "supports S' x"
show "S ⊆ S'"
proof (rule subsetCI)
fix a
assume "a ∈ S" and "a ∉ S'"
have "finite (S ∪ S')"
using ‹finite S› ‹finite S'› by simp
then obtain b where "b ∉ S ∪ S'" by (rule obtain_atom)
then have "b ∉ S" and "b ∉ S'" by simp_all
then have "(a ⇌ b) ∙ x = x"
using ‹a ∉ S'› ‹supports S' x› by (simp add: supports_def)
moreover have "(a ⇌ b) ∙ x ≠ x"
using ‹a ∈ S› ‹b ∉ S› by (rule a3)
ultimately show "False" by simp
qed
qed
end
lemma perm_swap_eq:
"(a ⇌ b) ∙ p = p ⟷ (p ∙ (a ⇌ b)) = (a ⇌ b)"
unfolding permute_perm_def by (metis add_diff_cancel minus_perm_def)
lemma supports_perm:
"perm_pt.supports {a. p ∙ a ≠ a} p"
by (simp add: perm_pt.supports_def perm_swap_eq eqvt)
lemma finite_perm_lemma:
fixes p :: "('a::infinite) perm"
shows "finite {a :: 'a. p ∙ a ≠ a}"
using finite_Rep_perm [of p]
unfolding permute_atom_def .
lemma supp_perm:
"perm_pt.supp p = {a. p ∙ a ≠ a}"
apply (intro perm_pt.finite_supp_unique supports_perm finite_perm_lemma)
apply (simp add: perm_swap_eq)
apply (auto simp: perm_eq_iff swap_atom eqvt)
done
lemma supp_swap:
"perm_pt.supp (a ⇌ b) = (if a = b then {} else {a, b})"
by (auto simp add: supp_perm swap_atom)
lemma supp_zero_perm:
"perm_pt.supp 0 = {}"
by (simp add: supp_perm)
lemma finite_supp_perm:
"finite (perm_pt.supp p)"
by (metis finite_perm_lemma supp_perm)
lemma plus_perm_eq:
assumes "perm_pt.supp p ∩ perm_pt.supp q = {}"
shows "p + q = q + p"
unfolding perm_eq_iff
proof
fix a :: "'a"
show "(p + q) ∙ a = (q + p) ∙ a"
proof -
{ assume "a ∉ perm_pt.supp p" "a ∉ perm_pt.supp q"
then have "(p + q) ∙ a = (q + p) ∙ a"
by (simp add: supp_perm)
}
moreover
{ assume a: "a ∈ perm_pt.supp p" "a ∉ perm_pt.supp q"
then have "p ∙ a ∈ perm_pt.supp p" by (simp add: supp_perm)
then have "p ∙ a ∉ perm_pt.supp q" using assms by auto
with a have "(p + q) ∙ a = (q + p) ∙ a"
by (simp add: supp_perm)
}
moreover
{ assume a: "a ∉ perm_pt.supp p" "a ∈ perm_pt.supp q"
then have "q ∙ a ∈ perm_pt.supp q" by (simp add: supp_perm)
then have "q ∙ a ∉ perm_pt.supp p" using assms by auto
with a have "(p + q) ∙ a = (q + p) ∙ a"
by (simp add: supp_perm)
}
ultimately show "(p + q) ∙ a = (q + p) ∙ a"
using assms by blast
qed
qed
lemma supp_plus_perm:
"perm_pt.supp (p + q) ⊆ perm_pt.supp p ∪ perm_pt.supp q"
by (auto simp add: supp_perm)
lemma supp_plus_perm_eq:
assumes "perm_pt.supp p ∩ perm_pt.supp q = {}"
shows "perm_pt.supp (p + q) = perm_pt.supp p ∪ perm_pt.supp q"
proof -
{ fix a
assume "a ∈ perm_pt.supp p"
then have "a ∉ perm_pt.supp q" using assms by auto
then have "a ∈ perm_pt.supp (p + q)" using ‹a ∈ perm_pt.supp p›
by (simp add: supp_perm)
}
moreover
{ fix a
assume "a ∈ perm_pt.supp q"
then have "a ∉ perm_pt.supp p" using assms by auto
then have "a ∈ perm_pt.supp (q + p)" using ‹a ∈ perm_pt.supp q›
by (simp add: supp_perm)
then have "a ∈ perm_pt.supp (p + q)" using assms plus_perm_eq
by metis
}
ultimately have "perm_pt.supp p ∪ perm_pt.supp q ⊆ perm_pt.supp (p + q)"
by blast
then show "perm_pt.supp (p + q) = perm_pt.supp p ∪ perm_pt.supp q"
using supp_plus_perm
by blast
qed
lemma atom_set_avoiding_aux:
fixes As Xs :: "('a::infinite) set"
assumes b: "Xs ⊆ As"
and c: "finite As"
shows "∃(p::('a::infinite) perm). (p ∙ Xs) ∩ As = {} ∧ perm_pt.supp p = (Xs ∪ (p ∙ Xs))"
proof -
from b c have "finite Xs" by (rule finite_subset)
then show ?thesis using b
proof (induct rule: finite_subset_induct)
case empty
have "0 ∙ {} ∩ As = {}" by (simp)
moreover
have "perm_pt.supp 0 = {} ∪ 0 ∙ {}" by (simp add: supp_zero_perm)
ultimately show ?case by blast
next
case (insert x Xs)
then obtain p where
p1: "(p ∙ Xs) ∩ As = {}" and
p2: "perm_pt.supp p = (Xs ∪ (p ∙ Xs))" by blast
from ‹x ∈ As› p1 have "x ∉ p ∙ Xs" by fast
with ‹x ∉ Xs› p2 have "x ∉ perm_pt.supp p" by fast
hence px: "p ∙ x = x" unfolding supp_perm by simp
have "finite (As ∪ p ∙ Xs ∪ perm_pt.supp p)"
using ‹finite As› ‹finite Xs›
by (simp add: set_pt.permute_set_eq_image finite_supp_perm)
then obtain y where "y ∉ (As ∪ p ∙ Xs ∪ perm_pt.supp p)"
by (rule atom_set_pt.obtain_atom)
hence y: "y ∉ As" "y ∉ p ∙ Xs" "y ∉ perm_pt.supp p"
by simp_all
hence py: "p ∙ y = y" "x ≠ y" using ‹x ∈ As›
by (auto simp add: supp_perm)
let ?q = "(x ⇌ y) + p"
have q: "?q ∙ insert x Xs = insert y (p ∙ Xs)"
unfolding atom_set_pt.insert_eqvt
using ‹p ∙ x = x›
using ‹x ∉ p ∙ Xs› ‹y ∉ p ∙ Xs›
by (simp add: swap_atom swap_set_not_in)
have "?q ∙ insert x Xs ∩ As = {}"
using ‹y ∉ As› ‹p ∙ Xs ∩ As = {}›
unfolding q by simp
moreover
have "perm_pt.supp (x ⇌ y) ∩ perm_pt.supp p = {}" using px py
unfolding supp_swap by (simp add: supp_perm)
then have "perm_pt.supp ?q = (perm_pt.supp (x ⇌ y) ∪ perm_pt.supp p)"
by (simp add: supp_plus_perm_eq)
then have "perm_pt.supp ?q = insert x Xs ∪ ?q ∙ insert x Xs"
using p2 ‹x ≠ y› unfolding q supp_swap
by auto
ultimately show ?case by blast
qed
qed
lemma (in permutation_type) finite_atom_set_avoiding:
fixes Xs :: "('a::infinite) set"
assumes "finite (supp c)"
and "finite Xs"
obtains p :: "('a::infinite) perm"
where "(p ∙ Xs) ♯ c" and "perm_pt.supp p = (Xs ∪ (p ∙ Xs))"
using assms and atom_set_avoiding_aux [of Xs "Xs ∪ supp c"]
unfolding fresh_set_def fresh_def by blast
lemma (in permutation_type) finite_atom_set_avoidingD:
assumes "finite (supp c)"
and "finite xs"
shows "∃p. (p ∙ xs) ♯ c"
using assms by (elim finite_atom_set_avoiding) auto
lemma (in permutation_type) permute_minus_comp_id [simp]:
fixes π :: "('a::infinite) perm"
shows "(op ∙ (- π)) ∘ (op ∙ π) = (id :: 'b ⇒ 'b)"
by auto
locale finitely_supported = permutation_type +
assumes finite_supp: "finite (supp x)"
begin
lemma atom_set_avoiding:
fixes Xs :: "('a::infinite) set"
assumes "finite Xs"
obtains p :: "('a::infinite) perm"
where "(p ∙ Xs) ♯ c" and "perm_pt.supp p = (Xs ∪ (p ∙ Xs))"
using assms and atom_set_avoiding_aux [of Xs "Xs ∪ supp c"]
and finite_atom_set_avoiding [OF finite_supp] by blast
lemma atom_set_avoidingD:
assumes "finite xs"
shows "∃p. (p ∙ xs) ♯ c"
using assms and finite_atom_set_avoidingD [OF finite_supp] by blast
lemma supp_eqvt [eqvt]:
shows "p ∙ (supp x) = supp (p ∙ x)"
proof -
interpret ap: pred_pt permute_atom ..
interpret asp: pred_pt permute_atom_set ..
interpret bf: fun_pt permute_bool permute_bool ..
have *: "fun_pt.permute_fun op ∙ op ∙ p Not = Not"
by (simp add: bf.permute_fun_def permute_bool_def)
show ?thesis
unfolding supp_def
unfolding atom_set_pt.Collect_eqvt
unfolding atom_pred_pt.lambda_eqvt
unfolding asp.apply_eqvt [of _ infinite]
by (simp add: bf.apply_eqvt * eqvt asp.permute_pred_def permute_eqvt [of p]
atom_pt.unpermute_def atom_pred_pt.lambda_eqvt
del: permute_eq_iff bool_pure.permute_pure)
qed
lemma rename_avoiding:
assumes "finite Xs"
obtains p t' where "t' = p ∙ t" "Xs ∩ supp t' = {}"
proof -
obtain p where 1: "- p ∙ Xs ∩ supp t = {}"
by (metis assms minus_minus atom_set_avoidingD fresh_set_disjoint)
obtain t' where "t' = p ∙ t" by simp
moreover then have "Xs ∩ supp t' = {}"
by (metis 1 atom_set_pt.empty_eqvt atom_set_pt.inter_eqvt atom_set_pt.permute_minus_cancel(1) supp_eqvt)
ultimately show ?thesis ..
qed
text ‹We can always rename finitely supported entities apart.›
lemma supp_fresh_set:
"∃p. supp (p ∙ x) ♯ y"
using atom_set_avoidingD [OF finite_supp]
by (simp add: eqvt)
lemma fresh_eqvt [eqvt]:
fixes a :: "'a"
shows "p ∙ (a ♯ x) = (p ∙ a) ♯ (p ∙ x)"
by (simp add: fresh_def eqvt del: bool_pure.permute_pure)
lemma fresh_permute_iff:
fixes a :: "'a"
shows "(p ∙ a) ♯ (p ∙ x) ⟷ a ♯ x"
by (simp only: fresh_eqvt [symmetric] permute_bool_def)
lemma fresh_permute_left:
fixes a :: "'a"
shows "a ♯ p ∙ x ⟷ (- p ∙ a) ♯ x"
proof
assume "a ♯ p ∙ x"
then have "- p ∙ a ♯ - p ∙ p ∙ x" by (simp only: fresh_permute_iff)
then show "- p ∙ a ♯ x" by simp
next
assume "- p ∙ a ♯ x"
then have "p ∙ - p ∙ a ♯ p ∙ x" by (simp only: fresh_permute_iff)
then show "a ♯ p ∙ x" by simp
qed
end
context list_pt
begin
adhoc_overloading
FRESH fresh elt.fresh
lemma supp_Nil [simp]:
"supp [] = {}"
by (simp add: supp_def)
lemma supp_Cons [simp]:
"supp (x # xs) = elt.supp x ∪ supp xs"
by (simp add: elt.supp_def supp_def Collect_imp_eq Collect_neg_eq)
lemma fresh_Nil [simp]:
"a ♯ []"
by (simp add: fresh_def)
lemma fresh_Cons [iff]:
"a ♯ (x # xs) ⟷ a ♯ x ∧ a ♯ xs"
by (simp add: elt.fresh_def fresh_def)
lemma supp_Union [simp]:
"supp xs = (⋃x∈set xs. elt.supp x)"
by (induct xs) (simp del: permute_list_def)+
end
context prod_pt
begin
lemma supp_Un [simp]:
"supp (x, y) = fst.supp x ∪ snd.supp y"
by (auto simp: supp_def fst.supp_def snd.supp_def eqvt)
lemma fst_eqvt [eqvt]:
"π ∙ (fst p) = fst (π ∙ p)"
by (cases p) (simp add: eqvt)
lemma snd_eqvt [eqvt]:
"π ∙ (snd p) = snd (π ∙ p)"
by (cases p) (simp add: eqvt)
end
end