--- a/Nominal/Abs.thy	Sat Mar 20 04:51:26 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 20 13:50:00 2010 +0100
@@ -377,128 +377,6 @@
 apply(simp add: eqvts)
 done
 
-lemma perm_zero:
-  assumes a: "\<forall>x::atom. p \<bullet> x = x"
-  shows "p = 0"
-using a
-by (simp add: expand_perm_eq)
-
-fun
-  add_perm 
-where
-  "add_perm [] = 0"
-| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
-
-fun
-  elem_perm
-where
-  "elem_perm [] = {}"
-| "elem_perm ((a, b) # xs) = {a, b} \<union> elem_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_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(drule perm_zero)
-apply(simp)
-apply(rule_tac x="[]" in exI)
-apply(simp add: supp_Nil)
-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(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 left_minus minus_unique 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
-
-lemma tt0:
-  fixes p::perm
-  shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"
-apply(auto simp add: fresh_star_def supp_perm fresh_def)
-done
-
-lemma uu0:
-  shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"
-apply(induct xs rule: add_perm.induct)
-apply(simp)
-apply(simp add: swap_fresh_fresh)
-done
-
-lemma yy0:
-  fixes xs::"(atom \<times> atom) list"
-  shows "supp xs = elem_perm xs"
-apply(induct xs rule: elem_perm.induct)
-apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)
-done
-
-lemma tt1:
-  shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-apply(drule tt0)
-apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")
-prefer 2
-apply(rule perm_list_exists)
-apply(erule exE)
-apply(simp only: yy0)
-apply(rule uu0)
-apply(auto)
-done
-
 
 lemma perm_induct_test:
   fixes P :: "perm => bool"
@@ -509,10 +387,6 @@
   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)
 oops
 
 lemma ii:
@@ -618,13 +492,13 @@
 apply(case_tac "a \<notin> supp x")
 apply(simp)
 apply(subgoal_tac "supp x \<sharp>* p")
-apply(drule tt1)
+apply(drule supp_perm_eq)
 apply(simp)
 apply(simp)
 apply(simp)
 apply(case_tac "a \<notin> supp y")
 apply(simp)
-apply(drule tt1)
+apply(drule supp_perm_eq)
 apply(clarify)
 apply(simp (no_asm_use))
 apply(simp)
@@ -635,7 +509,7 @@
 apply(simp)
 apply(case_tac "a \<sharp> p")
 apply(subgoal_tac "supp y \<sharp>* p")
-apply(drule tt1)
+apply(drule supp_perm_eq)
 apply(clarify)
 apply(simp (no_asm_use))
 apply(metis)