src/Pure/Isar/interpretation.ML
author wenzelm
Fri Feb 23 14:12:48 2018 +0100 (24 months ago ago)
changeset 67702 2d9918f5b33c
parent 67450 b0ae74b86ef3
child 67740 b6ce18784872
permissions -rw-r--r--
command 'interpret' no longer exposes resulting theorems as literal facts;
     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   type 'a rewrites = (Attrib.binding * 'a) list
    12 
    13   (*interpretation in proofs*)
    14   val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state
    15   val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state
    16 
    17   (*interpretation in local theories*)
    18   val interpretation: Expression.expression_i ->
    19     term rewrites -> local_theory -> Proof.state
    20   val interpretation_cmd: Expression.expression ->
    21     string rewrites -> local_theory -> Proof.state
    22 
    23   (*interpretation into global theories*)
    24   val global_interpretation: Expression.expression_i ->
    25     term defines -> term rewrites -> local_theory -> Proof.state
    26   val global_interpretation_cmd: Expression.expression ->
    27     string defines -> string rewrites -> local_theory -> Proof.state
    28 
    29   (*interpretation between locales*)
    30   val sublocale: Expression.expression_i ->
    31     term defines -> term rewrites -> local_theory -> Proof.state
    32   val sublocale_cmd: Expression.expression ->
    33     string defines -> string rewrites -> local_theory -> Proof.state
    34   val global_sublocale: string -> Expression.expression_i ->
    35     term defines -> term rewrites -> theory -> Proof.state
    36   val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
    37     string defines -> string rewrites -> theory -> Proof.state
    38 
    39   (*mixed Isar interface*)
    40   val isar_interpretation: Expression.expression_i ->
    41     term rewrites -> local_theory -> Proof.state
    42   val isar_interpretation_cmd: Expression.expression ->
    43     string rewrites -> local_theory -> Proof.state
    44 end;
    45 
    46 structure Interpretation : INTERPRETATION =
    47 struct
    48 
    49 (** common interpretation machinery **)
    50 
    51 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
    52 type 'a rewrites = (Attrib.binding * 'a) list
    53 
    54 (* reading of locale expressions with rewrite morphisms *)
    55 
    56 local
    57 
    58 fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
    59   let
    60     val rhs = prep_term lthy raw_rhs;
    61     val lthy' = Variable.declare_term rhs lthy;
    62     val ((_, (_, def)), lthy'') =
    63       Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
    64   in (def, lthy'') end;
    65 
    66 fun augment_with_defs _ [] _ ctxt = ([], ctxt)
    67       (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
    68   | augment_with_defs prep_term raw_defs deps lthy =
    69       let
    70         val (_, inner_lthy) =
    71           Local_Theory.open_target lthy
    72           ||> fold Locale.activate_declarations deps;
    73         val (inner_defs, inner_lthy') =
    74           fold_map (augment_with_def prep_term) raw_defs inner_lthy;
    75         val lthy' =
    76           inner_lthy'
    77           |> Local_Theory.close_target;
    78         val def_eqns =
    79           map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
    80       in (def_eqns, lthy') end;
    81 
    82 fun prep_eqns _ _ [] _ _ = ([], [])
    83   | prep_eqns prep_props prep_attr raw_eqns deps ctxt =
    84       let
    85         (* FIXME incompatibility, creating context for parsing rewrites equation may fail in
    86            presence of replaces clause *)
    87         val ctxt' = fold Locale.activate_declarations deps ctxt;
    88         val eqns =
    89           (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns;
    90         val attrss = map (apsnd (map (prep_attr ctxt)) o fst) raw_eqns;
    91       in (eqns, attrss) end;
    92 
    93 fun prep_interpretation prep_expr prep_term prep_props prep_attr
    94   expression raw_defs raw_eqns initial_ctxt =
    95   let
    96     val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
    97     val (def_eqns, def_ctxt) =
    98       augment_with_defs prep_term raw_defs deps expr_ctxt;
    99     val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt;
   100     val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
   101     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   102   in (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
   103 
   104 in
   105 
   106 fun cert_interpretation expression =
   107   prep_interpretation Expression.cert_goal_expression Syntax.check_term
   108     Syntax.check_props (K I) expression;
   109 
   110 fun read_interpretation expression =
   111   prep_interpretation Expression.read_goal_expression Syntax.read_term
   112     Syntax.read_props Attrib.check_src expression;
   113 
   114 end;
   115 
   116 
   117 (* interpretation machinery *)
   118 
   119 local
   120 
   121 fun meta_rewrite eqns ctxt =
   122   (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
   123 
   124 fun note_eqns_register pos note activate deps eqnss witss def_eqns thms attrss export export' ctxt =
   125   let
   126     val (thmss, thms') = split_last (unflat ((map o map) fst eqnss @ [attrss]) thms);
   127     val factss =
   128       map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss;
   129     val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
   130     val facts =
   131       (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) ::
   132         map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])]))
   133           attrss thms';
   134     val (eqns', ctxt'') = ctxt'
   135       |> note Thm.theoremK facts
   136       |-> meta_rewrite;
   137     val dep_morphs =
   138       map2 (fn (dep, morph) => fn wits =>
   139         let val morph' = morph
   140           $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
   141           $> Morphism.binding_morphism "position" (Binding.set_pos pos)
   142         in (dep, morph') end) deps witss;
   143     fun activate' (dep_morph, eqns) ctxt =
   144       activate dep_morph
   145         (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
   146         export ctxt;
   147   in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end;
   148 
   149 in
   150 
   151 fun generic_interpretation prep_interpretation setup_proof note add_registration
   152     expression raw_defs raw_eqns initial_ctxt =
   153   let
   154     val (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
   155       prep_interpretation expression raw_defs raw_eqns initial_ctxt;
   156     val pos = Position.thread_data ();
   157     fun after_qed witss eqns =
   158       note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns attrss export export';
   159   in setup_proof after_qed propss (flat (eq_propss @ [eqns])) goal_ctxt end;
   160 
   161 end;
   162 
   163 
   164 (** interfaces **)
   165 
   166 (* interpretation in proofs *)
   167 
   168 local
   169 
   170 fun gen_interpret prep_interpretation expression raw_eqns state =
   171   let
   172     val _ = Proof.assert_forward_or_chain state;
   173     fun lift_after_qed after_qed witss eqns =
   174       Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
   175     fun setup_proof after_qed propss eqns goal_ctxt =
   176       Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
   177         propss eqns goal_ctxt state;
   178     fun add_registration reg mixin export ctxt = ctxt
   179       |> Proof_Context.set_stmt false
   180       |> Context.proof_map (Locale.add_registration reg mixin export)
   181       |> Proof_Context.restore_stmt ctxt;
   182   in
   183     Proof.context_of state
   184     |> generic_interpretation prep_interpretation setup_proof
   185       Attrib.local_notes add_registration expression [] raw_eqns
   186   end;
   187 
   188 in
   189 
   190 val interpret = gen_interpret cert_interpretation;
   191 val interpret_cmd = gen_interpret read_interpretation;
   192 
   193 end;
   194 
   195 
   196 (* interpretation in local theories *)
   197 
   198 fun interpretation expression =
   199   generic_interpretation cert_interpretation Element.witness_proof_eqs
   200     Local_Theory.notes_kind Locale.activate_fragment expression [];
   201 
   202 fun interpretation_cmd expression =
   203   generic_interpretation read_interpretation Element.witness_proof_eqs
   204     Local_Theory.notes_kind Locale.activate_fragment expression [];
   205 
   206 
   207 (* interpretation into global theories *)
   208 
   209 fun global_interpretation expression =
   210   generic_interpretation cert_interpretation Element.witness_proof_eqs
   211     Local_Theory.notes_kind Local_Theory.theory_registration expression;
   212 
   213 fun global_interpretation_cmd expression =
   214   generic_interpretation read_interpretation Element.witness_proof_eqs
   215     Local_Theory.notes_kind Local_Theory.theory_registration expression;
   216 
   217 
   218 (* interpretation between locales *)
   219 
   220 fun sublocale expression =
   221   generic_interpretation cert_interpretation Element.witness_proof_eqs
   222     Local_Theory.notes_kind Local_Theory.locale_dependency expression;
   223 
   224 fun sublocale_cmd expression =
   225   generic_interpretation read_interpretation Element.witness_proof_eqs
   226     Local_Theory.notes_kind Local_Theory.locale_dependency expression;
   227 
   228 local
   229 
   230 fun gen_global_sublocale prep_loc prep_interpretation
   231     raw_locale expression raw_defs raw_eqns thy =
   232   let
   233     val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
   234     fun setup_proof after_qed =
   235       Element.witness_proof_eqs
   236         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   237   in
   238     lthy |>
   239       generic_interpretation prep_interpretation setup_proof
   240         Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
   241   end;
   242 
   243 in
   244 
   245 fun global_sublocale expression =
   246   gen_global_sublocale (K I) cert_interpretation expression;
   247 
   248 fun global_sublocale_cmd raw_expression =
   249   gen_global_sublocale Locale.check read_interpretation raw_expression;
   250 
   251 end;
   252 
   253 
   254 (* mixed Isar interface *)
   255 
   256 local
   257 
   258 fun register_or_activate lthy =
   259   if Named_Target.is_theory lthy
   260   then Local_Theory.theory_registration
   261   else Locale.activate_fragment;
   262 
   263 fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
   264   generic_interpretation prep_interpretation Element.witness_proof_eqs
   265     Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy;
   266 
   267 in
   268 
   269 fun isar_interpretation expression =
   270   gen_isar_interpretation cert_interpretation expression;
   271 fun isar_interpretation_cmd raw_expression =
   272   gen_isar_interpretation read_interpretation raw_expression;
   273 
   274 end;
   275 
   276 end;