--- a/Nominal/Ex/Classical.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -216,7 +216,7 @@
   apply(blast)
   done
 
-termination 
+termination (eqvt)
   by lexicographic_order
 
 nominal_primrec 
@@ -379,7 +379,7 @@
   apply(blast)
   done
 
-termination 
+termination (eqvt)
   by lexicographic_order
 
 lemma crename_name_eqvt[eqvt]:

--- a/Nominal/Ex/Lambda.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -43,7 +43,17 @@
 apply(all_trivials)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
+
+ML {*
+Item_Net.content; 
+Nominal_Function_Common.get_function
+*}
+
+ML {*
+Item_Net.content (Nominal_Function_Common.get_function @{context})
+*}
+
 
 lemma [eqvt]:
   shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)"
@@ -65,7 +75,7 @@
 apply(simp_all)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 lemma [eqvt]:
   shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)"
@@ -87,7 +97,7 @@
 apply(simp_all)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 lemma [eqvt]:
   shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)"
@@ -118,7 +128,7 @@
 apply(rule refl)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 nominal_datatype path = Left | Right | In
 
@@ -155,7 +165,7 @@
 apply(rule refl)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 lemma var_pos1:
   assumes "atom y \<notin> supp t"
@@ -195,7 +205,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 
 section {* free name function *}
@@ -221,7 +231,7 @@
 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 text {* a small test lemma *}
 lemma shows "supp t = set (frees_lst t)"
@@ -249,7 +259,7 @@
   apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
   done
 
-termination 
+termination (eqvt) 
   by lexicographic_order
 
 lemma "frees_set t = supp t"
@@ -272,7 +282,7 @@
   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
   
 thm height.simps
@@ -300,7 +310,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 lemma subst_eqvt[eqvt]:
@@ -486,7 +496,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 
@@ -513,7 +523,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 
@@ -543,7 +553,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 section {* De Bruijn Terms *}
@@ -594,7 +604,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 lemma transdb_eqvt[eqvt]:
@@ -665,7 +675,7 @@
 
 
 (* a small test
-termination sorry
+termination (eqvt) sorry
 
 lemma 
   assumes "x \<noteq> y"
@@ -719,7 +729,7 @@
   apply (simp add: eqvt_def permute_fun_app_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 

--- a/Nominal/Ex/LetRec.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -59,7 +59,9 @@
   apply (simp add: permute_fun_def)
   done
 
-termination by lexicographic_order
+thm height_trm_def height_bp_def
+
+termination (eqvt) by lexicographic_order
 
 end
 

--- a/Nominal/Ex/TypeSchemes.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -322,7 +322,7 @@
   apply(simp_all add: ty2.distinct)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 lemma subst_eqvt[eqvt]:

--- a/Nominal/Nominal2.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Nominal2.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -10,6 +10,7 @@
      ("nominal_function_core.ML")
      ("nominal_mutual.ML")
      ("nominal_function.ML")
+     ("nominal_termination.ML")
      ("nominal_dt_data.ML")
 begin
 
@@ -44,6 +45,7 @@
 use "nominal_function_core.ML"
 use "nominal_mutual.ML"
 use "nominal_function.ML"
+use "nominal_termination.ML"
 
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)

--- a/Nominal/nominal_function.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_function.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -9,15 +9,15 @@
 
 signature NOMINAL_FUNCTION =
 sig
-  include FUNCTION_DATA
+  include NOMINAL_FUNCTION_DATA
 
   val add_nominal_function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
-    (Proof.context -> tactic) -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
 
   val add_nominal_function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
-    (Proof.context -> tactic) -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
 
   val nominal_function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
@@ -30,7 +30,7 @@
   val setup : theory -> theory
   val get_congs : Proof.context -> thm list
 
-  val get_info : Proof.context -> term -> info
+  val get_info : Proof.context -> term -> nominal_info
 end
 
 
@@ -152,9 +152,12 @@
 
     fun afterqed [[proof]] lthy =
       let
-        val FunctionResult {fs, R, psimps, simple_pinducts,
-          termination, domintros, cases, ...} =
+        val NominalFunctionResult {fs, R, psimps, simple_pinducts,
+          termination, domintros, cases, eqvts, ...} =
           cont (Thm.close_derivation proof)
+  
+        val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps))
+        val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
 
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
@@ -179,7 +182,9 @@
 
         val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
-          fs=fs, R=R, defname=defname, is_partial=true }
+          fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
+
+        val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps'))
 
         val _ =
           if not is_external then ()

--- a/Nominal/nominal_function_common.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_function_common.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -7,11 +7,110 @@
 Redefinition of config datatype 
 *)
 
