# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270589620 -7200
# Node ID 4f41a0884b22a198e9f47f5e2524e88b334a0f22
# Parent  0c958e385691ab35e4778b747d2514b5d67773df
isarfied proof about existence of a permutation list

diff -r 0c958e385691 -r 4f41a0884b22 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Tue Apr 06 14:08:06 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Tue Apr 06 23:33:40 2010 +0200
@@ -385,69 +385,68 @@
 by (induct xs arbitrary: ys)
    (auto simp add: add_assoc)
 
+(* 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"
-apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
-apply(rename_tac p)
-apply(case_tac "supp p = {}")
-apply(simp)
-apply(simp add: supp_perm)
-apply(rule_tac x="[]" in exI)
-apply(simp add: supp_Nil)
-apply(simp add: expand_perm_eq)
-apply(subgoal_tac "\<exists>x. x \<in> supp p")
-defer
-apply(auto)[1]
-apply(erule exE)
-apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
-apply(drule mp)
-defer
-apply(erule exE)
-apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
-apply(simp add: add_perm_append)
-apply(erule conjE)
-apply(drule sym)
-apply(simp)
-apply(simp add: expand_perm_eq)
-apply(simp add: supp_append)
-apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)
-apply(rule conjI)
-prefer 2
-apply(auto)[1]
-apply (metis permute_atom_def_raw permute_minus_cancel(2))
-defer
-apply(rule psubset_card_mono)
-apply(simp add: finite_supp)
-apply(rule psubsetI)
-defer
-apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
-apply(blast)
-apply(simp add: supp_perm)
-defer
-apply(auto simp add: supp_perm)[1]
-apply(case_tac "x = xa")
-apply(simp)
-apply(case_tac "((- p) \<bullet> x) = xa")
-apply(simp)
-apply(case_tac "sort_of xa = sort_of x")
-apply(simp)
-apply(auto)[1]
-apply(simp)
-apply(simp)
-apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")
-apply(blast)
-apply(auto simp add: supp_perm)[1]
-apply(case_tac "x = xa")
-apply(simp)
-apply(case_tac "((- p) \<bullet> x) = xa")
-apply(simp)
-apply(case_tac "sort_of xa = sort_of x")
-apply(simp)
-apply(auto)[1]
-apply(simp)
-apply(simp)
-done
+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)
+    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
+    { 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)
+    }
+    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)
+      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))
+      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
+    }
+    ultimately show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast
+  qed
+qed
 
 section {* Lemma about support and permutations *}