# HG changeset patch # User haftmann # Date 1447487152 -3600 # Node ID 301e0b4ecd4522409f5a5ac27288b514bd402d29 # Parent 27ca6147e3b3d1589f3a98bd167bf97c7486aa1d coalesce permanent_interpretation.ML with interpretation.ML diff -r 27ca6147e3b3 -r 301e0b4ecd45 NEWS --- 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'. diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Doc/Codegen/Further.thy --- 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 \ 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 \ (*<*) diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Doc/Codegen/Setup.thy --- 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" diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Doc/Isar_Ref/Spec.thy --- 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 \Specifications\ @@ -739,9 +739,9 @@ subsubsection \Permanent locale interpretation\ text \ - Permanent locale interpretation is a library extension on top of - \<^theory_text>\interpretation\ and \<^theory_text>\sublocale\. 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>\interpretation\ and \<^theory_text>\sublocale\ + and provides \<^enum> a unified view on arbitrary suitable local theories as interpretation target; diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy --- 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" diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy --- 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" diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy --- 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" diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/HOL/IMP/Collecting.thy --- 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" diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/HOL/Library/Groups_Big_Fun.thy --- 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 \Abstract product\ diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/HOL/ROOT --- 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" diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Pure/Isar/interpretation.ML --- 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 = diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Pure/Isar/isar_syn.ML --- 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) => diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Pure/Pure.thy --- 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 @@ "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "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 diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Tools/Permanent_Interpretation.thy --- 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 diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Tools/permanent_interpretation.ML --- 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;