311 val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result |
310 val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result |
312 |
311 |
313 val _ = trace_msg (K "Proving respectfulness...") |
312 val _ = trace_msg (K "Proving respectfulness...") |
314 val raw_funs_rsp_aux = |
313 val raw_funs_rsp_aux = |
315 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
314 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
316 |
315 |
317 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
316 val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux |
|
317 |
|
318 fun match_const cnst th = |
|
319 (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = |
|
320 fst (dest_Const cnst); |
|
321 fun find_matching_rsp cnst = |
|
322 hd (filter (fn th => match_const cnst th) raw_funs_rsp); |
|
323 val raw_fv_rsp = map find_matching_rsp raw_fvs; |
|
324 val raw_bn_rsp = map find_matching_rsp raw_bns; |
|
325 val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns; |
318 |
326 |
319 val raw_size_rsp = |
327 val raw_size_rsp = |
320 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
328 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
321 |> map mk_funs_rsp |
329 |> map mk_funs_rsp |
322 |
330 |
323 val raw_constrs_rsp = |
331 val raw_constrs_rsp = |
324 raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
332 raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
325 |
333 |
326 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
334 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
327 |
335 |
328 val alpha_bn_rsp = |
336 val alpha_bn_rsp = |
329 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
337 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
330 |
338 |
331 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
339 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
332 |
340 |
333 (* noting the quot_respects lemmas *) |
|
334 val (_, lthy6) = |
|
335 Local_Theory.note ((Binding.empty, [rsp_attr]), |
|
336 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
|
337 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
|
338 |
|
339 val _ = trace_msg (K "Defining the quotient types...") |
341 val _ = trace_msg (K "Defining the quotient types...") |
340 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
342 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
341 |
343 |
342 val (qty_infos, lthy7) = |
344 val (qty_infos, lthy7) = |
343 let |
345 let |
344 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
346 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
345 in |
347 in |
346 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
348 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy5 |
347 end |
349 end |
348 |
350 |
349 val qtys = map #qtyp qty_infos |
351 val qtys = map #qtyp qty_infos |
350 val qty_full_names = map (fst o dest_Type) qtys |
352 val qty_full_names = map (fst o dest_Type) qtys |
351 val qty_names = map Long_Name.base_name qty_full_names |
353 val qty_names = map Long_Name.base_name qty_full_names |
352 |
354 |
353 val _ = trace_msg (K "Defining the quotient constants...") |
355 val _ = trace_msg (K "Defining the quotient constants...") |
354 val qconstrs_descrs = |
356 val qconstrs_descrs = |
355 (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) |
357 (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) |
356 (get_cnstrs dts) raw_all_cns |
358 (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp)) |
357 |
359 |
358 val qbns_descr = |
360 val qbns_descr = |
359 map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns |
361 map2 (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) bn_funs (raw_bns ~~ raw_bn_rsp) |
360 |
362 |
361 val qfvs_descr = |
363 val qfvs_descr = |
362 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs |
364 map2 (fn n => fn (t, th) => ("fv_" ^ n, t, NoSyn, th)) qty_names (raw_fvs ~~ raw_fv_rsp) |
363 |
365 |
364 val qfv_bns_descr = |
366 val qfv_bns_descr = |
365 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
367 map2 (fn (b, _, _) => fn (t, th) => ("fv_" ^ Variable.check_name b, t, NoSyn, th)) |
366 bn_funs raw_fv_bns |
368 bn_funs (raw_fv_bns ~~ raw_fv_bn_rsp) |
367 |
369 |
368 val qalpha_bns_descr = |
370 val qalpha_bns_descr = |
369 let |
371 let |
370 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
372 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
371 in |
373 in |
372 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
374 map2 (fn (b, _, _) => fn (t, th) => ("alpha_" ^ Variable.check_name b, t, NoSyn, th)) |
373 bn_funs alpha_bn_trms |
375 bn_funs (alpha_bn_trms ~~ alpha_bn_rsp) |
374 end |
376 end |
375 |
377 |
376 val qperm_descr = |
378 val qperm_descr = |
377 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) |
379 map2 (fn n => fn (t, th) => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, th)) |
378 qty_names raw_perm_funs |
380 qty_names (raw_perm_funs ~~ (take (length raw_perm_funs) alpha_permute_rsp)) |
379 |
381 |
380 val qsize_descr = |
382 val qsize_descr = |
381 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms |
383 map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names |
|
384 (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp)) |
382 |
385 |
383 val qperm_bn_descr = |
386 val qperm_bn_descr = |
384 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
387 map2 (fn (b, _, _) => fn (t, th) => ("permute_" ^ Variable.check_name b, t, NoSyn, th)) |
385 bn_funs raw_perm_bns |
388 bn_funs (raw_perm_bns ~~ raw_perm_bn_rsp) |
386 |
389 |
387 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
390 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
388 lthy8) = |
391 lthy8) = |
389 lthy7 |
392 lthy7 |
390 |> fold_map (define_qconsts qtys) qconstrs_descrs |
393 |> fold_map (define_qconsts qtys) qconstrs_descrs |