--- a/Nominal/Nominal2_Base.thy	Tue Jan 18 06:55:18 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 11:02:57 2011 +0100
@@ -518,6 +518,18 @@
   unfolding permute_set_eq
   using a by (auto simp add: swap_atom)
 
+lemma swap_set_in_eq:
+  assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
+  shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
+  unfolding permute_set_eq
+  using a by (auto simp add: swap_atom)
+
+lemma swap_set_both_in:
+  assumes a: "a \<in> S" "b \<in> S"
+  shows "(a \<rightleftharpoons> b) \<bullet> S = S"
+  unfolding permute_set_eq
+  using a by (auto simp add: swap_atom)
+
 lemma mem_permute_iff:
   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
   unfolding mem_def permute_fun_def permute_bool_def
@@ -1717,7 +1729,7 @@
 by (rule_tac S="supp p" in perm_struct_induct)
    (auto intro: zero swap)
 
-lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
+lemma perm_struct_induct2[consumes 1, case_names zero swap plus]:
   assumes S: "supp p \<subseteq> S"
   assumes zero: "P 0"
   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
@@ -1727,6 +1739,14 @@
 by (induct p rule: perm_struct_induct)
    (auto intro: zero plus swap simp add: supp_swap)
 
+lemma perm_simple_struct_induct2[case_names zero swap plus]:
+  assumes zero: "P 0"
+  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+by (rule_tac S="supp p" in perm_struct_induct2)
+   (auto intro: zero swap plus)
+
 lemma supp_perm_eq:
   assumes "(supp x) \<sharp>* p"
   shows "p \<bullet> x = x"
@@ -1751,7 +1771,7 @@
   from assms have "supp p \<subseteq> {a. a \<sharp> x}"
     unfolding supp_perm fresh_star_def fresh_def by auto
   then show "p \<bullet> x = x"
-  proof (induct p rule: perm_subset_induct)
+  proof (induct p rule: perm_struct_induct2)
     case zero
     show "0 \<bullet> x = x" by simp
   next
@@ -1925,7 +1945,6 @@
 
 section {* Renaming permutations *}
 
-
 lemma set_renaming_perm:
   assumes b: "finite bs"
   shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"