theory Abs
imports "Nominal2_Atoms"
"Nominal2_Eqvt"
"Nominal2_Supp"
"Nominal2_FSet"
"../Quotient"
"../Quotient_Product"
begin
fun
alpha_gen
where
alpha_gen[simp del]:
"alpha_gen (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_gen.simps alpha_res.simps alpha_lst.simps
notation
alpha_gen ("_ \<approx>gen _ _ _ _" [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)
(* monos *)
lemma [mono]:
shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen 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)
fun
alpha_abs
where
"alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
fun
alpha_abs_lst
where
"alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
fun
alpha_abs_res
where
"alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
notation
alpha_abs ("_ \<approx>abs _") and
alpha_abs_lst ("_ \<approx>abs'_lst _") and
alpha_abs_res ("_ \<approx>abs'_res _")
lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
lemma alphas_abs_refl:
shows "(bs, x) \<approx>abs (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 (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (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 (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (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 (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (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])
fun
aux_set
where
"aux_set (bs, x) = (supp x) - bs"
fun
aux_list
where
"aux_list (cs, x) = (supp x) - (set cs)"
lemma aux_abs_lemma:
assumes a: "(bs, x) \<approx>abs (cs, y)"
shows "aux_set (bs, x) = aux_set (cs, y)"
using a
by (induct rule: alpha_abs.induct)
(simp add: alphas_abs alphas)
lemma aux_abs_res_lemma:
assumes a: "(bs, x) \<approx>abs_res (cs, y)"
shows "aux_set (bs, x) = aux_set (cs, y)"
using a
by (induct rule: alpha_abs_res.induct)
(simp add: alphas_abs alphas)
lemma aux_abs_list_lemma:
assumes a: "(bs, x) \<approx>abs_lst (cs, y)"
shows "aux_list (bs, x) = aux_list (cs, y)"
using a
by (induct rule: alpha_abs_lst.induct)
(simp add: alphas_abs alphas)
quotient_type
'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
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 symp_def transp_def
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
quotient_definition
"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
quotient_definition
"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::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) 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 simp only:)
lemma [quot_respect]:
shows "(op= ===> alpha_abs ===> alpha_abs) 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 [quot_respect]:
shows "(alpha_abs ===> op=) aux_set aux_set"
and "(alpha_abs_res ===> op=) aux_set aux_set"
and "(alpha_abs_lst ===> op=) aux_list aux_list"
unfolding fun_rel_def
apply(rule_tac [!] allI)
apply(rule_tac [!] allI)
apply(case_tac [!] x, case_tac [!] y)
apply(rule_tac [!] impI)
by (simp_all only: aux_abs_lemma aux_abs_res_lemma aux_abs_list_lemma)
lemma abs_inducts:
shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1"
and "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2"
and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3"
by (lifting prod.induct[where 'a="atom set" and 'b="'a"]
prod.induct[where 'a="atom set" and 'b="'a"]
prod.induct[where 'a="atom list" and 'b="'a"])
lemma abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
apply(simp_all)
apply(lifting alphas_abs)
done
instantiation abs_gen :: (pt) pt
begin
quotient_definition
"permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
is
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
lemma permute_Abs[simp]:
fixes x::"'a::pt"
shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
apply(default)
apply(induct_tac [!] x rule: abs_inducts(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(induct_tac [!] x rule: abs_inducts(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(induct_tac [!] x rule: abs_inducts(3))
apply(simp_all)
done
end
lemmas permute_abs = permute_Abs 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 bs x = Abs ((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_abs
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_abs
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 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])
quotient_definition
"supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
is
"aux_set"
quotient_definition
"supp_res :: ('a::pt) abs_res \<Rightarrow> atom set"
is
"aux_set"
quotient_definition
"supp_lst :: ('a::pt) abs_lst \<Rightarrow> atom set"
is
"aux_list"
lemma aux_supps:
shows "supp_gen (Abs bs x) = (supp x) - bs"
and "supp_res (Abs_res bs x) = (supp x) - bs"
and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
by (lifting aux_set.simps aux_set.simps aux_list.simps)
lemma aux_supp_eqvt[eqvt]:
shows "(p \<bullet> supp_gen x) = supp_gen (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(induct_tac x rule: abs_inducts(1))
apply(simp add: aux_supps supp_eqvt Diff_eqvt)
apply(induct_tac y rule: abs_inducts(2))
apply(simp add: aux_supps supp_eqvt Diff_eqvt)
apply(induct_tac z rule: abs_inducts(3))
apply(simp add: aux_supps supp_eqvt Diff_eqvt set_eqvt)
done
lemma aux_fresh:
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (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)"
apply(rule_tac [!] fresh_fun_eqvt_app)
apply(simp_all add: eqvts_raw)
done
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
shows "(supp x) - as \<subseteq> supp (Abs 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
apply(auto dest!: aux_fresh simp add: aux_supps)
apply(simp_all add: fresh_def supp_finite_atom_set a)
done
lemma supp_abs_subset2:
assumes a: "finite (supp x)"
shows "supp (Abs 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)"
apply(rule_tac [!] supp_is_subset)
apply(simp_all add: abs_supports a)
done
lemma abs_finite_supp:
assumes a: "finite (supp x)"
shows "supp (Abs as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
apply(rule_tac [!] subset_antisym)
apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
done
lemma supp_abs:
fixes x::"'a::fs"
shows "supp (Abs as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
apply(rule_tac [!] abs_finite_supp)
apply(simp_all add: finite_supp)
done
instance abs_gen :: (fs) fs
apply(default)
apply(induct_tac x rule: abs_inducts(1))
apply(simp add: supp_abs finite_supp)
done
instance abs_res :: (fs) fs
apply(default)
apply(induct_tac x rule: abs_inducts(2))
apply(simp add: supp_abs finite_supp)
done
instance abs_lst :: (fs) fs
apply(default)
apply(induct_tac x rule: abs_inducts(3))
apply(simp add: supp_abs finite_supp)
done
lemma abs_fresh_iff:
fixes x::"'a::fs"
shows "a \<sharp> Abs 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
section {* BELOW is stuff that may or may not be needed *}
(* support of concrete atom sets *)
lemma supp_atom_image:
fixes as::"'a::at_base set"
shows "supp (atom ` as) = supp as"
apply(simp add: supp_def)
apply(simp add: image_eqvt)
apply(simp add: atom_eqvt_raw)
apply(simp add: atom_image_cong)
done
lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
apply (simp add: fresh_def)
apply (simp add: supp_atom_image)
apply (fold fresh_def)
apply (simp add: swap_fresh_fresh)
done
(* TODO: The following lemmas can be moved somewhere... *)
lemma Abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
by (lifting alpha_abs.simps(1))
lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
by auto
lemma split_prs2[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
lemma alpha_gen2:
"(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
(f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
\<and> pi \<bullet> bs = cs)"
by (simp add: alpha_gen)
lemma alpha_gen_compose_sym:
fixes pi
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
using b apply -
apply(simp add: alpha_gen)
apply(erule conjE)+
apply(rule conjI)
apply(simp add: fresh_star_def fresh_minus_perm)
apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
apply simp
apply(clarify)
apply(simp)
apply(rule a)
apply assumption
done
lemma alpha_gen_compose_sym2:
assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
(R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
using a
apply(simp add: alpha_gen)
apply clarify
apply (rule conjI)
apply(simp add: fresh_star_def fresh_minus_perm)
apply (rule conjI)
apply (rotate_tac 3)
apply (drule_tac pi="- pi" in r1)
apply simp
apply (rule conjI)
apply (rotate_tac -1)
apply (drule_tac pi="- pi" in r2)
apply simp_all
done
lemma alpha_gen_compose_trans:
fixes pi pia
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
using b c apply -
apply(simp add: alpha_gen)
apply(erule conjE)+
apply(simp add: fresh_star_plus)
apply(drule_tac x="- pia \<bullet> sa" in spec)
apply(drule mp)
apply(rotate_tac 5)
apply(drule_tac pi="- pia" in a)
apply(simp)
apply(rotate_tac 7)
apply(drule_tac pi="pia" in a)
apply(simp)
done
lemma alpha_gen_compose_trans2:
fixes pi pia
assumes b: "(aa, (t1, t2)) \<approx>gen
(\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
(\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
pia (ac, (sa1, sa2))"
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
(pia + pi) (ac, (sa1, sa2))"
using b c apply -
apply(simp add: alpha_gen2)
apply(simp add: alpha_gen)
apply(erule conjE)+
apply(simp add: fresh_star_plus)
apply(drule_tac x="- pia \<bullet> sa1" in spec)
apply(drule mp)
apply(rotate_tac 5)
apply(drule_tac pi="- pia" in r1)
apply(simp)
apply(rotate_tac -1)
apply(drule_tac pi="pia" in r1)
apply(simp)
apply(drule_tac x="- pia \<bullet> sa2" in spec)
apply(drule mp)
apply(rotate_tac 6)
apply(drule_tac pi="- pia" in r2)
apply(simp)
apply(rotate_tac -1)
apply(drule_tac pi="pia" in r2)
apply(simp)
done
lemma alpha_gen_refl:
assumes a: "R x x"
shows "(bs, x) \<approx>gen 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_gen_sym:
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
and b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen 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
apply (erule_tac [1] conjE)+
apply (erule_tac [2] conjE)+
apply (erule_tac [3] conjE)+
using a
apply (simp_all add: fresh_minus_perm)
apply (rotate_tac [!] -1)
apply (drule_tac [!] p="-p" in b)
apply (simp_all)
apply (metis permute_minus_cancel(2))
apply (metis permute_minus_cancel(2))
done
lemma alpha_gen_trans:
assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)"
and b: "R (p \<bullet> x) y"
and c: "R (q \<bullet> y) z"
and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen 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)"
unfolding alphas
unfolding fresh_star_def
apply (simp_all add: fresh_plus_perm)
apply (metis a c d permute_minus_cancel(2))+
done
lemma alpha_gen_eqvt:
assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
and b: "p \<bullet> (f x) = f (p \<bullet> x)"
and c: "p \<bullet> (f y) = f (p \<bullet> y)"
shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R 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 R 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 R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
unfolding alphas
unfolding set_eqvt[symmetric]
unfolding b[symmetric] c[symmetric]
unfolding Diff_eqvt[symmetric]
unfolding permute_eqvt[symmetric]
using a
by (auto simp add: fresh_star_permute_iff)
end