src/HOL/Tools/Function/function_common.ML

     Author:     Alexander Krauss, TU Muenchen
 
 Common definitions and other infrastructure for the function package.
 *)
 
-signature FUNCTION_DATA =
+signature FUNCTION_COMMON =
 sig
   type info =
    {is_partial : bool,
     defname : binding,
       (*contains no logical entities: invariant under morphisms:*)

     termination : thm,
     totality : thm option,
     cases : thm list,
     pelims: thm list list,
     elims: thm list list option}
-end
-
-structure Function_Data : FUNCTION_DATA =
-struct
-
-type info =
- {is_partial : bool,
-  defname : binding,
-    (*contains no logical entities: invariant under morphisms:*)
-  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Token.src list -> thm list -> local_theory -> thm list * local_theory,
-  fnames : binding list,
-  case_names : string list,
-  fs : term list,
-  R : term,
-  dom: term,
-  psimps: thm list,
-  pinducts: thm list,
-  simps : thm list option,
-  inducts : thm list option,
-  termination : thm,
-  totality : thm option,
-  cases : thm list,
-  pelims : thm list list,
-  elims : thm list list option}
-
-end
-
-signature FUNCTION_COMMON =
-sig
-  include FUNCTION_DATA
   val profile : bool Unsynchronized.ref
   val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
   val mk_acc : typ -> term -> term
   val split_def : Proof.context -> (string -> 'a) -> term ->
     string * (string * typ) list * term list * term list * term

   val mk_case_names : int -> string -> int -> string list
   val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) ->
     preproc
   val termination_rule_tac : Proof.context -> int -> tactic
   val store_termination_rule : thm -> Context.generic -> Context.generic
-  val get_functions : Proof.context -> (term * info) Item_Net.T
+  val retrieve_function_data : Proof.context -> term -> (term * info) list
   val add_function_data : info -> Context.generic -> Context.generic
   val termination_prover_tac : bool -> Proof.context -> tactic
   val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic ->
     Context.generic
   val get_preproc: Proof.context -> preproc

 end
 
 structure Function_Common : FUNCTION_COMMON =
 struct
 
-open Function_Data
-
 local open Function_Lib in
+
+(* info *)
+
+type info =
+ {is_partial : bool,
+  defname : binding,
+    (*contains no logical entities: invariant under morphisms:*)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
+  fnames : binding list,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  dom: term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination : thm,
+  totality : thm option,
+  cases : thm list,
+  pelims : thm list list,
+  elims : thm list list option}
+
+fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
+  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
+    let
+      val term = Morphism.term phi
+      val thm = Morphism.thm phi
+      val fact = Morphism.fact phi
+    in
+      { add_simps = add_simps, case_names = case_names, fnames = fnames,
+        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
+        pinducts = fact pinducts, simps = Option.map fact simps,
+        inducts = Option.map fact inducts, termination = thm termination,
+        totality = Option.map thm totality, defname = Morphism.binding phi defname,
+        is_partial = is_partial, cases = fact cases,
+        elims = Option.map (map fact) elims, pelims = map fact pelims }
+    end
 
 
 (* profiling *)
 
 val profile = Unsynchronized.ref false

 fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt)))
 
 val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
 
 val get_functions = #2 o Data.get o Context.Proof
-fun add_function_data (info : info as {fs, termination, ...}) =
-  (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
-  #> store_termination_rule termination
+
+fun retrieve_function_data ctxt t =
+  Item_Net.retrieve (get_functions ctxt) t
+  |> (map o apsnd)
+      (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+
+val add_function_data =
+  transform_function_data Morphism.trim_context_morphism #>
+  (fn info as {fs, termination, ...} =>
+    (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
+    #> store_termination_rule termination)
 
 fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt
 val set_termination_prover = Data.map o @{apply 4(3)} o K
 
 val get_preproc = #4 o Data.get o Context.Proof

   cases : thm list,
   pelims : thm list list,
   termination : thm,
   domintros : thm list option}
 
-fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
-  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
-    let
-      val term = Morphism.term phi
-      val thm = Morphism.thm phi
-      val fact = Morphism.fact phi
-    in
-      { add_simps = add_simps, case_names = case_names, fnames = fnames,
-        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
-        pinducts = fact pinducts, simps = Option.map fact simps,
-        inducts = Option.map fact inducts, termination = thm termination,
-        totality = Option.map thm totality, defname = Morphism.binding phi defname,
-        is_partial = is_partial, cases = fact cases,
-        elims = Option.map (map fact) elims, pelims = map fact pelims }
-    end
-
 fun lift_morphism ctxt f =
   let
     fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t))
   in
     Morphism.morphism "lift_morphism"

 
     fun match (trm, data) =
       SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
         handle Pattern.MATCH => NONE
   in
-    get_first match (Item_Net.retrieve (get_functions ctxt) t)
+    get_first match (retrieve_function_data ctxt t)
   end
 
 fun import_last_function ctxt =
   (case Item_Net.content (get_functions ctxt) of
     [] => NONE