446 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) |
446 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) |
447 | _ => ty |
447 | _ => ty |
448 ) |
448 ) |
449 *} |
449 *} |
450 |
450 |
|
451 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
|
452 ML {* fun exchange_ty rty (qty as (Type (qtys, _))) ty = |
|
453 let val (s, tys) = dest_Type ty in |
|
454 if Type.raw_instance (Logic.varifyT ty, rty) |
|
455 then Type (qtys, tys) |
|
456 else Type (s, map (exchange_ty rty qty) tys) |
|
457 end |
|
458 handle _ => ty |
|
459 *} |
|
460 |
|
461 ML {* |
|
462 fun negF absF = repF |
|
463 | negF repF = absF |
|
464 |
|
465 fun get_fun_noexchange flag (rty, qty) lthy ty = |
|
466 let |
|
467 fun get_fun_aux s fs_tys = |
|
468 let |
|
469 val (fs, tys) = split_list fs_tys |
|
470 val (otys, ntys) = split_list tys |
|
471 val oty = Type (s, otys) |
|
472 val nty = Type (s, ntys) |
|
473 val ftys = map (op -->) tys |
|
474 in |
|
475 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
|
476 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
|
477 | NONE => error ("no map association for type " ^ s)) |
|
478 end |
|
479 |
|
480 fun get_fun_fun fs_tys = |
|
481 let |
|
482 val (fs, tys) = split_list fs_tys |
|
483 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
|
484 val oty = nty1 --> oty2 |
|
485 val nty = oty1 --> nty2 |
|
486 val ftys = map (op -->) tys |
|
487 in |
|
488 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
|
489 end |
|
490 |
|
491 fun get_const flag (rty, qty) = |
|
492 let |
|
493 val thy = ProofContext.theory_of lthy |
|
494 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
495 in |
|
496 case flag of |
|
497 absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
|
498 | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
|
499 end |
|
500 |
|
501 fun mk_identity ty = Abs ("", ty, Bound 0) |
|
502 |
|
503 in |
|
504 if (Type.raw_instance (Logic.varifyT ty, rty)) |
|
505 then (get_const flag (ty, (exchange_ty rty qty ty))) |
|
506 else (case ty of |
|
507 TFree _ => (mk_identity ty, (ty, ty)) |
|
508 | Type (_, []) => (mk_identity ty, (ty, ty)) |
|
509 | Type ("fun" , [ty1, ty2]) => |
|
510 get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] |
|
511 | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys) |
|
512 | _ => raise ERROR ("no type variables")) |
|
513 end |
|
514 *} |
451 |
515 |
452 ML {* |
516 ML {* |
453 fun old_get_fun flag rty qty lthy ty = |
517 fun old_get_fun flag rty qty lthy ty = |
454 get_fun flag [(qty, rty)] lthy ty |
518 get_fun_noexchange flag (rty, qty) lthy ty |
455 |
519 *} |
456 fun old_make_const_def nconst_bname otrm mx rty qty lthy = |
520 |
457 make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy |
521 ML {* |
458 *} |
522 fun find_matching_types rty ty = |
|
523 let val (s, tys) = dest_Type ty in |
|
524 if Type.raw_instance (Logic.varifyT ty, rty) |
|
525 then [ty] |
|
526 else flat (map (find_matching_types rty) tys) |
|
527 end |
|
528 *} |
|
529 |
|
530 ML {* |
|
531 fun get_fun_new flag rty qty lthy ty = |
|
532 let |
|
533 val tys = find_matching_types rty ty; |
|
534 val qenv = map (fn t => (exchange_ty rty qty t, t)) tys; |
|
535 val xchg_ty = exchange_ty rty qty ty |
|
536 in |
|
537 get_fun flag qenv lthy xchg_ty |
|
538 end |
|
539 *} |
|
540 |
|
541 (* |
|
542 consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
543 axioms Rl_eq: "EQUIV Rl" |
|
544 |
|
545 quotient ql = "'a list" / "Rl" |
|
546 by (rule Rl_eq) |
|
547 |
|
548 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} |
|
549 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} |
|
550 ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *} |
|
551 |
|
552 ML {* |
|
553 fst (get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt)) |
|
554 *} |
|
555 ML {* |
|
556 fst (get_fun_new absF al aq @{context} (fastype_of ttt)) |
|
557 *} |
|
558 ML {* |
|
559 fun mk_abs tm = |
|
560 let |
|
561 val ty = fastype_of tm |
|
562 in fst (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end |
|
563 fun mk_repabs tm = |
|
564 let |
|
565 val ty = fastype_of tm |
|
566 in fst (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end |
|
567 *} |
|
568 ML {* |
|
569 cterm_of @{theory} (mk_repabs ttt) |
|
570 *} |
|
571 *) |
459 |
572 |
460 text {* Does the same as 'subst' in a given prop or theorem *} |
573 text {* Does the same as 'subst' in a given prop or theorem *} |
461 ML {* |
574 ML {* |
462 fun eqsubst_prop ctxt thms t = |
575 fun eqsubst_prop ctxt thms t = |
463 let |
576 let |
497 *} |
610 *} |
498 |
611 |
499 ML {* |
612 ML {* |
500 fun build_repabs_term lthy thm constructors rty qty = |
613 fun build_repabs_term lthy thm constructors rty qty = |
501 let |
614 let |
502 fun mk_rep tm = |
615 val rty = Logic.varifyT rty; |
503 let |
616 val qty = Logic.varifyT qty; |
504 val ty = old_exchange_ty rty qty (fastype_of tm) |
617 |
505 in fst (old_get_fun repF rty qty lthy ty) $ tm end |
618 fun mk_abs tm = |
506 |
619 let |
507 fun mk_abs tm = |
620 val ty = fastype_of tm |
508 let |
621 in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end |
509 val ty = old_exchange_ty rty qty (fastype_of tm) in |
622 fun mk_repabs tm = |
510 fst (old_get_fun absF rty qty lthy ty) $ tm end |
623 let |
|
624 val ty = fastype_of tm |
|
625 in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ (mk_abs tm) end |
511 |
626 |
512 fun is_constructor (Const (x, _)) = member (op =) constructors x |
627 fun is_constructor (Const (x, _)) = member (op =) constructors x |
513 | is_constructor _ = false; |
628 | is_constructor _ = false; |
514 |
629 |
515 fun build_aux lthy tm = |
630 fun build_aux lthy tm = |
519 val (vs, t) = Term.dest_abs a; |
634 val (vs, t) = Term.dest_abs a; |
520 val v = Free(vs, vty); |
635 val v = Free(vs, vty); |
521 val t' = lambda v (build_aux lthy t) |
636 val t' = lambda v (build_aux lthy t) |
522 in |
637 in |
523 if (not (needs_lift rty (fastype_of tm))) then t' |
638 if (not (needs_lift rty (fastype_of tm))) then t' |
524 else mk_rep (mk_abs ( |
639 else mk_repabs ( |
525 if not (needs_lift rty vty) then t' |
640 if not (needs_lift rty vty) then t' |
526 else |
641 else |
527 let |
642 let |
528 val v' = mk_rep (mk_abs v); |
643 val v' = mk_repabs v; |
529 val t1 = Envir.beta_norm (t' $ v') |
644 val t1 = Envir.beta_norm (t' $ v') |
530 in |
645 in |
531 lambda v t1 |
646 lambda v t1 |
532 end |
647 end |
533 )) |
648 ) |
534 end |
649 end |
535 | x => |
650 | x => |
536 let |
651 let |
537 val (opp, tms0) = Term.strip_comb tm |
652 val (opp, tms0) = Term.strip_comb tm |
538 val tms = map (build_aux lthy) tms0 |
653 val tms = map (build_aux lthy) tms0 |
539 val ty = fastype_of tm |
654 val ty = fastype_of tm |
540 in |
655 in |
541 if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) |
656 if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) |
542 then (list_comb (opp, (hd tms0) :: (tl tms))) |
657 then (list_comb (opp, (hd tms0) :: (tl tms))) |
543 else if (is_constructor opp andalso needs_lift rty ty) then |
658 else if (is_constructor opp andalso needs_lift rty ty) then |
544 mk_rep (mk_abs (list_comb (opp,tms))) |
659 mk_repabs (list_comb (opp,tms)) |
545 else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then |
660 else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then |
546 mk_rep(mk_abs(list_comb(opp,tms))) |
661 mk_repabs(list_comb(opp,tms)) |
547 else if tms = [] then opp |
662 else if tms = [] then opp |
548 else list_comb(opp, tms) |
663 else list_comb(opp, tms) |
549 end |
664 end |
550 in |
665 in |
551 repeat_eqsubst_prop lthy @{thms id_def_sym} |
666 repeat_eqsubst_prop lthy @{thms id_def_sym} |
822 *} |
937 *} |
823 |
938 |
824 ML {* |
939 ML {* |
825 fun applic_prs lthy rty qty absrep ty = |
940 fun applic_prs lthy rty qty absrep ty = |
826 let |
941 let |
|
942 val rty = Logic.varifyT rty; |
|
943 val qty = Logic.varifyT qty; |
827 fun absty ty = |
944 fun absty ty = |
828 old_exchange_ty rty qty ty |
945 exchange_ty rty qty ty |
829 fun mk_rep tm = |
946 fun mk_rep tm = |
830 let |
947 let |
831 val ty = old_exchange_ty rty qty (fastype_of tm) |
948 val ty = exchange_ty qty rty (fastype_of tm) |
832 in fst (old_get_fun repF rty qty lthy ty) $ tm end; |
949 in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end; |
833 fun mk_abs tm = |
950 fun mk_abs tm = |
834 let |
951 let |
835 val ty = old_exchange_ty rty qty (fastype_of tm) in |
952 val ty = fastype_of tm |
836 fst (old_get_fun absF rty qty lthy ty) $ tm end; |
953 in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end |
837 val (l, ltl) = Term.strip_type ty; |
954 val (l, ltl) = Term.strip_type ty; |
838 val nl = map absty l; |
955 val nl = map absty l; |
839 val vs = map (fn _ => "x") l; |
956 val vs = map (fn _ => "x") l; |
840 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
957 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
841 val args = map Free (vfs ~~ nl); |
958 val args = map Free (vfs ~~ nl); |