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 

   285   unfolding unpermute_def by simp

   286   unfolding unpermute_def by simp

   286 

   287 

   287 use "nominal_permeq.ML"

   288 use "nominal_permeq.ML"

   288 setup Nominal_Permeq.setup

   289 setup Nominal_Permeq.setup

   289 

   290 

   290 method_setup perm_simp =

   294 method_setup perm_simp =

   291  {* Attrib.thms >> 

   295  {* Attrib.thms >> 

   292     (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}

   296     (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}

   293  {* pushes permutations inside *}

   297  {* pushes permutations inside *}

   294 

   298 

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

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

   370 apply(perm_simp)

   374 apply(perm_simp)

   371 (* apply(perm_strict_simp) *)

   375 (* apply(perm_strict_simp) *)

   372 oops

   376 oops

   373 

   377 

   374 end

   380 end