src/Tools/interpretation_with_defs.ML

learn new facts on query if there aren't too many of them in MaSh

(*  Title:      Tools/interpretation_with_defs.ML
    Author:     Florian Haftmann, TU Muenchen

Interpretation accompanied with mixin definitions.  EXPERIMENTAL.
*)

signature INTERPRETATION_WITH_DEFS =
sig
  val interpretation: Expression.expression_i ->
    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
    theory -> Proof.state
  val interpretation_cmd: Expression.expression ->
    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
    theory -> Proof.state
end;

structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
struct

fun note_eqns_register deps witss def_eqns attrss eqns export export' =
  let
    fun meta_rewrite context =
      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
        maps snd;
  in
    Attrib.generic_notes Thm.lemmaK
      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    #-> (fn facts => `(fn context => meta_rewrite context facts))
    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
      fn context =>
        Locale.add_registration
          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
          (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
            Option.map (rpair true))
          export context) (deps ~~ witss))
  end;

local

fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr
    expression raw_defs raw_eqns theory =
  let
    val (_, (_, defs_ctxt)) =
      prep_decl expression I [] (Proof_Context.init_global theory);

    val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
      |> Syntax.check_terms defs_ctxt;
    val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;

    val (def_eqns, theory') = theory
      |> Named_Target.theory_init
      |> fold_map (Local_Theory.define) defs
      |>> map (Thm.symmetric o snd o snd)
      |> Local_Theory.exit_result_global (map o Morphism.thm);

    val ((propss, deps, export), expr_ctxt) = theory'
      |> Proof_Context.init_global
      |> prep_expr expression;

    val eqns = map (parse_prop expr_ctxt o snd) raw_eqns
      |> Syntax.check_terms expr_ctxt;
    val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns;
    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    val export' = Variable.export_morphism goal_ctxt expr_ctxt;

    fun after_qed witss eqns =
      (Proof_Context.background_theory o Context.theory_map)
        (note_eqns_register deps witss def_eqns attrss eqns export export');

  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;

in

fun interpretation x = gen_interpretation Expression.cert_goal_expression
  Expression.cert_declaration (K I) (K I) (K I) x;
fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression
  Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x;

end;

val _ =
  Outer_Syntax.command @{command_spec "interpretation"}
    "prove interpretation of locale expression in theory"
    (Parse.!!! (Parse_Spec.locale_expression true) --
      Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
      >> (fn ((expr, defs), equations) => Toplevel.print o
          Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));

end;