--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 10:40:06 2011 +0100
@@ -84,13 +84,16 @@
 apply(simp)
 done
 
-print_theorems
-
 termination 
   by (relation "measure size") (auto simp add: lam.size)
 
+thm frees_set.simps
+thm frees_set.induct
 
-thm frees_set.simps
+lemma "frees_set t = supp t"
+apply(induct rule: frees_set.induct)
+apply(simp_all add: lam.supp supp_at_base)
+done
 
 lemma fresh_fun_eqvt_app3:
   assumes a: "eqvt f"
@@ -159,8 +162,6 @@
 
 thm hei.f.simps
 
-
-
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -207,6 +208,7 @@
 | "height (Lam [x].t) = height t + 1"
   unfolding eqvt_def height_graph_def
   apply (rule, perm_simp, rule)
+apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply (erule Abs1_eq_fdest)
@@ -229,6 +231,7 @@
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
   unfolding eqvt_def frees_lst_graph_def
   apply (rule, perm_simp, rule)
+apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
 apply (erule Abs1_eq_fdest)
@@ -258,6 +261,7 @@
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
+apply(rule TrueI)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
@@ -413,25 +417,34 @@
   "lookup [] n x = LNVar x"
 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
 
+lemma supp_lookup:
+  shows "supp (lookup xs n x) \<subseteq> supp x"
+  apply(induct arbitrary: n rule: lookup.induct)
+  apply(simp add: ln.supp)
+  apply(simp add: ln.supp pure_supp)
+  done
+  
+
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec
+nominal_primrec (invariant "\<lambda>x y. supp y \<subseteq> supp x")
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
-  unfolding eqvt_def trans_graph_def
-  apply (rule, perm_simp, rule)
+apply(simp add: eqvt_def trans_graph_def)
+apply (rule, perm_simp, rule)
+defer
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 apply(simp_all add: fresh_star_def)[3]
 apply(blast)
 apply(blast)
-apply(simp_all add: lam.distinct lam.eq_iff)
+apply(simp_all)
 apply(elim conjE)
 apply clarify
 apply (erule Abs1_eq_fdest)
@@ -443,6 +456,13 @@
 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
 apply (simp add: eqvt_at_def)
 apply (metis atom_name_def swap_fresh_fresh)
+apply(simp add: fresh_def)
+defer
+apply(erule trans_graph.induct)
+defer
+apply(simp add: lam.supp ln.supp)
+apply(blast)
+apply(simp add: lam.supp ln.supp)
 oops
 
 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"
@@ -549,13 +569,14 @@
   by (induct l arbitrary: n) (simp_all add: permute_pure)
 
 nominal_primrec
-  trans :: "lam \<Rightarrow> name list \<Rightarrow> db option"
+  transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
 where
-  "trans (Var x) l = vindex l x 0"
-| "trans (App t1 t2) xs = dbapp_in (trans t1 xs) (trans t2 xs)"
-| "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs = dblam_in (trans t (x # xs))"
-  unfolding eqvt_def trans_graph_def
+  "transdb (Var x) l = vindex l x 0"
+| "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)"
+| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))"
+  unfolding eqvt_def transdb_graph_def
   apply (rule, perm_simp, rule)
+  apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def fresh_at_list)
@@ -570,13 +591,13 @@
 termination
   by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size)
 
-lemma trans_eqvt[eqvt]:
-  "p \<bullet> trans t l = trans (p \<bullet>t) (p \<bullet>l)"
+lemma transdb_eqvt[eqvt]:
+  "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"
   apply (nominal_induct t avoiding: l p rule: lam.strong_induct)
   apply (simp add: vindex_eqvt)
   apply (simp_all add: permute_pure)
   apply (simp add: fresh_at_list)
-  apply (subst trans.simps)
+  apply (subst transdb.simps)
   apply (simp add: fresh_at_list[symmetric])
   apply (drule_tac x="name # l" in meta_spec)
   apply auto
@@ -659,6 +680,7 @@
 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
   apply (simp add: eqvt_def map_term_graph_def)
   apply (rule, perm_simp, rule)
+  apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
   apply (erule Abs1_eq_fdest)

--- a/Nominal/Ex/TypeSchemes.thy	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jun 07 10:40:06 2011 +0100
@@ -174,6 +174,7 @@
 apply(assumption)
 apply(simp)
 --"Eqvt done"
