|
1 (* Title: Tools/permanent_interpretation.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Permanent interpretation accompanied with mixin definitions. |
|
5 *) |
|
6 |
|
7 signature PERMANENT_INTERPRETATION = |
|
8 sig |
|
9 val permanent_interpretation: Expression.expression_i -> |
|
10 (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list -> |
|
11 local_theory -> Proof.state |
|
12 val permanent_interpretation_cmd: Expression.expression -> |
|
13 (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list -> |
|
14 local_theory -> Proof.state |
|
15 end; |
|
16 |
|
17 structure Permanent_Interpretation : PERMANENT_INTERPRETATION = |
|
18 struct |
|
19 |
|
20 local |
|
21 |
|
22 (* reading *) |
|
23 |
|
24 fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = |
|
25 let |
|
26 (*reading*) |
|
27 val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt; |
|
28 val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt; |
|
29 val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt; |
|
30 val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
|
31 val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
|
32 |
|
33 (*defining*) |
|
34 val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
|
35 ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; |
|
36 val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt; |
|
37 val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs; |
|
38 val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt; |
|
39 (*the "if" prevents restoring a proof context which is no local theory*) |
|
40 |
|
41 (*setting up*) |
|
42 val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt; |
|
43 (*FIXME: only re-prepare if defs are given*) |
|
44 val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns; |
|
45 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
|
46 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
|
47 in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
|
48 |
|
49 val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I); |
|
50 val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src; |
|
51 |
|
52 |
|
53 (* generic interpretation machinery *) |
|
54 |
|
55 fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt); |
|
56 |
|
57 fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = |
|
58 let |
|
59 val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) |
|
60 :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; |
|
61 val (eqns', ctxt') = ctxt |
|
62 |> note Thm.lemmaK facts |
|
63 |-> meta_rewrite; |
|
64 val dep_morphs = map2 (fn (dep, morph) => fn wits => |
|
65 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; |
|
66 fun activate' dep_morph ctxt = activate dep_morph |
|
67 (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt; |
|
68 in |
|
69 ctxt' |
|
70 |> fold activate' dep_morphs |
|
71 end; |
|
72 |
|
73 fun generic_interpretation prep_interpretation setup_proof note add_registration |
|
74 expression raw_defs raw_eqns initial_ctxt = |
|
75 let |
|
76 val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = |
|
77 prep_interpretation expression raw_defs raw_eqns initial_ctxt; |
|
78 fun after_qed witss eqns = |
|
79 note_eqns_register note add_registration deps witss def_eqns eqns attrss export export'; |
|
80 in setup_proof after_qed propss eqns goal_ctxt end; |
|
81 |
|
82 |
|
83 (* interpretation with permanent registration *) |
|
84 |
|
85 fun subscribe lthy = |
|
86 if Named_Target.is_theory lthy |
|
87 then Generic_Target.theory_registration |
|
88 else Generic_Target.locale_dependency (Named_Target.the_name lthy); |
|
89 |
|
90 fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy = |
|
91 generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy) |
|
92 expression raw_defs raw_eqns lthy |
|
93 |
|
94 in |
|
95 |
|
96 fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x; |
|
97 fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x; |
|
98 |
|
99 end; |
|
100 |
|
101 val _ = |
|
102 Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"} |
|
103 "prove interpretation of locale expression into named theory" |
|
104 (Parse.!!! (Parse_Spec.locale_expression true) -- |
|
105 Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
|
106 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- |
|
107 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
|
108 >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns)); |
|
109 |
|
110 end; |