--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 09 21:51:01 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 10:36:09 2010 +0200
@@ -282,15 +282,19 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
-ML {* @{const Trueprop} *}
-
 use "nominal_permeq.ML"
 setup Nominal_Permeq.setup
 
 method_setup perm_simp =
- {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *}
+ {* Attrib.thms >> 
+    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}
  {* 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"]))) *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations *}
+
 declare [[trace_eqvt = true]]
 
 lemma 
@@ -352,13 +356,6 @@
 oops
 
 lemma 
-  fixes p q r::"perm"
-  and   x::"'a::pt"
-  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
-apply(perm_simp)
-oops
-
-lemma 
   fixes C D::"bool"
   shows "B (p \<bullet> (C = D))"
 apply(perm_simp)
@@ -369,6 +366,7 @@
 text {* Problem: there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
 apply(perm_simp)
+(* apply(perm_strict_simp) *)
 oops
 
 

--- a/Nominal-General/nominal_permeq.ML	Fri Apr 09 21:51:01 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Sun Apr 11 10:36:09 2010 +0200
@@ -1,59 +1,90 @@
-(*  Title:      nominal_thmdecls.ML
-    Author:     Brian Huffman, Christian Urban
+(*  Title:      nominal_permeq.ML
+    Author:     Christian Urban
+    Author:     Brian Huffman
 *)
 
 signature NOMINAL_PERMEQ =
 sig
-  val eqvt_tac: Proof.context -> thm list -> int -> tactic 
+  val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
+  val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
   val trace_eqvt: bool Config.T
   val setup: theory -> theory
 end;
 
-(* TODO:
+(* 
+
+- eqvt_tac and eqvt_strict_tac take a list of theorems
+  which are first tried to simplify permutations
+
+  the string list contains constants that should not be
+  analysed (for example there is no raw eqvt-lemma for
+  the constant The; therefore it should not be analysed 
 
- - provide a method interface with the usual add and del options
+- setting [[trace_eqvt = true]] switches on tracing 
+  information  
+
 
- - print a warning if for a constant no eqvt lemma is stored
+TODO:
+
+ - provide a proper parser for the method (see Nominal2_Eqvt)
+   
+ - proably the list of bad constant should be a dataslot
 
 *)
 
-
 structure Nominal_Permeq: NOMINAL_PERMEQ =
 struct
 
-fun is_head_Trueprop trm = 
-  case (head_of trm) of 
-    @{const "Trueprop"} => true 
-  | _ => false 
+open Nominal_ThmDecls;
 
-(* debugging infrastructure *)
+(* tracing infrastructure *)
 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
 
 fun trace_enabled ctxt = Config.get ctxt trace_eqvt
 
-fun trace_conv ctxt conv ct =
+fun trace_msg ctxt result = 
+let
+  val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
+  val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
+in
+  tracing (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
+end
+
+fun trace_conv ctxt conv ctrm =
+let
+  val result = conv ctrm
+in
+  if Thm.is_reflexive result 
+  then result
+  else (trace_msg ctxt result; result)
+end
+
+(* this conversion always fails, but prints 
+   out the analysed term  *)
+fun trace_info_conv ctxt ctrm = 
 let
-  val result = conv ct
-  val _ = 
-    if trace_enabled ctxt andalso not (Thm.is_reflexive result) 
-    then  
+  val trm = term_of ctrm
+  val _ = case (head_of trm) of 
+      @{const "Trueprop"} => ()
+    | _ => tracing ("Analysing term " ^ Syntax.string_of_term ctxt trm)
+in
+  Conv.no_conv ctrm
+end
+
+
+(* conversion for applications: 
+   only applies the conversion, if the head of the
+   application is not a "bad head" *)
+fun has_bad_head bad_hds trm = 
+  case (head_of trm) of 
+    Const (s, _) => member (op=) bad_hds s 
+  | _ => false 
+
+fun eqvt_apply_conv bad_hds ctrm =
+  case (term_of ctrm) of
+    Const (@{const_name "permute"}, _) $ _ $ (trm $ _) =>
       let
-        val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
-        val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
-      in
-        warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) 
-      end
-    else ()
-in
-  result
-end;
-
-(* conversion for applications *)
-fun eqvt_apply_conv ctxt ct =
-  case (term_of ct) of
-    (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
-      let
-        val (perm, t) = Thm.dest_comb ct
+        val (perm, t) = Thm.dest_comb ctrm
         val (_, p) = Thm.dest_comb perm
         val (f, x) = Thm.dest_comb t
         val a = ctyp_of_term x;
@@ -61,42 +92,65 @@
         val ty_insts = map SOME [b, a]
         val term_insts = map SOME [p, f, x]                        
       in
-        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+        if has_bad_head bad_hds trm
+        then Conv.no_conv ctrm
+        else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
-  | _ => Conv.no_conv ct
+  | _ => Conv.no_conv ctrm
 
 (* conversion for lambdas *)
-fun eqvt_lambda_conv ctxt ct =
-  case (term_of ct) of
-    (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
-      Conv.rewr_conv @{thm eqvt_lambda} ct
-  | _ => Conv.no_conv ct
+fun eqvt_lambda_conv ctrm =
+  case (term_of ctrm) of
+    Const (@{const_name "permute"}, _) $ _ $ (Abs _) =>
+      Conv.rewr_conv @{thm eqvt_lambda} ctrm
+  | _ => Conv.no_conv ctrm
+
+(* conversion that raises an error or prints a warning message, 
+   if a permutation on a constant or application cannot be analysed *)
+fun progress_info_conv ctxt strict_flag ctrm =
+let
+  fun msg trm = 
+    (if strict_flag then error else warning) 
+      ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+
+  val _ = case (term_of ctrm) of
+      Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
+    | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
+    | _ => () 
+in
+  Conv.all_conv ctrm 
+end
 
 
 (* main conversion *)
-fun eqvt_conv ctxt thms ctrm =
+fun eqvt_conv ctxt strict_flag thms bad_hds ctrm =
 let
-  val trm = term_of ctrm 
-  val _ = if trace_enabled ctxt andalso not (is_head_Trueprop trm)
-    then warning ("analysing " ^ Syntax.string_of_term ctxt trm) 
-    else ()
-  val wrapper = if trace_enabled ctxt then trace_conv ctxt else I			
+  val first_conv_wrapper = 
+    if trace_enabled ctxt 
+    then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
+    else Conv.first_conv
+
+  val pre_thms = thms @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt)
+  val post_thms = @{thms permute_pure[THEN eq_reflection]}
 in
-  Conv.first_conv (map wrapper
-    [ More_Conv.rewrs_conv thms,
-      Conv.rewr_conv @{thm eqvt_bound},
-      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
-      eqvt_apply_conv ctxt,
-      eqvt_lambda_conv ctxt,
-      More_Conv.rewrs_conv @{thms permute_pure[THEN eq_reflection]},
-      Conv.all_conv
-    ]) ctrm
+  first_conv_wrapper
+    [ More_Conv.rewrs_conv pre_thms,
+      eqvt_apply_conv bad_hds,
+      eqvt_lambda_conv,
+      More_Conv.rewrs_conv post_thms,
+      progress_info_conv ctxt strict_flag
+    ] ctrm
 end
 
+(* raises an error if some permutations cannot be eliminated *)
+fun eqvt_strict_tac ctxt thms bad_hds = 
+  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true thms bad_hds) ctxt)
 
-fun eqvt_tac ctxt thms = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt)
+(* prints a warning message if some permutations cannot be eliminated *)
+fun eqvt_tac ctxt thms bad_hds = 
+  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false thms bad_hds) ctxt)
 
+(* setup of the configuration value *)
 val setup =
   trace_eqvt_setup