--- a/NEWS Sat Nov 14 08:45:51 2015 +0100
+++ b/NEWS Sat Nov 14 08:45:52 2015 +0100
@@ -314,6 +314,9 @@
* Keyword 'rewrites' identifies rewrite morphisms in interpretation
commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
+* Command 'permanent_interpretation' is available in Pure, without
+need to load a separate theory.
+
* Command 'print_definitions' prints dependencies of definitional
specifications. This functionality used to be part of 'print_theory'.
--- a/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:52 2015 +0100
@@ -220,8 +220,7 @@
(*>*) text \<open>
Fortunately, an even more succint approach is available using command
- @{command permanent_interpretation}. This is available
- by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}.
+ @{command permanent_interpretation}.
Then the pattern above collapses to
\<close> (*<*)
--- a/src/Doc/Codegen/Setup.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Doc/Codegen/Setup.thy Sat Nov 14 08:45:52 2015 +0100
@@ -1,7 +1,6 @@
theory Setup
imports
Complex_Main
- "~~/src/Tools/Permanent_Interpretation"
"~~/src/HOL/Library/Dlist"
"~~/src/HOL/Library/RBT"
"~~/src/HOL/Library/Mapping"
--- a/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:52 2015 +0100
@@ -1,7 +1,7 @@
(*:maxLineLen=78:*)
theory Spec
-imports Base Main "~~/src/Tools/Permanent_Interpretation"
+imports Base Main
begin
chapter \<open>Specifications\<close>
@@ -739,9 +739,9 @@
subsubsection \<open>Permanent locale interpretation\<close>
text \<open>
- Permanent locale interpretation is a library extension on top of
- \<^theory_text>\<open>interpretation\<close> and \<^theory_text>\<open>sublocale\<close>. It is available by importing theory
- @{file "~~/src/Tools/Permanent_Interpretation.thy"} and provides
+ Permanent locale interpretation is an extension on top
+ of \<^theory_text>\<open>interpretation\<close> and \<^theory_text>\<open>sublocale\<close>
+ and provides
\<^enum> a unified view on arbitrary suitable local theories as interpretation
target;
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Sat Nov 14 08:45:52 2015 +0100
@@ -3,7 +3,7 @@
section "Denotational Abstract Interpretation"
theory Abs_Int_den0_fun
-imports "~~/src/Tools/Permanent_Interpretation" "../Big_Step"
+imports "../Big_Step"
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Sat Nov 14 08:45:52 2015 +0100
@@ -1,9 +1,9 @@
(* Author: Tobias Nipkow *)
theory Abs_Int0_ITP
-imports "~~/src/Tools/Permanent_Interpretation"
- "~~/src/HOL/Library/While_Combinator"
- "Collecting_ITP"
+imports
+ "~~/src/HOL/Library/While_Combinator"
+ Collecting_ITP
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Sat Nov 14 08:45:52 2015 +0100
@@ -1,5 +1,5 @@
theory Collecting_ITP
-imports "~~/src/Tools/Permanent_Interpretation" Complete_Lattice_ix "ACom_ITP"
+imports Complete_Lattice_ix "ACom_ITP"
begin
subsection "Collecting Semantics of Commands"
--- a/src/HOL/IMP/Collecting.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/IMP/Collecting.thy Sat Nov 14 08:45:52 2015 +0100
@@ -1,6 +1,5 @@
theory Collecting
imports Complete_Lattice Big_Step ACom
- "~~/src/Tools/Permanent_Interpretation"
begin
subsection "The generic Step function"
--- a/src/HOL/Library/Groups_Big_Fun.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sat Nov 14 08:45:52 2015 +0100
@@ -5,7 +5,6 @@
theory Groups_Big_Fun
imports
Main
- "~~/src/Tools/Permanent_Interpretation"
begin
subsection \<open>Abstract product\<close>
--- a/src/HOL/ROOT Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/ROOT Sat Nov 14 08:45:52 2015 +0100
@@ -115,7 +115,6 @@
session "HOL-IMP" in IMP = HOL +
options [document_variants = document]
theories [document = false]
- "~~/src/Tools/Permanent_Interpretation"
"~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Char_ord"
"~~/src/HOL/Library/List_lexord"
--- a/src/Pure/Isar/interpretation.ML Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML Sat Nov 14 08:45:52 2015 +0100
@@ -1,18 +1,24 @@
(* Title: Pure/Isar/interpretation.ML
Author: Clemens Ballarin, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
Locale interpretation.
*)
signature INTERPRETATION =
sig
- val permanent_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
- local_theory -> Proof.state
- val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
- local_theory -> Proof.state
val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
val interpret_cmd: Expression.expression -> (Attrib.binding * string) list ->
bool -> Proof.state -> Proof.state
+ val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
+ local_theory -> Proof.state
+ val permanent_interpretation: Expression.expression_i ->
+ (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
+ local_theory -> Proof.state
+ val permanent_interpretation_cmd: Expression.expression ->
+ (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
+ local_theory -> Proof.state
+
val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list ->
local_theory -> Proof.state
@@ -29,7 +35,9 @@
local
-(* reading *)
+(** reading **)
+
+(* without mixin definitions *)
fun prep_with_extended_syntax prep_prop deps ctxt props =
let
@@ -55,7 +63,44 @@
prep_interpretation Expression.read_goal_expression Syntax.parse_prop Attrib.check_src;
-(* generic interpretation machinery *)
+(* with mixin definitions *)
+
+fun prep_interpretation_with_defs prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
+ let
+ (*reading*)
+ val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
+ val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
+ val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
+ val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
+ val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
+
+ (*defining*)
+ val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
+ ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
+ val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
+ val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
+ val def_eqns = defs
+ |> map (Thm.symmetric o
+ Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
+
+ (*setting up*)
+ val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
+ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
+ val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
+ in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
+
+val cert_interpretation_with_defs =
+ prep_interpretation_with_defs Expression.cert_goal_expression (K I) (K I) (K I);
+
+val read_interpretation_with_defs =
+ prep_interpretation_with_defs Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
+
+
+(** generic interpretation machinery **)
+
+(* without mixin definitions *)
+
+local
fun meta_rewrite ctxt eqns =
map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
@@ -80,6 +125,8 @@
|> fold activate' dep_morphs
end;
+in
+
fun generic_interpretation prep_interpretation setup_proof note activate
expression raw_eqns initial_ctxt =
let
@@ -89,8 +136,48 @@
note_eqns_register note activate deps witss eqns attrss export export';
in setup_proof after_qed propss eqns goal_ctxt end;
+end;
-(* first dimension: proof vs. local theory *)
+
+(* without mixin definitions *)
+
+local
+
+fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+
+fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
+ let
+ val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
+ :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
+ val (eqns', ctxt') = ctxt
+ |> note Thm.theoremK facts
+ |-> meta_rewrite;
+ val dep_morphs = map2 (fn (dep, morph) => fn wits =>
+ (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
+ fun activate' dep_morph ctxt = activate dep_morph
+ (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
+ in
+ ctxt'
+ |> fold activate' dep_morphs
+ end;
+
+in
+
+fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration
+ expression raw_defs raw_eqns initial_ctxt =
+ let
+ val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
+ prep_interpretation expression raw_defs raw_eqns initial_ctxt;
+ fun after_qed witss eqns =
+ note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
+ in setup_proof after_qed propss eqns goal_ctxt end;
+
+end;
+
+
+(** first dimension: proof vs. local theory **)
+
+(* proof *)
fun gen_interpret prep_interpretation expression raw_eqns int state =
let
@@ -106,12 +193,23 @@
Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
end;
+
+(* local theory *)
+
fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
generic_interpretation prep_interpretation Element.witness_proof_eqs
Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
-(* second dimension: relation to underlying target *)
+(* local theory with mixin definitions *)
+
+fun gen_interpretation_with_defs prep_interpretation expression raw_defs raw_eqns =
+ Local_Theory.assert_bottom true
+ #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
+
+
+(** second dimension: relation to underlying target **)
fun subscribe_or_activate lthy =
if Named_Target.is_theory lthy
@@ -127,7 +225,7 @@
in Local_Theory.subscription end;
-(* special case: global sublocale command *)
+(** special case: global sublocale command **)
fun gen_sublocale_global prep_loc prep_interpretation
raw_locale expression raw_eqns thy =
@@ -145,19 +243,17 @@
in
-(* interfaces *)
+(** interfaces **)
fun interpret x = gen_interpret cert_interpretation x;
fun interpret_cmd x = gen_interpret read_interpretation x;
-fun permanent_interpretation expression raw_eqns =
- Local_Theory.assert_bottom true
- #> gen_local_theory_interpretation cert_interpretation
- (K Local_Theory.subscription) expression raw_eqns;
-
fun ephemeral_interpretation x =
gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
+fun permanent_interpretation x = gen_interpretation_with_defs cert_interpretation_with_defs x;
+fun permanent_interpretation_cmd x = gen_interpretation_with_defs read_interpretation_with_defs x;
+
fun interpretation x =
gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
fun interpretation_cmd x =
--- a/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:52 2015 +0100
@@ -417,6 +417,15 @@
Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
val _ =
+ Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
+ "prove interpretation of locale expression into named theory"
+ (Parse.!!! (Parse_Spec.locale_expression true) --
+ Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
+ Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+ >> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns));
+
+val _ =
Outer_Syntax.command @{command_keyword interpretation}
"prove interpretation of locale expression in local theory"
(interpretation_args >> (fn (expr, equations) =>
--- a/src/Pure/Pure.thy Sat Nov 14 08:45:51 2015 +0100
+++ b/src/Pure/Pure.thy Sat Nov 14 08:45:52 2015 +0100
@@ -9,7 +9,7 @@
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
- "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
+ "defines" "defining" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
"shows" "structure" "unchecked" "where" "when" "|"
@@ -35,7 +35,7 @@
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
- and "sublocale" "interpretation" :: thy_goal
+ and "permanent_interpretation" "interpretation" "sublocale" :: thy_goal
and "interpret" :: prf_goal % "proof"
and "class" :: thy_decl_block
and "subclass" :: thy_goal
--- a/src/Tools/Permanent_Interpretation.thy Sat Nov 14 08:45:51 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: Tools/Permanent_Interpretation.thy
- Author: Florian Haftmann, TU Muenchen
-*)
-
-section {* Permanent interpretation accompanied with mixin definitions. *}
-
-theory Permanent_Interpretation
-imports Pure
-keywords "defining" and "permanent_interpretation" :: thy_goal
-begin
-
-ML_file "~~/src/Tools/permanent_interpretation.ML"
-
-end
--- a/src/Tools/permanent_interpretation.ML Sat Nov 14 08:45:51 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-(* Title: Tools/permanent_interpretation.ML
- Author: Florian Haftmann, TU Muenchen
-
-Permanent interpretation accompanied with mixin definitions.
-*)
-
-signature PERMANENT_INTERPRETATION =
-sig
- val permanent_interpretation: Expression.expression_i ->
- (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
- local_theory -> Proof.state
- val permanent_interpretation_cmd: Expression.expression ->
- (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
- local_theory -> Proof.state
-end;
-
-structure Permanent_Interpretation : PERMANENT_INTERPRETATION =
-struct
-
-local
-
-(* reading *)
-
-fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
- let
- (*reading*)
- val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
- val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
- val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
- val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
- val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
-
- (*defining*)
- val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
- ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
- val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
- val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
- val def_eqns = defs
- |> map (Thm.symmetric o
- Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
-
- (*setting up*)
- val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
- val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
- val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
- in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
-
-val cert_interpretation =
- prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
-
-val read_interpretation =
- prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
-
-
-(* generic interpretation machinery *)
-
-fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
-
-fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
- let
- val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
- :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
- val (eqns', ctxt') = ctxt
- |> note Thm.theoremK facts
- |-> meta_rewrite;
- val dep_morphs = map2 (fn (dep, morph) => fn wits =>
- (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
- fun activate' dep_morph ctxt = activate dep_morph
- (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
- in
- ctxt'
- |> fold activate' dep_morphs
- end;
-
-fun generic_interpretation prep_interpretation setup_proof note add_registration
- expression raw_defs raw_eqns initial_ctxt =
- let
- val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
- prep_interpretation expression raw_defs raw_eqns initial_ctxt;
- fun after_qed witss eqns =
- note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
- in setup_proof after_qed propss eqns goal_ctxt end;
-
-
-(* interpretation with permanent registration *)
-
-fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
- Local_Theory.assert_bottom true
- #> generic_interpretation prep_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
-
-in
-
-fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
-fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
-
-end;
-
-val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
- "prove interpretation of locale expression into named theory"
- (Parse.!!! Parse_Spec.locale_expression --
- Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
- -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
- Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
- >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
-
-end;