separate ML module for interpretation
authorhaftmann
Sat Nov 14 08:45:51 2015 +0100 (2015-11-14)
changeset 6166927ca6147e3b3
parent 61668 9a51e4dfc5d9
child 61670 301e0b4ecd45
separate ML module for interpretation
src/HOL/Statespace/state_space.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/interpretation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/ROOT.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Sat Nov 14 08:45:51 2015 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Nov 14 08:45:51 2015 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  fun prove_interpretation_in ctxt_tac (name, expr) thy =
     1.6     thy
     1.7 -   |> Expression.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
     1.8 +   |> Interpretation.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
     1.9     |> Proof.global_terminal_proof
    1.10           ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    1.11     |> Proof_Context.theory_of
     2.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 14 08:45:51 2015 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 14 08:45:51 2015 +0100
     2.3 @@ -36,27 +36,11 @@
     2.4    val add_locale_cmd: binding -> binding ->
     2.5      expression -> Element.context list -> theory -> string * local_theory
     2.6  
     2.7 -  (* Interpretation *)
     2.8 +  (* Processing of locale expressions *)
     2.9    val cert_goal_expression: expression_i -> Proof.context ->
    2.10      (term list list * (string * morphism) list * morphism) * Proof.context
    2.11    val read_goal_expression: expression -> Proof.context ->
    2.12      (term list list * (string * morphism) list * morphism) * Proof.context
    2.13 -  val permanent_interpretation: expression_i -> (Attrib.binding * term) list ->
    2.14 -    local_theory -> Proof.state
    2.15 -  val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list ->
    2.16 -    local_theory -> Proof.state
    2.17 -  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    2.18 -  val interpret_cmd: expression -> (Attrib.binding * string) list ->
    2.19 -    bool -> Proof.state -> Proof.state
    2.20 -  val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    2.21 -  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    2.22 -    local_theory -> Proof.state
    2.23 -  val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    2.24 -  val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    2.25 -  val sublocale_global: string -> expression_i ->
    2.26 -    (Attrib.binding * term) list -> theory -> Proof.state
    2.27 -  val sublocale_global_cmd: xstring * Position.T -> expression ->
    2.28 -    (Attrib.binding * string) list -> theory -> Proof.state
    2.29  
    2.30    (* Diagnostic *)
    2.31    val print_dependencies: Proof.context -> bool -> expression -> unit
    2.32 @@ -848,155 +832,6 @@
    2.33  end;
    2.34  
    2.35  
    2.36 -(*** Interpretation ***)
    2.37 -
    2.38 -local
    2.39 -
    2.40 -(* reading *)
    2.41 -
    2.42 -fun prep_with_extended_syntax prep_prop deps ctxt props =
    2.43 -  let
    2.44 -    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    2.45 -  in
    2.46 -    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
    2.47 -      |> Variable.export_terms deps_ctxt ctxt
    2.48 -  end;
    2.49 -
    2.50 -fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
    2.51 -  let
    2.52 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    2.53 -    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    2.54 -    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
    2.55 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    2.56 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    2.57 -  in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    2.58 -
    2.59 -val cert_interpretation =
    2.60 -  prep_interpretation cert_goal_expression (K I) (K I);
    2.61 -
    2.62 -val read_interpretation =
    2.63 -  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.check_src;
    2.64 -
    2.65 -
    2.66 -(* generic interpretation machinery *)
    2.67 -
    2.68 -fun meta_rewrite ctxt eqns =
    2.69 -  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
    2.70 -
    2.71 -fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
    2.72 -  let
    2.73 -    val facts = map2 (fn attrs => fn eqn =>
    2.74 -      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    2.75 -    val (eqns', ctxt') = ctxt
    2.76 -      |> note Thm.theoremK facts
    2.77 -      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
    2.78 -    val dep_morphs =
    2.79 -      map2 (fn (dep, morph) => fn wits =>
    2.80 -          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
    2.81 -        deps witss;
    2.82 -    fun activate' dep_morph ctxt =
    2.83 -      activate dep_morph
    2.84 -        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
    2.85 -        export ctxt;
    2.86 -  in
    2.87 -    ctxt'
    2.88 -    |> fold activate' dep_morphs
    2.89 -  end;
    2.90 -
    2.91 -fun generic_interpretation prep_interpretation setup_proof note activate
    2.92 -    expression raw_eqns initial_ctxt =
    2.93 -  let
    2.94 -    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
    2.95 -      prep_interpretation expression raw_eqns initial_ctxt;
    2.96 -    fun after_qed witss eqns =
    2.97 -      note_eqns_register note activate deps witss eqns attrss export export';
    2.98 -  in setup_proof after_qed propss eqns goal_ctxt end;
    2.99 -
   2.100 -
   2.101 -(* first dimension: proof vs. local theory *)
   2.102 -
   2.103 -fun gen_interpret prep_interpretation expression raw_eqns int state =
   2.104 -  let
   2.105 -    val _ = Proof.assert_forward_or_chain state;
   2.106 -    val ctxt = Proof.context_of state;
   2.107 -    fun lift_after_qed after_qed witss eqns =
   2.108 -      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
   2.109 -    fun setup_proof after_qed propss eqns goal_ctxt =
   2.110 -      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
   2.111 -        propss eqns goal_ctxt int state;
   2.112 -  in
   2.113 -    generic_interpretation prep_interpretation setup_proof
   2.114 -      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
   2.115 -  end;
   2.116 -
   2.117 -fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
   2.118 -  generic_interpretation prep_interpretation Element.witness_proof_eqs
   2.119 -    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
   2.120 -
   2.121 -
   2.122 -(* second dimension: relation to underlying target *)
   2.123 -
   2.124 -fun subscribe_or_activate lthy =
   2.125 -  if Named_Target.is_theory lthy
   2.126 -  then Local_Theory.subscription
   2.127 -  else Locale.activate_fragment;
   2.128 -
   2.129 -fun subscribe_locale_only lthy =
   2.130 -  let
   2.131 -    val _ =
   2.132 -      if Named_Target.is_theory lthy
   2.133 -      then error "Not possible on level of global theory"
   2.134 -      else ();
   2.135 -  in Local_Theory.subscription end;
   2.136 -
   2.137 -
   2.138 -(* special case: global sublocale command *)
   2.139 -
   2.140 -fun gen_sublocale_global prep_loc prep_interpretation
   2.141 -    raw_locale expression raw_eqns thy =
   2.142 -  let
   2.143 -    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
   2.144 -    fun setup_proof after_qed =
   2.145 -      Element.witness_proof_eqs
   2.146 -        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   2.147 -  in
   2.148 -    lthy |>
   2.149 -      generic_interpretation prep_interpretation setup_proof
   2.150 -        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
   2.151 -  end;
   2.152 -
   2.153 -in
   2.154 -
   2.155 -
   2.156 -(* interfaces *)
   2.157 -
   2.158 -fun interpret x = gen_interpret cert_interpretation x;
   2.159 -fun interpret_cmd x = gen_interpret read_interpretation x;
   2.160 -
   2.161 -fun permanent_interpretation expression raw_eqns =
   2.162 -  Local_Theory.assert_bottom true
   2.163 -  #> gen_local_theory_interpretation cert_interpretation
   2.164 -    (K Local_Theory.subscription) expression raw_eqns;
   2.165 -
   2.166 -fun ephemeral_interpretation x =
   2.167 -  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
   2.168 -
   2.169 -fun interpretation x =
   2.170 -  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
   2.171 -fun interpretation_cmd x =
   2.172 -  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
   2.173 -
   2.174 -fun sublocale x =
   2.175 -  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
   2.176 -fun sublocale_cmd x =
   2.177 -  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
   2.178 -
   2.179 -fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
   2.180 -fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
   2.181 -
   2.182 -end;
   2.183 -
   2.184 -
   2.185  (** Print the instances that would be activated by an interpretation
   2.186    of the expression in the current context (clean = false) or in an
   2.187    empty context (clean = true). **)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/interpretation.ML	Sat Nov 14 08:45:51 2015 +0100
     3.3 @@ -0,0 +1,176 @@
     3.4 +(*  Title:      Pure/Isar/interpretation.ML
     3.5 +    Author:     Clemens Ballarin, TU Muenchen
     3.6 +
     3.7 +Locale interpretation.
     3.8 +*)
     3.9 +
    3.10 +signature INTERPRETATION =
    3.11 +sig
    3.12 +  val permanent_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
    3.13 +    local_theory -> Proof.state
    3.14 +  val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
    3.15 +    local_theory -> Proof.state
    3.16 +  val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    3.17 +  val interpret_cmd: Expression.expression -> (Attrib.binding * string) list ->
    3.18 +    bool -> Proof.state -> Proof.state
    3.19 +  val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    3.20 +  val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list ->
    3.21 +    local_theory -> Proof.state
    3.22 +  val sublocale: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    3.23 +  val sublocale_cmd: Expression.expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    3.24 +  val sublocale_global: string -> Expression.expression_i ->
    3.25 +    (Attrib.binding * term) list -> theory -> Proof.state
    3.26 +  val sublocale_global_cmd: xstring * Position.T -> Expression.expression ->
    3.27 +    (Attrib.binding * string) list -> theory -> Proof.state
    3.28 +end;
    3.29 +
    3.30 +structure Interpretation : INTERPRETATION =
    3.31 +struct
    3.32 +
    3.33 +local
    3.34 +
    3.35 +(* reading *)
    3.36 +
    3.37 +fun prep_with_extended_syntax prep_prop deps ctxt props =
    3.38 +  let
    3.39 +    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    3.40 +  in
    3.41 +    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
    3.42 +      |> Variable.export_terms deps_ctxt ctxt
    3.43 +  end;
    3.44 +
    3.45 +fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
    3.46 +  let
    3.47 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    3.48 +    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    3.49 +    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
    3.50 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    3.51 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    3.52 +  in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    3.53 +
    3.54 +val cert_interpretation =
    3.55 +  prep_interpretation Expression.cert_goal_expression (K I) (K I);
    3.56 +
    3.57 +val read_interpretation =
    3.58 +  prep_interpretation Expression.read_goal_expression Syntax.parse_prop Attrib.check_src;
    3.59 +
    3.60 +
    3.61 +(* generic interpretation machinery *)
    3.62 +
    3.63 +fun meta_rewrite ctxt eqns =
    3.64 +  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
    3.65 +
    3.66 +fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
    3.67 +  let
    3.68 +    val facts = map2 (fn attrs => fn eqn =>
    3.69 +      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    3.70 +    val (eqns', ctxt') = ctxt
    3.71 +      |> note Thm.theoremK facts
    3.72 +      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
    3.73 +    val dep_morphs =
    3.74 +      map2 (fn (dep, morph) => fn wits =>
    3.75 +          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
    3.76 +        deps witss;
    3.77 +    fun activate' dep_morph ctxt =
    3.78 +      activate dep_morph
    3.79 +        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
    3.80 +        export ctxt;
    3.81 +  in
    3.82 +    ctxt'
    3.83 +    |> fold activate' dep_morphs
    3.84 +  end;
    3.85 +
    3.86 +fun generic_interpretation prep_interpretation setup_proof note activate
    3.87 +    expression raw_eqns initial_ctxt =
    3.88 +  let
    3.89 +    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
    3.90 +      prep_interpretation expression raw_eqns initial_ctxt;
    3.91 +    fun after_qed witss eqns =
    3.92 +      note_eqns_register note activate deps witss eqns attrss export export';
    3.93 +  in setup_proof after_qed propss eqns goal_ctxt end;
    3.94 +
    3.95 +
    3.96 +(* first dimension: proof vs. local theory *)
    3.97 +
    3.98 +fun gen_interpret prep_interpretation expression raw_eqns int state =
    3.99 +  let
   3.100 +    val _ = Proof.assert_forward_or_chain state;
   3.101 +    val ctxt = Proof.context_of state;
   3.102 +    fun lift_after_qed after_qed witss eqns =
   3.103 +      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
   3.104 +    fun setup_proof after_qed propss eqns goal_ctxt =
   3.105 +      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
   3.106 +        propss eqns goal_ctxt int state;
   3.107 +  in
   3.108 +    generic_interpretation prep_interpretation setup_proof
   3.109 +      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
   3.110 +  end;
   3.111 +
   3.112 +fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
   3.113 +  generic_interpretation prep_interpretation Element.witness_proof_eqs
   3.114 +    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
   3.115 +
   3.116 +
   3.117 +(* second dimension: relation to underlying target *)
   3.118 +
   3.119 +fun subscribe_or_activate lthy =
   3.120 +  if Named_Target.is_theory lthy
   3.121 +  then Local_Theory.subscription
   3.122 +  else Locale.activate_fragment;
   3.123 +
   3.124 +fun subscribe_locale_only lthy =
   3.125 +  let
   3.126 +    val _ =
   3.127 +      if Named_Target.is_theory lthy
   3.128 +      then error "Not possible on level of global theory"
   3.129 +      else ();
   3.130 +  in Local_Theory.subscription end;
   3.131 +
   3.132 +
   3.133 +(* special case: global sublocale command *)
   3.134 +
   3.135 +fun gen_sublocale_global prep_loc prep_interpretation
   3.136 +    raw_locale expression raw_eqns thy =
   3.137 +  let
   3.138 +    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
   3.139 +    fun setup_proof after_qed =
   3.140 +      Element.witness_proof_eqs
   3.141 +        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   3.142 +  in
   3.143 +    lthy |>
   3.144 +      generic_interpretation prep_interpretation setup_proof
   3.145 +        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
   3.146 +  end;
   3.147 +
   3.148 +in
   3.149 +
   3.150 +
   3.151 +(* interfaces *)
   3.152 +
   3.153 +fun interpret x = gen_interpret cert_interpretation x;
   3.154 +fun interpret_cmd x = gen_interpret read_interpretation x;
   3.155 +
   3.156 +fun permanent_interpretation expression raw_eqns =
   3.157 +  Local_Theory.assert_bottom true
   3.158 +  #> gen_local_theory_interpretation cert_interpretation
   3.159 +    (K Local_Theory.subscription) expression raw_eqns;
   3.160 +
   3.161 +fun ephemeral_interpretation x =
   3.162 +  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
   3.163 +
   3.164 +fun interpretation x =
   3.165 +  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
   3.166 +fun interpretation_cmd x =
   3.167 +  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
   3.168 +
   3.169 +fun sublocale x =
   3.170 +  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
   3.171 +fun sublocale_cmd x =
   3.172 +  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
   3.173 +
   3.174 +fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
   3.175 +fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
   3.176 +
   3.177 +end;
   3.178 +
   3.179 +end;
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:51 2015 +0100
     4.3 @@ -412,21 +412,21 @@
     4.4      "prove sublocale relation between a locale and a locale expression"
     4.5      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
     4.6        interpretation_args >> (fn (loc, (expr, equations)) =>
     4.7 -        Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
     4.8 +        Toplevel.theory_to_proof (Interpretation.sublocale_global_cmd loc expr equations)))
     4.9      || interpretation_args >> (fn (expr, equations) =>
    4.10 -        Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
    4.11 +        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
    4.12  
    4.13  val _ =
    4.14    Outer_Syntax.command @{command_keyword interpretation}
    4.15      "prove interpretation of locale expression in local theory"
    4.16      (interpretation_args >> (fn (expr, equations) =>
    4.17 -      Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
    4.18 +      Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));
    4.19  
    4.20  val _ =
    4.21    Outer_Syntax.command @{command_keyword interpret}
    4.22      "prove interpretation of locale expression in proof context"
    4.23      (interpretation_args >> (fn (expr, equations) =>
    4.24 -      Toplevel.proof' (Expression.interpret_cmd expr equations)));
    4.25 +      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
    4.26  
    4.27  
    4.28  (* classes *)
     5.1 --- a/src/Pure/ROOT.ML	Sat Nov 14 08:45:51 2015 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Sat Nov 14 08:45:51 2015 +0100
     5.3 @@ -271,6 +271,7 @@
     5.4  use "Isar/class.ML";
     5.5  use "Isar/named_target.ML";
     5.6  use "Isar/expression.ML";
     5.7 +use "Isar/interpretation.ML";
     5.8  use "Isar/class_declaration.ML";
     5.9  use "Isar/bundle.ML";
    5.10  use "Isar/experiment.ML";