# HG changeset patch
# User urbanc
# Date 1144337380 -7200
# Node ID 2e1c7ca05ee0d81a1940d84d8e6b1d1494c97d2a
# Parent  36e537f89585a07c1546ffaecbf22c7b20a59d50
modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem

also deleted the perm_compose' rule from the set
of rules that are automatically tried

diff -r 36e537f89585 -r 2e1c7ca05ee0 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 06 16:13:17 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 06 17:29:40 2006 +0200
@@ -54,16 +54,54 @@
 	    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 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)
+      (* applies the pt_perm_compose lemma              *)
+      (*                                                *)
+      (*     pi1 o (pi2 o x) = (pi1 o pi2) o (pi1 o x)  *)
+      (*                                                *)
+      (* in the restricted case where pi1 is a swapping *)
+      (* (a b) coming from a "supports problem"; in     *)
+      (* this rule would cause loops in the simplifier  *) 
+      val pt_perm_compose = thm "pt_perm_compose";
+	  
+      fun perm_compose_simproc i sg ss redex =
+      (case redex of
+        (Const ("nominal.perm", _) $ (pi1 as Const ("List.list.Cons", _) $
+         (Const ("Pair", _) $ Free (a as (_, T as Type (tname, _))) $ Free b) $ 
+           Const ("List.list.Nil", _)) $ (Const ("nominal.perm", 
+            Type ("fun", [Type ("List.list", [Type ("*", [U, _])]), _])) $ pi2 $ t)) =>
+        let
+            val ({bounds = (_, xs), ...}, _) = rep_ss ss
+            val ai = find_index (fn (x, _) => x = a) xs
+	    val bi = find_index (fn (x, _) => x = b) xs
+	    val tname' = Sign.base_name tname
+        in
+            if ai = length xs - i - 1 andalso 
+               bi = length xs - i - 2 andalso 
+               T = U andalso pi1 <> pi2 then
+                SOME (Drule.instantiate'
+	              [SOME (ctyp_of sg (fastype_of t))]
+		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
+		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
+	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose)))
+            else NONE
+        end
+       | _ => NONE);
+
+      fun perm_compose i =
+	Simplifier.simproc (the_context()) "perm_compose" 
+	["nominal.perm [(a, b)] (nominal.perm pi t)"] (perm_compose_simproc i);
+         
+      (* 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 perm_pi_simp  = dynamic_thms ss "perm_pi_simp"
+      val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
     in
       ("general simplification step", 
-        FIRST [rtac conjI i, asm_full_simp_tac (ss' addsimprocs [perm_eval]) i])
+        FIRST [rtac conjI i, 
+               SUBGOAL (fn (g, i) => asm_full_simp_tac 
+                 (ss' addsimprocs [perm_eval,perm_compose (length (Logic.strip_params g)-2)]) i) i])
     end;
 
 (* applies the perm_compose rule - this rule would loop in the simplifier     *)
@@ -114,7 +152,7 @@
     if n=0 then K all_tac
     else DETERM o 
          (FIRST'[fn i => tactical (perm_eval_tac ss i),
-                 fn i => tactical (apply_perm_compose_tac ss i),
+                 (*fn i => tactical (apply_perm_compose_tac ss i),*)
 		 fn i => tactical (apply_cong_tac i), 
                  fn i => tactical (unfold_perm_fun_def_tac i),
 		 fn i => tactical (expand_fun_eq_tac i)]