528 in ListPair.map eta_Var (ixs, take (n+1) Ts) end |
528 in ListPair.map eta_Var (ixs, take (n+1) Ts) end |
529 val lhs = list_comb(f,xn_list("X",k-1)) |
529 val lhs = list_comb(f,xn_list("X",k-1)) |
530 val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
530 val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
531 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
531 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
532 |
532 |
533 fun find_subst sg T = |
533 fun find_subst ctxt T = |
534 let fun find (thm::thms) = |
534 let fun find (thm::thms) = |
535 let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm)); |
535 let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm)); |
536 val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, [])); |
536 val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, [])); |
537 val eqT::_ = binder_types cT |
537 val eqT::_ = binder_types cT |
538 in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
538 in if Sign.typ_instance (Proof_Context.theory_of ctxt) (T,eqT) then SOME(thm,va,vb,P) |
539 else find thms |
539 else find thms |
540 end |
540 end |
541 | find [] = NONE |
541 | find [] = NONE |
542 in find subst_thms end; |
542 in find subst_thms end; |
543 |
543 |
544 fun mk_cong sg (f,aTs,rT) (refl,eq) = |
544 fun mk_cong ctxt (f,aTs,rT) (refl,eq) = |
545 let val k = length aTs; |
545 let val k = length aTs; |
546 fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = |
546 fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = |
547 let val ca = Thm.global_cterm_of sg va |
547 let val ca = Thm.cterm_of ctxt va |
548 and cx = Thm.global_cterm_of sg (eta_Var(("X"^si,0),T)) |
548 and cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T)) |
549 val cb = Thm.global_cterm_of sg vb |
549 val cb = Thm.cterm_of ctxt vb |
550 and cy = Thm.global_cterm_of sg (eta_Var(("Y"^si,0),T)) |
550 and cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T)) |
551 val cP = Thm.global_cterm_of sg P |
551 val cP = Thm.cterm_of ctxt P |
552 and cp = Thm.global_cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) |
552 and cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs)) |
553 in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; |
553 in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; |
554 fun mk(c,T::Ts,i,yik) = |
554 fun mk(c,T::Ts,i,yik) = |
555 let val si = radixstring(26,"a",i) |
555 let val si = radixstring(26,"a",i) |
556 in case find_subst sg T of |
556 in case find_subst ctxt T of |
557 NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) |
557 NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) |
558 | SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) |
558 | SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) |
559 in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end |
559 in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end |
560 end |
560 end |
561 | mk(c,[],_,_) = c; |
561 | mk(c,[],_,_) = c; |
562 in mk(refl,rev aTs,k-1,[]) end; |
562 in mk(refl,rev aTs,k-1,[]) end; |
563 |
563 |
564 fun mk_cong_type sg (f,T) = |
564 fun mk_cong_type ctxt (f,T) = |
565 let val (aTs,rT) = strip_type T; |
565 let val (aTs,rT) = strip_type T; |
566 fun find_refl(r::rs) = |
566 fun find_refl(r::rs) = |
567 let val (Const(eq,eqT),_,_) = dest_red(Thm.concl_of r) |
567 let val (Const(eq,eqT),_,_) = dest_red(Thm.concl_of r) |
568 in if Sign.typ_instance sg (rT, hd(binder_types eqT)) |
568 in if Sign.typ_instance (Proof_Context.theory_of ctxt) (rT, hd(binder_types eqT)) |
569 then SOME(r,(eq,body_type eqT)) else find_refl rs |
569 then SOME(r,(eq,body_type eqT)) else find_refl rs |
570 end |
570 end |
571 | find_refl([]) = NONE; |
571 | find_refl([]) = NONE; |
572 in case find_refl refl_thms of |
572 in case find_refl refl_thms of |
573 NONE => [] | SOME(refl) => [mk_cong sg (f,aTs,rT) refl] |
573 NONE => [] | SOME(refl) => [mk_cong ctxt (f,aTs,rT) refl] |
574 end; |
574 end; |
575 |
575 |
576 fun mk_cong_thy thy f = |
576 fun mk_congs' ctxt f = |
577 let val T = case Sign.const_type thy f of |
577 let val T = case Sign.const_type (Proof_Context.theory_of ctxt) f of |
578 NONE => error(f^" not declared") | SOME(T) => T; |
578 NONE => error(f^" not declared") | SOME(T) => T; |
579 val T' = Logic.incr_tvar 9 T; |
579 val T' = Logic.incr_tvar 9 T; |
580 in mk_cong_type thy (Const(f,T'),T') end; |
580 in mk_cong_type ctxt (Const(f,T'),T') end; |
581 |
581 |
582 fun mk_congs thy = maps (mk_cong_thy thy); |
582 val mk_congs = maps o mk_congs'; |
583 |
583 |
584 fun mk_typed_congs thy = |
584 fun mk_typed_congs ctxt = |
585 let |
585 let |
586 fun readfT(f,s) = |
586 fun readfT(f,s) = |
587 let |
587 let |
588 val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s); |
588 val T = Logic.incr_tvar 9 (Syntax.read_typ ctxt s); |
589 val t = case Sign.const_type thy f of |
589 val t = case Sign.const_type (Proof_Context.theory_of ctxt) f of |
590 SOME(_) => Const(f,T) | NONE => Free(f,T) |
590 SOME(_) => Const(f,T) | NONE => Free(f,T) |
591 in (t,T) end |
591 in (t,T) end |
592 in maps (mk_cong_type thy o readfT) end; |
592 in maps (mk_cong_type ctxt o readfT) end; |
593 |
593 |
594 end; |
594 end; |
595 end; |
595 end; |