4 Interpretation accompanied with mixin definitions. EXPERIMENTAL. |
4 Interpretation accompanied with mixin definitions. EXPERIMENTAL. |
5 *) |
5 *) |
6 |
6 |
7 signature INTERPRETATION_WITH_DEFS = |
7 signature INTERPRETATION_WITH_DEFS = |
8 sig |
8 sig |
9 val interpretation: Expression.expression_i -> |
9 val permanent_interpretation: Expression.expression_i -> |
10 (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list -> |
10 (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list -> |
11 theory -> Proof.state |
11 local_theory -> Proof.state |
12 val interpretation_cmd: Expression.expression -> |
12 val permanent_interpretation_cmd: Expression.expression -> |
13 (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list -> |
13 (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list -> |
14 theory -> Proof.state |
14 local_theory -> Proof.state |
15 end; |
15 end; |
16 |
16 |
17 structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS = |
17 structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS = |
18 struct |
18 struct |
19 |
19 |
20 fun note_eqns_register deps witss def_eqns attrss eqns export export' = |
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 = |
21 let |
25 let |
22 fun meta_rewrite context = |
26 (*reading*) |
23 map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o |
27 val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt; |
24 maps snd; |
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; |
25 in |
68 in |
26 Attrib.generic_notes Thm.lemmaK |
69 ctxt' |
27 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns) |
70 |> fold activate' dep_morphs |
28 #-> (fn facts => `(fn context => meta_rewrite context facts)) |
|
29 #-> (fn eqns => fold (fn ((dep, morph), wits) => |
|
30 fn context => |
|
31 Locale.add_registration |
|
32 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
|
33 (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |> |
|
34 Option.map (rpair true)) |
|
35 export context) (deps ~~ witss)) |
|
36 end; |
71 end; |
37 |
72 |
38 local |
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; |
39 |
81 |
40 fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr |
|
41 expression raw_defs raw_eqns theory = |
|
42 let |
|
43 val (_, (_, defs_ctxt)) = |
|
44 prep_decl expression I [] (Proof_Context.init_global theory); |
|
45 |
82 |
46 val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs |
83 (* interpretation with permanent registration *) |
47 |> Syntax.check_terms defs_ctxt; |
|
48 val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
|
49 ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; |
|
50 |
84 |
51 val (def_eqns, theory') = theory |
85 fun subscribe lthy = |
52 |> Named_Target.theory_init |
86 if Named_Target.is_theory lthy |
53 |> fold_map (Local_Theory.define) defs |
87 then Generic_Target.theory_registration |
54 |>> map (Thm.symmetric o snd o snd) |
88 else Generic_Target.locale_dependency (Named_Target.the_name lthy); |
55 |> Local_Theory.exit_result_global (map o Morphism.thm); |
|
56 |
89 |
57 val ((propss, deps, export), expr_ctxt) = theory' |
90 fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy = |
58 |> Proof_Context.init_global |
91 generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy) |
59 |> prep_expr expression; |
92 expression raw_defs raw_eqns lthy |
60 |
|
61 val eqns = map (parse_prop expr_ctxt o snd) raw_eqns |
|
62 |> Syntax.check_terms expr_ctxt; |
|
63 val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns; |
|
64 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
|
65 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
|
66 |
|
67 fun after_qed witss eqns = |
|
68 (Proof_Context.background_theory o Context.theory_map) |
|
69 (note_eqns_register deps witss def_eqns attrss eqns export export'); |
|
70 |
|
71 in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; |
|
72 |
93 |
73 in |
94 in |
74 |
95 |
75 fun interpretation x = gen_interpretation Expression.cert_goal_expression |
96 fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x; |
76 Expression.cert_declaration (K I) (K I) (K I) x; |
97 fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x; |
77 fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression |
|
78 Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x; |
|
79 |
98 |
80 end; |
99 end; |
81 |
100 |
82 val _ = |
101 val _ = |
83 Outer_Syntax.command @{command_spec "interpretation"} |
102 Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"} |
84 "prove interpretation of locale expression in theory" |
103 "prove interpretation of locale expression into named theory" |
85 (Parse.!!! (Parse_Spec.locale_expression true) -- |
104 (Parse.!!! (Parse_Spec.locale_expression true) -- |
86 Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
105 Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
87 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] -- |
106 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] -- |
88 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
107 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
89 >> (fn ((expr, defs), equations) => Toplevel.print o |
108 >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns)); |
90 Toplevel.theory_to_proof (interpretation_cmd expr defs equations))); |
|
91 |
109 |
92 end; |
110 end; |