350 val qty_full_names = map (fst o dest_Type) qtys |
350 val qty_full_names = map (fst o dest_Type) qtys |
351 val qty_names = map Long_Name.base_name qty_full_names |
351 val qty_names = map Long_Name.base_name qty_full_names |
352 |
352 |
353 val _ = trace_msg (K "Defining the quotient constants...") |
353 val _ = trace_msg (K "Defining the quotient constants...") |
354 val qconstrs_descrs = |
354 val qconstrs_descrs = |
355 (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns |
355 (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) |
|
356 (get_cnstrs dts) raw_all_cns |
356 |
357 |
357 val qbns_descr = |
358 val qbns_descr = |
358 map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns |
359 map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns |
359 |
360 |
360 val qfvs_descr = |
361 val qfvs_descr = |
361 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
362 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs |
362 |
363 |
363 val qfv_bns_descr = |
364 val qfv_bns_descr = |
364 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns |
365 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
|
366 bn_funs raw_fv_bns |
365 |
367 |
366 val qalpha_bns_descr = |
368 val qalpha_bns_descr = |
367 let |
369 let |
368 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
370 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
369 in |
371 in |
370 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms |
372 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
|
373 bn_funs alpha_bn_trms |
371 end |
374 end |
372 |
375 |
373 val qperm_descr = |
376 val qperm_descr = |
374 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
377 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) |
|
378 qty_names raw_perm_funs |
375 |
379 |
376 val qsize_descr = |
380 val qsize_descr = |
377 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
381 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms |
378 |
382 |
379 val qperm_bn_descr = |
383 val qperm_bn_descr = |
380 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns |
384 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
381 |
385 bn_funs raw_perm_bns |
|
386 |
382 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
387 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
383 lthy8) = |
388 lthy8) = |
384 lthy7 |
389 lthy7 |
385 |> fold_map (define_qconsts qtys) qconstrs_descrs |
390 |> fold_map (define_qconsts qtys) qconstrs_descrs |
386 ||>> define_qconsts qtys qbns_descr |
391 ||>> define_qconsts qtys qbns_descr |