Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: interpretation.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Isar/interpretation.ML
    Author:     Clemens Ballarin, TU Muenchen
    Author:     Florian Haftmann, TU Muenchen

Locale interpretation.
*)

signature INTERPRETATION =
sig
  type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list

  (*interpretation in proofs*)
  val interpret: Expression.expression_i -> Proof.state -> Proof.state
  val interpret_cmd: Expression.expression -> Proof.state -> Proof.state

  (*interpretation in local theories*)
  val interpretation: Expression.expression_i -> local_theory -> Proof.state
  val interpretation_cmd: Expression.expression -> local_theory -> Proof.state

  (*interpretation into global theories*)
  val global_interpretation: Expression.expression_i ->
    term defines -> local_theory -> Proof.state
  val global_interpretation_cmd: Expression.expression ->
    string defines -> local_theory -> Proof.state

  (*interpretation between locales*)
  val sublocale: Expression.expression_i ->
    term defines -> local_theory -> Proof.state
  val sublocale_cmd: Expression.expression ->
    string defines -> local_theory -> Proof.state
  val global_sublocale: string -> Expression.expression_i ->
    term defines -> theory -> Proof.state
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
    string defines -> theory -> Proof.state

  (*mixed Isar interface*)
  val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state
  val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state
end;

structure Interpretation : INTERPRETATION =
struct

(** common interpretation machinery **)

type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list

(* reading of locale expressions with rewrite morphisms *)

local

fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
  let
    val rhs = prep_term lthy raw_rhs;
    val lthy' = Variable.declare_term rhs lthy;
    val ((_, (_, def)), lthy'') =
      Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
  in (Thm.symmetric def, lthy'') end;

fun augment_with_defs _ [] _ = pair []
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
  | augment_with_defs prep_term raw_defs deps =
      Local_Theory.begin_nested
      #> snd
      #> fold Locale.activate_declarations deps
      #> fold_map (augment_with_def prep_term) raw_defs
      #> Local_Theory.end_nested_result Morphism.fact;

fun prep_interpretation prep_expr prep_term
  expression raw_defs initial_ctxt =
  let
    val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
    val (def_eqns, def_ctxt) =
      augment_with_defs prep_term raw_defs deps expr_ctxt;
    val export' = Proof_Context.export_morphism def_ctxt expr_ctxt;
  in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end;

in

fun cert_interpretation expression =
  prep_interpretation Expression.cert_goal_expression Syntax.check_term expression;

fun read_interpretation expression =
  prep_interpretation Expression.read_goal_expression Syntax.read_term expression;

end;

(* interpretation machinery *)

local

fun abs_def_rule eqns ctxt =
  (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);

fun note_eqns_register note add_registration
    deps eqnss witss def_eqns thms export export' ctxt =
  let
    val factss = thms
      |> unflat ((map o map) #1 eqnss)
      |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
    val (eqnss', ctxt') =
      fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
    val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
    val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
    val deps' =
      (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
    fun register (dep, eqns) ctxt =
      ctxt |> add_registration
        {inst = dep,
          mixin =
            Option.map (rpair true)
              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
          export = export};
  in ctxt'' |> fold register (deps' ~~ eqnss') end;

in

fun generic_interpretation prep_interpretation setup_proof note add_registration
    expression raw_defs initial_ctxt =
  let
    val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
      prep_interpretation expression raw_defs initial_ctxt;
    fun after_qed witss eqns =
      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
  in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;

end;

(** interfaces **)

(* interpretation in proofs *)

local

fun setup_proof state after_qed propss eqns goal_ctxt =
  Element.witness_local_proof_eqs
    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
    "interpret" propss eqns goal_ctxt state;

fun gen_interpret prep_interpretation expression state =
  Proof.assert_forward_or_chain state
  |> Proof.context_of
  |> generic_interpretation prep_interpretation (setup_proof state)
    Attrib.local_notes Locale.add_registration_proof expression [];

in

val interpret = gen_interpret cert_interpretation;
val interpret_cmd = gen_interpret read_interpretation;

end;

(* interpretation in local theories *)

val add_registration_local_theory =
  Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;

fun interpretation expression =
  generic_interpretation cert_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind add_registration_local_theory expression [];

fun interpretation_cmd expression =
  generic_interpretation read_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind add_registration_local_theory expression [];

(* interpretation into global theories *)

fun global_interpretation expression =
  generic_interpretation cert_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind Local_Theory.theory_registration expression;

fun global_interpretation_cmd expression =
  generic_interpretation read_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind Local_Theory.theory_registration expression;

(* interpretation between locales *)

fun sublocale expression =
  generic_interpretation cert_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;

fun sublocale_cmd expression =
  generic_interpretation read_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;

local

fun gen_global_sublocale prep_loc prep_interpretation
    raw_locale expression raw_defs thy =
  let
    val lthy = Named_Target.init [] (prep_loc thy raw_locale) thy;
    fun setup_proof after_qed =
      Element.witness_proof_eqs
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
  in
    lthy |>
      generic_interpretation prep_interpretation setup_proof
        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs
  end;

in

fun global_sublocale expression =
  gen_global_sublocale (K I) cert_interpretation expression;

fun global_sublocale_cmd raw_expression =
  gen_global_sublocale Locale.check read_interpretation raw_expression;

end;

(* mixed Isar interface *)

local

fun register_or_activate lthy =
  if Named_Target.is_theory lthy
  then Local_Theory.theory_registration
  else add_registration_local_theory;

fun gen_isar_interpretation prep_interpretation expression lthy =
  generic_interpretation prep_interpretation Element.witness_proof_eqs
    Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy;

in

fun isar_interpretation expression =
  gen_isar_interpretation cert_interpretation expression;
fun isar_interpretation_cmd raw_expression =
  gen_isar_interpretation read_interpretation raw_expression;

end;

end;

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.