+signature NOMINAL_FUNCTION_DATA =
+sig
+
+type nominal_info =
+ {is_partial : bool,
+  defname : string,
+    (* contains no logical entities: invariant under morphisms: *)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination: thm,
+  eqvts: thm list}
+
+end
 
 
 structure Nominal_Function_Common =
 struct
 
+type nominal_info =
+ {is_partial : bool,
+  defname : string,
+    (* contains no logical entities: invariant under morphisms: *)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination: thm,
+  eqvts: thm list}
+
+fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
+  simps, inducts, termination, defname, is_partial, eqvts} : nominal_info) phi =
+    let
+      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
+      val name = Binding.name_of o Morphism.binding phi o Binding.name
+    in
+      { add_simps = add_simps, case_names = case_names,
+        fs = map term fs, R = term R, psimps = fact psimps,
+        pinducts = fact pinducts, simps = Option.map fact simps,
+        inducts = Option.map fact inducts, termination = thm termination,
+        defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts }
+    end
+
+structure NominalFunctionData = Generic_Data
+(
+  type T = (term * nominal_info) Item_Net.T;
+  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
+  val extend = I;
+  fun merge tabs : T = Item_Net.merge tabs;
+)
+
+val get_function = NominalFunctionData.get o Context.Proof;
+
+
+fun lift_morphism thy f =
+  let
+    val term = Drule.term_rule thy f
+  in
+    Morphism.thm_morphism f $> Morphism.term_morphism term
+    $> Morphism.typ_morphism (Logic.type_map term)
+  end
+
+fun import_function_data t ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val ct = cterm_of thy t
+    val inst_morph = lift_morphism thy o Thm.instantiate
+
+    fun match (trm, data) =
+      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+      handle Pattern.MATCH => NONE
+  in
+    get_first match (Item_Net.retrieve (get_function ctxt) t)
+  end
+
+fun import_last_function ctxt =
+  case Item_Net.content (get_function ctxt) of
+    [] => NONE
+  | (t, data) :: _ =>
+    let
+      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    in
+      import_function_data t' ctxt'
+    end
+
+val all_function_data = Item_Net.content o get_function
+
+fun add_function_data (data : nominal_info as {fs, termination, ...}) =
+  NominalFunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
+  #> Function_Common.store_termination_rule termination
+
+
+
 
 (* Configuration management *)
 datatype nominal_function_opt
@@ -48,4 +147,15 @@
   NominalFunctionConfig { sequential=false, default=NONE,
     domintros=false, partials=true, inv=NONE}
 
+datatype nominal_function_result = NominalFunctionResult of
+ {fs: term list,
+  G: term,
+  R: term,
+  psimps : thm list,
+  simple_pinducts : thm list,
+  cases : thm,
+  termination : thm,
+  domintros : thm list option,
+  eqvts : thm list}
+
 end

--- a/Nominal/nominal_function_core.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -19,7 +19,7 @@
     -> local_theory
     -> (term   (* f *)
         * thm  (* goalstate *)
-        * (thm -> Function_Common.function_result) (* continuation *)
+        * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
        ) * local_theory
 
 end
@@ -1062,6 +1062,8 @@
 
         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
 
+        val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
+
         val psimps = PROFILE "Proving simplification rules"
           (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
 
@@ -1077,9 +1079,9 @@
            else NONE
 
       in
-        FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+        NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
           psimps=psimps, simple_pinducts=[simple_pinduct],
-          termination=total_intro, domintros=dom_intros}
+          termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]}
       end
   in
     ((f, goalstate, mk_partial_rules), lthy)

--- a/Nominal/nominal_mutual.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -17,7 +17,7 @@
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Function_Common.function_result) (* proof continuation *)
+        * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
        ) * local_theory)
 
 end
@@ -255,8 +255,15 @@
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   let
     val result = inner_cont proof
-    val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
-      termination, domintros, ...} = result
+    val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
+      termination, domintros, eqvts,...} = result
+
+    (*
+    val _ = tracing ("premutual induct:\n" ^ @{make_string} simple_pinduct)
+    val _ = tracing ("premutual termination:\n" ^ @{make_string} termination)
+    val _ = tracing ("premutual psimps:\n" ^ cat_lines (map @{make_string} psimps))
+    val _ = tracing ("premutual eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
+    *)
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -275,11 +282,17 @@
     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 _ = tracing ("postmutual psimps:\n" ^ cat_lines (map @{make_string} mpsimps))
+    val _ = tracing ("postmutual induct:\n" ^ cat_lines (map @{make_string} minducts))
+    val _ = tracing ("postmutual termination:\n" ^ @{make_string} mtermination)
+    *)
   in
-    FunctionResult { fs=fs, G=G, R=R,
+    NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros}
+      domintros=mdomintros, eqvts=eqvts }
   end
 
 (* nominal *)