319 val raw_size_rsp = |
319 val raw_size_rsp = |
320 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
320 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
321 |> map mk_funs_rsp |
321 |> map mk_funs_rsp |
322 |
322 |
323 val raw_constrs_rsp = |
323 val raw_constrs_rsp = |
324 raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
324 raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
325 |
325 |
326 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
326 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
327 |
327 |
328 val alpha_bn_rsp = |
328 val alpha_bn_rsp = |
329 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
329 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
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]), |
336 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
336 raw_funs_rsp @ alpha_permute_rsp @ |
337 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
337 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
|
338 |
|
339 val _ = tracing (PolyML.makestring (raw_size_rsp, raw_funs_rsp, alpha_permute_rsp, |
|
340 alpha_bn_rsp, raw_perm_bn_rsp)) |
338 |
341 |
339 val _ = trace_msg (K "Defining the quotient types...") |
342 val _ = trace_msg (K "Defining the quotient types...") |
340 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
343 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
341 |
344 |
342 val (qty_infos, lthy7) = |
345 val (qty_infos, lthy7) = |
346 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
349 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
347 end |
350 end |
348 |
351 |
349 val qtys = map #qtyp qty_infos |
352 val qtys = map #qtyp qty_infos |
350 val qty_full_names = map (fst o dest_Type) qtys |
353 val qty_full_names = map (fst o dest_Type) qtys |
351 val qty_names = map Long_Name.base_name qty_full_names |
354 val qty_names = map Long_Name.base_name qty_full_names |
352 |
355 |
353 val _ = trace_msg (K "Defining the quotient constants...") |
356 val _ = trace_msg (K "Defining the quotient constants...") |
354 val qconstrs_descrs = |
357 val qconstrs_descrs = |
355 (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) |
358 (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) |
356 (get_cnstrs dts) raw_all_cns |
359 (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp)) |
357 |
360 |
358 val qbns_descr = |
361 val qbns_descr = |
359 map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns |
362 map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns |
360 |
363 |
361 val qfvs_descr = |
364 val qfvs_descr = |
376 val qperm_descr = |
379 val qperm_descr = |
377 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) |
380 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) |
378 qty_names raw_perm_funs |
381 qty_names raw_perm_funs |
379 |
382 |
380 val qsize_descr = |
383 val qsize_descr = |
381 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms |
384 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 |
386 |
383 val qperm_bn_descr = |
387 val qperm_bn_descr = |
384 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
388 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
385 bn_funs raw_perm_bns |
389 bn_funs raw_perm_bns |
386 |
390 |