--- 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 {*