src/HOL/Nominal/nominal_permeq.ML

 (* $Id$ *)
 
 (* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
-
-(* tries until depth 40 the following (in that order):                     *)
-(*                                                                         *)
-(*  - simplification plus analysing perm_swaps, perm_fresh_fresh, perm_bij *)
-(*  - permutation compositions (on the left hand side of =)                *)
-(*  - simplification of permutation on applications and abstractions       *)
-(*  - analysing congruences (from Stefan Berghofer's datatype pkg)         *)
-(*  - unfolding permutation on functions                                   *)
-(*  - expanding equalities of functions                                    *)
-(*                                                                         *)
-(*  for supports - it first unfolds the definitions and strips of intros   *)
 
 local
 
 (* pulls out dynamically a thm via the simpset *)
 fun dynamic_thms ss name = 
     ProofContext.get_thms (Simplifier.the_context ss) (Name name);
+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 initial_simp_tac ss i =
+fun perm_eval_tac ss i =
     let
+        val perm_eq_app   = thm "nominal.pt_fun_app_eq";
+        val at_inst       = dynamic_thm ss "at_name_inst";
+        val pt_inst       = dynamic_thm ss "pt_name_inst";
+
+        fun perm_eval_simproc sg ss redex =
+        (case redex of 
+        (* case pi o (f x) == (pi o f) (pi o x)    *)
+        (* special treatment in cases of constants *)
+        (Const("nominal.perm",Type("fun",[Type("List.list",[Type("*",[ty,_])]),_])) $ pi $ (f $ x)) 
+        => let
+             val _ = warning ("type: "^Sign.string_of_typ (sign_of (the_context())) ty)
+           in
+
+           (case f of
+                    (* nothing to do on constants *)
+                    (* FIXME: proper treatment of constants *)
+                      Const(_,_)                   => NONE
+                    | (Const(_,_) $ _)             => NONE
+                    | ((Const(_,_) $ _) $ _)       => NONE
+                    | (((Const(_,_) $ _) $ _) $ _) => NONE
+                    | _ => 
+                       (* FIXME: analyse type here or at "pty"*)
+		       SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection))
+            end
+
+        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
+        | (Const("nominal.perm",_) $ pi $ (Abs _)) 
+        => let 
+             val perm_fun_def = thm "nominal.perm_fun_def"
+           in SOME (perm_fun_def) end
+
+        (* no redex otherwise *) 
+        | _ => NONE);
+
+	val perm_eval =
+	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
+	    ["nominal.perm pi x"] perm_eval_simproc;
+
         (* these lemmas are created dynamically according to the atom types *) 
-	val perm_swap  = dynamic_thms ss "perm_swap";
-        val perm_fresh = dynamic_thms ss "perm_fresh_fresh";
-        val perm_bij   = dynamic_thms ss "perm_bij";
-        val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij)
+	val perm_swap     = dynamic_thms ss "perm_swap";
+        val perm_fresh    = dynamic_thms ss "perm_fresh_fresh";
+        val perm_bij      = dynamic_thms ss "perm_bij";
+        val perm_compose' = dynamic_thms ss "perm_compose'";
+        val perm_pi_simp  = dynamic_thms ss "perm_pi_simp";
+        val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp)
+                     addsimprocs [perm_eval];
+                    
     in
       ("general simplification step", FIRST [rtac conjI i, asm_full_simp_tac ss' i])
     end;
 
 (* applies the perm_compose rule - this rule would loop in the simplifier     *)
 (* in case there are more atom-types we have to check every possible instance *)
-(* of perm_compose *)
+(* of perm_compose                                                            *)
 fun apply_perm_compose_tac ss i = 
     let
 	val perm_compose = dynamic_thms ss "perm_compose"; 
         val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
     in
 	("analysing permutation compositions on the lhs",FIRST (tacs))
-    end
-
-(* applies the perm_eq_lam and perm_eq_app simplifications     *)
-(* FIXME: it seems the order of perm_app_eq and perm_lam_eq is *)
-(* significant                                                 *)   
-fun apply_app_lam_simp_tac ss i =
-    let 
-	val perm_app_eq  = dynamic_thms ss "perm_app_eq";
-        val perm_lam_eq  = thm "nominal.perm_eq_lam"
-    in
-     ("simplification of permutations on applications and lambdas", 
-      asm_full_simp_tac (HOL_basic_ss addsimps (perm_app_eq@[perm_lam_eq])) i)
     end
 
 (* applying Stefan's smart congruence tac *)
 fun apply_cong_tac i = 
     ("application of congruence",

     EVERY [CHANGED tac, print_tac ("after "^msg)]; 
 fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
 
 (* Main Tactic *)
 
-(* "repeating"-depth is set to 40 - this seems sufficient *)
 fun perm_simp_tac tactical ss i = 
+    DETERM (tactical (perm_eval_tac ss i));
+
+(* perm_simp_tac plus additional tactics to decide            *)
+(* support problems                                           *)
+(* the "repeating"-depth is set to 40 - this seems sufficient *)
+fun perm_supports_tac tactical ss i = 
     DETERM (REPEAT_DETERM_N 40 
-      (FIRST[tactical (initial_simp_tac ss i),
+      (FIRST[tactical (perm_eval_tac ss i),
              tactical (apply_perm_compose_tac ss i),
-             tactical (apply_app_lam_simp_tac ss i),
              tactical (apply_cong_tac i), 
              tactical (unfold_perm_fun_def_tac i),
              tactical (expand_fun_eq_tac i)]));
 
-(* tactic that first unfolds the support definition *)
-(* and strips of intros, then applies perm_simp_tac *)
+(* tactic that first unfolds the support definition          *)
+(* and strips off the intros, then applies perm_supports_tac *)
 fun supports_tac tactical ss i =
   let 
       val supports_def = thm "nominal.op supports_def";
       val fresh_def    = thm "nominal.fresh_def";
       val fresh_prod   = thm "nominal.fresh_prod";

   in
       EVERY [tactical ("unfolding of supports ",simp_tac (HOL_basic_ss addsimps simps) i),
              tactical ("stripping of foralls  " ,REPEAT_DETERM (rtac allI i)),
              tactical ("geting rid of the imps",rtac impI i),
              tactical ("eliminating conjuncts ",REPEAT_DETERM (etac  conjE i)),
-             tactical ("applying perm_simp    ",perm_simp_tac tactical ss i)]
+             tactical ("applying perm_simp    ",perm_supports_tac tactical ss i)]
   end;
 
 in