324 |
324 |
325 ML {* |
325 ML {* |
326 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
326 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
327 let |
327 let |
328 (* definition of the raw datatypes *) |
328 (* definition of the raw datatypes *) |
329 |
329 val _ = warning "Definition of raw datatypes"; |
330 val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
330 val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
331 if get_STEPS lthy > 0 |
331 if get_STEPS lthy > 0 |
332 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
332 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
333 else raise TEST lthy |
333 else raise TEST lthy |
334 |
334 |
345 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
345 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
346 val induct_thm = #induct dtinfo; |
346 val induct_thm = #induct dtinfo; |
347 val exhaust_thms = map #exhaust dtinfos; |
347 val exhaust_thms = map #exhaust dtinfos; |
348 |
348 |
349 (* definitions of raw permutations *) |
349 (* definitions of raw permutations *) |
|
350 val _ = warning "Definition of raw permutations"; |
350 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
351 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
351 if get_STEPS lthy0 > 1 |
352 if get_STEPS lthy0 > 1 |
352 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 |
353 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 |
353 else raise TEST lthy0 |
354 else raise TEST lthy0 |
354 |
355 |
358 |
359 |
359 val thy = Local_Theory.exit_global lthy2a; |
360 val thy = Local_Theory.exit_global lthy2a; |
360 val thy_name = Context.theory_name thy |
361 val thy_name = Context.theory_name thy |
361 |
362 |
362 (* definition of raw fv_functions *) |
363 (* definition of raw fv_functions *) |
|
364 val _ = warning "Definition of raw fv-functions"; |
363 val lthy3 = Theory_Target.init NONE thy; |
365 val lthy3 = Theory_Target.init NONE thy; |
364 |
366 |
365 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
367 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
366 if get_STEPS lthy3 > 2 |
368 if get_STEPS lthy3 > 2 |
367 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
369 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
368 else raise TEST lthy3 |
370 else raise TEST lthy3 |
369 |
371 |
370 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
371 val bns = raw_bn_funs ~~ bn_nos; |
|
372 |
|
373 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
372 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
374 if get_STEPS lthy3a > 3 |
373 if get_STEPS lthy3a > 3 |
375 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a |
374 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a |
376 else raise TEST lthy3a |
375 else raise TEST lthy3a |
377 |
376 |
378 (* definition of raw alphas *) |
377 (* definition of raw alphas *) |
|
378 val _ = warning "Definition of alphas"; |
379 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
379 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
380 if get_STEPS lthy3b > 4 |
380 if get_STEPS lthy3b > 4 |
381 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b |
381 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b |
382 else raise TEST lthy3b |
382 else raise TEST lthy3b |
383 |
383 |
384 (* definition of alpha-distinct lemmas *) |
384 (* definition of alpha-distinct lemmas *) |
|
385 val _ = warning "Distinct theorems"; |
385 val (alpha_distincts, alpha_bn_distincts) = |
386 val (alpha_distincts, alpha_bn_distincts) = |
386 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
387 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
387 |
388 |
388 (* definition of raw_alpha_eq_iff lemmas *) |
389 (* definition of raw_alpha_eq_iff lemmas *) |
|
390 val _ = warning "Eq-iff theorems"; |
389 val alpha_eq_iff = |
391 val alpha_eq_iff = |
390 if get_STEPS lthy > 5 |
392 if get_STEPS lthy > 5 |
391 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
393 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
392 else raise TEST lthy4 |
394 else raise TEST lthy4 |
393 |
395 |
416 else raise TEST lthy4 |
418 else raise TEST lthy4 |
417 |
419 |
418 (* proving alpha equivalence *) |
420 (* proving alpha equivalence *) |
419 val _ = warning "Proving equivalence" |
421 val _ = warning "Proving equivalence" |
420 |
422 |
|
423 val alpha_refl_thms = |
|
424 if get_STEPS lthy > 9 |
|
425 then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy_tmp'' |
|
426 else raise TEST lthy4 |
|
427 |
421 val alpha_sym_thms = |
428 val alpha_sym_thms = |
422 if get_STEPS lthy > 9 |
429 if get_STEPS lthy > 10 |
423 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' |
430 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' |
424 else raise TEST lthy4 |
431 else raise TEST lthy4 |
425 |
432 |
426 val alpha_trans_thms = |
433 val alpha_trans_thms = |
427 if get_STEPS lthy > 10 |
434 if get_STEPS lthy > 11 |
428 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
435 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
429 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
436 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
430 else raise TEST lthy4 |
437 else raise TEST lthy4 |
431 |
438 |
432 |
439 |
433 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
440 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
434 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
441 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
435 val _ = tracing ("alpha_trans\n" ^ |
442 val _ = tracing ("alpha_refl\n" ^ |
436 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms)) |
443 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
437 |
444 |
438 val _ = |
445 val _ = |
439 if get_STEPS lthy > 11 |
446 if get_STEPS lthy > 12 |
440 then true else raise TEST lthy4 |
447 then true else raise TEST lthy4 |
|
448 |
|
449 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
450 val bns = raw_bn_funs ~~ bn_nos; |
441 |
451 |
442 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
452 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
443 |
453 |
444 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
454 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
445 val alpha_equivp = |
455 val alpha_equivp = |