# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271575598 -7200
# Node ID f4477d3fe520849001f1b0968714afba61fcf2b4
# Parent  6d4e4bf9bce661b00bbb2f6084c1fe7e29576ea5
preliminary parser for perm_simp metod

diff -r 6d4e4bf9bce6 -r f4477d3fe520 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 16 16:29:11 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 18 09:26:38 2010 +0200
@@ -289,14 +289,21 @@
 use "nominal_permeq.ML"
 setup Nominal_Permeq.setup
 
+ML {*
+val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
+val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
+  (Scan.repeat (Args.const true))) []
+*}
+
 method_setup perm_simp =
- {* Attrib.thms >> 
-    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}
+ {* test1 -- test2 >> 
+    (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
  {* pushes permutations inside *}
 
 method_setup perm_strict_simp =
- {* Attrib.thms >> 
-    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *}
+ {* test1 -- test2 >> 
+    (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL 
+       (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
  {* pushes permutations inside, raises an error if it cannot solve all permutations *}
 
 declare [[trace_eqvt = true]]
@@ -369,9 +376,8 @@
 
 text {* Problem: there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
-apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*})
-apply(perm_simp)
-(* apply(perm_strict_simp) *)
+apply(perm_strict_simp exclude: The)
+apply(perm_simp exclude: The)
 oops
 
 (* automatic equivariance procedure for 
diff -r 6d4e4bf9bce6 -r f4477d3fe520 Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Fri Apr 16 16:29:11 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Sun Apr 18 09:26:38 2010 +0200
@@ -5,8 +5,8 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-(* this should not be a raw equivariant rule *)
-(* we force it to be                         *)
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
 thm eqvts
 (*declare permute_pure[eqvt]*)