# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271846239 -7200
# Node ID e2e963f4e90dbcfed491dfc6a2a8f97340b9bda3
# Parent  39951d71bfceb3640b8908f74d8887ffa3f73bd1
added an improved version of the induction principle for permutations

diff -r 39951d71bfce -r e2e963f4e90d Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 10:09:07 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 12:37:19 2010 +0200
@@ -392,15 +392,16 @@
 
 text {* Induction principle for permutations *}
 
-lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]:
+
+lemma perm_struct_induct[consumes 1, case_names zero swap]:
   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)"
+  assumes swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> 
+    \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
   shows "P p"
 proof -
   have "finite (supp p)" by (simp add: finite_supp)
-  then show ?thesis using S
+  then show "P p" using S
   proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
     case (psubset p)
     then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
@@ -412,23 +413,20 @@
     moreover
     { assume "supp p \<noteq> {}"
       then obtain a where a0: "a \<in> supp p" by blast
-      then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as
+      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as
 	by (auto simp add: supp_atom supp_perm swap_atom)
-      let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)"
+      let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
       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" using as by auto
+      ultimately have "supp ?q \<subset> supp p" using a2 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
+      ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 
       moreover 
-      have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq)
+      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
       ultimately have "P p" by simp
     }
     ultimately show "P p" by blast
@@ -441,9 +439,9 @@
   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
+using S
+by (induct p rule: perm_struct_induct)
+   (auto intro: zero plus swap simp add: supp_swap)
 
 lemma supp_perm_eq:
   assumes "(supp x) \<sharp>* p"
@@ -452,6 +450,23 @@
   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_struct_induct)
+    case zero
+    show "0 \<bullet> x = x" by simp
+  next
+    case (swap p a b)
+    then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
+    then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+  qed
+qed
+
+lemma supp_perm_eq_test:
+  assumes "(supp x) \<sharp>* p"
+  shows "p \<bullet> x = x"
+proof -
+  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