# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267639840 -3600
# Node ID 5b31e49678fc0b45a39ba13f6a29c143b9a761f3
# Parent  103eb390f1b1a82fbe42e2584ee6769dd5bdeb90
added a lemma that permutations can be represented as sums of swapping

diff -r 103eb390f1b1 -r 5b31e49678fc Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Mar 03 14:46:14 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 03 19:10:40 2010 +0100
@@ -415,48 +415,104 @@
 apply(simp add: supp_swap)
 done
 
+lemma perm_zero:
+  assumes a: "\<forall>x::atom. p \<bullet> x = x"
+  shows "p = 0"
+using a
+by (simp add: expand_perm_eq)
 
-thm supp_perm
+fun
+  add_perm 
+where
+  "add_perm [] = 0"
+| "add_perm ((a,b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
+
+lemma add_perm_apend:
+  shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
+apply(induct xs arbitrary: ys)
+apply(auto simp add: add_assoc)
+done
 
-(* 
-lemma perm_induct_test:
-  fixes P :: "perm => bool"
-  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>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
-  shows "P p"
-sorry
+lemma
+  fixes p::perm
+  shows "\<exists>xs. p = add_perm xs"
+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(drule perm_zero)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+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_apend)
+apply(drule sym)
+apply(simp)
+apply(simp add: expand_perm_eq)
+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)
+apply(auto simp add: supp_perm)
+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
 
 lemma tt1:
-  assumes a: "finite (supp p)"
-  shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-using a
-unfolding fresh_star_def fresh_def
-apply(induct F\<equiv>"supp p" arbitrary: p rule: finite.induct)
-apply(simp add: supp_perm)
-defer
-apply(case_tac "a \<in> A")
-apply(simp add: insert_absorb)
-apply(subgoal_tac "A = supp p - {a}")
-prefer 2
-apply(blast)
-apply(case_tac "p \<bullet> a = a")
-apply(simp add: supp_perm)
-apply(drule_tac x="p + (((- p) \<bullet> a) \<rightleftharpoons> a)" in meta_spec)
+  shows "(supp x) \<sharp>* add_perm xs \<Longrightarrow> (add_perm xs) \<bullet> x = x"
+apply(induct xs rule: add_perm.induct)
+apply(simp)
+apply(simp)
+apply(case_tac "a = b")
 apply(simp)
 apply(drule meta_mp)
-apply(rule subset_antisym)
-apply(rule subsetI)
-apply(simp)
-apply(simp add: supp_perm)
-apply(case_tac "xa = p \<bullet> a")
-apply(simp)
-apply(case_tac "p \<bullet> a = (- p) \<bullet> a")
-apply(simp)
 defer
 apply(simp)
+apply(rule swap_fresh_fresh)
+apply(simp add: fresh_def)
+apply(auto)[1]
+apply(simp add: fresh_star_def fresh_def supp_perm)
+apply(drule_tac x="a" in bspec)
+apply(simp)
 oops
 
+
+lemma perm_induct_test:
+  fixes P :: "perm => bool"
+  assumes fin: "finite (supp p)" 
+  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>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+using fin
+apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)
+apply(simp add: supp_perm)
+apply(drule perm_zero)
+apply(simp add: zero)
+apply(rotate_tac 3)
+sorry
+
+
+
 lemma tt:
   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
 apply(induct p rule: perm_induct_test)