--- a/Nominal/Abs.thy Sat Sep 04 06:23:31 2010 +0800
+++ b/Nominal/Abs.thy Sat Sep 04 06:48:14 2010 +0800
@@ -8,10 +8,10 @@
begin
fun
- alpha_gen
+ alpha_set
where
- alpha_gen[simp del]:
- "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ 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>
@@ -36,17 +36,17 @@
R (pi \<bullet> x) y \<and>
pi \<bullet> bs = cs"
-lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
+lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
notation
- alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
+ 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_gen bs R1 \<le> alpha_gen bs R2"
+ 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)
@@ -55,7 +55,7 @@
section {* Equivariance *}
lemma alpha_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)"
+ 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
@@ -70,7 +70,7 @@
lemma alpha_refl:
assumes a: "R x x"
- shows "(bs, x) \<approx>gen R f 0 (bs, 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
@@ -80,7 +80,7 @@
lemma alpha_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)"
+ 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
@@ -89,7 +89,7 @@
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>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)"
+ 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
@@ -99,7 +99,7 @@
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>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, 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)"
apply(auto intro!: alpha_sym)
@@ -113,12 +113,12 @@
apply(assumption)
done
-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)"
+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>gen R f (q + p) (ds, z)"
+ shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
apply(rule alpha_trans)
defer
apply(rule a)
@@ -173,16 +173,16 @@
apply(simp add: permute_eqvt[symmetric])
done
-lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
section {* General Abstractions *}
fun
- alpha_abs
+ alpha_abs_set
where
[simp del]:
- "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+ "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
fun
alpha_abs_lst
@@ -197,15 +197,15 @@
"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_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.simps alpha_abs_res.simps alpha_abs_lst.simps
+lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
lemma alphas_abs_refl:
- shows "(bs, x) \<approx>abs (bs, x)"
+ 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
@@ -215,7 +215,7 @@
(simp_all add: fresh_zero_perm)
lemma alphas_abs_sym:
- shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
+ 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
@@ -225,7 +225,7 @@
(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)"
+ 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
@@ -236,7 +236,7 @@
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)"
+ 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
@@ -249,7 +249,7 @@
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
quotient_type
- 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
+ '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)
@@ -257,9 +257,9 @@
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
quotient_definition
- Abs ("[_]set. _" [60, 60] 60)
+ Abs_set ("[_]set. _" [60, 60] 60)
where
- "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
+ "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
@@ -278,21 +278,21 @@
"Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
lemma [quot_respect]:
- shows "(op= ===> op= ===> alpha_abs) Pair Pair"
+ 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 ===> alpha_abs) permute permute"
+ 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_exhausts:
- shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
+ 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"]
@@ -300,22 +300,22 @@
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)"
+ shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (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
+instantiation abs_set :: (pt) pt
begin
quotient_definition
- "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
+ "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[simp]:
fixes x::"'a::pt"
- shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+ 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
@@ -374,7 +374,7 @@
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)"
+ 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_abs
@@ -401,7 +401,7 @@
(auto simp add: supp_perm swap_atom)
lemma abs_supports:
- shows "((supp x) - as) supports (Abs as x)"
+ 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
@@ -409,15 +409,15 @@
by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
function
- supp_gen :: "('a::pt) abs_gen \<Rightarrow> atom set"
+ supp_set :: "('a::pt) abs_set \<Rightarrow> atom set"
where
- "supp_gen (Abs as x) = supp x - as"
+ "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_gen
+termination supp_set
by (auto intro!: local.termination)
function
@@ -445,7 +445,7 @@
by (auto intro!: local.termination)
lemma [eqvt]:
- shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
+ 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))
@@ -457,7 +457,7 @@
done
lemma aux_fresh:
- shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
+ 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)
@@ -465,7 +465,7 @@
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
- shows "(supp x) - as \<subseteq> supp (Abs as 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
@@ -474,7 +474,7 @@
lemma supp_abs_subset2:
assumes a: "finite (supp x)"
- shows "supp (Abs as x) \<subseteq> (supp x) - as"
+ 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)
@@ -482,7 +482,7 @@
lemma abs_finite_supp:
assumes a: "finite (supp x)"
- shows "supp (Abs as x) = (supp x) - as"
+ 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)
@@ -490,13 +490,13 @@
lemma supp_abs:
fixes x::"'a::fs"
- shows "supp (Abs as x) = (supp x) - as"
+ 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_gen :: (fs) fs
+instance abs_set :: (fs) fs
apply(default)
apply(case_tac x rule: abs_exhausts(1))
apply(simp add: supp_abs finite_supp)
@@ -516,7 +516,7 @@
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)"
+ 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
@@ -524,7 +524,7 @@
by auto
lemma Abs_eq_iff:
- shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+ 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)