coalesce permanent_interpretation.ML with interpretation.ML
authorhaftmann
Sat Nov 14 08:45:52 2015 +0100 (2015-11-14)
changeset 61670301e0b4ecd45
parent 61669 27ca6147e3b3
child 61671 20d4cd2ceab2
coalesce permanent_interpretation.ML with interpretation.ML
NEWS
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Setup.thy
src/Doc/Isar_Ref/Spec.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
src/HOL/IMP/Collecting.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/ROOT
src/Pure/Isar/interpretation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Tools/Permanent_Interpretation.thy
src/Tools/permanent_interpretation.ML
     1.1 --- a/NEWS	Sat Nov 14 08:45:51 2015 +0100
     1.2 +++ b/NEWS	Sat Nov 14 08:45:52 2015 +0100
     1.3 @@ -314,6 +314,9 @@
     1.4  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
     1.5  commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
     1.6  
     1.7 +* Command 'permanent_interpretation' is available in Pure, without
     1.8 +need to load a separate theory.
     1.9 +
    1.10  * Command 'print_definitions' prints dependencies of definitional
    1.11  specifications. This functionality used to be part of 'print_theory'.
    1.12  
     2.1 --- a/src/Doc/Codegen/Further.thy	Sat Nov 14 08:45:51 2015 +0100
     2.2 +++ b/src/Doc/Codegen/Further.thy	Sat Nov 14 08:45:52 2015 +0100
     2.3 @@ -220,8 +220,7 @@
     2.4  
     2.5  (*>*) text \<open>
     2.6    Fortunately, an even more succint approach is available using command
     2.7 -  @{command permanent_interpretation}.  This is available
     2.8 -  by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}.
     2.9 +  @{command permanent_interpretation}.
    2.10    Then the pattern above collapses to
    2.11  \<close> (*<*)
    2.12  
     3.1 --- a/src/Doc/Codegen/Setup.thy	Sat Nov 14 08:45:51 2015 +0100
     3.2 +++ b/src/Doc/Codegen/Setup.thy	Sat Nov 14 08:45:52 2015 +0100
     3.3 @@ -1,7 +1,6 @@
     3.4  theory Setup
     3.5  imports
     3.6    Complex_Main
     3.7 -  "~~/src/Tools/Permanent_Interpretation"
     3.8    "~~/src/HOL/Library/Dlist"
     3.9    "~~/src/HOL/Library/RBT"
    3.10    "~~/src/HOL/Library/Mapping"
     4.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Nov 14 08:45:51 2015 +0100
     4.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Nov 14 08:45:52 2015 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (*:maxLineLen=78:*)
     4.5  
     4.6  theory Spec
     4.7 -imports Base Main "~~/src/Tools/Permanent_Interpretation"
     4.8 +imports Base Main
     4.9  begin
    4.10  
    4.11  chapter \<open>Specifications\<close>
    4.12 @@ -739,9 +739,9 @@
    4.13  subsubsection \<open>Permanent locale interpretation\<close>
    4.14  
    4.15  text \<open>
    4.16 -  Permanent locale interpretation is a library extension on top of
    4.17 -  \<^theory_text>\<open>interpretation\<close> and \<^theory_text>\<open>sublocale\<close>. It is available by importing theory
    4.18 -  @{file "~~/src/Tools/Permanent_Interpretation.thy"} and provides
    4.19 +  Permanent locale interpretation is an extension on top
    4.20 +  of \<^theory_text>\<open>interpretation\<close> and \<^theory_text>\<open>sublocale\<close>
    4.21 +  and provides
    4.22  
    4.23      \<^enum> a unified view on arbitrary suitable local theories as interpretation
    4.24      target;
     5.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Sat Nov 14 08:45:51 2015 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Sat Nov 14 08:45:52 2015 +0100
     5.3 @@ -3,7 +3,7 @@
     5.4  section "Denotational Abstract Interpretation"
     5.5  
     5.6  theory Abs_Int_den0_fun
     5.7 -imports "~~/src/Tools/Permanent_Interpretation" "../Big_Step"
     5.8 +imports "../Big_Step"
     5.9  begin
    5.10  
    5.11  subsection "Orderings"
     6.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Sat Nov 14 08:45:51 2015 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
     6.3 @@ -1,9 +1,9 @@
     6.4  (* Author: Tobias Nipkow *)
     6.5  
     6.6  theory Abs_Int0_ITP
     6.7 -imports "~~/src/Tools/Permanent_Interpretation"
     6.8 -        "~~/src/HOL/Library/While_Combinator"
     6.9 -        "Collecting_ITP"
    6.10 +imports
    6.11 +  "~~/src/HOL/Library/While_Combinator"
    6.12 +  Collecting_ITP
    6.13  begin
    6.14  
    6.15  subsection "Orderings"
     7.1 --- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Sat Nov 14 08:45:51 2015 +0100
     7.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
     7.3 @@ -1,5 +1,5 @@
     7.4  theory Collecting_ITP
     7.5 -imports "~~/src/Tools/Permanent_Interpretation" Complete_Lattice_ix "ACom_ITP"
     7.6 +imports Complete_Lattice_ix "ACom_ITP"
     7.7  begin
     7.8  
     7.9  subsection "Collecting Semantics of Commands"
     8.1 --- a/src/HOL/IMP/Collecting.thy	Sat Nov 14 08:45:51 2015 +0100
     8.2 +++ b/src/HOL/IMP/Collecting.thy	Sat Nov 14 08:45:52 2015 +0100
     8.3 @@ -1,6 +1,5 @@
     8.4  theory Collecting
     8.5  imports Complete_Lattice Big_Step ACom
     8.6 -  "~~/src/Tools/Permanent_Interpretation"
     8.7  begin
     8.8  
     8.9  subsection "The generic Step function"
     9.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Nov 14 08:45:51 2015 +0100
     9.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sat Nov 14 08:45:52 2015 +0100
     9.3 @@ -5,7 +5,6 @@
     9.4  theory Groups_Big_Fun
     9.5  imports
     9.6    Main
     9.7 -  "~~/src/Tools/Permanent_Interpretation"
     9.8  begin
     9.9  
    9.10  subsection \<open>Abstract product\<close>
    10.1 --- a/src/HOL/ROOT	Sat Nov 14 08:45:51 2015 +0100
    10.2 +++ b/src/HOL/ROOT	Sat Nov 14 08:45:52 2015 +0100
    10.3 @@ -115,7 +115,6 @@
    10.4  session "HOL-IMP" in IMP = HOL +
    10.5    options [document_variants = document]
    10.6    theories [document = false]
    10.7 -    "~~/src/Tools/Permanent_Interpretation"
    10.8      "~~/src/HOL/Library/While_Combinator"
    10.9      "~~/src/HOL/Library/Char_ord"
   10.10      "~~/src/HOL/Library/List_lexord"
    11.1 --- a/src/Pure/Isar/interpretation.ML	Sat Nov 14 08:45:51 2015 +0100
    11.2 +++ b/src/Pure/Isar/interpretation.ML	Sat Nov 14 08:45:52 2015 +0100
    11.3 @@ -1,18 +1,24 @@
    11.4  (*  Title:      Pure/Isar/interpretation.ML
    11.5      Author:     Clemens Ballarin, TU Muenchen
    11.6 +    Author:     Florian Haftmann, TU Muenchen
    11.7  
    11.8  Locale interpretation.
    11.9  *)
   11.10  
   11.11  signature INTERPRETATION =
   11.12  sig
   11.13 -  val permanent_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
   11.14 -    local_theory -> Proof.state
   11.15 -  val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
   11.16 -    local_theory -> Proof.state
   11.17    val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
   11.18    val interpret_cmd: Expression.expression -> (Attrib.binding * string) list ->
   11.19      bool -> Proof.state -> Proof.state
   11.20 +  val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
   11.21 +    local_theory -> Proof.state
   11.22 +  val permanent_interpretation: Expression.expression_i ->
   11.23 +    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
   11.24 +    local_theory -> Proof.state
   11.25 +  val permanent_interpretation_cmd: Expression.expression ->
   11.26 +    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
   11.27 +    local_theory -> Proof.state
   11.28 +
   11.29    val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
   11.30    val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list ->
   11.31      local_theory -> Proof.state
   11.32 @@ -29,7 +35,9 @@
   11.33  
   11.34  local
   11.35  
   11.36 -(* reading *)
   11.37 +(** reading **)
   11.38 +
   11.39 +(* without mixin definitions *)
   11.40  
   11.41  fun prep_with_extended_syntax prep_prop deps ctxt props =
   11.42    let
   11.43 @@ -55,7 +63,44 @@
   11.44    prep_interpretation Expression.read_goal_expression Syntax.parse_prop Attrib.check_src;
   11.45  
   11.46  
   11.47 -(* generic interpretation machinery *)
   11.48 +(* with mixin definitions *)
   11.49 +
   11.50 +fun prep_interpretation_with_defs prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
   11.51 +  let
   11.52 +    (*reading*)
   11.53 +    val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
   11.54 +    val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
   11.55 +    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
   11.56 +    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
   11.57 +    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
   11.58 +
   11.59 +    (*defining*)
   11.60 +    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
   11.61 +      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
   11.62 +    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
   11.63 +    val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
   11.64 +    val def_eqns = defs
   11.65 +      |> map (Thm.symmetric o
   11.66 +        Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
   11.67 +
   11.68 +    (*setting up*)
   11.69 +    val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
   11.70 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
   11.71 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
   11.72 +  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
   11.73 +
   11.74 +val cert_interpretation_with_defs =
   11.75 +  prep_interpretation_with_defs Expression.cert_goal_expression (K I) (K I) (K I);
   11.76 +
   11.77 +val read_interpretation_with_defs =
   11.78 +  prep_interpretation_with_defs Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
   11.79 +
   11.80 +
   11.81 +(** generic interpretation machinery **)
   11.82 +
   11.83 +(* without mixin definitions *)
   11.84 +
   11.85 +local
   11.86  
   11.87  fun meta_rewrite ctxt eqns =
   11.88    map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
   11.89 @@ -80,6 +125,8 @@
   11.90      |> fold activate' dep_morphs
   11.91    end;
   11.92  
   11.93 +in
   11.94 +
   11.95  fun generic_interpretation prep_interpretation setup_proof note activate
   11.96      expression raw_eqns initial_ctxt =
   11.97    let
   11.98 @@ -89,8 +136,48 @@
   11.99        note_eqns_register note activate deps witss eqns attrss export export';
  11.100    in setup_proof after_qed propss eqns goal_ctxt end;
  11.101  
  11.102 +end;
  11.103  
  11.104 -(* first dimension: proof vs. local theory *)
  11.105 +
  11.106 +(* without mixin definitions *)
  11.107 +
  11.108 +local
  11.109 +
  11.110 +fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
  11.111 +
  11.112 +fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
  11.113 +  let
  11.114 +    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
  11.115 +      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
  11.116 +    val (eqns', ctxt') = ctxt
  11.117 +      |> note Thm.theoremK facts
  11.118 +      |-> meta_rewrite;
  11.119 +    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
  11.120 +      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
  11.121 +    fun activate' dep_morph ctxt = activate dep_morph
  11.122 +      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
  11.123 +  in
  11.124 +    ctxt'
  11.125 +    |> fold activate' dep_morphs
  11.126 +  end;
  11.127 +
  11.128 +in
  11.129 +
  11.130 +fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration
  11.131 +    expression raw_defs raw_eqns initial_ctxt =
  11.132 +  let
  11.133 +    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
  11.134 +      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
  11.135 +    fun after_qed witss eqns =
  11.136 +      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
  11.137 +  in setup_proof after_qed propss eqns goal_ctxt end;
  11.138 +
  11.139 +end;
  11.140 +
  11.141 +
  11.142 +(** first dimension: proof vs. local theory **)
  11.143 +
  11.144 +(* proof *)
  11.145  
  11.146  fun gen_interpret prep_interpretation expression raw_eqns int state =
  11.147    let
  11.148 @@ -106,12 +193,23 @@
  11.149        Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
  11.150    end;
  11.151  
  11.152 +
  11.153 +(* local theory *)
  11.154 +
  11.155  fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
  11.156    generic_interpretation prep_interpretation Element.witness_proof_eqs
  11.157      Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
  11.158  
  11.159  
  11.160 -(* second dimension: relation to underlying target *)
  11.161 +(* local theory with mixin definitions *)
  11.162 +
  11.163 +fun gen_interpretation_with_defs prep_interpretation expression raw_defs raw_eqns =
  11.164 +  Local_Theory.assert_bottom true
  11.165 +  #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
  11.166 +    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
  11.167 +
  11.168 +
  11.169 +(** second dimension: relation to underlying target **)
  11.170  
  11.171  fun subscribe_or_activate lthy =
  11.172    if Named_Target.is_theory lthy
  11.173 @@ -127,7 +225,7 @@
  11.174    in Local_Theory.subscription end;
  11.175  
  11.176  
  11.177 -(* special case: global sublocale command *)
  11.178 +(** special case: global sublocale command **)
  11.179  
  11.180  fun gen_sublocale_global prep_loc prep_interpretation
  11.181      raw_locale expression raw_eqns thy =
  11.182 @@ -145,19 +243,17 @@
  11.183  in
  11.184  
  11.185  
  11.186 -(* interfaces *)
  11.187 +(** interfaces **)
  11.188  
  11.189  fun interpret x = gen_interpret cert_interpretation x;
  11.190  fun interpret_cmd x = gen_interpret read_interpretation x;
  11.191  
  11.192 -fun permanent_interpretation expression raw_eqns =
  11.193 -  Local_Theory.assert_bottom true
  11.194 -  #> gen_local_theory_interpretation cert_interpretation
  11.195 -    (K Local_Theory.subscription) expression raw_eqns;
  11.196 -
  11.197  fun ephemeral_interpretation x =
  11.198    gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
  11.199  
  11.200 +fun permanent_interpretation x = gen_interpretation_with_defs cert_interpretation_with_defs x;
  11.201 +fun permanent_interpretation_cmd x = gen_interpretation_with_defs read_interpretation_with_defs x;
  11.202 +
  11.203  fun interpretation x =
  11.204    gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
  11.205  fun interpretation_cmd x =
    12.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
    12.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:52 2015 +0100
    12.3 @@ -417,6 +417,15 @@
    12.4          Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
    12.5  
    12.6  val _ =
    12.7 +  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
    12.8 +    "prove interpretation of locale expression into named theory"
    12.9 +    (Parse.!!! (Parse_Spec.locale_expression true) --
   12.10 +      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   12.11 +        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
   12.12 +      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   12.13 +      >> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns));
   12.14 +
   12.15 +val _ =
   12.16    Outer_Syntax.command @{command_keyword interpretation}
   12.17      "prove interpretation of locale expression in local theory"
   12.18      (interpretation_args >> (fn (expr, equations) =>
    13.1 --- a/src/Pure/Pure.thy	Sat Nov 14 08:45:51 2015 +0100
    13.2 +++ b/src/Pure/Pure.thy	Sat Nov 14 08:45:52 2015 +0100
    13.3 @@ -9,7 +9,7 @@
    13.4      "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
    13.5      "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    13.6      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    13.7 -    "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    13.8 +    "defines" "defining" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    13.9      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
   13.10      "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
   13.11      "shows" "structure" "unchecked" "where" "when" "|"
   13.12 @@ -35,7 +35,7 @@
   13.13    and "include" "including" :: prf_decl
   13.14    and "print_bundles" :: diag
   13.15    and "context" "locale" "experiment" :: thy_decl_block
   13.16 -  and "sublocale" "interpretation" :: thy_goal
   13.17 +  and "permanent_interpretation" "interpretation" "sublocale" :: thy_goal
   13.18    and "interpret" :: prf_goal % "proof"
   13.19    and "class" :: thy_decl_block
   13.20    and "subclass" :: thy_goal
    14.1 --- a/src/Tools/Permanent_Interpretation.thy	Sat Nov 14 08:45:51 2015 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,14 +0,0 @@
    14.4 -(*  Title:   Tools/Permanent_Interpretation.thy
    14.5 -    Author:  Florian Haftmann, TU Muenchen
    14.6 -*)
    14.7 -
    14.8 -section {* Permanent interpretation accompanied with mixin definitions. *}
    14.9 -
   14.10 -theory Permanent_Interpretation
   14.11 -imports Pure
   14.12 -keywords "defining" and "permanent_interpretation" :: thy_goal
   14.13 -begin
   14.14 -
   14.15 -ML_file "~~/src/Tools/permanent_interpretation.ML"
   14.16 -
   14.17 -end
    15.1 --- a/src/Tools/permanent_interpretation.ML	Sat Nov 14 08:45:51 2015 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,108 +0,0 @@
    15.4 -(*  Title:   Tools/permanent_interpretation.ML
    15.5 -    Author:  Florian Haftmann, TU Muenchen
    15.6 -
    15.7 -Permanent interpretation accompanied with mixin definitions.
    15.8 -*)
    15.9 -
   15.10 -signature PERMANENT_INTERPRETATION =
   15.11 -sig
   15.12 -  val permanent_interpretation: Expression.expression_i ->
   15.13 -    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
   15.14 -    local_theory -> Proof.state
   15.15 -  val permanent_interpretation_cmd: Expression.expression ->
   15.16 -    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
   15.17 -    local_theory -> Proof.state
   15.18 -end;
   15.19 -
   15.20 -structure Permanent_Interpretation : PERMANENT_INTERPRETATION =
   15.21 -struct
   15.22 -
   15.23 -local
   15.24 -
   15.25 -(* reading *)
   15.26 -
   15.27 -fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
   15.28 -  let
   15.29 -    (*reading*)
   15.30 -    val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
   15.31 -    val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
   15.32 -    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
   15.33 -    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
   15.34 -    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
   15.35 -
   15.36 -    (*defining*)
   15.37 -    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
   15.38 -      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
   15.39 -    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
   15.40 -    val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
   15.41 -    val def_eqns = defs
   15.42 -      |> map (Thm.symmetric o
   15.43 -        Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
   15.44 -
   15.45 -    (*setting up*)
   15.46 -    val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
   15.47 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
   15.48 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
   15.49 -  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
   15.50 -
   15.51 -val cert_interpretation =
   15.52 -  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
   15.53 -
   15.54 -val read_interpretation =
   15.55 -  prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
   15.56 -
   15.57 -
   15.58 -(* generic interpretation machinery *)
   15.59 -
   15.60 -fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
   15.61 -
   15.62 -fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
   15.63 -  let
   15.64 -    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
   15.65 -      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
   15.66 -    val (eqns', ctxt') = ctxt
   15.67 -      |> note Thm.theoremK facts
   15.68 -      |-> meta_rewrite;
   15.69 -    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
   15.70 -      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
   15.71 -    fun activate' dep_morph ctxt = activate dep_morph
   15.72 -      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
   15.73 -  in
   15.74 -    ctxt'
   15.75 -    |> fold activate' dep_morphs
   15.76 -  end;
   15.77 -
   15.78 -fun generic_interpretation prep_interpretation setup_proof note add_registration
   15.79 -    expression raw_defs raw_eqns initial_ctxt =
   15.80 -  let
   15.81 -    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
   15.82 -      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
   15.83 -    fun after_qed witss eqns =
   15.84 -      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
   15.85 -  in setup_proof after_qed propss eqns goal_ctxt end;
   15.86 -
   15.87 -
   15.88 -(* interpretation with permanent registration *)
   15.89 -
   15.90 -fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
   15.91 -  Local_Theory.assert_bottom true
   15.92 -  #> generic_interpretation prep_interpretation Element.witness_proof_eqs
   15.93 -    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
   15.94 -
   15.95 -in
   15.96 -
   15.97 -fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
   15.98 -fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
   15.99 -
  15.100 -end;
  15.101 -
  15.102 -val _ =
  15.103 -  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
  15.104 -    "prove interpretation of locale expression into named theory"
  15.105 -    (Parse.!!! Parse_Spec.locale_expression --
  15.106 -      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
  15.107 -        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
  15.108 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
  15.109 -      >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
  15.110 -
  15.111 -end;