# HG changeset patch
# User urbanc
# Date 1141233980 -3600
# Node ID 20a73345dd6e255340e0ad4f438650dc1afa69b5
# Parent  c8faffc8e6fb7db1294ce432bcab59211825f852
fixed a problem where a permutation is not analysed
when the term is of the form

   (pi o f) x1...xn

This was the case because the head of this term is the
constant "nominal.perm". Now an applicability predicate
decides the right behaviour of the simproc

diff -r c8faffc8e6fb -r 20a73345dd6e src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 01 18:24:31 2006 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 01 18:26:20 2006 +0100
@@ -10,18 +10,29 @@
 fun dynamic_thm ss name = 
     ProofContext.get_thm (Simplifier.the_context ss) (Name name);
 
-(* FIXME: make it usable for all atom-types *)
 (* initial simplification step in the tactic *)
 fun perm_eval_tac ss i =
     let
         fun perm_eval_simproc sg ss redex =
+        let 
+	   
+           (* the "application" case below is only applicable when the head   *)
+           (* of f is not a constant  or when it is a permuattion with two or *) 
+           (* more arguments                                                  *)
+           fun applicable t = 
+	       (case (strip_comb t) of
+		  (Const ("nominal.perm",_),ts) => (length ts) >= 2
+		| (Const _,_) => false
+		| _ => true)
+
+	in
         (case redex of 
-        (* case pi o (f x) == (pi o f) (pi o x)            *)
-        (* special treatment when head of f is a constants *)
+        (* case pi o (f x) == (pi o f) (pi o x)          *)
+        (* special treatment according to the head of f  *)
         (Const("nominal.perm",
-           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
-           (case (head_of f) of
-                Const _ => NONE     (* nothing to do on constants *)
+          Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
+	   (case (applicable f) of
+                false => NONE  
               | _ => 
 		let
 		    val name = Sign.base_name n
@@ -37,7 +48,7 @@
            in SOME (perm_fun_def) end
 
         (* no redex otherwise *) 
-        | _ => NONE);
+        | _ => NONE) end
 
 	val perm_eval =
 	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
@@ -87,7 +98,7 @@
 
 (* debugging *)
 fun DEBUG_tac (msg,tac) = 
-    EVERY [CHANGED tac, print_tac ("after "^msg)]; 
+    CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
 fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
 
 (* Main Tactic *)