679 der = infer_derivs (Forall_elim ct, [der]), |
679 der = infer_derivs (Forall_elim ct, [der]), |
680 maxidx = max[maxidx, maxt], |
680 maxidx = max[maxidx, maxt], |
681 shyps = [], |
681 shyps = [], |
682 hyps = hyps, |
682 hyps = hyps, |
683 prop = betapply(A,t)}) |
683 prop = betapply(A,t)}) |
684 in nodup_Vars thm "forall_elim"; thm end |
684 in if maxt >= 0 andalso maxidx >= 0 |
|
685 then nodup_Vars thm "forall_elim" |
|
686 else () (*no new Vars: no expensive check!*) ; |
|
687 thm |
|
688 end |
685 | _ => raise THM("forall_elim: not quantified", 0, [th]) |
689 | _ => raise THM("forall_elim: not quantified", 0, [th]) |
686 end |
690 end |
687 handle TERM _ => |
691 handle TERM _ => |
688 raise THM("forall_elim: incompatible signatures", 0, [th]); |
692 raise THM("forall_elim: incompatible signatures", 0, [th]); |
689 |
693 |
747 der = infer_derivs (Transitive, [der1, der2]), |
751 der = infer_derivs (Transitive, [der1, der2]), |
748 maxidx = max[max1,max2], |
752 maxidx = max[max1,max2], |
749 shyps = [], |
753 shyps = [], |
750 hyps = hyps1 union hyps2, |
754 hyps = hyps1 union hyps2, |
751 prop = eq$t1$t2}) |
755 prop = eq$t1$t2}) |
752 in nodup_Vars thm "transitive"; thm end |
756 in if max1 >= 0 andalso max2 >= 0 |
|
757 then nodup_Vars thm "transitive" |
|
758 else () (*no new Vars: no expensive check!*) ; |
|
759 thm |
|
760 end |
753 | _ => err"premises" |
761 | _ => err"premises" |
754 end; |
762 end; |
755 |
763 |
756 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) |
764 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) |
757 fun beta_conversion ct = |
765 fun beta_conversion ct = |
849 der = infer_derivs (Combination, [der1, der2]), |
857 der = infer_derivs (Combination, [der1, der2]), |
850 maxidx = max[max1,max2], |
858 maxidx = max[max1,max2], |
851 shyps = shyps1 union shyps2, |
859 shyps = shyps1 union shyps2, |
852 hyps = hyps1 union hyps2, |
860 hyps = hyps1 union hyps2, |
853 prop = Logic.mk_equals(f$t, g$u)} |
861 prop = Logic.mk_equals(f$t, g$u)} |
854 in nodup_Vars thm "combination"; thm end |
862 in if max1 >= 0 andalso max2 >= 0 |
|
863 then nodup_Vars thm "combination" |
|
864 else () (*no new Vars: no expensive check!*) ; |
|
865 thm |
|
866 end |
855 | _ => raise THM("combination: premises", 0, [th1,th2]) |
867 | _ => raise THM("combination: premises", 0, [th1,th2]) |
856 end; |
868 end; |
857 |
869 |
858 |
870 |
859 (* Equality introduction |
871 (* Equality introduction |