offical tool
authorhaftmann
Wed Feb 19 22:08:47 2014 +0100 (2014-02-19)
changeset 55601b7f4da504b75
parent 55600 3c7610b8dcfc
child 55602 257bd115fcca
offical tool
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
src/HOL/IMP/Collecting.thy
src/HOL/ROOT
src/HOL/ex/Interpretation_with_Defs.thy
src/Tools/Permanent_Interpretation.thy
src/Tools/interpretation_with_defs.ML
src/Tools/permanent_interpretation.ML
     1.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Wed Feb 19 22:05:15 2014 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Wed Feb 19 22:08:47 2014 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  header "Denotational Abstract Interpretation"
     1.5  
     1.6  theory Abs_Int_den0_fun
     1.7 -imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step"
     1.8 +imports "~~/src/Tools/Permanent_Interpretation" "../Big_Step"
     1.9  begin
    1.10  
    1.11  subsection "Orderings"
     2.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Wed Feb 19 22:05:15 2014 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Wed Feb 19 22:08:47 2014 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (* Author: Tobias Nipkow *)
     2.5  
     2.6  theory Abs_Int0_ITP
     2.7 -imports "~~/src/HOL/ex/Interpretation_with_Defs"
     2.8 +imports "~~/src/Tools/Permanent_Interpretation"
     2.9          "~~/src/HOL/Library/While_Combinator"
    2.10          "Collecting_ITP"
    2.11  begin
     3.1 --- a/src/HOL/IMP/Collecting.thy	Wed Feb 19 22:05:15 2014 +0100
     3.2 +++ b/src/HOL/IMP/Collecting.thy	Wed Feb 19 22:08:47 2014 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  theory Collecting
     3.5  imports Complete_Lattice Big_Step ACom
     3.6 -        "~~/src/HOL/ex/Interpretation_with_Defs"
     3.7 +  "~~/src/Tools/Permanent_Interpretation"
     3.8  begin
     3.9  
    3.10  subsection "The generic Step function"
     4.1 --- a/src/HOL/ROOT	Wed Feb 19 22:05:15 2014 +0100
     4.2 +++ b/src/HOL/ROOT	Wed Feb 19 22:08:47 2014 +0100
     4.3 @@ -111,7 +111,7 @@
     4.4  session "HOL-IMP" in IMP = HOL +
     4.5    options [document_graph, document_variants=document]
     4.6    theories [document = false]
     4.7 -    "~~/src/HOL/ex/Interpretation_with_Defs"
     4.8 +    "~~/src/Tools/Permanent_Interpretation"
     4.9      "~~/src/HOL/Library/While_Combinator"
    4.10      "~~/src/HOL/Library/Char_ord"
    4.11      "~~/src/HOL/Library/List_lexord"
     5.1 --- a/src/HOL/ex/Interpretation_with_Defs.thy	Wed Feb 19 22:05:15 2014 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,14 +0,0 @@
     5.4 -(*  Title:      HOL/ex/Interpretation_with_Defs.thy
     5.5 -    Author:     Florian Haftmann, TU Muenchen
     5.6 -*)
     5.7 -
     5.8 -header {* Interpretation accompanied with mixin definitions.  EXPERIMENTAL. *}
     5.9 -
    5.10 -theory Interpretation_with_Defs
    5.11 -imports Pure
    5.12 -keywords "defining" and "permanent_interpretation" :: thy_goal
    5.13 -begin
    5.14 -
    5.15 -ML_file "~~/src/Tools/interpretation_with_defs.ML"
    5.16 -
    5.17 -end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Permanent_Interpretation.thy	Wed Feb 19 22:08:47 2014 +0100
     6.3 @@ -0,0 +1,14 @@
     6.4 +(*  Title:   Tools/Permanent_Interpretation.thy
     6.5 +    Author:  Florian Haftmann, TU Muenchen
     6.6 +*)
     6.7 +
     6.8 +header {* Permanent interpretation accompanied with mixin definitions. *}
     6.9 +
    6.10 +theory Permanent_Interpretation
    6.11 +imports Pure
    6.12 +keywords "defining" and "permanent_interpretation" :: thy_goal
    6.13 +begin
    6.14 +
    6.15 +ML_file "~~/src/Tools/permanent_interpretation.ML"
    6.16 +
    6.17 +end
     7.1 --- a/src/Tools/interpretation_with_defs.ML	Wed Feb 19 22:05:15 2014 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,110 +0,0 @@
     7.4 -(*  Title:      Tools/interpretation_with_defs.ML
     7.5 -    Author:     Florian Haftmann, TU Muenchen
     7.6 -
     7.7 -Interpretation accompanied with mixin definitions.  EXPERIMENTAL.
     7.8 -*)
     7.9 -
    7.10 -signature INTERPRETATION_WITH_DEFS =
    7.11 -sig
    7.12 -  val permanent_interpretation: Expression.expression_i ->
    7.13 -    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
    7.14 -    local_theory -> Proof.state
    7.15 -  val permanent_interpretation_cmd: Expression.expression ->
    7.16 -    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
    7.17 -    local_theory -> Proof.state
    7.18 -end;
    7.19 -
    7.20 -structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
    7.21 -struct
    7.22 -
    7.23 -local
    7.24 -
    7.25 -(* reading *)
    7.26 -
    7.27 -fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
    7.28 -  let
    7.29 -    (*reading*)
    7.30 -    val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt;
    7.31 -    val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt;
    7.32 -    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
    7.33 -    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
    7.34 -    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
    7.35 -
    7.36 -    (*defining*)
    7.37 -    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
    7.38 -      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
    7.39 -    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt;
    7.40 -    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs;
    7.41 -    val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt;
    7.42 -      (*the "if" prevents restoring a proof context which is no local theory*)
    7.43 -
    7.44 -    (*setting up*)
    7.45 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt;
    7.46 -      (*FIXME: only re-prepare if defs are given*)
    7.47 -    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns;
    7.48 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    7.49 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    7.50 -  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
    7.51 -
    7.52 -val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
    7.53 -val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src;
    7.54 -
    7.55 -
    7.56 -(* generic interpretation machinery *)
    7.57 -
    7.58 -fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    7.59 -
    7.60 -fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
    7.61 -  let
    7.62 -    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
    7.63 -      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    7.64 -    val (eqns', ctxt') = ctxt
    7.65 -      |> note Thm.lemmaK facts
    7.66 -      |-> meta_rewrite;
    7.67 -    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
    7.68 -      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
    7.69 -    fun activate' dep_morph ctxt = activate dep_morph
    7.70 -      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    7.71 -  in
    7.72 -    ctxt'
    7.73 -    |> fold activate' dep_morphs
    7.74 -  end;
    7.75 -
    7.76 -fun generic_interpretation prep_interpretation setup_proof note add_registration
    7.77 -    expression raw_defs raw_eqns initial_ctxt = 
    7.78 -  let
    7.79 -    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = 
    7.80 -      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
    7.81 -    fun after_qed witss eqns =
    7.82 -      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
    7.83 -  in setup_proof after_qed propss eqns goal_ctxt end;
    7.84 -
    7.85 -
    7.86 -(* interpretation with permanent registration *)
    7.87 -
    7.88 -fun subscribe lthy =
    7.89 -  if Named_Target.is_theory lthy
    7.90 -  then Generic_Target.theory_registration
    7.91 -  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
    7.92 -
    7.93 -fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
    7.94 -  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
    7.95 -    expression raw_defs raw_eqns lthy
    7.96 -
    7.97 -in
    7.98 -
    7.99 -fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
   7.100 -fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
   7.101 -
   7.102 -end;
   7.103 -
   7.104 -val _ =
   7.105 -  Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
   7.106 -    "prove interpretation of locale expression into named theory"
   7.107 -    (Parse.!!! (Parse_Spec.locale_expression true) --
   7.108 -      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   7.109 -        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
   7.110 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   7.111 -      >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
   7.112 -
   7.113 -end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/permanent_interpretation.ML	Wed Feb 19 22:08:47 2014 +0100
     8.3 @@ -0,0 +1,110 @@
     8.4 +(*  Title:   Tools/permanent_interpretation.ML
     8.5 +    Author:  Florian Haftmann, TU Muenchen
     8.6 +
     8.7 +Permanent interpretation accompanied with mixin definitions.
     8.8 +*)
     8.9 +
    8.10 +signature PERMANENT_INTERPRETATION =
    8.11 +sig
    8.12 +  val permanent_interpretation: Expression.expression_i ->
    8.13 +    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
    8.14 +    local_theory -> Proof.state
    8.15 +  val permanent_interpretation_cmd: Expression.expression ->
    8.16 +    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
    8.17 +    local_theory -> Proof.state
    8.18 +end;
    8.19 +
    8.20 +structure Permanent_Interpretation : PERMANENT_INTERPRETATION =
    8.21 +struct
    8.22 +
    8.23 +local
    8.24 +
    8.25 +(* reading *)
    8.26 +
    8.27 +fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
    8.28 +  let
    8.29 +    (*reading*)
    8.30 +    val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt;
    8.31 +    val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt;
    8.32 +    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
    8.33 +    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
    8.34 +    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
    8.35 +
    8.36 +    (*defining*)
    8.37 +    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
    8.38 +      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
    8.39 +    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt;
    8.40 +    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs;
    8.41 +    val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt;
    8.42 +      (*the "if" prevents restoring a proof context which is no local theory*)
    8.43 +
    8.44 +    (*setting up*)
    8.45 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt;
    8.46 +      (*FIXME: only re-prepare if defs are given*)
    8.47 +    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns;
    8.48 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    8.49 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    8.50 +  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
    8.51 +
    8.52 +val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
    8.53 +val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src;
    8.54 +
    8.55 +
    8.56 +(* generic interpretation machinery *)
    8.57 +
    8.58 +fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    8.59 +
    8.60 +fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
    8.61 +  let
    8.62 +    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
    8.63 +      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    8.64 +    val (eqns', ctxt') = ctxt
    8.65 +      |> note Thm.lemmaK facts
    8.66 +      |-> meta_rewrite;
    8.67 +    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
    8.68 +      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
    8.69 +    fun activate' dep_morph ctxt = activate dep_morph
    8.70 +      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    8.71 +  in
    8.72 +    ctxt'
    8.73 +    |> fold activate' dep_morphs
    8.74 +  end;
    8.75 +
    8.76 +fun generic_interpretation prep_interpretation setup_proof note add_registration
    8.77 +    expression raw_defs raw_eqns initial_ctxt = 
    8.78 +  let
    8.79 +    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = 
    8.80 +      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
    8.81 +    fun after_qed witss eqns =
    8.82 +      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
    8.83 +  in setup_proof after_qed propss eqns goal_ctxt end;
    8.84 +
    8.85 +
    8.86 +(* interpretation with permanent registration *)
    8.87 +
    8.88 +fun subscribe lthy =
    8.89 +  if Named_Target.is_theory lthy
    8.90 +  then Generic_Target.theory_registration
    8.91 +  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
    8.92 +
    8.93 +fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
    8.94 +  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
    8.95 +    expression raw_defs raw_eqns lthy
    8.96 +
    8.97 +in
    8.98 +
    8.99 +fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
   8.100 +fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
   8.101 +
   8.102 +end;
   8.103 +
   8.104 +val _ =
   8.105 +  Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
   8.106 +    "prove interpretation of locale expression into named theory"
   8.107 +    (Parse.!!! (Parse_Spec.locale_expression true) --
   8.108 +      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   8.109 +        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
   8.110 +      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   8.111 +      >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
   8.112 +
   8.113 +end;