330 |
330 |
331 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
331 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
332 |
332 |
333 (* noting the quot_respects lemmas *) |
333 (* noting the quot_respects lemmas *) |
334 val (_, lthy6) = |
334 val (_, lthy6) = |
335 Local_Theory.note ((Binding.empty, [rsp_attr]), |
335 Local_Theory.note ((Binding.empty, [rsp_attr]), raw_funs_rsp) lthy5 |
336 raw_funs_rsp @ alpha_permute_rsp @ |
336 |
337 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
337 val _ = tracing (PolyML.makestring (raw_funs_rsp)) |
338 |
|
339 val _ = tracing (PolyML.makestring (raw_size_rsp, raw_funs_rsp, alpha_permute_rsp, |
|
340 alpha_bn_rsp, raw_perm_bn_rsp)) |
|
341 |
338 |
342 val _ = trace_msg (K "Defining the quotient types...") |
339 val _ = trace_msg (K "Defining the quotient types...") |
343 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
340 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
344 |
341 |
345 val (qty_infos, lthy7) = |
342 val (qty_infos, lthy7) = |
370 |
367 |
371 val qalpha_bns_descr = |
368 val qalpha_bns_descr = |
372 let |
369 let |
373 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
370 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
374 in |
371 in |
375 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
372 map2 (fn (b, _, _) => fn (t, th) => ("alpha_" ^ Variable.check_name b, t, NoSyn, th)) |
376 bn_funs alpha_bn_trms |
373 bn_funs (alpha_bn_trms ~~ alpha_bn_rsp) |
377 end |
374 end |
378 |
375 |
379 val qperm_descr = |
376 val qperm_descr = |
380 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) |
377 map2 (fn n => fn (t, th) => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, th)) |
381 qty_names raw_perm_funs |
378 qty_names (raw_perm_funs ~~ (take (length raw_perm_funs) alpha_permute_rsp)) |
382 |
379 |
383 val qsize_descr = |
380 val qsize_descr = |
384 map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names |
381 map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names |
385 (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp)) |
382 (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp)) |
386 |
383 |
387 val qperm_bn_descr = |
384 val qperm_bn_descr = |
388 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
385 map2 (fn (b, _, _) => fn (t, th) => ("permute_" ^ Variable.check_name b, t, NoSyn, th)) |
389 bn_funs raw_perm_bns |
386 bn_funs (raw_perm_bns ~~ raw_perm_bn_rsp) |
390 |
387 |
391 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
388 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
392 lthy8) = |
389 lthy8) = |
393 lthy7 |
390 lthy7 |
394 |> fold_map (define_qconsts qtys) qconstrs_descrs |
391 |> fold_map (define_qconsts qtys) qconstrs_descrs |