7 *)

     7 *)

     8 theory Nominal2_Eqvt

     8 theory Nominal2_Eqvt

     9 imports Nominal2_Base Nominal2_Atoms

     9 imports Nominal2_Base Nominal2_Atoms

    10 uses ("nominal_thmdecls.ML")

    10 uses ("nominal_thmdecls.ML")

    11      ("nominal_permeq.ML")

    11      ("nominal_permeq.ML")

    12 begin

    13 begin

    13 

    14 

    14 

    15 

    15 section {* Logical Operators *}

    16 section {* Logical Operators *}

    16 

    17 

   282 

   283 

   283 lemma eqvt_bound:

   284 lemma eqvt_bound:

   284   shows "p \<bullet> unpermute p x \<equiv> x"

   285   shows "p \<bullet> unpermute p x \<equiv> x"

   285   unfolding unpermute_def by simp

   286   unfolding unpermute_def by simp

   286 

   287 

   287 use "nominal_permeq.ML"

   289 use "nominal_permeq.ML"

   288 setup Nominal_Permeq.setup

   290 setup Nominal_Permeq.setup

   289 

   291 

   290 method_setup perm_simp =

   292 method_setup perm_simp =

   291  {* Attrib.thms >> 

   293  {* Attrib.thms >> 

   369 lemma "p \<bullet> (THE x. P x) = foo"

   371 lemma "p \<bullet> (THE x. P x) = foo"

   370 apply(perm_simp)

   372 apply(perm_simp)

   371 (* apply(perm_strict_simp) *)

   373 (* apply(perm_strict_simp) *)

   372 oops

   374 oops

   373 

   375 

   374 end

   380 end