--- a/Nominal-General/Nominal2_Supp.thy	Tue Apr 06 23:33:40 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 07 17:37:29 2010 +0200
@@ -371,98 +371,80 @@
   apply(simp add: swap_set_in)
 done
 
-
-section {* transpositions of permutations *}
-
-fun
-  add_perm 
-where
-  "add_perm [] = 0"
-| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
-
-lemma add_perm_append:
-  shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
-by (induct xs arbitrary: ys)
-   (auto simp add: add_assoc)
+text {* Induction principle for permutations *}
 
-(* this induction is the fixed version of the one in Finite_Set.thy *)
-lemma finite_psubset_induct2[consumes 1, case_names psubset]:
-  assumes major: "finite A" 
-  and     minor: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A" 
-  shows "P A"
-using major
-proof (induct A taking: card rule: measure_induct_rule)
-  case (less A)
-  have fact: "finite A" by fact
-  have ih: "\<And>B. \<lbrakk>card B < card A; finite B\<rbrakk> \<Longrightarrow> P B" by fact
-  { fix B 
-    assume asm: "B \<subset> A"
-    from asm have "card B < card A" using psubset_card_mono fact by blast
-    moreover
-    from asm have "B \<subseteq> A" by auto
-    then have "finite B" using fact finite_subset by blast
-    ultimately 
-    have "P B" using ih by simp
-  }
-  then show "P A" using minor fact by blast
-qed
-
-lemma perm_list_exists:
-  fixes p::perm
-  shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
+lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]:
+  assumes S: "supp p \<subseteq> S"
+  assumes zero: "P 0"
+  assumes swap: "\<And>a b. supp (a \<rightleftharpoons> b) \<subseteq> S \<Longrightarrow> P (a \<rightleftharpoons> b)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
 proof -
   have "finite (supp p)" by (simp add: finite_supp)
-  then show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
-  proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct2)
+  then show ?thesis using S
+  proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
     case (psubset p)
-    have ih: "\<And>q. (supp q) \<subset> (supp p) \<Longrightarrow> (\<exists>xs. q = add_perm xs \<and> supp xs \<subseteq> supp q)" by fact
+    then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
+    have as: "supp p \<subseteq> S" by fact
     { assume "supp p = {}"
       then have "p = 0" by (simp add: supp_perm expand_perm_eq)
-      then have "p = add_perm [] \<and> supp [] \<subseteq> supp p" by (simp add: supp_Nil)
+      then have "P p" using zero by simp
     }
     moreover
     { assume "supp p \<noteq> {}"
       then obtain a where a0: "a \<in> supp p" by blast
-      let ?q = "p + (((- p) \<bullet> a) \<rightleftharpoons> a)"
-      have a1: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
+      then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as
+	by (auto simp add: supp_atom supp_perm swap_atom)
+      let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)"
+      have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
       moreover
       have "a \<notin> supp ?q" by (simp add: supp_perm)
       then have "supp ?q \<noteq> supp p" using a0 by auto
-      ultimately have "(supp ?q) \<subset> (supp p)" by auto
-      then obtain xs where a: "?q = add_perm xs" and b: "supp xs \<subseteq> supp ?q" using ih by blast
-      let ?xs' = "xs @ [((- p) \<bullet> a, a)]"
-      have "supp [(- p \<bullet> a, a)] \<subseteq> supp p" using a0
-	by (simp add: supp_Cons supp_Nil supp_Pair supp_atom supp_perm) (metis permute_minus_cancel(1))
+      ultimately have "supp ?q \<subset> supp p" using as by auto
+      then have "P ?q" using ih by simp
+      moreover
+      have "supp ?q \<subseteq> S" using as a2 by simp
+      moreover
+      have "P (- p \<bullet> a \<rightleftharpoons> a)" using a1 swap by simp
+      ultimately 
+      have "P (?q + (- p \<bullet> a \<rightleftharpoons> a))" using a1 plus by simp
       moreover 
-      have "supp xs \<subseteq> supp p" using b a1 by blast 
-      ultimately  
-      have"supp ?xs' \<subseteq> supp p" by (simp add: supp_append)
-      moreover
-      have "p = add_perm ?xs'" using a[symmetric]
-	by (simp add: add_perm_append expand_perm_eq)
-      ultimately 
-      have "p = add_perm ?xs' \<and> supp ?xs' \<subseteq> supp p" by simp
-      then have "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast
+      have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq)
+      ultimately have "P p" by simp
     }
-    ultimately show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast
+    ultimately show "P p" by blast
   qed
 qed
 
-section {* Lemma about support and permutations *}
+lemma perm_subset_induct [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)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+apply(rule perm_subset_induct_aux[OF S])
+apply(auto simp add: zero swap plus supp_swap split: if_splits)
+done
 
 lemma supp_perm_eq:
-  assumes a: "(supp x) \<sharp>* p"
+  assumes "(supp x) \<sharp>* p"
   shows "p \<bullet> x = x"
 proof -
-  obtain xs where eq: "p = add_perm xs" and sub: "supp xs \<subseteq> supp p"
-    using perm_list_exists by blast
-  from a have "\<forall>a \<in> supp p. a \<sharp> x"
-    by (auto simp add: fresh_star_def fresh_def supp_perm)
-  with eq sub have "\<forall>a \<in> supp xs. a \<sharp> x" by auto
-  then have "add_perm xs \<bullet> x = x" 
-    by (induct xs rule: add_perm.induct)
-       (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh)
-  then show "p \<bullet> x = x" using eq by simp
+  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)
+    case zero
+    show "0 \<bullet> x = x" by simp
+  next
+    case (swap a b)
+    then have "a \<sharp> x" "b \<sharp> x" by simp_all
+    then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+  next
+    case (plus p1 p2)
+    have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
+    then show "(p1 + p2) \<bullet> x = x" by simp
+  qed
 qed
 
 section {* at_set_avoiding2 *}