Added lemma at_fin_set_fresh.
authorberghofe
Thu Jan 24 11:23:11 2008 +0100 (2008-01-24)
changeset 25950a3067f6f08a2
parent 25949 850b4c2d0f17
child 25951 6ebe26bfed18
Added lemma at_fin_set_fresh.
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Jan 23 23:35:23 2008 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Jan 24 11:23:11 2008 +0100
     1.3 @@ -1947,6 +1947,13 @@
     1.4    then show "X\<subseteq>(supp X)" by blast
     1.5  qed
     1.6  
     1.7 +lemma at_fin_set_fresh:
     1.8 +  fixes X::"'x set" 
     1.9 +  assumes at: "at TYPE('x)"
    1.10 +  and     fs: "finite X"
    1.11 +  shows "(x \<sharp> X) = (x \<notin> X)"
    1.12 +  by (simp add: at_fin_set_supp fresh_def at fs)
    1.13 +
    1.14  section {* Permutations acting on Functions *}
    1.15  (*==========================================*)
    1.16