+apply(rule TrueI)
 apply (case_tac x)
 apply simp apply clarify 
 apply (rule_tac y="b" in ty_tys.exhaust(1))
@@ -344,6 +345,7 @@
 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
+  apply(rule TrueI)
   apply(case_tac x)
   apply(simp)
   apply(rule_tac y="b" in ty2.exhaust)
@@ -384,7 +386,7 @@
   "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
   unfolding eqvt_def substs_graph_def
   apply (rule, perm_simp, rule)
-  apply auto[1]
+  apply auto[2]
   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
   apply auto
   apply (subst (asm) Abs_eq_res_set)

--- a/Nominal/Nominal2.thy	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/Nominal2.thy	Tue Jun 07 10:40:06 2011 +0100
@@ -6,6 +6,7 @@
      ("nominal_dt_quot.ML")
      ("nominal_induct.ML")
      ("nominal_inductive.ML")
+     ("nominal_function_common.ML")
      ("nominal_function_core.ML")
      ("nominal_mutual.ML")
      ("nominal_function.ML")
@@ -35,6 +36,7 @@
 (***************************************)
 (* forked code of the function package *)
 (* for defining nominal functions      *)
+use "nominal_function_common.ML"
 use "nominal_function_core.ML"
 use "nominal_mutual.ML"
 use "nominal_function.ML"

--- a/Nominal/nominal_function_common.ML	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/nominal_function_common.ML	Tue Jun 07 10:40:06 2011 +0100
@@ -4,182 +4,14 @@
     heavily based on the code of Alexander Krauss
     (code forked on 5 June 2011)
 
-Common definitions and other infrastructure for the function package.
+Redefinition of config datatype 
 *)
 
-signature FUNCTION_DATA =
-sig
 
-type 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}
-
-end
-
-structure Function_Data : FUNCTION_DATA =
-struct
-
-type 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}
-
-end
 
 structure Nominal_Function_Common =
 struct
 
