--- a/Nominal/Nominal2_Abs.thy Wed Nov 30 14:58:19 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy Mon Dec 05 15:34:12 2011 +0000
@@ -451,6 +451,10 @@
apply(auto simp add: alphas_abs)[1]
done
+lemma alpha_res_alpha_set:
+ "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
+ using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
+
section {* Quotient types *}
quotient_type
@@ -497,38 +501,34 @@
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))"
+ shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (bs', y))"
+ and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (bs', y))"
+ and "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op =) supp p (cs', 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)"
+ shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')"
+ and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')"
+ and "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op=) supp p (cs', y) \<and> supp p \<subseteq> set cs \<union> set cs')"
by (lifting alphas_abs_stronger)
-lemma alpha_res_alpha_set:
- "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
- using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
lemma Abs_eq_res_set:
- "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
+ shows "[bs]res. x = [cs]res. y \<longleftrightarrow> [bs \<inter> supp x]set. x = [cs \<inter> supp y]set. y"
unfolding Abs_eq_iff alpha_res_alpha_set by rule
lemma Abs_eq_res_supp:
assumes asm: "supp x \<subseteq> bs"
- shows "([as]res. x) = ([as \<inter> bs]res. x)"
+ shows "[as]res. x = [as \<inter> bs]res. x"
unfolding Abs_eq_iff alphas
apply (rule_tac x="0::perm" in exI)
apply (simp add: fresh_star_zero)
using asm by blast
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"
+ shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1"
+ and "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2"
+ and "(\<And>bs (x::'a::pt). y3 = [bs]lst. 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"])
@@ -544,7 +544,7 @@
lemma permute_Abs_set[simp]:
fixes x::"'a::pt"
- shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
+ shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)"
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
@@ -565,7 +565,7 @@
lemma permute_Abs_res[simp]:
fixes x::"'a::pt"
- shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
+ shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)"
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
@@ -586,7 +586,7 @@
lemma permute_Abs_lst[simp]:
fixes x::"'a::pt"
- shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
+ shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)"
by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
instance
@@ -603,8 +603,8 @@
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)"
+ shows "[bs]set. x = [(a \<rightleftharpoons> b) \<bullet> bs]set. ((a \<rightleftharpoons> b) \<bullet> x)"
+ and "[bs]res. x = [(a \<rightleftharpoons> b) \<bullet> bs]res. ((a \<rightleftharpoons> b) \<bullet> x)"
unfolding Abs_eq_iff
unfolding alphas
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
@@ -617,7 +617,7 @@
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)"
+ shows "[bs]lst. x = [(a \<rightleftharpoons> b) \<bullet> bs]lst. ((a \<rightleftharpoons> b) \<bullet> x)"
unfolding Abs_eq_iff
unfolding alphas
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
@@ -628,9 +628,9 @@
(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)"
+ shows "((supp x) - as) supports ([as]set. x)"
+ and "((supp x) - as) supports ([as]res. x)"
+ and "((supp x) - set bs) supports ([bs]lst. x)"
unfolding supports_def
unfolding permute_Abs
by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
@@ -638,26 +638,26 @@
function
supp_set :: "('a::pt) abs_set \<Rightarrow> atom set"
where
- "supp_set (Abs_set as x) = supp x - as"
+ "supp_set ([as]set. 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)
+ by lexicographic_order
function
supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
where
- "supp_res (Abs_res as x) = supp x - as"
+ "supp_res ([as]res. 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)
+ by lexicographic_order
function
supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
@@ -668,8 +668,8 @@
apply(simp add: Abs_eq_iff alphas_abs alphas)
done
-termination supp_lst
- by (auto intro!: local.termination)
+termination supp_lst
+ by lexicographic_order
lemma supp_funs_eqvt[eqvt]:
shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
@@ -684,44 +684,43 @@
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)"
+ shows "a \<sharp> [bs]set. x \<Longrightarrow> a \<sharp> supp_set ([bs]set. x)"
+ and "a \<sharp> [bs]res. x \<Longrightarrow> a \<sharp> supp_res ([bs]res. x)"
+ and "a \<sharp> [cs]lst. x \<Longrightarrow> a \<sharp> supp_lst ([cs]lst. 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)"
+ shows "(supp x) - as \<subseteq> supp ([as]set. x)"
+ and "(supp x) - as \<subseteq> supp ([as]res. x)"
+ and "(supp x) - (set bs) \<subseteq> supp ([bs]lst. 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)"
+ shows "supp ([as]set. x) \<subseteq> (supp x) - as"
+ and "supp ([as]res. x) \<subseteq> (supp x) - as"
+ and "supp ([bs]lst. 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])
+ shows "supp ([as]set. x) = (supp x) - as"
+ and "supp ([as]res. x) = (supp x) - as"
+ and "supp ([bs]lst. x) = (supp x) - (set bs)"
+using Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]
+ by blast+
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)
+ shows "supp ([as]set. x) = (supp x) - as"
+ and "supp ([as]res. x) = (supp x) - as"
+ and "supp ([bs]lst. x) = (supp x) - (set bs)"
+by (simp_all add: Abs_finite_supp finite_supp)
instance abs_set :: (fs) fs
apply(default)
@@ -743,38 +742,40 @@
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)"
+ shows "a \<sharp> [bs]set. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ and "a \<sharp> [bs]res. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ and "a \<sharp> [cs]lst. 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"
+ shows "as \<sharp>* ([bs]set. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
+ and "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
+ and "as \<sharp>* ([cs]lst. 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"
+ shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']set. x)"
+ and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)"
+ and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)"
unfolding fresh_star_def
by(auto simp add: Abs_fresh_iff)
lemma Abs_fresh_star2:
fixes x::"'a::fs"
- shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x"
- and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x"
- and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x"
+ shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]set. x) \<longleftrightarrow> as \<sharp>* x"
+ and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]res. x) \<longleftrightarrow> as \<sharp>* x"
+ and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* ([ds]lst. x) \<longleftrightarrow> cs \<sharp>* x"
unfolding fresh_star_def Abs_fresh_iff
by auto
+section {* Abstractions of single atoms *}
+
lemma Abs1_eq:
fixes x::"'a::fs"
shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
@@ -886,7 +887,7 @@
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
+ from set_renaming_perm2
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)"
@@ -906,7 +907,7 @@
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
+ from set_renaming_perm2
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)"
@@ -925,7 +926,7 @@
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
+ from 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)"