--- a/Nominal/TySch.thy	Thu Mar 11 17:49:07 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 11 19:24:07 2010 +0100
@@ -15,6 +15,23 @@
 datatype tyS =
   All "name set" "ty"
 
+lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s"
+apply (simp add: supp_def)
+apply (simp add: eqvts eqvts_raw)
+(* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*)
+sorry
+
+lemma atom_image_swap_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at) set); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+apply (simp add: fresh_def)
+apply (simp add: support_image)
+apply (fold fresh_def)
+apply (simp add: swap_fresh_fresh)
+done
+
+lemma "\<lbrakk>a \<sharp> atom ` fun; a \<sharp> t; b \<sharp> atom ` fun; b \<sharp> t\<rbrakk> \<Longrightarrow> All ((a \<rightleftharpoons> b) \<bullet> fun) t = All fun t"
+apply (simp add: atom_image_swap_fresh)
+done
+
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *}
 print_theorems