9 uses ("nominal_thmdecls.ML")

     9 uses ("nominal_thmdecls.ML")

    10      ("nominal_permeq.ML")

    10      ("nominal_permeq.ML")

    11 begin

    11 begin

    12 

    12 

    13 section {* Logical Operators *}

    13 section {* Logical Operators *}

    15 

    14 

    16 lemma eq_eqvt:

    15 lemma eq_eqvt:

    17   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"

    16   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"

    18   unfolding permute_eq_iff permute_bool_def ..

    17   unfolding permute_eq_iff permute_bool_def ..

    19 

    18 

   212 

   211 

   213 lemma snd_eqvt:

   212 lemma snd_eqvt:

   214   "p \<bullet> (snd x) = snd (p \<bullet> x)"

   213   "p \<bullet> (snd x) = snd (p \<bullet> x)"

   215  by (cases x) simp

   214  by (cases x) simp

   216 

   215 

   218 section {* Units *}

   216 section {* Units *}

   219 

   217 

   220 lemma supp_unit:

   218 lemma supp_unit:

   221   shows "supp () = {}"

   219   shows "supp () = {}"

   222   by (simp add: supp_def)

   220   by (simp add: supp_def)

   243   supp_eqvt fresh_eqvt

   241   supp_eqvt fresh_eqvt

   244   permute_pure

   242   permute_pure

   245 

   243 

   246   (* datatypes *)

   244   (* datatypes *)

   247   permute_prod.simps append_eqvt rev_eqvt set_eqvt

   245   permute_prod.simps append_eqvt rev_eqvt set_eqvt

   249 

   247 

   250   (* sets *)

   248   (* sets *)

   251   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt

   249   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt

   252   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt

   250   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt

   253 

   251