--- a/Nominal/Ex/Lambda.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -644,8 +644,8 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Inl var_fresh_subst)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
 done
 
 

--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -288,26 +288,6 @@
 
 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 *}
 
@@ -383,17 +363,24 @@
   apply (rule, perm_simp, rule)
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
-  apply auto
+  apply auto[1]
+  apply(simp)
+  apply(erule conjE)
   apply (erule Abs_res_fcb)
   apply (simp add: Abs_fresh_iff)
-  apply (simp add: Abs_fresh_iff)
-  apply auto[1]
-  apply (simp add: fresh_def fresh_star_def)
-  apply (rule contra_subsetD[OF  supp_subst])
-  apply simp
-  apply blast
+  apply(simp add: fresh_def)
+  apply(simp add: supp_Abs)
+  apply(rule impI)
+  apply(subgoal_tac "x \<notin> supp \<theta>")
+  prefer 2
+  apply(auto simp add: fresh_star_def fresh_def)[1]
+  apply(subgoal_tac "x \<in> supp t")
+  using supp_subst
+  apply(blast)
+  using supp_subst
+  apply(blast)
   apply clarify
-  apply (simp add: subst_eqvt)
+  apply (simp add: subst2.eqvt)
   apply (subst Abs_eq_iff)
   apply (rule_tac x="0::perm" in exI)
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
@@ -415,7 +402,6 @@
   apply blast
   done
 
-
 text {* Some Tests about Alpha-Equality *}
 
 lemma

--- a/Nominal/Nominal2_Base.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -529,8 +529,8 @@
 primrec 
   permute_sum 
 where
-  "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
-| "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
+  Inl_eqvt: "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
+| Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
 
 instance 
 by (default) (case_tac [!] x, simp_all)
@@ -545,8 +545,8 @@
 primrec 
   permute_list 
 where
-  "p \<bullet> [] = []"
-| "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
+  Nil_eqvt:  "p \<bullet> [] = []"
+| Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
 
 instance 
 by (default) (induct_tac [!] x, simp_all)
@@ -567,8 +567,8 @@
 primrec 
   permute_option 
 where
-  "p \<bullet> None = None"
-| "p \<bullet> (Some x) = Some (p \<bullet> x)"
+  None_eqvt: "p \<bullet> None = None"
+| Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
 
 instance 
 by (default) (induct_tac [!] x, simp_all)

--- a/Nominal/nominal_library.ML	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/nominal_library.ML	Fri Jul 22 11:37:16 2011 +0100
@@ -64,6 +64,7 @@
   val fold_append: term list -> term
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
+  val fold_conj_balanced: term list -> term 
 
   (* functions for de-Bruijn open terms *)
   val mk_binop_env: typ list -> string -> term * term -> term
@@ -94,6 +95,8 @@
 
   (* transformation into the object logic *)
   val atomize: thm -> thm
+  val atomize_rule: int -> thm -> thm 
+  val atomize_concl: thm -> thm
 
   (* applies a tactic to a formula composed of conjunctions *)
   val conj_tac: (int -> tactic) -> int -> tactic
@@ -249,6 +252,7 @@
   | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)
 
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
+fun fold_conj_balanced ts = Balanced_Tree.make HOLogic.mk_conj ts
 
 
 (* functions for de-Bruijn open terms *)
@@ -476,7 +480,12 @@
 
 
 (* transformes a theorem into one of the object logic *)
-val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars;
+fun atomize_rule i thm =
+  Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm
+fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm
+
+
 
 (* applies a tactic to a formula composed of conjunctions *)
 fun conj_tac tac i =

--- a/Nominal/nominal_mutual.ML	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Fri Jul 22 11:37:16 2011 +0100
@@ -8,6 +8,7 @@
 Mutual recursive nominal function definitions.
 *)
 
+
 signature NOMINAL_FUNCTION_MUTUAL =
 sig
 
@@ -193,87 +194,46 @@
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => print_tac "start" 
-         THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs)
-         THEN (print_tac "second")
+      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (print_tac "third")
-         THEN (simp_tac (simpset_of ctxt)) 1
-         THEN (print_tac "fourth")
-      ) (* FIXME: global simpset?!! *)
+         THEN (simp_tac (simpset_of ctxt)) 1) (* 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}
+val inl_perm = @{lemma "x = Inl y ==> Sum_Type.Projl (permute p x) = permute p (Sum_Type.Projl x)" by simp}
+val inr_perm = @{lemma "x = Inr y ==> Sum_Type.Projr (permute p x) = permute p (Sum_Type.Projr x)" by simp}
 
-fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
+fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, _)
   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) =
+    val (cond, 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)
+        [] => ([], psimp, I)
+      | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (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']
+    val ss = HOL_basic_ss addsimps 
+      @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @
+      @{thms Projr.simps Projl.simps} @
+      [(cond MRS eqvt_thm) RS @{thm sym}] @ 
+      [inl_perm, inr_perm, simp] 
+    val goal_lhs = mk_perm p (list_comb (f, args))
+    val goal_rhs = list_comb (f, map (mk_perm p) args)
   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) 
