1 (*  Title:      Atoms

     1 (*  Title:      Atoms

     2     Authors:    Brian Huffman, Christian Urban

     2     Authors:    Brian Huffman, Christian Urban

     3 

     3 

     4     Instantiations of concrete atoms 

     4     Instantiations of concrete atoms 

     5 *)

     5 *)

     6 theory Atoms

     7 theory Atoms

     7 imports Nominal2_Base

     8 imports Nominal2_Base

     9 begin

     9 begin

    10 

    10 

    11 

    11 

    12 

    12 

    13 section {* @{const nat_of} is an example of a function 

    13 section {* @{const nat_of} is an example of a function 

   223 

   223 

   224 declare [[coercion "atom::var1\<Rightarrow>atom"]]

   224 declare [[coercion "atom::var1\<Rightarrow>atom"]]

   225 

   225 

   226 declare [[coercion "atom::var2\<Rightarrow>atom"]]

   226 declare [[coercion "atom::var2\<Rightarrow>atom"]]

   227 

   227 

   229 lemma

   228 lemma

   230   fixes a::"var1" and b::"var2"

   229   fixes a::"var1" and b::"var2"

   231   shows "a \<sharp> t \<and> b \<sharp> t"

   230   shows "a \<sharp> t \<and> b \<sharp> t"

   232 oops

   231 oops

   234 

   233 

   235 (* does not yet work: it needs image as

   234 (* does not yet work: it needs image as

   236    coercion map *)

   235    coercion map *)

   237 

   236 

   238 lemma

   237 lemma