added generalised definitions for freshness of sets of atoms
authorurbanc
Thu Apr 03 11:48:48 2008 +0200 (2008-04-03)
changeset 26522b05cdd060c3e
parent 26521 f8c4e79db153
child 26523 18ccad3ecb2e
added generalised definitions for freshness of sets of atoms
and lists of atoms
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Apr 02 15:58:57 2008 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Apr 03 11:48:48 2008 +0200
     1.3 @@ -393,6 +393,19 @@
     1.4    Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
     1.5  *}
     1.6  
     1.7 +section {* generalisation of freshness to lists and sets of atoms *}
     1.8 +(*================================================================*)
     1.9 + 
    1.10 +consts
    1.11 +  fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
    1.12 +
    1.13 +defs (overloaded)
    1.14 +  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
    1.15 +
    1.16 +defs (overloaded)
    1.17 +  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
    1.18 +
    1.19 +lemmas fresh_star_def = fresh_star_list fresh_star_set
    1.20  
    1.21  section {* Abstract Properties for Permutations and  Atoms *}
    1.22  (*=========================================================*)