303 fun get_STEPS ctxt = Config.get ctxt STEPS |
303 fun get_STEPS ctxt = Config.get ctxt STEPS |
304 *} |
304 *} |
305 |
305 |
306 setup STEPS_setup |
306 setup STEPS_setup |
307 |
307 |
|
308 ML {* dtyp_no_of_typ *} |
|
309 |
308 ML {* |
310 ML {* |
309 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
311 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
310 let |
312 let |
311 (* definition of the raw datatypes *) |
313 (* definition of the raw datatypes *) |
312 val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) = |
314 val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) = |
325 val rel_dtinfos = List.take (dtinfos, (length dts)); |
327 val rel_dtinfos = List.take (dtinfos, (length dts)); |
326 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
328 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
327 val induct_thm = #induct dtinfo; |
329 val induct_thm = #induct dtinfo; |
328 val exhaust_thms = map #exhaust dtinfos; |
330 val exhaust_thms = map #exhaust dtinfos; |
329 |
331 |
|
332 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
333 val bns = raw_bn_funs ~~ bn_nos; |
|
334 |
330 (* definitions of raw permutations *) |
335 (* definitions of raw permutations *) |
331 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
336 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
332 if get_STEPS lthy1 > 2 |
337 if get_STEPS lthy1 > 2 |
333 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
338 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
334 else raise TEST lthy1 |
339 else raise TEST lthy1 |
352 val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
357 val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
353 if get_STEPS lthy > 4 |
358 if get_STEPS lthy > 4 |
354 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a |
359 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a |
355 else raise TEST lthy3a |
360 else raise TEST lthy3a |
356 |
361 |
357 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
362 (* HERE *) |
358 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
363 (* definition of raw_alpha_eq_iff lemmas *) |
359 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
|
360 |
|
361 val bns = raw_bn_funs ~~ bn_nos; |
|
362 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts)); |
364 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts)); |
363 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
365 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
364 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts)) |
366 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts)) |
365 |
367 |
366 (* definition of raw_alpha_eq_iff lemmas *) |
|
367 val alpha_eq_iff = |
368 val alpha_eq_iff = |
368 if get_STEPS lthy > 5 |
369 if get_STEPS lthy > 5 |
369 then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
370 then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
370 else raise TEST lthy4 |
371 else raise TEST lthy4 |
371 |
372 |
373 |
374 |
374 (* proving equivariance lemmas for bns, fvs and alpha *) |
375 (* proving equivariance lemmas for bns, fvs and alpha *) |
375 val _ = warning "Proving equivariance"; |
376 val _ = warning "Proving equivariance"; |
376 val (bv_eqvt, lthy5) = |
377 val (bv_eqvt, lthy5) = |
377 if get_STEPS lthy > 6 |
378 if get_STEPS lthy > 6 |
378 then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 |
379 then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) raw_bn_funs lthy4 |
379 else raise TEST lthy4 |
380 else raise TEST lthy4 |
380 |
381 |
381 val (fv_eqvt, lthy6) = |
382 val (fv_eqvt, lthy6) = |
382 if get_STEPS lthy > 7 |
383 if get_STEPS lthy > 7 |
383 then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 |
384 then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 |