# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265037204 -3600
# Node ID 83d5a7cd2cc682820dd9cc730778ad3c795dfa2d
# Parent  1dd314a00b0c25f3f9c73ab4ed81aa5af22ef32c
updated from nominal-huffman

diff -r 1dd314a00b0c -r 83d5a7cd2cc6 Quot/Nominal/Nominal2_Supp.thy
--- a/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 15:57:37 2010 +0100
+++ b/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:13:24 2010 +0100
@@ -345,23 +345,21 @@
   using not_fresh_nat_of [unfolded fresh_def] by auto
 
 
-(*
-section {* Characterisation of the support of sets of atoms *}
+section {* Support for sets of atoms *}
 
-lemma swap_set_ineq:
-  fixes a b::"'a::at"
-  assumes "a \<in> S" "b \<notin> S"
-  shows "(a \<leftrightarrow> b) \<bullet> S \<noteq> S"
-using assms
-unfolding permute_set_eq 
-by (auto simp add: permute_flip_at)
+lemma supp_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(auto simp add: permute_set_eq_vimage vimage_def swap_atom)[1]
+  apply(rule assms)
+  apply(auto simp add: permute_set_eq swap_atom)[1]
+done
 
-lemma supp_finite:
-  fixes S::"'a::at set"
-  assumes asm: "finite S"
-  shows "(supp S) = atom ` S"
-sorry
 
+(*
 lemma supp_infinite:
   fixes S::"atom set"
   assumes asm: "finite (UNIV - S)"