theory Abs
imports "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
"Quotient"
"Quotient_List"
"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)
(* equivariance *)
lemma alpha_gen_eqvt[eqvt]:
shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
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)
(* equivalence *)
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 (- p \<bullet> y) x"
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
using a
by (auto simp add: fresh_minus_perm)
lemma alpha_gen_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>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)"
apply(auto intro!: alpha_gen_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_gen_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>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)"
using a
unfolding alphas fresh_star_def
by (simp_all add: fresh_plus_perm)
lemma alpha_gen_trans_eqvt:
assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
and a: "(bs, x) \<approx>gen 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>gen R f (q + p) (ds, z)"
apply(rule alpha_gen_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_gen_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_gen_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_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
lemma test:
shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
and "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
and "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
by (simp_all add: alphas)
section {* General Abstractions *}
fun
alpha_abs
where
[simp del]:
"alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (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 (infix "\<approx>abs" 50) and
alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
alpha_abs_res (infix "\<approx>abs'_res" 50)
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])
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 ("[_]set. _" [60, 60] 60)
where
"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 ("[_]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) 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 abs_exhausts:
shows "(\<And>as (x::'a::pt). y1 = Abs 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"])
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)"
unfolding alphas_abs
by (lifting alphas_abs)
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(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 = 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])
function
supp_gen :: "('a::pt) abs_gen \<Rightarrow> atom set"
where
"supp_gen (Abs 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_gen
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 [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(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 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)"
by (rule_tac [!] fresh_fun_eqvt_app)
(simp_all add: eqvts_raw)
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
by (auto dest!: aux_fresh)
(simp_all add: fresh_def supp_finite_atom_set a)
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)"
by (rule_tac [!] supp_is_subset)
(simp_all add: abs_supports a)
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)"
by (rule_tac [!] subset_antisym)
(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
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)"
by (rule_tac [!] abs_finite_supp)
(simp_all add: finite_supp)
instance abs_gen :: (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 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 *}
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: eqvts_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))"
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 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 alphas2:
"(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)"
"(bs, x1, x2) \<approx>res (\<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)"
"(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) =
(f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
\<and> pi \<bullet> bsl = csl)"
by (simp_all add: alphas)
lemma alphas3:
"(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
(f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
by (simp add: alphas)
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: alphas)
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_res_compose_sym:
fixes pi
assumes b: "(aa, t) \<approx>res (\<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>res R f (- pi) (aa, t)"
using b apply -
apply(simp add: alphas)
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(rule a)
apply assumption
done
lemma alpha_lst_compose_sym:
fixes pi
assumes b: "(aa, t) \<approx>lst (\<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>lst R f (- pi) (aa, t)"
using b apply -
apply(simp add: alphas)
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
lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym
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: alphas)
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_res_compose_sym2:
assumes a: "(aa, t1, t2) \<approx>res (\<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>res (\<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: alphas)
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 (rotate_tac -1)
apply (drule_tac pi="- pi" in r2)
apply simp
done
lemma alpha_lst_compose_sym2:
assumes a: "(aa, t1, t2) \<approx>lst (\<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>lst (\<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: alphas)
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
lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2
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: alphas)
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_res_compose_trans:
fixes pi pia
assumes b: "(aa, t) \<approx>res (\<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>res 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>res R f (pia + pi) (ac, sa)"
using b c apply -
apply(simp add: alphas)
apply(erule conjE)+
apply(simp add: fresh_star_plus)
apply(drule_tac x="- pia \<bullet> sa" in spec)
apply(drule mp)
apply(drule_tac pi="- pia" in a)
apply(simp)
apply(rotate_tac 6)
apply(drule_tac pi="pia" in a)
apply(simp)
done
lemma alpha_lst_compose_trans:
fixes pi pia
assumes b: "(aa, t) \<approx>lst (\<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>lst 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>lst R f (pia + pi) (ac, sa)"
using b c apply -
apply(simp add: alphas)
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
lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans
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: alphas2)
apply(simp add: alphas)
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_res_compose_trans2:
fixes pi pia
assumes b: "(aa, (t1, t2)) \<approx>res
(\<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>res (\<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>res (\<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: alphas2)
apply(simp add: alphas)
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_lst_compose_trans2:
fixes pi pia
assumes b: "(aa, (t1, t2)) \<approx>lst
(\<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>lst (\<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>lst (\<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: alphas2)
apply(simp add: alphas)
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
lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
lemma alpha_gen_simpler:
assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
and fin_fv: "finite (f x)"
and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
(f x - bs) \<sharp>* pi \<and>
R (pi \<bullet> x) y \<and>
pi \<bullet> bs = cs"
apply rule
unfolding alpha_gen
apply clarify
apply (erule conjE)+
apply (simp)
apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
apply (rule sym)
apply simp
apply (rule supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (rule finite_Diff)
apply (rule fin_fv)
apply (assumption)
apply (simp add: eqvts fv_eqvt)
apply (subst fv_rsp)
apply assumption
apply (simp)
done
lemma alpha_lst_simpler:
assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
and fin_fv: "finite (f x)"
and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
(f x - set bs) \<sharp>* pi \<and>
R (pi \<bullet> x) y \<and>
pi \<bullet> bs = cs"
apply rule
unfolding alpha_lst
apply clarify
apply (erule conjE)+
apply (simp)
apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
apply (rule sym)
apply simp
apply (rule supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (rule finite_Diff)
apply (rule fin_fv)
apply (assumption)
apply (simp add: eqvts fv_eqvt)
apply (subst fv_rsp)
apply assumption
apply (simp)
done
fun
prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
where
"prod_fv fvx fvy (x, y) = (fvx x \<union> fvy 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"
by auto
lemma [quot_preserve]:
assumes q1: "Quotient R1 abs1 rep1"
and q2: "Quotient R2 abs2 rep2"
shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
by (simp add: expand_fun_eq 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.simps
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)
end