src/Pure/Isar/interpretation.ML
author wenzelm
Thu Aug 30 14:38:24 2018 +0200 (14 months ago)
changeset 68854 404e04f649d4
parent 68852 becaeaa334ae
child 68855 59ce31e15c33
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Isar/interpretation.ML
     2     Author:     Clemens Ballarin, TU Muenchen
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Locale interpretation.
     6 *)
     7 
     8 signature INTERPRETATION =
     9 sig
    10   type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
    11 
    12   (*interpretation in proofs*)
    13   val interpret: Expression.expression_i -> Proof.state -> Proof.state
    14   val interpret_cmd: Expression.expression -> Proof.state -> Proof.state
    15 
    16   (*interpretation in local theories*)
    17   val interpretation: Expression.expression_i -> local_theory -> Proof.state
    18   val interpretation_cmd: Expression.expression -> local_theory -> Proof.state
    19 
    20   (*interpretation into global theories*)
    21   val global_interpretation: Expression.expression_i ->
    22     term defines -> local_theory -> Proof.state
    23   val global_interpretation_cmd: Expression.expression ->
    24     string defines -> local_theory -> Proof.state
    25 
    26   (*interpretation between locales*)
    27   val sublocale: Expression.expression_i ->
    28     term defines -> local_theory -> Proof.state
    29   val sublocale_cmd: Expression.expression ->
    30     string defines -> local_theory -> Proof.state
    31   val global_sublocale: string -> Expression.expression_i ->
    32     term defines -> theory -> Proof.state
    33   val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
    34     string defines -> theory -> Proof.state
    35 
    36   (*mixed Isar interface*)
    37   val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state
    38   val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state
    39 end;
    40 
    41 structure Interpretation : INTERPRETATION =
    42 struct
    43 
    44 (** common interpretation machinery **)
    45 
    46 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
    47 
    48 (* reading of locale expressions with rewrite morphisms *)
    49 
    50 local
    51 
    52 fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
    53   let
    54     val rhs = prep_term lthy raw_rhs;
    55     val lthy' = Variable.declare_term rhs lthy;
    56     val ((_, (_, def)), lthy'') =
    57       Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
    58   in (def, lthy'') end;
    59 
    60 fun augment_with_defs _ [] _ ctxt = ([], ctxt)
    61       (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
    62   | augment_with_defs prep_term raw_defs deps lthy =
    63       let
    64         val (_, inner_lthy) =
    65           Local_Theory.open_target lthy
    66           ||> fold Locale.activate_declarations deps;
    67         val (inner_defs, inner_lthy') =
    68           fold_map (augment_with_def prep_term) raw_defs inner_lthy;
    69         val lthy' =
    70           inner_lthy'
    71           |> Local_Theory.close_target;
    72         val def_eqns =
    73           map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
    74       in (def_eqns, lthy') end;
    75 
    76 fun prep_interpretation prep_expr prep_term
    77   expression raw_defs initial_ctxt =
    78   let
    79     val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
    80     val (def_eqns, def_ctxt) =
    81       augment_with_defs prep_term raw_defs deps expr_ctxt;
    82     val export' = Variable.export_morphism def_ctxt expr_ctxt;
    83   in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end;
    84 
    85 in
    86 
    87 fun cert_interpretation expression =
    88   prep_interpretation Expression.cert_goal_expression Syntax.check_term expression;
    89 
    90 fun read_interpretation expression =
    91   prep_interpretation Expression.read_goal_expression Syntax.read_term expression;
    92 
    93 end;
    94 
    95 
    96 (* interpretation machinery *)
    97 
    98 local
    99 
   100 fun abs_def_rule eqns ctxt =
   101   (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
   102 
   103 fun note_eqns_register pos note add_registration
   104     deps eqnss witss def_eqns thms export export' ctxt =
   105   let
   106     val factss = thms
   107       |> unflat ((map o map) #1 eqnss)
   108       |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
   109     val (eqnss', ctxt') =
   110       fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
   111     val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
   112     val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
   113     val deps' =
   114       (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
   115         let val morph' = morph
   116           $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
   117           $> Morphism.binding_morphism "position" (Binding.set_pos pos)
   118         in (dep, morph') end);
   119     fun register (dep, eqns) ctxt =
   120       ctxt |> add_registration
   121         {dep = dep,
   122           mixin =
   123             Option.map (rpair true)
   124               (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
   125           export = export};
   126   in ctxt'' |> fold register (deps' ~~ eqnss') end;
   127 
   128 in
   129 
   130 fun generic_interpretation prep_interpretation setup_proof note add_registration
   131     expression raw_defs initial_ctxt =
   132   let
   133     val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
   134       prep_interpretation expression raw_defs initial_ctxt;
   135     val pos = Position.thread_data ();
   136     fun after_qed witss eqns =
   137       note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
   138   in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
   139 
   140 end;
   141 
   142 
   143 (** interfaces **)
   144 
   145 (* interpretation in proofs *)
   146 
   147 local
   148 
   149 fun setup_proof state after_qed propss eqns goal_ctxt =
   150   Element.witness_local_proof_eqs
   151     (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
   152     "interpret" propss eqns goal_ctxt state;
   153 
   154 fun gen_interpret prep_interpretation expression state =
   155   Proof.assert_forward_or_chain state
   156   |> Proof.context_of
   157   |> generic_interpretation prep_interpretation (setup_proof state)
   158     Attrib.local_notes Locale.add_registration_proof expression [];
   159 
   160 in
   161 
   162 val interpret = gen_interpret cert_interpretation;
   163 val interpret_cmd = gen_interpret read_interpretation;
   164 
   165 end;
   166 
   167 
   168 (* interpretation in local theories *)
   169 
   170 fun interpretation expression =
   171   generic_interpretation cert_interpretation Element.witness_proof_eqs
   172     Local_Theory.notes_kind Locale.activate_fragment expression [];
   173 
   174 fun interpretation_cmd expression =
   175   generic_interpretation read_interpretation Element.witness_proof_eqs
   176     Local_Theory.notes_kind Locale.activate_fragment expression [];
   177 
   178 
   179 (* interpretation into global theories *)
   180 
   181 fun global_interpretation expression =
   182   generic_interpretation cert_interpretation Element.witness_proof_eqs
   183     Local_Theory.notes_kind Local_Theory.theory_registration expression;
   184 
   185 fun global_interpretation_cmd expression =
   186   generic_interpretation read_interpretation Element.witness_proof_eqs
   187     Local_Theory.notes_kind Local_Theory.theory_registration expression;
   188 
   189 
   190 (* interpretation between locales *)
   191 
   192 fun sublocale expression =
   193   generic_interpretation cert_interpretation Element.witness_proof_eqs
   194     Local_Theory.notes_kind Local_Theory.locale_dependency expression;
   195 
   196 fun sublocale_cmd expression =
   197   generic_interpretation read_interpretation Element.witness_proof_eqs
   198     Local_Theory.notes_kind Local_Theory.locale_dependency expression;
   199 
   200 local
   201 
   202 fun gen_global_sublocale prep_loc prep_interpretation
   203     raw_locale expression raw_defs thy =
   204   let
   205     val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
   206     fun setup_proof after_qed =
   207       Element.witness_proof_eqs
   208         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   209   in
   210     lthy |>
   211       generic_interpretation prep_interpretation setup_proof
   212         Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs
   213   end;
   214 
   215 in
   216 
   217 fun global_sublocale expression =
   218   gen_global_sublocale (K I) cert_interpretation expression;
   219 
   220 fun global_sublocale_cmd raw_expression =
   221   gen_global_sublocale Locale.check read_interpretation raw_expression;
   222 
   223 end;
   224 
   225 
   226 (* mixed Isar interface *)
   227 
   228 local
   229 
   230 fun register_or_activate lthy =
   231   if Named_Target.is_theory lthy
   232   then Local_Theory.theory_registration
   233   else Locale.activate_fragment;
   234 
   235 fun gen_isar_interpretation prep_interpretation expression lthy =
   236   generic_interpretation prep_interpretation Element.witness_proof_eqs
   237     Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy;
   238 
   239 in
   240 
   241 fun isar_interpretation expression =
   242   gen_isar_interpretation cert_interpretation expression;
   243 fun isar_interpretation_cmd raw_expression =
   244   gen_isar_interpretation read_interpretation raw_expression;
   245 
   246 end;
   247 
   248 end;