114 |
114 |
115 (* interpretation machinery *) |
115 (* interpretation machinery *) |
116 |
116 |
117 local |
117 local |
118 |
118 |
119 fun meta_rewrite eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); |
119 fun meta_rewrite eqns ctxt = |
|
120 (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); |
120 |
121 |
121 fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = |
122 fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = |
122 let |
123 let |
123 val facts = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) |
124 val facts = |
124 :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; |
125 (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) :: |
|
126 map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) |
|
127 attrss eqns; |
125 val (eqns', ctxt') = ctxt |
128 val (eqns', ctxt') = ctxt |
126 |> note Thm.theoremK facts |
129 |> note Thm.theoremK facts |
127 |-> meta_rewrite; |
130 |-> meta_rewrite; |
128 val dep_morphs = map2 (fn (dep, morph) => fn wits => |
131 val dep_morphs = |
129 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; |
132 map2 (fn (dep, morph) => fn wits => |
130 fun activate' dep_morph ctxt = activate dep_morph |
133 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) |
131 (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt; |
134 deps witss; |
132 in |
135 fun activate' dep_morph ctxt = |
133 ctxt' |
136 activate dep_morph |
134 |> fold activate' dep_morphs |
137 (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) |
135 end; |
138 export ctxt; |
|
139 in ctxt' |> fold activate' dep_morphs end; |
136 |
140 |
137 in |
141 in |
138 |
142 |
139 fun generic_interpretation prep_interpretation setup_proof note add_registration |
143 fun generic_interpretation prep_interpretation setup_proof note add_registration |
140 expression raw_defs raw_eqns initial_ctxt = |
144 expression raw_defs raw_eqns initial_ctxt = |