# HG changeset patch
# User ballarin
# Date 1221657690 -7200
# Node ID 5b2af04ec9fb016227a3c5dd3a546e0a65b89736
# Parent  4bf450d50c32d75080fe9af8036423352a735127
Public interface to interpretation morphism.

diff -r 4bf450d50c32 -r 5b2af04ec9fb doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Wed Sep 17 11:42:25 2008 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Wed Sep 17 15:21:30 2008 +0200
@@ -91,8 +91,8 @@
 \begin{isamarkuptext}%
 Further interpretations are necessary to reuse theorems from
   the other locales.  In \isa{lattice} the operations \isa{{\isasymsqinter}} and
-  \isa{{\isasymsqunion}} are substituted by \isa{min} and
-  \isa{max}.  The entire proof for the
+  \isa{{\isasymsqunion}} are substituted by \isa{ord{\isacharunderscore}class{\isachardot}min} and
+  \isa{ord{\isacharunderscore}class{\isachardot}max}.  The entire proof for the
   interpretation is reproduced in order to give an example of a more
   elaborate interpretation proof.%
 \end{isamarkuptext}%
@@ -196,9 +196,9 @@
   \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
   \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
   \isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
-  \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
+  \quad \isa{ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
   \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
-  \quad \isa{max\ {\isacharquery}x\ {\isacharparenleft}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ min\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
+  \quad \isa{ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ ord{\isacharunderscore}class{\isachardot}min\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
   \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
   \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
 \end{tabular}
diff -r 4bf450d50c32 -r 5b2af04ec9fb src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 17 11:42:25 2008 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 17 15:21:30 2008 +0200
@@ -63,7 +63,7 @@
 (** auxiliary **)
 
 fun prove_interpretation tac prfx_atts expr inst =
-  Locale.interpretation_i I prfx_atts expr inst
+  Locale.interpretation_i I prfx_atts expr inst #> snd
   #> Proof.global_terminal_proof
       (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
   #> ProofContext.theory_of;
diff -r 4bf450d50c32 -r 5b2af04ec9fb src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 17 11:42:25 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 17 15:21:30 2008 +0200
@@ -400,7 +400,7 @@
       opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
         >> (fn ((name, expr), insts) => Toplevel.print o
             Toplevel.theory_to_proof
-              (Locale.interpretation I (true, Name.name_of name) expr insts)));
+              (Locale.interpretation I (true, Name.name_of name) expr insts #> snd)));
 
 val _ =
   OuterSyntax.command "interpret"
@@ -409,7 +409,7 @@
     (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
       >> (fn ((name, expr), insts) => Toplevel.print o
           Toplevel.proof'
-            (Locale.interpret Seq.single (true, Name.name_of name) expr insts)));
+            (fn int => Locale.interpret Seq.single (true, Name.name_of name) expr insts int #> snd)));
 
 
 (* classes *)
diff -r 4bf450d50c32 -r 5b2af04ec9fb src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 17 11:42:25 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 17 15:21:30 2008 +0200
@@ -96,24 +96,32 @@
   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
 
+  (* Interpretation *)
+  val get_interpret_morph: theory -> string -> string ->
+    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
+    string -> term list -> Morphism.morphism
   val interpretation_i: (Proof.context -> Proof.context) ->
     bool * string -> expr ->
     term option list * (Attrib.binding * term) list ->
-    theory -> Proof.state
+    theory ->
+    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   val interpretation: (Proof.context -> Proof.context) ->
     bool * string -> expr ->
     string option list * (Attrib.binding * string) list ->
-    theory -> Proof.state
+    theory ->
+    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
   val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
     bool * string -> expr ->
     term option list * (Attrib.binding * term) list ->
-    bool -> Proof.state -> Proof.state
+    bool -> Proof.state ->
+    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   val interpret: (Proof.state -> Proof.state Seq.seq) ->
     bool * string -> expr ->
     string option list * (Attrib.binding * string) list ->
-    bool -> Proof.state -> Proof.state
+    bool -> Proof.state ->
+    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
 end;
 
 structure Locale: LOCALE =
@@ -240,8 +248,12 @@
       T * (term list * (((bool * string) * string) * Element.witness list)) list
     val add_witness: term list -> Element.witness -> T -> T
     val add_equation: term list -> thm -> T -> T
-(*    val update_morph: term list -> Element.witness list * thm list -> T -> T *)
-(*    val get_morph: theory -> T -> term list -> string list -> Morphism.morphism *)
+(*
+    val update_morph: term list -> Morphism.morphism -> T -> T
+    val get_morph: theory -> T ->
+      term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
+      Morphism.morphism
+*)
   end =
 struct
   (* A registration is indexed by parameter instantiation.
@@ -350,15 +362,6 @@
       (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
       ts regs;
 
-  (* update morphism of registration;
-     only if instantiation is exact, otherwise exception Option raised *)
-(*
-  fun update_morph ts (wits, eqns') regs =
-    gen_add (fn (x, e, i, thms, eqns, _) =>
-      (x, e, i, thms, eqns, (wits, eqns')))
-      ts regs;
-*)
-
 end;
 
 
@@ -1646,19 +1649,24 @@
   in ((tinst, inst), wits, eqns) end;
 
 
-(* standardise export morphism *)
-
-(* clone from Element.generalize_facts *)
-fun standardize thy export facts =
+(* compute morphism and apply to args *)
+
+fun inst_morph thy prfx param_prfx insts prems eqns export =
   let
+    (* standardise export morphism *)
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
       (* FIXME sync with exp_fact *)
     val exp_typ = Logic.type_map exp_term;
-    val morphism =
+    val export' =
       Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
-  in Element.facts_map (Element.morph_ctxt morphism) facts end;
-
+  in
+    Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
+      Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
+      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
+      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
+      export'
+  end;
 
 fun morph_ctxt' phi = Element.map_ctxt
   {name = I,
@@ -1668,20 +1676,21 @@
    fact = Morphism.fact phi,
    attrib = Args.morph_values phi};
 
-
-(* compute morphism and apply to args *)
-
-fun inst_morph thy prfx param_prfx insts prems eqns =
-  Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
-    Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
-    Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
-    Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
-
-fun interpret_args thy inst exp attrib args =
-  args |> Element.facts_map (morph_ctxt' inst) |>
-(* morph_ctxt' suppresses application of name morphism.  FIXME *)
-    standardize thy exp |> Attrib.map_facts attrib;
-
+fun interpret_args thy inst attrib args =
+  args |> Element.facts_map (morph_ctxt' inst) |> Attrib.map_facts attrib;
+    (* morph_ctxt' suppresses application of name morphism.  FIXME *)
+
+(* public interface to interpretation morphism *)
+
+fun get_interpret_morph thy prfx param_prfx (exp, imp) target ext_ts =
+  let
+    val parms = the_locale thy target |> #params |> map fst;
+    val ids = flatten (ProofContext.init thy, intern_expr thy)
+      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
+    val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
+  in
+    inst_morph thy prfx param_prfx insts prems eqns exp
+  end;
 
 (* store instantiations of args for all registered interpretations
    of the theory *)
@@ -1700,7 +1709,7 @@
         val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
         val attrib = Attrib.attribute_i thy;
         val args' = args
-          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns) exp attrib
+          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns exp) attrib
           |> add_param_prefixss pprfx;
       in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   in fold activate regs thy end;
@@ -2110,7 +2119,7 @@
         let
           val ctxt = mk_ctxt thy_ctxt;
           val facts' = facts |>
-              interpret_args (ProofContext.theory_of ctxt) inst exp (attrib thy_ctxt) |>
+              interpret_args (ProofContext.theory_of ctxt) inst (attrib thy_ctxt) |>
               add_param_prefixss pprfx;
         in snd (note_interp kind loc prfx facts' thy_ctxt) end
       | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
@@ -2125,7 +2134,7 @@
         val ids = flatten (ProofContext.init thy, intern_expr thy)
           (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
         val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
-        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns;
+        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns exp;
       in
         fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt
       end;
@@ -2284,7 +2293,9 @@
 
     val propss = map extract_asms_elems inst_elemss @ eqn_elems;
 
-  in (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs) end;
+  in
+    (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
+  end;
 
 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   test_global_registration
@@ -2416,7 +2427,7 @@
 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
   (* prfx = (flag indicating full qualification, name prefix) *)
   let
-    val (propss, activate) = prep_registration thy prfx raw_expr raw_insts;
+    val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
     fun after_qed' results =
       ProofContext.theory (activate (prep_result propss results))
       #> after_qed;
@@ -2426,6 +2437,7 @@
     |> Proof.theorem_i NONE after_qed' (prep_propp propss)
     |> Element.refine_witness
     |> Seq.hd
+    |> pair morphs
   end;
 
 fun gen_interpret prep_registration after_qed prfx expr insts int state =
@@ -2433,7 +2445,7 @@
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
-    val (propss, activate) = prep_registration ctxt prfx expr insts;
+    val (propss, activate, morphs) = prep_registration ctxt prfx expr insts;
     fun after_qed' results =
       Proof.map_context (K (ctxt |> activate (prep_result propss results)))
       #> Proof.put_facts NONE
@@ -2443,6 +2455,7 @@
     |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
       "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
     |> Element.refine_witness |> Seq.hd
+    |> pair morphs
   end;
 
 in