haftmann@41829: (*  Title:      Tools/interpretation_with_defs.ML
haftmann@41829:     Author:     Florian Haftmann, TU Muenchen
haftmann@41829: 
haftmann@41829: Interpretation accompanied with mixin definitions.  EXPERIMENTAL.
haftmann@41829: *)
haftmann@41829: 
haftmann@41829: signature INTERPRETATION_WITH_DEFS =
haftmann@41829: sig
haftmann@41829:   val interpretation: Expression.expression_i ->
haftmann@41829:     (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
haftmann@41829:     theory -> Proof.state
haftmann@41829:   val interpretation_cmd: Expression.expression ->
haftmann@41829:     (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
haftmann@41829:     theory -> Proof.state
haftmann@41829: end;
haftmann@41829: 
haftmann@41829: structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
haftmann@41829: struct
haftmann@41829: 
wenzelm@47730: fun note_eqns_register deps witss def_eqns attrss eqns export export' =
haftmann@41829:   let
haftmann@41829:     fun meta_rewrite context =
haftmann@41829:       map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
haftmann@41829:         maps snd;
haftmann@41829:   in
wenzelm@47730:     Element.generic_note_thmss Thm.lemmaK
haftmann@41829:       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
wenzelm@47730:     #-> (fn facts => `(fn context => meta_rewrite context facts))
wenzelm@47730:     #-> (fn eqns => fold (fn ((dep, morph), wits) =>
haftmann@41829:       fn context =>
wenzelm@47730:         Locale.add_registration
wenzelm@47730:           (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
haftmann@41829:           (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
haftmann@41829:             Option.map (rpair true))
haftmann@41829:           export context) (deps ~~ witss))
haftmann@41829:   end;
haftmann@41829: 
haftmann@41829: local
haftmann@41829: 
haftmann@41829: fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr
haftmann@41829:     expression raw_defs raw_eqns theory =
haftmann@41829:   let
haftmann@41829:     val (_, (_, defs_ctxt)) =
wenzelm@43232:       prep_decl expression I [] (Proof_Context.init_global theory);
haftmann@41829: 
haftmann@41829:     val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
haftmann@41829:       |> Syntax.check_terms defs_ctxt;
wenzelm@47780:     val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
wenzelm@47780:       ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
haftmann@41829: 
haftmann@41829:     val (def_eqns, theory') = theory
haftmann@41829:       |> Named_Target.theory_init
haftmann@41829:       |> fold_map (Local_Theory.define) defs
haftmann@41829:       |>> map (Thm.symmetric o snd o snd)
haftmann@41829:       |> Local_Theory.exit_result_global (map o Morphism.thm);
haftmann@41829: 
haftmann@41829:     val ((propss, deps, export), expr_ctxt) = theory'
wenzelm@43232:       |> Proof_Context.init_global
haftmann@41829:       |> prep_expr expression;
haftmann@41829: 
haftmann@41829:     val eqns = map (parse_prop expr_ctxt o snd) raw_eqns
haftmann@41829:       |> Syntax.check_terms expr_ctxt;
haftmann@41829:     val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns;
haftmann@41829:     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
haftmann@41829:     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
haftmann@41829: 
haftmann@41829:     fun after_qed witss eqns =
wenzelm@43232:       (Proof_Context.background_theory o Context.theory_map)
haftmann@41829:         (note_eqns_register deps witss def_eqns attrss eqns export export');
haftmann@41829: 
haftmann@41829:   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
haftmann@41829: 
haftmann@41829: in
haftmann@41829: 
haftmann@41829: fun interpretation x = gen_interpretation Expression.cert_goal_expression
haftmann@41829:   Expression.cert_declaration (K I) (K I) (K I) x;
haftmann@41829: fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression
haftmann@41829:   Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x;
haftmann@41829: 
haftmann@41829: end;
haftmann@41829: 
haftmann@41829: val _ =
haftmann@41829:   Outer_Syntax.command "interpretation"
haftmann@41829:     "prove interpretation of locale expression in theory" Keyword.thy_goal
haftmann@41829:     (Parse.!!! (Parse_Spec.locale_expression true) --
wenzelm@47823:       Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
wenzelm@47823:         -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
haftmann@41829:       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
haftmann@41829:       >> (fn ((expr, defs), equations) => Toplevel.print o
haftmann@41829:           Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
haftmann@41829: 
haftmann@41829: end;