Public interface to interpretation morphism.
authorballarin
Wed Sep 17 15:21:30 2008 +0200 (2008-09-17)
changeset 282595b2af04ec9fb
parent 28258 4bf450d50c32
child 28260 703046c93ffe
Public interface to interpretation morphism.
doc-src/Locales/Locales/document/Examples3.tex
src/Pure/Isar/class.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
     1.1 --- a/doc-src/Locales/Locales/document/Examples3.tex	Wed Sep 17 11:42:25 2008 +0200
     1.2 +++ b/doc-src/Locales/Locales/document/Examples3.tex	Wed Sep 17 15:21:30 2008 +0200
     1.3 @@ -91,8 +91,8 @@
     1.4  \begin{isamarkuptext}%
     1.5  Further interpretations are necessary to reuse theorems from
     1.6    the other locales.  In \isa{lattice} the operations \isa{{\isasymsqinter}} and
     1.7 -  \isa{{\isasymsqunion}} are substituted by \isa{min} and
     1.8 -  \isa{max}.  The entire proof for the
     1.9 +  \isa{{\isasymsqunion}} are substituted by \isa{ord{\isacharunderscore}class{\isachardot}min} and
    1.10 +  \isa{ord{\isacharunderscore}class{\isachardot}max}.  The entire proof for the
    1.11    interpretation is reproduced in order to give an example of a more
    1.12    elaborate interpretation proof.%
    1.13  \end{isamarkuptext}%
    1.14 @@ -196,9 +196,9 @@
    1.15    \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
    1.16    \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
    1.17    \isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
    1.18 -  \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
    1.19 +  \quad \isa{ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
    1.20    \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
    1.21 -  \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}} \\
    1.22 +  \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}} \\
    1.23    \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
    1.24    \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
    1.25  \end{tabular}
     2.1 --- a/src/Pure/Isar/class.ML	Wed Sep 17 11:42:25 2008 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Sep 17 15:21:30 2008 +0200
     2.3 @@ -63,7 +63,7 @@
     2.4  (** auxiliary **)
     2.5  
     2.6  fun prove_interpretation tac prfx_atts expr inst =
     2.7 -  Locale.interpretation_i I prfx_atts expr inst
     2.8 +  Locale.interpretation_i I prfx_atts expr inst #> snd
     2.9    #> Proof.global_terminal_proof
    2.10        (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
    2.11    #> ProofContext.theory_of;
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Sep 17 11:42:25 2008 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 17 15:21:30 2008 +0200
     3.3 @@ -400,7 +400,7 @@
     3.4        opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
     3.5          >> (fn ((name, expr), insts) => Toplevel.print o
     3.6              Toplevel.theory_to_proof
     3.7 -              (Locale.interpretation I (true, Name.name_of name) expr insts)));
     3.8 +              (Locale.interpretation I (true, Name.name_of name) expr insts #> snd)));
     3.9  
    3.10  val _ =
    3.11    OuterSyntax.command "interpret"
    3.12 @@ -409,7 +409,7 @@
    3.13      (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
    3.14        >> (fn ((name, expr), insts) => Toplevel.print o
    3.15            Toplevel.proof'
    3.16 -            (Locale.interpret Seq.single (true, Name.name_of name) expr insts)));
    3.17 +            (fn int => Locale.interpret Seq.single (true, Name.name_of name) expr insts int #> snd)));
    3.18  
    3.19  
    3.20  (* classes *)
     4.1 --- a/src/Pure/Isar/locale.ML	Wed Sep 17 11:42:25 2008 +0200
     4.2 +++ b/src/Pure/Isar/locale.ML	Wed Sep 17 15:21:30 2008 +0200
     4.3 @@ -96,24 +96,32 @@
     4.4    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
     4.5    val add_declaration: string -> declaration -> Proof.context -> Proof.context
     4.6  
     4.7 +  (* Interpretation *)
     4.8 +  val get_interpret_morph: theory -> string -> string ->
     4.9 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    4.10 +    string -> term list -> Morphism.morphism
    4.11    val interpretation_i: (Proof.context -> Proof.context) ->
    4.12      bool * string -> expr ->
    4.13      term option list * (Attrib.binding * term) list ->
    4.14 -    theory -> Proof.state
    4.15 +    theory ->
    4.16 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    4.17    val interpretation: (Proof.context -> Proof.context) ->
    4.18      bool * string -> expr ->
    4.19      string option list * (Attrib.binding * string) list ->
    4.20 -    theory -> Proof.state
    4.21 +    theory ->
    4.22 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    4.23    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    4.24      xstring * expr -> theory -> Proof.state
    4.25    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    4.26      bool * string -> expr ->
    4.27      term option list * (Attrib.binding * term) list ->
    4.28 -    bool -> Proof.state -> Proof.state
    4.29 +    bool -> Proof.state ->
    4.30 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    4.31    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    4.32      bool * string -> expr ->
    4.33      string option list * (Attrib.binding * string) list ->
    4.34 -    bool -> Proof.state -> Proof.state
    4.35 +    bool -> Proof.state ->
    4.36 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    4.37  end;
    4.38  
    4.39  structure Locale: LOCALE =
    4.40 @@ -240,8 +248,12 @@
    4.41        T * (term list * (((bool * string) * string) * Element.witness list)) list
    4.42      val add_witness: term list -> Element.witness -> T -> T
    4.43      val add_equation: term list -> thm -> T -> T
    4.44 -(*    val update_morph: term list -> Element.witness list * thm list -> T -> T *)
    4.45 -(*    val get_morph: theory -> T -> term list -> string list -> Morphism.morphism *)
    4.46 +(*
    4.47 +    val update_morph: term list -> Morphism.morphism -> T -> T
    4.48 +    val get_morph: theory -> T ->
    4.49 +      term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
    4.50 +      Morphism.morphism
    4.51 +*)
    4.52    end =
    4.53  struct
    4.54    (* A registration is indexed by parameter instantiation.
    4.55 @@ -350,15 +362,6 @@
    4.56        (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
    4.57        ts regs;
    4.58  
    4.59 -  (* update morphism of registration;
    4.60 -     only if instantiation is exact, otherwise exception Option raised *)
    4.61 -(*
    4.62 -  fun update_morph ts (wits, eqns') regs =
    4.63 -    gen_add (fn (x, e, i, thms, eqns, _) =>
    4.64 -      (x, e, i, thms, eqns, (wits, eqns')))
    4.65 -      ts regs;
    4.66 -*)
    4.67 -
    4.68  end;
    4.69  
    4.70  
    4.71 @@ -1646,19 +1649,24 @@
    4.72    in ((tinst, inst), wits, eqns) end;
    4.73  
    4.74  
    4.75 -(* standardise export morphism *)
    4.76 -
    4.77 -(* clone from Element.generalize_facts *)
    4.78 -fun standardize thy export facts =
    4.79 +(* compute morphism and apply to args *)
    4.80 +
    4.81 +fun inst_morph thy prfx param_prfx insts prems eqns export =
    4.82    let
    4.83 +    (* standardise export morphism *)
    4.84      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
    4.85      val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
    4.86        (* FIXME sync with exp_fact *)
    4.87      val exp_typ = Logic.type_map exp_term;
    4.88 -    val morphism =
    4.89 +    val export' =
    4.90        Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
    4.91 -  in Element.facts_map (Element.morph_ctxt morphism) facts end;
    4.92 -
    4.93 +  in
    4.94 +    Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
    4.95 +      Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
    4.96 +      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
    4.97 +      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
    4.98 +      export'
    4.99 +  end;
   4.100  
   4.101  fun morph_ctxt' phi = Element.map_ctxt
   4.102    {name = I,
   4.103 @@ -1668,20 +1676,21 @@
   4.104     fact = Morphism.fact phi,
   4.105     attrib = Args.morph_values phi};
   4.106  
   4.107 -
   4.108 -(* compute morphism and apply to args *)
   4.109 -
   4.110 -fun inst_morph thy prfx param_prfx insts prems eqns =
   4.111 -  Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
   4.112 -    Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   4.113 -    Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   4.114 -    Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
   4.115 -
   4.116 -fun interpret_args thy inst exp attrib args =
   4.117 -  args |> Element.facts_map (morph_ctxt' inst) |>
   4.118 -(* morph_ctxt' suppresses application of name morphism.  FIXME *)
   4.119 -    standardize thy exp |> Attrib.map_facts attrib;
   4.120 -
   4.121 +fun interpret_args thy inst attrib args =
   4.122 +  args |> Element.facts_map (morph_ctxt' inst) |> Attrib.map_facts attrib;
   4.123 +    (* morph_ctxt' suppresses application of name morphism.  FIXME *)
   4.124 +
   4.125 +(* public interface to interpretation morphism *)
   4.126 +
   4.127 +fun get_interpret_morph thy prfx param_prfx (exp, imp) target ext_ts =
   4.128 +  let
   4.129 +    val parms = the_locale thy target |> #params |> map fst;
   4.130 +    val ids = flatten (ProofContext.init thy, intern_expr thy)
   4.131 +      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
   4.132 +    val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   4.133 +  in
   4.134 +    inst_morph thy prfx param_prfx insts prems eqns exp
   4.135 +  end;
   4.136  
   4.137  (* store instantiations of args for all registered interpretations
   4.138     of the theory *)
   4.139 @@ -1700,7 +1709,7 @@
   4.140          val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   4.141          val attrib = Attrib.attribute_i thy;
   4.142          val args' = args
   4.143 -          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns) exp attrib
   4.144 +          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns exp) attrib
   4.145            |> add_param_prefixss pprfx;
   4.146        in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   4.147    in fold activate regs thy end;
   4.148 @@ -2110,7 +2119,7 @@
   4.149          let
   4.150            val ctxt = mk_ctxt thy_ctxt;
   4.151            val facts' = facts |>
   4.152 -              interpret_args (ProofContext.theory_of ctxt) inst exp (attrib thy_ctxt) |>
   4.153 +              interpret_args (ProofContext.theory_of ctxt) inst (attrib thy_ctxt) |>
   4.154                add_param_prefixss pprfx;
   4.155          in snd (note_interp kind loc prfx facts' thy_ctxt) end
   4.156        | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
   4.157 @@ -2125,7 +2134,7 @@
   4.158          val ids = flatten (ProofContext.init thy, intern_expr thy)
   4.159            (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
   4.160          val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
   4.161 -        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns;
   4.162 +        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns exp;
   4.163        in
   4.164          fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt
   4.165        end;
   4.166 @@ -2284,7 +2293,9 @@
   4.167  
   4.168      val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   4.169  
   4.170 -  in (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs) end;
   4.171 +  in
   4.172 +    (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
   4.173 +  end;
   4.174  
   4.175  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   4.176    test_global_registration
   4.177 @@ -2416,7 +2427,7 @@
   4.178  fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
   4.179    (* prfx = (flag indicating full qualification, name prefix) *)
   4.180    let
   4.181 -    val (propss, activate) = prep_registration thy prfx raw_expr raw_insts;
   4.182 +    val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
   4.183      fun after_qed' results =
   4.184        ProofContext.theory (activate (prep_result propss results))
   4.185        #> after_qed;
   4.186 @@ -2426,6 +2437,7 @@
   4.187      |> Proof.theorem_i NONE after_qed' (prep_propp propss)
   4.188      |> Element.refine_witness
   4.189      |> Seq.hd
   4.190 +    |> pair morphs
   4.191    end;
   4.192  
   4.193  fun gen_interpret prep_registration after_qed prfx expr insts int state =
   4.194 @@ -2433,7 +2445,7 @@
   4.195    let
   4.196      val _ = Proof.assert_forward_or_chain state;
   4.197      val ctxt = Proof.context_of state;
   4.198 -    val (propss, activate) = prep_registration ctxt prfx expr insts;
   4.199 +    val (propss, activate, morphs) = prep_registration ctxt prfx expr insts;
   4.200      fun after_qed' results =
   4.201        Proof.map_context (K (ctxt |> activate (prep_result propss results)))
   4.202        #> Proof.put_facts NONE
   4.203 @@ -2443,6 +2455,7 @@
   4.204      |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
   4.205        "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
   4.206      |> Element.refine_witness |> Seq.hd
   4.207 +    |> pair morphs
   4.208    end;
   4.209  
   4.210  in