--- a/Nominal/Nominal2_Abs.thy Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy Tue Jan 18 06:55:18 2011 +0100
@@ -250,6 +250,102 @@
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_set:
+ assumes a: "(as, x) \<approx>set (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 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 supp_property_list:
+ assumes a: "(as, x) \<approx>lst (op =) supp p (as', x')"
+ shows "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'"
+proof -
+ from a have "(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)
+ have "(supp x' - set as') \<union> (supp x' \<inter> set 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 - set as) \<union> (supp x \<inter> set as))" by auto
+ also have "\<dots> = (p \<bullet> (supp x - set as)) \<union> (p \<bullet> (supp x \<inter> set as))" by (simp add: union_eqvt)
+ also have "\<dots> = (supp x - set as) \<union> (p \<bullet> (supp x \<inter> set as))" using * by simp
+ also have "\<dots> = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" using a by (simp add: alphas)
+ finally
+ have "(supp x' - set as') \<union> (supp x' \<inter> set as') = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" .
+ moreover
+ have "(supp x' - set as') \<inter> (supp x' \<inter> set as') = {}" by auto
+ moreover
+ have "(supp x - set as) \<inter> (supp x \<inter> set as) = {}" by auto
+ then have "p \<bullet> ((supp x - set as) \<inter> (supp x \<inter> set as) = {})" by (simp add: permute_bool_def)
+ then have "(p \<bullet> (supp x - set as)) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" by (perm_simp) (simp)
+ then have "(supp x - set as) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using * by simp
+ then have "(supp x' - set as') \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using a by (simp add: alphas)
+ ultimately show "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'"
+ by (auto dest: disjoint_right_eq)
+qed
+
+
+
+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"
@@ -550,7 +646,8 @@
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 *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+ 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 **
@@ -558,8 +655,8 @@
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
+ 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:
@@ -569,7 +666,8 @@
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 *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+ 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 **
@@ -577,8 +675,8 @@
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
+ 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:
@@ -587,7 +685,8 @@
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 *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
+ 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 **
@@ -595,8 +694,8 @@
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
+ 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
--- a/Nominal/Nominal2_Base.thy Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Base.thy Tue Jan 18 06:55:18 2011 +0100
@@ -1785,7 +1785,22 @@
by (metis permute_minus_cancel permute_plus)
qed
-
+lemma atom_set_perm_eq:
+ assumes a: "as \<sharp>* p"
+ shows "p \<bullet> as = as"
+proof -
+ from a have "supp p \<subseteq> {a. a \<notin> as}"
+ unfolding supp_perm fresh_star_def fresh_def by auto
+ then show "p \<bullet> as = as"
+ proof (induct p rule: perm_struct_induct)
+ case zero
+ show "0 \<bullet> as = as" by simp
+ next
+ case (swap p a b)
+ then have "a \<notin> as" "b \<notin> as" "p \<bullet> as = as" by simp_all
+ then show "((a \<rightleftharpoons> b) + p) \<bullet> as = as" by (simp add: swap_set_not_in)
+ qed
+qed
section {* Avoiding of atom sets *}
@@ -1910,38 +1925,34 @@
section {* Renaming permutations *}
+
lemma set_renaming_perm:
assumes b: "finite bs"
- shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+ shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
using b
proof (induct)
case empty
- have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
+ have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
by (simp add: permute_set_eq supp_perm)
- then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
+ then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
next
case (insert a bs)
- then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs"
- by (simp add: insert_eqvt)
- then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast
+ then have " \<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" by simp
+ then obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs"
+ by (metis empty_subsetI insert(3) supp_swap)
{ assume 1: "q \<bullet> a = p \<bullet> a"
- have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
+ have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp
moreover
have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
using ** by (auto simp add: insert_eqvt)
ultimately
- have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+ have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
}
moreover
{ assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
- { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
- moreover
- have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
- ultimately
- have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def
- by (simp add: insert_eqvt swap_set_not_in)
- }
+ have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def
+ by (auto simp add: swap_atom)
moreover
{ have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
using **
@@ -1961,45 +1972,38 @@
unfolding q'_def using supp_plus_perm by blast
}
ultimately
- have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+ have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
}
- ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ ultimately show "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
by blast
qed
+
lemma list_renaming_perm:
- fixes bs::"atom list"
- shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
+ shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)"
proof (induct bs)
case Nil
- have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
- by (simp add: permute_set_eq supp_perm)
- then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
+ have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
+ by (simp add: supp_zero_perm)
+ then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
next
case (Cons a bs)
- then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"
- by (simp add: insert_eqvt)
- then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast
+ then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by simp
+ then 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)
{ assume 1: "a \<in> set bs"
have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
- then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp
+ then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp
moreover
have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
ultimately
- have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+ have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
}
moreover
{ assume 2: "a \<notin> set bs"
def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
- { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric]
- by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
- moreover
- have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs`
- by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
- ultimately
- have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def
- by (simp add: swap_fresh_fresh)
- }
+ have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b"
+ unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp add: swap_atom)
moreover
{ have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
using **
@@ -2019,14 +2023,13 @@
unfolding q'_def using supp_plus_perm by blast
}
ultimately
- have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+ have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
}
- ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
by blast
qed
-
section {* Concrete Atoms Types *}
text {*
--- a/Nominal/Nominal2_Eqvt.thy Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy Tue Jan 18 06:55:18 2011 +0100
@@ -113,11 +113,6 @@
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
by (perm_simp add: permute_minus_cancel) (rule refl)
-lemma ex1_eqvt[eqvt]:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
- unfolding Ex1_def
- by (perm_simp) (rule refl)
-
lemma ex1_eqvt2:
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
by (perm_simp add: permute_minus_cancel) (rule refl)