+    Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
+      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+         THEN (asm_full_simp_tac ss 1))
+    |> singleton (ProofContext.export ctxt' ctxt)
     |> restore_cond
     |> export
   end
 
-fun mk_meqvts ctxt eqvt_thm f_defs =
-  let
-    val ctrm1 = eqvt_thm
-      |> cprop_of
-      |> snd o Thm.dest_implies
-      |> Thm.dest_arg
-      |> Thm.dest_arg1
-      |> Thm.dest_arg
-
-    fun resolve f_def =
-      let
-        val ctrm2 = f_def
-          |> cprop_of
-          |> Thm.dest_equals_lhs
-        val _ = tracing ("ctrm1:\n" ^ @{make_string} ctrm1)
-        val _ = tracing ("ctrm2:\n" ^ @{make_string} ctrm2)
-      in
-        eqvt_thm
-	|> Thm.instantiate (Thm.match (ctrm1, ctrm2))
-        |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps}))
-        |> Local_Defs.unfold ctxt [f_def] 
-      end
-  in
-    map resolve f_defs
-  end
-
-
 fun mk_applied_form ctxt caTs thm =
   let
     val thy = ProofContext.theory_of ctxt
@@ -324,6 +284,66 @@
     fst (fold_map (project induct_inst) parts 0)
   end
 
+
+fun forall_elim s (Const ("all", _) $ Abs (_, _, t)) = subst_bound (s, t)
+  | forall_elim _ t = t
+
+val forall_elim_list = fold forall_elim
+
+fun split_conj_thm th =
+  (split_conj_thm (th RS conjunct1)) @ (split_conj_thm (th RS conjunct2)) handle THM _ => [th];
+
+fun prove_eqvt ctxt fs argTss eqvts_thms induct_thms =
+  let
+    fun aux argTs s = argTs
+      |> map (pair s)
+      |> Variable.variant_frees ctxt fs
+    val argss' = map2 aux argTss (Name.invent (Variable.names_of ctxt) "" (length fs)) 
+    val argss = (map o map) Free argss'
+    val arg_namess = (map o map) fst argss'
+    val insts = (map o map) SOME arg_namess 
+   
+    val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt
+    val p = Free (p_name, @{typ perm})
+
+    val acc_prems = 
+     map prop_of induct_thms
+     |> map2 forall_elim_list argss 
+     |> map (strip_qnt_body "all")
+     |> map (curry Logic.nth_prem 1)
+     |> map HOLogic.dest_Trueprop
+
+    fun mk_goal acc_prem (f, args) = 
+      let
+        val goal_lhs = mk_perm p (list_comb (f, args))
+        val goal_rhs = list_comb (f, map (mk_perm p) args)
+      in
+        HOLogic.mk_imp (acc_prem, HOLogic.mk_eq (goal_lhs, goal_rhs))
+      end
+
+    val goal = fold_conj_balanced (map2 mk_goal acc_prems (fs ~~ argss))
+      |> HOLogic.mk_Trueprop
+
+    val induct_thm = case induct_thms of
+        [thm] => thm
+          |> Drule.gen_all 
+          |> Thm.permute_prems 0 1
+          |> (fn thm => atomize_rule (length (prems_of thm) - 1) thm)
+      | thms => thms
+          |> map Drule.gen_all 
+          |> map (Rule_Cases.add_consumes 1)
+          |> snd o Rule_Cases.strict_mutual_rule ctxt'
+          |> atomize_concl
+
+    fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
+  in
+    Goal.prove ctxt' (flat arg_namess) [] goal
+      (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> split_conj_thm
+    |> map (fn th => th RS mp)
+  end
+
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   let
     val result = inner_cont proof
@@ -332,13 +352,16 @@
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
-        (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
+          (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
       parts
       |> split_list
 
     val all_orig_fdefs =
       map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
 
+    val cargTss =
+      map (fn MutualPart {f = SOME f, cargTs, ...} => cargTs) parts
+
     fun mk_mpsimp fqgar sum_psimp =
       in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
 
@@ -351,11 +374,12 @@
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
     val meqvts = map2 mk_meqvts fqgars psimps
+    val meqvt_funs = prove_eqvt lthy fs cargTss meqvts minducts
  in
     NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros, eqvts=meqvts }
+      domintros=mdomintros, eqvts=meqvt_funs }
   end
 
 (* nominal *)

--- a/Nominal/nominal_termination.ML	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/nominal_termination.ML	Fri Jul 22 11:37:16 2011 +0100
@@ -42,6 +42,7 @@
       val { termination, fs, R, add_simps, case_names, psimps,
         pinducts, defname, eqvts, ...} = info
       val domT = domain_type (fastype_of R)
+
       val goal = HOLogic.mk_Trueprop
                    (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
       fun afterqed [[totality]] lthy =
@@ -50,14 +51,9 @@
           val remove_domain_condition =
             full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
           val tsimps = map remove_domain_condition psimps
-          val tinduct = map remove_domain_condition pinducts
+          val tinducts = 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
@@ -67,7 +63,7 @@
           ||>> Local_Theory.note
              ((qualify "induct",
                [Attrib.internal (K (Rule_Cases.case_names case_names))]),
-              tinduct)
+              tinducts)
           |-> (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,