98 local |
98 local |
99 |
99 |
100 fun meta_rewrite eqns ctxt = |
100 fun meta_rewrite eqns ctxt = |
101 (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); |
101 (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); |
102 |
102 |
103 fun note_eqns_register pos note activate deps eqnss witss def_eqns thms export export' ctxt = |
103 fun note_eqns_register pos note add_registration |
104 let |
104 deps eqnss witss def_eqns thms export export' ctxt = |
105 val thmss = unflat ((map o map) fst eqnss) thms; |
105 let |
106 val factss = |
106 val factss = thms |
107 map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss; |
107 |> unflat ((map o map) #1 eqnss) |
108 val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; |
108 |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); |
|
109 val (eqnss', ctxt') = |
|
110 fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; |
109 val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); |
111 val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); |
110 val (eqns', ctxt'') = ctxt' |
112 val (eqns', ctxt'') = ctxt' |
111 |> note Thm.theoremK [defs] |
113 |> note Thm.theoremK [defs] |
112 |-> meta_rewrite; |
114 |-> meta_rewrite; |
113 val dep_morphs = |
115 val dep_morphs = |
114 map2 (fn (dep, morph) => fn wits => |
116 map2 (fn (dep, morph) => fn wits => |
115 let val morph' = morph |
117 let val morph' = morph |
116 $> Element.satisfy_morphism (map (Element.transform_witness export') wits) |
118 $> Element.satisfy_morphism (map (Element.transform_witness export') wits) |
117 $> Morphism.binding_morphism "position" (Binding.set_pos pos) |
119 $> Morphism.binding_morphism "position" (Binding.set_pos pos) |
118 in (dep, morph') end) deps witss; |
120 in (dep, morph') end) deps witss; |
119 fun activate' (dep_morph, eqns) ctxt = |
121 fun register (dep_morph, eqns) ctxt = |
120 activate dep_morph |
122 add_registration dep_morph |
121 (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns'))) |
123 (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns'))) |
122 export ctxt; |
124 export ctxt; |
123 in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end; |
125 in ctxt'' |> fold register (dep_morphs ~~ eqnss') end; |
124 |
126 |
125 in |
127 in |
126 |
128 |
127 fun generic_interpretation prep_interpretation setup_proof note add_registration |
129 fun generic_interpretation prep_interpretation setup_proof note add_registration |
128 expression raw_defs initial_ctxt = |
130 expression raw_defs initial_ctxt = |