theory Nominal2_Abs+ −
imports "Nominal2_Base" + −
"Nominal2_Eqvt" + −
"~~/src/HOL/Quotient" + −
"~~/src/HOL/Library/Quotient_List"+ −
"~~/src/HOL/Library/Quotient_Product" + −
begin+ −
+ −
+ −
section {* Abstractions *}+ −
+ −
fun+ −
alpha_set + −
where+ −
alpha_set[simp del]:+ −
"alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow> + −
f x - bs = f y - cs \<and> + −
(f x - bs) \<sharp>* pi \<and> + −
R (pi \<bullet> x) y \<and>+ −
pi \<bullet> bs = cs"+ −
+ −
fun+ −
alpha_res+ −
where+ −
alpha_res[simp del]:+ −
"alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow> + −
f x - bs = f y - cs \<and> + −
(f x - bs) \<sharp>* pi \<and> + −
R (pi \<bullet> x) y"+ −
+ −
fun+ −
alpha_lst+ −
where+ −
alpha_lst[simp del]:+ −
"alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow> + −
f x - set bs = f y - set cs \<and> + −
(f x - set bs) \<sharp>* pi \<and> + −
R (pi \<bullet> x) y \<and>+ −
pi \<bullet> bs = cs"+ −
+ −
lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps+ −
+ −
notation+ −
alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and+ −
alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and+ −
alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) + −
+ −
section {* Mono *}+ −
+ −
lemma [mono]: + −
shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"+ −
and "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"+ −
and "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"+ −
by (case_tac [!] bs, case_tac [!] cs) + −
(auto simp add: le_fun_def le_bool_def alphas)+ −
+ −
section {* Equivariance *}+ −
+ −
lemma alpha_eqvt[eqvt]:+ −
shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (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)" + −
unfolding alphas+ −
unfolding permute_eqvt[symmetric]+ −
unfolding set_eqvt[symmetric]+ −
unfolding permute_fun_app_eq[symmetric]+ −
unfolding Diff_eqvt[symmetric]+ −
by (auto simp add: permute_bool_def fresh_star_permute_iff)+ −
+ −
+ −
section {* Equivalence *}+ −
+ −
lemma alpha_refl:+ −
assumes a: "R x x"+ −
shows "(bs, x) \<approx>set R f 0 (bs, x)"+ −
and "(bs, x) \<approx>res R f 0 (bs, x)"+ −
and "(cs, x) \<approx>lst R f 0 (cs, x)"+ −
using a + −
unfolding alphas+ −
unfolding fresh_star_def+ −
by (simp_all add: fresh_zero_perm)+ −
+ −
lemma alpha_sym:+ −
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"+ −
shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set 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+ −
using a+ −
by (auto simp add: fresh_minus_perm)+ −
+ −
lemma alpha_trans:+ −
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>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set 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)"+ −
using a+ −
unfolding alphas fresh_star_def+ −
by (simp_all add: fresh_plus_perm)+ −
+ −
lemma alpha_sym_eqvt:+ −
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" + −
and b: "p \<bullet> R = R"+ −
shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set 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)"+ −
apply(auto intro!: alpha_sym)+ −
apply(drule_tac [!] a)+ −
apply(rule_tac [!] p="p" in permute_boolE)+ −
apply(perm_simp add: permute_minus_cancel b)+ −
apply(assumption)+ −
apply(perm_simp add: permute_minus_cancel b)+ −
apply(assumption)+ −
apply(perm_simp add: permute_minus_cancel b)+ −
apply(assumption)+ −
done+ −
+ −
lemma alpha_set_trans_eqvt:+ −
assumes b: "(cs, y) \<approx>set R f q (ds, z)"+ −
and a: "(bs, x) \<approx>set R f p (cs, y)" + −
and d: "q \<bullet> R = R"+ −
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"+ −
shows "(bs, x) \<approx>set R f (q + p) (ds, z)"+ −
apply(rule alpha_trans)+ −
defer+ −
apply(rule a)+ −
apply(rule b)+ −
apply(drule c)+ −
apply(rule_tac p="q" in permute_boolE)+ −
apply(perm_simp add: permute_minus_cancel d)+ −
apply(assumption)+ −
apply(rotate_tac -1)+ −
apply(drule_tac p="q" in permute_boolI)+ −
apply(perm_simp add: permute_minus_cancel d)+ −
apply(simp add: permute_eqvt[symmetric])+ −
done+ −
+ −
lemma alpha_res_trans_eqvt:+ −
assumes b: "(cs, y) \<approx>res R f q (ds, z)"+ −
and a: "(bs, x) \<approx>res R f p (cs, y)" + −
and d: "q \<bullet> R = R"+ −
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"+ −
shows "(bs, x) \<approx>res R f (q + p) (ds, z)"+ −
apply(rule alpha_trans)+ −
defer+ −
apply(rule a)+ −
apply(rule b)+ −
apply(drule c)+ −
apply(rule_tac p="q" in permute_boolE)+ −
apply(perm_simp add: permute_minus_cancel d)+ −
apply(assumption)+ −
apply(rotate_tac -1)+ −
apply(drule_tac p="q" in permute_boolI)+ −
apply(perm_simp add: permute_minus_cancel d)+ −
apply(simp add: permute_eqvt[symmetric])+ −
done+ −
+ −
lemma alpha_lst_trans_eqvt:+ −
assumes b: "(cs, y) \<approx>lst R f q (ds, z)"+ −
and a: "(bs, x) \<approx>lst R f p (cs, y)" + −
and d: "q \<bullet> R = R"+ −
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"+ −
shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"+ −
apply(rule alpha_trans)+ −
defer+ −
apply(rule a)+ −
apply(rule b)+ −
apply(drule c)+ −
apply(rule_tac p="q" in permute_boolE)+ −
apply(perm_simp add: permute_minus_cancel d)+ −
apply(assumption)+ −
apply(rotate_tac -1)+ −
apply(drule_tac p="q" in permute_boolI)+ −
apply(perm_simp add: permute_minus_cancel d)+ −
apply(simp add: permute_eqvt[symmetric])+ −
done+ −
+ −
lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt+ −
+ −
+ −
section {* General Abstractions *}+ −
+ −
fun+ −
alpha_abs_set + −
where+ −
[simp del]:+ −
"alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"+ −
+ −
fun+ −
alpha_abs_lst+ −
where+ −
[simp del]:+ −
"alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"+ −
+ −
fun+ −
alpha_abs_res+ −
where+ −
[simp del]:+ −
"alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"+ −
+ −
notation+ −
alpha_abs_set (infix "\<approx>abs'_set" 50) and+ −
alpha_abs_lst (infix "\<approx>abs'_lst" 50) and+ −
alpha_abs_res (infix "\<approx>abs'_res" 50)+ −
+ −
lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps+ −
+ −
+ −
lemma alphas_abs_refl:+ −
shows "(bs, x) \<approx>abs_set (bs, x)"+ −
and "(bs, x) \<approx>abs_res (bs, x)"+ −
and "(cs, x) \<approx>abs_lst (cs, x)" + −
unfolding alphas_abs+ −
unfolding alphas+ −
unfolding fresh_star_def+ −
by (rule_tac [!] x="0" in exI)+ −
(simp_all add: fresh_zero_perm)+ −
+ −
lemma alphas_abs_sym:+ −
shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"+ −
and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"+ −
and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"+ −
unfolding alphas_abs+ −
unfolding alphas+ −
unfolding fresh_star_def+ −
by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)+ −
(auto simp add: fresh_minus_perm)+ −
+ −
lemma alphas_abs_trans:+ −
shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"+ −
and "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"+ −
and "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"+ −
unfolding alphas_abs+ −
unfolding alphas+ −
unfolding fresh_star_def+ −
apply(erule_tac [!] exE, erule_tac [!] exE)+ −
apply(rule_tac [!] x="pa + p" in exI)+ −
by (simp_all add: fresh_plus_perm)+ −
+ −
lemma alphas_abs_eqvt:+ −
shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_set (p \<bullet> cs, p \<bullet> y)"+ −
and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"+ −
and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"+ −
unfolding alphas_abs+ −
unfolding alphas+ −
unfolding set_eqvt[symmetric]+ −
unfolding supp_eqvt[symmetric]+ −
unfolding Diff_eqvt[symmetric]+ −
apply(erule_tac [!] exE)+ −
apply(rule_tac [!] x="p \<bullet> pa" in exI)+ −
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])+ −
+ −
+ −
section {* Strengthening the equivalence *}+ −
+ −
lemma disjoint_right_eq:+ −
assumes a: "A \<union> B1 = A \<union> B2"+ −
and b: "A \<inter> B1 = {}" "A \<inter> B2 = {}"+ −
shows "B1 = B2"+ −
using a b+ −
by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2)+ −
+ −
lemma supp_property_res:+ −
assumes a: "(as, x) \<approx>res (op =) supp p (as', x')"+ −
shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"+ −
proof -+ −
from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas)+ −
then have *: "p \<bullet> (supp x - as) = (supp x - as)" + −
by (simp add: atom_set_perm_eq)+ −
have "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto+ −
also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas)+ −
also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt)+ −
also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto+ −
also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt)+ −
also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp+ −
also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas)+ −
finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" .+ −
moreover + −
have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto+ −
moreover + −
have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto+ −
then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def)+ −
then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp)+ −
then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp+ −
then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas)+ −
ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"+ −
by (auto dest: disjoint_right_eq)+ −
qed + −
+ −
lemma alpha_abs_res_stronger1_aux:+ −
assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"+ −
shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" + −
proof -+ −
from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas)+ −
then have #: "p' \<bullet> (supp x - as) = (supp x - as)" + −
by (simp add: atom_set_perm_eq)+ −
obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"+ −
using set_renaming_perm2 by blast+ −
from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto+ −
from 0 have 1: "(supp x - as) \<sharp>* p" using *+ −
by (auto simp add: fresh_star_def fresh_perm)+ −
then have 2: "(supp x - as) \<inter> supp p = {}"+ −
by (auto simp add: fresh_star_def fresh_def)+ −
have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto+ −
have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))" + −
using b by simp+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as)))"+ −
by (simp add: union_eqvt)+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> (supp x \<inter> as))" + −
using # by auto+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using asm+ −
by (simp add: supp_property_res)+ −
finally have "supp p \<subseteq> (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" .+ −
then + −
have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto+ −
moreover + −
have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas)+ −
ultimately + −
show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast+ −
qed+ −
+ −
lemma alpha_abs_res_stronger1:+ −
assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"+ −
shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"+ −
using alpha_abs_res_stronger1_aux[OF asm] by auto+ −
+ −
lemma alpha_abs_set_stronger1:+ −
assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')"+ −
shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"+ −
proof -+ −
from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas)+ −
then have #: "p' \<bullet> (supp x - as) = (supp x - as)" + −
by (simp add: atom_set_perm_eq)+ −
obtain p where *: "\<forall>b \<in> (supp x \<union> as). p \<bullet> b = p' \<bullet> b" + −
and **: "supp p \<subseteq> (supp x \<union> as) \<union> p' \<bullet> (supp x \<union> as)"+ −
using set_renaming_perm2 by blast+ −
from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast+ −
then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto+ −
from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast+ −
then have zb: "p \<bullet> as = p' \<bullet> as" + −
apply(auto simp add: permute_set_eq)+ −
apply(rule_tac x="xa" in exI)+ −
apply(simp)+ −
done+ −
have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)+ −
from 0 have 1: "(supp x - as) \<sharp>* p" using *+ −
by (auto simp add: fresh_star_def fresh_perm)+ −
then have 2: "(supp x - as) \<inter> supp p = {}"+ −
by (auto simp add: fresh_star_def fresh_def)+ −
have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto+ −
have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as" + −
using b by simp+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> + −
((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as" by (simp add: union_eqvt)+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> (supp x \<inter> as)) \<union> p' \<bullet> as"+ −
using # by auto+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> ((supp x \<inter> as) \<union> as)" using union_eqvt+ −
by auto+ −
also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> as" + −
by (metis Int_commute Un_commute sup_inf_absorb)+ −
also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" by blast+ −
finally have "supp p \<subseteq> (supp x - as) \<union> as \<union> p' \<bullet> as" .+ −
then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast+ −
moreover + −
have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)+ −
ultimately + −
show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast+ −
qed+ −
+ −
lemma alpha_abs_lst_stronger1:+ −
assumes asm: "(as, x) \<approx>lst (op =) supp p' (as', x')"+ −
shows "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'"+ −
proof -+ −
from asm have 0: "(supp x - set as) \<sharp>* p'" by (auto simp only: alphas)+ −
then have #: "p' \<bullet> (supp x - set as) = (supp x - set as)" + −
by (simp add: atom_set_perm_eq)+ −
obtain p where *: "\<forall>b \<in> (supp x \<union> set as). p \<bullet> b = p' \<bullet> b" + −
and **: "supp p \<subseteq> (supp x \<union> set as) \<union> p' \<bullet> (supp x \<union> set as)"+ −
using set_renaming_perm2 by blast+ −
from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast+ −
then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto+ −
from * have "\<forall>b \<in> set as. p \<bullet> b = p' \<bullet> b" by blast+ −
then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)+ −
have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)+ −
from 0 have 1: "(supp x - set as) \<sharp>* p" using *+ −
by (auto simp add: fresh_star_def fresh_perm)+ −
then have 2: "(supp x - set as) \<inter> supp p = {}"+ −
by (auto simp add: fresh_star_def fresh_def)+ −
have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto+ −
have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast+ −
also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> + −
(p' \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))) \<union> p' \<bullet> set as" using b by simp+ −
also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> + −
((p' \<bullet> (supp x - set as)) \<union> (p' \<bullet> (supp x \<inter> set as))) \<union> p' \<bullet> set as" by (simp add: union_eqvt)+ −
also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> + −
(p' \<bullet> (supp x \<inter> set as)) \<union> p' \<bullet> set as" using # by auto+ −
also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> ((supp x \<inter> set as) \<union> set as)" + −
using union_eqvt by auto+ −
also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> set as" + −
by (metis Int_commute Un_commute sup_inf_absorb)+ −
also have "\<dots> = (supp x - set as) \<union> set as \<union> p' \<bullet> set as" by blast+ −
finally have "supp p \<subseteq> (supp x - set as) \<union> set as \<union> p' \<bullet> set as" .+ −
then have "supp p \<subseteq> set as \<union> p' \<bullet> set as" using 2 by blast+ −
moreover + −
have "(as, x) \<approx>lst (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)+ −
ultimately + −
show "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'" using zc by blast + −
qed+ −
+ −
lemma alphas_abs_stronger:+ −
shows "(as, x) \<approx>abs_set (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"+ −
and "(as, x) \<approx>abs_res (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"+ −
and "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow> + −
(\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"+ −
apply(rule iffI)+ −
apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1]+ −
apply(auto simp add: alphas_abs)[1]+ −
apply(rule iffI)+ −
apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1]+ −
apply(auto simp add: alphas_abs)[1]+ −
apply(rule iffI)+ −
apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1]+ −
apply(auto simp add: alphas_abs)[1]+ −
done+ −
+ −
section {* Quotient types *}+ −
+ −
quotient_type + −
'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"+ −
and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"+ −
and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"+ −
apply(rule_tac [!] equivpI)+ −
unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def+ −
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)+ −
+ −
quotient_definition+ −
Abs_set ("[_]set. _" [60, 60] 60)+ −
where+ −
"Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"+ −
is+ −
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"+ −
+ −
quotient_definition+ −
Abs_res ("[_]res. _" [60, 60] 60)+ −
where+ −
"Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"+ −
is+ −
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"+ −
+ −
quotient_definition+ −
Abs_lst ("[_]lst. _" [60, 60] 60)+ −
where+ −
"Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"+ −
is+ −
"Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"+ −
+ −
lemma [quot_respect]:+ −
shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"+ −
and "(op= ===> op= ===> alpha_abs_res) Pair Pair"+ −
and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"+ −
unfolding fun_rel_def+ −
by (auto intro: alphas_abs_refl)+ −
+ −
lemma [quot_respect]:+ −
shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"+ −
and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"+ −
and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"+ −
unfolding fun_rel_def+ −
by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)+ −
+ −
lemma Abs_eq_iff:+ −
shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"+ −
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"+ −
and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"+ −
by (lifting alphas_abs)+ −
+ −
lemma Abs_eq_iff2:+ −
shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"+ −
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"+ −
and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> + −
(\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"+ −
by (lifting alphas_abs_stronger)+ −
+ −
lemma Abs_exhausts:+ −
shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"+ −
and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"+ −
and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"+ −
by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]+ −
prod.exhaust[where 'a="atom set" and 'b="'a"]+ −
prod.exhaust[where 'a="atom list" and 'b="'a"])+ −
+ −
instantiation abs_set :: (pt) pt+ −
begin+ −
+ −
quotient_definition+ −
"permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"+ −
is+ −
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"+ −
+ −
lemma permute_Abs_set[simp]:+ −
fixes x::"'a::pt" + −
shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"+ −
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])+ −
+ −
instance+ −
apply(default)+ −
apply(case_tac [!] x rule: Abs_exhausts(1))+ −
apply(simp_all)+ −
done+ −
+ −
end+ −
+ −
instantiation abs_res :: (pt) pt+ −
begin+ −
+ −
quotient_definition+ −
"permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"+ −
is+ −
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"+ −
+ −
lemma permute_Abs_res[simp]:+ −
fixes x::"'a::pt" + −
shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"+ −
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])+ −
+ −
instance+ −
apply(default)+ −
apply(case_tac [!] x rule: Abs_exhausts(2))+ −
apply(simp_all)+ −
done+ −
+ −
end+ −
+ −
instantiation abs_lst :: (pt) pt+ −
begin+ −
+ −
quotient_definition+ −
"permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"+ −
is+ −
"permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"+ −
+ −
lemma permute_Abs_lst[simp]:+ −
fixes x::"'a::pt" + −
shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"+ −
by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])+ −
+ −
instance+ −
apply(default)+ −
apply(case_tac [!] x rule: Abs_exhausts(3))+ −
apply(simp_all)+ −
done+ −
+ −
end+ −
+ −
lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst+ −
+ −
+ −
lemma Abs_swap1:+ −
assumes a1: "a \<notin> (supp x) - bs"+ −
and a2: "b \<notin> (supp x) - bs"+ −
shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"+ −
and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"+ −
unfolding Abs_eq_iff+ −
unfolding alphas+ −
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] + −
unfolding fresh_star_def fresh_def+ −
unfolding swap_set_not_in[OF a1 a2] + −
using a1 a2+ −
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)+ −
(auto simp add: supp_perm swap_atom)+ −
+ −
lemma Abs_swap2:+ −
assumes a1: "a \<notin> (supp x) - (set bs)"+ −
and a2: "b \<notin> (supp x) - (set bs)"+ −
shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"+ −
unfolding Abs_eq_iff+ −
unfolding alphas+ −
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]+ −
unfolding fresh_star_def fresh_def+ −
unfolding swap_set_not_in[OF a1 a2]+ −
using a1 a2+ −
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)+ −
(auto simp add: supp_perm swap_atom)+ −
+ −
lemma Abs_supports:+ −
shows "((supp x) - as) supports (Abs_set as x)"+ −
and "((supp x) - as) supports (Abs_res as x)"+ −
and "((supp x) - set bs) supports (Abs_lst bs x)"+ −
unfolding supports_def+ −
unfolding permute_Abs+ −
by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])+ −
+ −
function+ −
supp_set :: "('a::pt) abs_set \<Rightarrow> atom set"+ −
where+ −
"supp_set (Abs_set as x) = supp x - as"+ −
apply(case_tac x rule: Abs_exhausts(1))+ −
apply(simp)+ −
apply(simp add: Abs_eq_iff alphas_abs alphas)+ −
done+ −
+ −
termination supp_set + −
by (auto intro!: local.termination)+ −
+ −
function+ −
supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"+ −
where+ −
"supp_res (Abs_res as x) = supp x - as"+ −
apply(case_tac x rule: Abs_exhausts(2))+ −
apply(simp)+ −
apply(simp add: Abs_eq_iff alphas_abs alphas)+ −
done+ −
+ −
termination supp_res + −
by (auto intro!: local.termination)+ −
+ −
function+ −
supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"+ −
where+ −
"supp_lst (Abs_lst cs x) = (supp x) - (set cs)"+ −
apply(case_tac x rule: Abs_exhausts(3))+ −
apply(simp)+ −
apply(simp add: Abs_eq_iff alphas_abs alphas)+ −
done+ −
+ −
termination supp_lst + −
by (auto intro!: local.termination)+ −
+ −
lemma supp_funs_eqvt[eqvt]:+ −
shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"+ −
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"+ −
and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"+ −
apply(case_tac x rule: Abs_exhausts(1))+ −
apply(simp add: supp_eqvt Diff_eqvt)+ −
apply(case_tac y rule: Abs_exhausts(2))+ −
apply(simp add: supp_eqvt Diff_eqvt)+ −
apply(case_tac z rule: Abs_exhausts(3))+ −
apply(simp add: supp_eqvt Diff_eqvt set_eqvt)+ −
done+ −
+ −
lemma Abs_fresh_aux:+ −
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"+ −
and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"+ −
and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"+ −
by (rule_tac [!] fresh_fun_eqvt_app)+ −
(auto simp only: eqvt_def eqvts_raw)+ −
+ −
lemma Abs_supp_subset1:+ −
assumes a: "finite (supp x)"+ −
shows "(supp x) - as \<subseteq> supp (Abs_set as x)"+ −
and "(supp x) - as \<subseteq> supp (Abs_res as x)"+ −
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"+ −
unfolding supp_conv_fresh+ −
by (auto dest!: Abs_fresh_aux)+ −
(simp_all add: fresh_def supp_finite_atom_set a)+ −
+ −
lemma Abs_supp_subset2:+ −
assumes a: "finite (supp x)"+ −
shows "supp (Abs_set as x) \<subseteq> (supp x) - as"+ −
and "supp (Abs_res as x) \<subseteq> (supp x) - as"+ −
and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"+ −
by (rule_tac [!] supp_is_subset)+ −
(simp_all add: Abs_supports a)+ −
+ −
lemma Abs_finite_supp:+ −
assumes a: "finite (supp x)"+ −
shows "supp (Abs_set as x) = (supp x) - as"+ −
and "supp (Abs_res as x) = (supp x) - as"+ −
and "supp (Abs_lst bs x) = (supp x) - (set bs)"+ −
by (rule_tac [!] subset_antisym)+ −
(simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])+ −
+ −
lemma supp_Abs:+ −
fixes x::"'a::fs"+ −
shows "supp (Abs_set as x) = (supp x) - as"+ −
and "supp (Abs_res as x) = (supp x) - as"+ −
and "supp (Abs_lst bs x) = (supp x) - (set bs)"+ −
by (rule_tac [!] Abs_finite_supp)+ −
(simp_all add: finite_supp)+ −
+ −
instance abs_set :: (fs) fs+ −
apply(default)+ −
apply(case_tac x rule: Abs_exhausts(1))+ −
apply(simp add: supp_Abs finite_supp)+ −
done+ −
+ −
instance abs_res :: (fs) fs+ −
apply(default)+ −
apply(case_tac x rule: Abs_exhausts(2))+ −
apply(simp add: supp_Abs finite_supp)+ −
done+ −
+ −
instance abs_lst :: (fs) fs+ −
apply(default)+ −
apply(case_tac x rule: Abs_exhausts(3))+ −
apply(simp add: supp_Abs finite_supp)+ −
done+ −
+ −
lemma Abs_fresh_iff:+ −
fixes x::"'a::fs"+ −
shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"+ −
and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"+ −
and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"+ −
unfolding fresh_def+ −
unfolding supp_Abs+ −
by auto+ −
+ −
lemma Abs_fresh_star_iff:+ −
fixes x::"'a::fs"+ −
shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x"+ −
and "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x"+ −
and "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x"+ −
unfolding fresh_star_def+ −
by (auto simp add: Abs_fresh_iff)+ −
+ −
lemma Abs_fresh_star:+ −
fixes x::"'a::fs"+ −
shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"+ −
and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x"+ −
and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x"+ −
unfolding fresh_star_def+ −
by(auto simp add: Abs_fresh_iff)+ −
+ −
+ −
subsection {* Renaming of bodies of abstractions *}+ −
+ −
(* FIXME: finiteness assumption is not needed *)+ −
+ −
lemma Abs_rename_set:+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> bs) \<sharp>* x" + −
and b: "finite bs"+ −
shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"+ −
proof -+ −
from b set_renaming_perm + −
obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast+ −
have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)+ −
have "[bs]set. x = q \<bullet> ([bs]set. x)"+ −
apply(rule perm_supp_eq[symmetric])+ −
using a **+ −
unfolding Abs_fresh_star_iff+ −
unfolding fresh_star_def+ −
by auto+ −
also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp+ −
finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: ***)+ −
then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis+ −
qed+ −
+ −
lemma Abs_rename_res:+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> bs) \<sharp>* x" + −
and b: "finite bs"+ −
shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"+ −
proof -+ −
from b set_renaming_perm + −
obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast+ −
have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)+ −
have "[bs]res. x = q \<bullet> ([bs]res. x)"+ −
apply(rule perm_supp_eq[symmetric])+ −
using a **+ −
unfolding Abs_fresh_star_iff+ −
unfolding fresh_star_def+ −
by auto+ −
also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp+ −
finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: ***)+ −
then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis+ −
qed+ −
+ −
lemma Abs_rename_lst:+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> (set bs)) \<sharp>* x" + −
shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"+ −
proof -+ −
from a list_renaming_perm + −
obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast+ −
have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt)+ −
have "[bs]lst. x = q \<bullet> ([bs]lst. x)"+ −
apply(rule perm_supp_eq[symmetric])+ −
using a **+ −
unfolding Abs_fresh_star_iff+ −
unfolding fresh_star_def+ −
by auto+ −
also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp+ −
finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: ***)+ −
then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis+ −
qed+ −
+ −
+ −
text {* for deep recursive binders *}+ −
+ −
lemma Abs_rename_set':+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> bs) \<sharp>* x" + −
and b: "finite bs"+ −
shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"+ −
using Abs_rename_set[OF a b] by metis+ −
+ −
lemma Abs_rename_res':+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> bs) \<sharp>* x" + −
and b: "finite bs"+ −
shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"+ −
using Abs_rename_res[OF a b] by metis+ −
+ −
lemma Abs_rename_lst':+ −
fixes x::"'a::fs"+ −
assumes a: "(p \<bullet> (set bs)) \<sharp>* x" + −
shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"+ −
using Abs_rename_lst[OF a] by metis+ −
+ −
section {* Infrastructure for building tuples of relations and functions *}+ −
+ −
fun+ −
prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"+ −
where+ −
"prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"+ −
+ −
definition + −
prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"+ −
where+ −
"prod_alpha = prod_rel"+ −
+ −
lemma [quot_respect]:+ −
shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"+ −
unfolding fun_rel_def+ −
unfolding prod_rel_def+ −
by auto+ −
+ −
lemma [quot_preserve]:+ −
assumes q1: "Quotient R1 abs1 rep1"+ −
and q2: "Quotient R2 abs2 rep2"+ −
shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"+ −
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])+ −
+ −
lemma [mono]: + −
shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"+ −
unfolding prod_alpha_def+ −
by auto+ −
+ −
lemma [eqvt]: + −
shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"+ −
unfolding prod_alpha_def+ −
unfolding prod_rel_def+ −
by (perm_simp) (rule refl)+ −
+ −
lemma [eqvt]: + −
shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"+ −
unfolding prod_fv.simps+ −
by (perm_simp) (rule refl)+ −
+ −
lemma prod_fv_supp:+ −
shows "prod_fv supp supp = supp"+ −
by (rule ext)+ −
(auto simp add: prod_fv.simps supp_Pair)+ −
+ −
lemma prod_alpha_eq:+ −
shows "prod_alpha (op=) (op=) = (op=)"+ −
unfolding prod_alpha_def+ −
by (auto intro!: ext)+ −
+ −
+ −
end+ −
+ −