# HG changeset patch # User haftmann # Date 1392844127 -3600 # Node ID b7f4da504b7538367479a8ab03ada36d40554d76 # Parent 3c7610b8dcfc096845ec7ae8edc88d8694e3c6f3 offical tool diff -r 3c7610b8dcfc -r b7f4da504b75 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Wed Feb 19 22:05:15 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Wed Feb 19 22:08:47 2014 +0100 @@ -3,7 +3,7 @@ header "Denotational Abstract Interpretation" theory Abs_Int_den0_fun -imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step" +imports "~~/src/Tools/Permanent_Interpretation" "../Big_Step" begin subsection "Orderings" diff -r 3c7610b8dcfc -r b7f4da504b75 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Wed Feb 19 22:05:15 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Wed Feb 19 22:08:47 2014 +0100 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int0_ITP -imports "~~/src/HOL/ex/Interpretation_with_Defs" +imports "~~/src/Tools/Permanent_Interpretation" "~~/src/HOL/Library/While_Combinator" "Collecting_ITP" begin diff -r 3c7610b8dcfc -r b7f4da504b75 src/HOL/IMP/Collecting.thy --- a/src/HOL/IMP/Collecting.thy Wed Feb 19 22:05:15 2014 +0100 +++ b/src/HOL/IMP/Collecting.thy Wed Feb 19 22:08:47 2014 +0100 @@ -1,6 +1,6 @@ theory Collecting imports Complete_Lattice Big_Step ACom - "~~/src/HOL/ex/Interpretation_with_Defs" + "~~/src/Tools/Permanent_Interpretation" begin subsection "The generic Step function" diff -r 3c7610b8dcfc -r b7f4da504b75 src/HOL/ROOT --- a/src/HOL/ROOT Wed Feb 19 22:05:15 2014 +0100 +++ b/src/HOL/ROOT Wed Feb 19 22:08:47 2014 +0100 @@ -111,7 +111,7 @@ session "HOL-IMP" in IMP = HOL + options [document_graph, document_variants=document] theories [document = false] - "~~/src/HOL/ex/Interpretation_with_Defs" + "~~/src/Tools/Permanent_Interpretation" "~~/src/HOL/Library/While_Combinator" "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord" diff -r 3c7610b8dcfc -r b7f4da504b75 src/HOL/ex/Interpretation_with_Defs.thy --- a/src/HOL/ex/Interpretation_with_Defs.thy Wed Feb 19 22:05:15 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: HOL/ex/Interpretation_with_Defs.thy - Author: Florian Haftmann, TU Muenchen -*) - -header {* Interpretation accompanied with mixin definitions. EXPERIMENTAL. *} - -theory Interpretation_with_Defs -imports Pure -keywords "defining" and "permanent_interpretation" :: thy_goal -begin - -ML_file "~~/src/Tools/interpretation_with_defs.ML" - -end diff -r 3c7610b8dcfc -r b7f4da504b75 src/Tools/Permanent_Interpretation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Permanent_Interpretation.thy Wed Feb 19 22:08:47 2014 +0100 @@ -0,0 +1,14 @@ +(* Title: Tools/Permanent_Interpretation.thy + Author: Florian Haftmann, TU Muenchen +*) + +header {* 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 3c7610b8dcfc -r b7f4da504b75 src/Tools/interpretation_with_defs.ML --- a/src/Tools/interpretation_with_defs.ML Wed Feb 19 22:05:15 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -(* Title: Tools/interpretation_with_defs.ML - Author: Florian Haftmann, TU Muenchen - -Interpretation accompanied with mixin definitions. EXPERIMENTAL. -*) - -signature INTERPRETATION_WITH_DEFS = -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 Interpretation_With_Defs : INTERPRETATION_WITH_DEFS = -struct - -local - -(* reading *) - -fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = - let - (*reading*) - val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt; - val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt; - 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 initial_ctxt; - val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs; - val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt; - (*the "if" prevents restoring a proof context which is no local theory*) - - (*setting up*) - val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt; - (*FIXME: only re-prepare if defs are given*) - val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns; - val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; - val export' = Variable.export_morphism goal_ctxt expr_ctxt; - 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.intern_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.lemmaK 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 subscribe lthy = - if Named_Target.is_theory lthy - then Generic_Target.theory_registration - else Generic_Target.locale_dependency (Named_Target.the_name lthy); - -fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy = - generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy) - expression raw_defs raw_eqns lthy - -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_spec "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) => permanent_interpretation_cmd expr defs eqns)); - -end; diff -r 3c7610b8dcfc -r b7f4da504b75 src/Tools/permanent_interpretation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/permanent_interpretation.ML Wed Feb 19 22:08:47 2014 +0100 @@ -0,0 +1,110 @@ +(* 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 ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt; + val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt; + 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 initial_ctxt; + val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs; + val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt; + (*the "if" prevents restoring a proof context which is no local theory*) + + (*setting up*) + val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt; + (*FIXME: only re-prepare if defs are given*) + val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns; + val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; + val export' = Variable.export_morphism goal_ctxt expr_ctxt; + 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.intern_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.lemmaK 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 subscribe lthy = + if Named_Target.is_theory lthy + then Generic_Target.theory_registration + else Generic_Target.locale_dependency (Named_Target.the_name lthy); + +fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy = + generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy) + expression raw_defs raw_eqns lthy + +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_spec "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) => permanent_interpretation_cmd expr defs eqns)); + +end;