# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271859858 -7200
# Node ID 289988027abfb3bef4a6b26a660f7d72c88717f4
# Parent  ec45c81d1ca6102cb9d81416c26579dfca3c97ac
added a variant of the induction principle for permutations

diff -r ec45c81d1ca6 -r 289988027abf Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 12:38:20 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 16:24:18 2010 +0200
@@ -433,6 +433,13 @@
   qed
 qed
 
+lemma perm_struct_induct2[case_names zero swap]:
+  assumes zero: "P 0"
+  assumes swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  shows "P p"
+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]:
   assumes S: "supp p \<subseteq> S"
   assumes zero: "P 0"