423 else raise TEST lthy6 |
423 else raise TEST lthy6 |
424 |
424 |
425 (* defining the quotient type *) |
425 (* defining the quotient type *) |
426 val _ = warning "Declaring the quotient types" |
426 val _ = warning "Declaring the quotient types" |
427 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
427 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
428 val qty_binds = map (fn (_, bind, _, _) => bind) dts (* not used *) |
428 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
429 val qty_names = map Name.of_binding qty_binds; (* not used *) |
429 val qty_names = map Name.of_binding qty_binds; |
430 val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *) |
430 val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *) |
431 |
431 |
432 val (qty_infos, lthy7) = |
432 val (qty_infos, lthy7) = |
433 if get_STEPS lthy > 14 |
433 if get_STEPS lthy > 14 |
434 then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
434 then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
435 else raise TEST lthy6 |
435 else raise TEST lthy6 |
436 |
436 |
437 val qtys = map #qtyp qty_infos |
437 val qtys = map #qtyp qty_infos |
438 val qconstr_descrs = |
438 |
|
439 (* defining of quotient term-constructors, binding functions, free vars functions *) |
|
440 val qconstr_descr = |
439 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
441 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
440 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
442 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
441 |
443 |
442 val (qconstrs, lthy8) = |
444 val qbns_descr = |
|
445 map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs |
|
446 |
|
447 val qfvs_descr = |
|
448 map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs |
|
449 |
|
450 |
|
451 val (qs, lthy8) = |
443 if get_STEPS lthy > 15 |
452 if get_STEPS lthy > 15 |
444 then qconst_defs qtys qconstr_descrs lthy7 |
453 then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7 |
445 else raise TEST lthy7 |
454 else raise TEST lthy7 |
446 |
455 |
|
456 val _ = tracing ("raw fvs " ^ commas (map @{make_string} raw_fvs)) |
|
457 val _ = tracing ("raw fv_bns " ^ commas (map @{make_string} raw_fv_bns)) |
|
458 |
447 (* HERE *) |
459 (* HERE *) |
448 |
|
449 val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys)) |
|
450 val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs)) |
|
451 val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys)) |
|
452 val _ = tracing ("qconstrs " ^ commas (map @{make_string} qconstrs)) |
|
453 |
460 |
454 val _ = |
461 val _ = |
455 if get_STEPS lthy > 16 |
462 if get_STEPS lthy > 16 |
456 then true else raise TEST lthy8 |
463 then true else raise TEST lthy8 |
457 |
464 |
496 fun const_rsp_tac _ = |
503 fun const_rsp_tac _ = |
497 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
504 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
498 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
505 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
499 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
506 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
500 const_rsp_tac) raw_consts lthy11a |
507 const_rsp_tac) raw_consts lthy11a |
501 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
508 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
502 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) |
509 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) |
503 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; |
510 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; |
504 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
511 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
505 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
512 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
506 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs |
513 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs |