206 ||>> pair raw_binds |
206 ||>> pair raw_binds |
207 end |
207 end |
208 *} |
208 *} |
209 |
209 |
210 ML {* add_primrec_wrapper *} |
210 ML {* add_primrec_wrapper *} |
|
211 |
|
212 lemma equivp_hack: "equivp x" |
|
213 sorry |
|
214 ML {* |
|
215 fun equivp_hack ctxt rel = |
|
216 let |
|
217 val thy = ProofContext.theory_of ctxt |
|
218 val ty = domain_type (fastype_of rel) |
|
219 val cty = ctyp_of thy ty |
|
220 val ct = cterm_of thy rel |
|
221 in |
|
222 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
|
223 end |
|
224 *} |
|
225 |
211 |
226 |
212 ML {* |
227 ML {* |
213 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
228 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
214 let |
229 let |
215 val thy = ProofContext.theory_of lthy |
230 val thy = ProofContext.theory_of lthy |
247 val bns = raw_bn_funs ~~ bn_nos; |
262 val bns = raw_bn_funs ~~ bn_nos; |
248 val alpha_intros = #intrs alpha; |
263 val alpha_intros = #intrs alpha; |
249 val alpha_cases = #elims alpha |
264 val alpha_cases = #elims alpha |
250 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 |
265 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 |
251 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
266 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
252 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
267 (* val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
253 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
268 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
254 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
269 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
255 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
270 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
256 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
271 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
257 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
272 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
|
273 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
258 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
274 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
259 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
275 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
260 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
276 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
261 val qty_binds = map (fn (_, b, _, _) => b) dts; |
277 val qty_binds = map (fn (_, b, _, _) => b) dts; |
262 val qty_names = map Name.of_binding qty_binds; |
278 val qty_names = map Name.of_binding qty_binds; |
297 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
313 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
298 val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def; |
314 val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def; |
299 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
315 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
300 val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; |
316 val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; |
301 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
317 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
302 in |
318 val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
303 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy17) |
319 val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; |
304 end |
320 val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
305 *} |
321 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*) |
306 |
322 in |
|
323 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
|
324 end |
|
325 *} |
|
326 ML fold |
307 ML name_of_typ |
327 ML name_of_typ |
308 |
328 |
309 ML {* |
329 ML {* |
310 (* parsing the datatypes and declaring *) |
330 (* parsing the datatypes and declaring *) |
311 (* constructors in the local theory *) |
331 (* constructors in the local theory *) |