1 theory Abs

     1 theory Abs

     2 imports "../Nominal-General/Nominal2_Atoms" 

     2 imports "../Nominal-General/Nominal2_Atoms" 

     3         "../Nominal-General/Nominal2_Eqvt" 

     3         "../Nominal-General/Nominal2_Eqvt" 

     4         "../Nominal-General/Nominal2_Supp" 

     4         "../Nominal-General/Nominal2_Supp" 

     6         "Quotient" 

     5         "Quotient" 

     7         "Quotient_Product" 

     7         "Quotient_Product" 

     8 begin

     8 begin

     9 

     9 

    10 fun

    10 fun

    11   alpha_gen 

    11   alpha_gen 

   395   unfolding supp_abs

   395   unfolding supp_abs

   396   by auto

   396   by auto

   397 

   397 

   398 section {* BELOW is stuff that may or may not be needed *}

   398 section {* BELOW is stuff that may or may not be needed *}

   399 

   399 

   401 lemma supp_atom_image:

   400 lemma supp_atom_image:

   402   fixes as::"'a::at_base set"

   401   fixes as::"'a::at_base set"

   403   shows "supp (atom ` as) = supp as"

   402   shows "supp (atom ` as) = supp as"

   404 apply(simp add: supp_def)

   403 apply(simp add: supp_def)

   405 apply(simp add: image_eqvt)

   404 apply(simp add: image_eqvt)

   407 apply(simp add: atom_image_cong)

   406 apply(simp add: atom_image_cong)

   408 done

   407 done

   409 

   408 

   410 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"

   409 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"

   411   apply (simp add: fresh_def)

   410   apply (simp add: fresh_def)