--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 10:43:43 2011 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 19:09:06 2011 +0100
@@ -53,6 +53,16 @@
 apply(simp_all)
 done
 
+lemma TEST1:
+  assumes "x = Inl y"
+  shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"
+using assms by simp
+
+lemma TEST2:
+  assumes "x = Inr y"
+  shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"
+using assms by simp
+
 lemma test:
   assumes a: "\<exists>y. f x = Inl y"
   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
@@ -275,6 +285,30 @@
   apply blast
   done
 
+
+termination (eqvt) by lexicographic_order
+
+thm subst_substs.eqvt[no_vars]
+thm subst_def
+thm substs_def
+thm Sum_Type.Projr.simps
+
+lemma
+ shows "(p \<bullet> subst x y) = subst (p \<bullet> x) (p \<bullet> y)"
+ and   "(p \<bullet> substs x' y') = substs (p \<bullet> x') (p \<bullet> y')"
+unfolding subst_def substs_def
+thm permute_fun_app_eq
+thm Sum_Type.Projl_def sum_rec_def
+apply(simp add: permute_fun_def)
+unfolding subst_substs_sumC_def
+thm subst_substs.eqvt
+apply(case_tac x)
+apply(simp)
+apply(case_tac a)
+apply(simp)
+thm subst_def
+apply(simp)
+
 section {* defined as two separate nominal datatypes *}
 
 nominal_datatype ty2 =

--- a/Nominal/nominal_mutual.ML	Tue Jul 19 10:43:43 2011 +0200
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 19:09:06 2011 +0100
@@ -193,9 +193,56 @@
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+      (fn _ => print_tac "start" 
+         THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+         THEN (print_tac "second")
          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
+         THEN (print_tac "third")
+         THEN (simp_tac (simpset_of ctxt)) 1
+         THEN (print_tac "fourth")
+      ) (* FIXME: global simpset?!! *)
+    |> restore_cond
+    |> export
+  end
+
+val test1 = @{lemma "x = Inl y ==> permute p (Sum_Type.Projl x) = Sum_Type.Projl (permute p x)" by simp}
+val test2 = @{lemma "x = Inr y ==> permute p (Sum_Type.Projr x) = Sum_Type.Projr (permute p x)" by simp}
+
+fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
+  import (export : thm -> thm) sum_psimp_eq =
+  let
+    val (MutualPart {f=SOME f, ...}) = get_part fname parts
+ 
+    val psimp = import sum_psimp_eq
+    val (simp, restore_cond) =
+      case cprems_of psimp of
+        [] => (psimp, I)
+      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
+      | _ => raise General.Fail "Too many conditions"
+
+    val eqvt_thm' = import eqvt_thm
+    val (simp', restore_cond') =
+      case cprems_of eqvt_thm' of
+        [] => (eqvt_thm, I)
+      | [cond] => (Thm.implies_elim eqvt_thm' (Thm.assume cond), Thm.implies_intr cond)
+      | _ => raise General.Fail "Too many conditions"
+
+    val _ = tracing ("sum_psimp:\n" ^ @{make_string} sum_psimp_eq)
+    val _ = tracing ("psimp:\n" ^ @{make_string} psimp)
+    val _ = tracing ("simp:\n" ^ @{make_string} simp)
+    val _ = tracing ("eqvt:\n" ^ @{make_string} eqvt_thm)
+    
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt		   
+    val p = Free (p, @{typ perm})
+    val ss = HOL_basic_ss addsimps [simp RS test1, simp']
+  in
+    Goal.prove ctxt' [] []
+      (HOLogic.Trueprop $ 
+         HOLogic.mk_eq (mk_perm p (list_comb (f, args)), list_comb (f, map (mk_perm p) args)))
+      (fn _ => print_tac "eqvt start" 
+         THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+         THEN (asm_full_simp_tac ss 1)
+         THEN all_tac) 
     |> restore_cond
     |> export
   end
@@ -295,12 +342,15 @@
     fun mk_mpsimp fqgar sum_psimp =
       in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
 
+    fun mk_meqvts fqgar sum_psimp =
+      in_context lthy fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp
+
     val rew_ss = HOL_basic_ss addsimps all_f_defs
     val mpsimps = map2 mk_mpsimp fqgars psimps
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
-    val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*)
+    val meqvts = map2 mk_meqvts fqgars psimps
  in
     NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,

--- a/Nominal/nominal_termination.ML	Tue Jul 19 10:43:43 2011 +0200
+++ b/Nominal/nominal_termination.ML	Tue Jul 19 19:09:06 2011 +0100
@@ -52,7 +52,12 @@
           val tsimps = map remove_domain_condition psimps
           val tinduct = map remove_domain_condition pinducts
           val teqvts = map remove_domain_condition eqvts
-  
+
+          val _ = tracing ("tot psimps1:\n" ^ cat_lines (map @{make_string} psimps))
+          val _ = tracing ("tot psimps2:\n" ^ cat_lines (map @{make_string} tsimps))
+          val _ = tracing ("tot induct1:\n" ^ cat_lines (map @{make_string} pinducts))
+          val _ = tracing ("tot induct2:\n" ^ cat_lines (map @{make_string} tinduct))
+
           fun qualify n = Binding.name n
             |> Binding.qualify true defname
         in
@@ -66,7 +71,7 @@
           |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy =>
             let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
               case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
-              simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=eqvts }
+              simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts }
             in
               (info',
                lthy