-open Function_Data
-
-local open Function_Lib in
-
-(* Profiling *)
-val profile = Unsynchronized.ref false;
-
-fun PROFILE msg = if !profile then timeap_msg msg else I
-
-
-val acc_const_name = @{const_name accp}
-fun mk_acc domT R =
-  Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
-
-val function_name = suffix "C"
-val graph_name = suffix "_graph"
-val rel_name = suffix "_rel"
-val dom_name = suffix "_dom"
-
-(* Termination rules *)
-
-structure TerminationRule = Generic_Data
-(
-  type T = thm list
-  val empty = []
-  val extend = I
-  val merge = Thm.merge_thms
-);
-
-val get_termination_rules = TerminationRule.get
-val store_termination_rule = TerminationRule.map o cons
-val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
-
-
-(* Function definition result data *)
-
-datatype function_result = FunctionResult of
- {fs: term list,
-  G: term,
-  R: term,
-  psimps : thm list,
-  simple_pinducts : thm list,
-  cases : thm,
-  termination : thm,
-  domintros : thm list option}
-
-fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
-  simps, inducts, termination, defname, is_partial} : 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 }
-    end
-
-structure FunctionData = Generic_Data
-(
-  type T = (term * 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 = FunctionData.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 : info as {fs, termination, ...}) =
-  FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
-  #> store_termination_rule termination
-
-
-(* Simp rules for termination proofs *)
-
-structure Termination_Simps = Named_Thms
-(
-  val name = "termination_simp"
-  val description = "simplification rules for termination proofs"
-)
-
-
-(* Default Termination Prover *)
-
-structure TerminationProver = Generic_Data
-(
-  type T = Proof.context -> tactic
-  val empty = (fn _ => error "Termination prover not configured")
-  val extend = I
-  fun merge (a, _) = a
-)
-
-val set_termination_prover = TerminationProver.put
-val get_termination_prover = TerminationProver.get o Context.Proof
-
 
 (* Configuration management *)
 datatype nominal_function_opt
@@ -216,149 +48,4 @@
   NominalFunctionConfig { sequential=false, default=NONE,
     domintros=false, partials=true, inv=NONE}
 
-
-(* Analyzing function equations *)
-
-fun split_def ctxt check_head geq =
-  let
-    fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
-    val qs = Term.strip_qnt_vars "all" geq
-    val imp = Term.strip_qnt_body "all" geq
-    val (gs, eq) = Logic.strip_horn imp
-
-    val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
-      handle TERM _ => error (input_error "Not an equation")
-
-    val (head, args) = strip_comb f_args
-
-    val fname = fst (dest_Free head) handle TERM _ => ""
-    val _ = check_head fname
-  in
-    (fname, qs, gs, args, rhs)
-  end
-
-(* Check for all sorts of errors in the input *)
-fun check_defs ctxt fixes eqs =
-  let
-    val fnames = map (fst o fst) fixes
-
-    fun check geq =
-      let
-        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
-
-        fun check_head fname =
-          member (op =) fnames fname orelse
-          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
-
-        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
-
-        val _ = length args > 0 orelse input_error "Function has no arguments:"
-
-        fun add_bvs t is = add_loose_bnos (t, 0, is)
-        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
-                    |> map (fst o nth (rev qs))
-
-        val _ = null rvs orelse input_error
-          ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
-           " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
-
-        val _ = forall (not o Term.exists_subterm
-          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
-          orelse input_error "Defined function may not occur in premises or arguments"
-
-        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
-        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
-        val _ = null funvars orelse (warning (cat_lines
-          ["Bound variable" ^ plural " " "s " funvars ^
-          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
-          " in function position.", "Misspelled constructor???"]); true)
-      in
-        (fname, length args)
-      end
-
-    val grouped_args = AList.group (op =) (map check eqs)
-    val _ = grouped_args
-      |> map (fn (fname, ars) =>
-        length (distinct (op =) ars) = 1
-        orelse error ("Function " ^ quote fname ^
-          " has different numbers of arguments in different equations"))
-
-    val not_defined = subtract (op =) (map fst grouped_args) fnames
-    val _ = null not_defined
-      orelse error ("No defining equations for function" ^
-        plural " " "s " not_defined ^ commas_quote not_defined)
-
-    fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
-      orelse error (cat_lines
-      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
-       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
-
-    val _ = map check_sorts fixes
-  in
-    ()
-  end
-
-(* Preprocessors *)
-
-type fixes = ((string * typ) * mixfix) list
-type 'a spec = (Attrib.binding * 'a list) list
-type preproc = nominal_function_config -> Proof.context -> fixes -> term spec ->
-  (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
-
-val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
-  HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
-
-fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
-  | mk_case_names _ n 0 = []
-  | mk_case_names _ n 1 = [n]
-  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
-
-fun empty_preproc check _ ctxt fixes spec =
-  let
-    val (bnds, tss) = split_list spec
-    val ts = flat tss
-    val _ = check ctxt fixes ts
-    val fnames = map (fst o fst) fixes
-    val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
-
-    fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
-      (indices ~~ xs) |> map (map snd)
-
-    (* using theorem names for case name currently disabled *)
-    val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
-  in
-    (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
-  end
-
-structure Preprocessor = Generic_Data
-(
-  type T = preproc
-  val empty : T = empty_preproc check_defs
-  val extend = I
-  fun merge (a, _) = a
-)
-
-val get_preproc = Preprocessor.get o Context.Proof
-val set_preproc = Preprocessor.map o K
-
-
-
-local
-  val option_parser = Parse.group "option"
-    ((Parse.reserved "sequential" >> K Sequential)
-     || ((Parse.reserved "default" |-- Parse.term) >> Default)
-     || (Parse.reserved "domintros" >> K DomIntros)
-     || (Parse.reserved "no_partials" >> K No_Partials))
-
-  fun config_parser default =
-    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
-     >> (fn opts => fold Nominal_Function_Common.apply_opt opts default)
-in
-  fun function_parser default_cfg =
-      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
 end
-
-
-end
-end

--- a/Nominal/nominal_function_core.ML	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jun 07 10:40:06 2011 +0100
@@ -8,48 +8,6 @@
 *)
 
 
-structure Nominal_Function_Common =
-struct
-
-
-(* Configuration management *)
-datatype nominal_function_opt
-  = Sequential
-  | Default of string
-  | DomIntros
-  | No_Partials
-  | Invariant of string
-
-datatype nominal_function_config = NominalFunctionConfig of
- {sequential: bool,
-  default: string option,
-  domintros: bool,
-  partials: bool,
-  inv: string option}
-
-fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv}
-  | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv}
-  | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv}
-  | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv}
-  | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s}
-
-val nominal_default_config =
-  NominalFunctionConfig { sequential=false, default=NONE,
-    domintros=false, partials=true, inv=NONE}
-
-end
-
-
 signature NOMINAL_FUNCTION_CORE =
 sig
   val trace: bool Unsynchronized.ref