24 val sign_of_cterm : cterm -> Sign.sg |
24 val sign_of_cterm : cterm -> Sign.sg |
25 val term_of : cterm -> term |
25 val term_of : cterm -> term |
26 val cterm_of : Sign.sg -> term -> cterm |
26 val cterm_of : Sign.sg -> term -> cterm |
27 val ctyp_of_term : cterm -> ctyp |
27 val ctyp_of_term : cterm -> ctyp |
28 val read_cterm : Sign.sg -> string * typ -> cterm |
28 val read_cterm : Sign.sg -> string * typ -> cterm |
29 val cterm_fun : (term -> term) -> (cterm -> cterm) |
|
30 val adjust_maxidx : cterm -> cterm |
29 val adjust_maxidx : cterm -> cterm |
31 val read_def_cterm : |
30 val read_def_cterm : |
32 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
31 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
33 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
32 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
34 val read_def_cterms : |
33 val read_def_cterms : |
84 val equal_intr : thm -> thm -> thm |
83 val equal_intr : thm -> thm -> thm |
85 val equal_elim : thm -> thm -> thm |
84 val equal_elim : thm -> thm -> thm |
86 val implies_intr_hyps : thm -> thm |
85 val implies_intr_hyps : thm -> thm |
87 val flexflex_rule : thm -> thm Seq.seq |
86 val flexflex_rule : thm -> thm Seq.seq |
88 val instantiate : |
87 val instantiate : |
89 (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm |
88 (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
90 val trivial : cterm -> thm |
89 val trivial : cterm -> thm |
91 val class_triv : Sign.sg -> class -> thm |
90 val class_triv : Sign.sg -> class -> thm |
92 val varifyT : thm -> thm |
91 val varifyT : thm -> thm |
93 val varifyT' : string list -> thm -> thm * (string * indexname) list |
92 val varifyT' : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list |
94 val freezeT : thm -> thm |
93 val freezeT : thm -> thm |
95 val dest_state : thm * int -> |
94 val dest_state : thm * int -> |
96 (term * term) list * term list * term * term |
95 (term * term) list * term list * term * term |
97 val lift_rule : (thm * int) -> thm -> thm |
96 val lift_rule : (thm * int) -> thm -> thm |
98 val incr_indexes : int -> thm -> thm |
97 val incr_indexes : int -> thm -> thm |
127 val name_of_thm : thm -> string |
126 val name_of_thm : thm -> string |
128 val tags_of_thm : thm -> tag list |
127 val tags_of_thm : thm -> tag list |
129 val name_thm : string * thm -> thm |
128 val name_thm : string * thm -> thm |
130 val rename_boundvars : term -> term -> thm -> thm |
129 val rename_boundvars : term -> term -> thm -> thm |
131 val cterm_match : cterm * cterm -> |
130 val cterm_match : cterm * cterm -> |
132 (indexname * ctyp) list * (cterm * cterm) list |
131 (ctyp * ctyp) list * (cterm * cterm) list |
133 val cterm_first_order_match : cterm * cterm -> |
132 val cterm_first_order_match : cterm * cterm -> |
134 (indexname * ctyp) list * (cterm * cterm) list |
133 (ctyp * ctyp) list * (cterm * cterm) list |
135 val cterm_incr_indexes : int -> cterm -> cterm |
134 val cterm_incr_indexes : int -> cterm -> cterm |
136 val terms_of_tpairs : (term * term) list -> term list |
135 val terms_of_tpairs : (term * term) list -> term list |
137 end; |
136 end; |
138 |
137 |
139 structure Thm: THM = |
138 structure Thm: THM = |
184 (*create a cterm by checking a "raw" term with respect to a signature*) |
183 (*create a cterm by checking a "raw" term with respect to a signature*) |
185 fun cterm_of sign tm = |
184 fun cterm_of sign tm = |
186 let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm |
185 let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm |
187 in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx} |
186 in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx} |
188 end; |
187 end; |
189 |
|
190 fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t); |
|
191 |
188 |
192 |
189 |
193 exception CTERM of string; |
190 exception CTERM of string; |
194 |
191 |
195 (*Destruct application in cterms*) |
192 (*Destruct application in cterms*) |
219 |
216 |
220 (*Form cterm out of a function and an argument*) |
217 (*Form cterm out of a function and an argument*) |
221 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) |
218 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) |
222 (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = |
219 (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = |
223 if T = dty then |
220 if T = dty then |
224 Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x) |
221 Cterm{t = f $ x, |
225 else f $ x, (*no new Vars: no expensive check!*) |
|
226 sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, |
222 sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, |
227 maxidx=Int.max(maxidx1, maxidx2)} |
223 maxidx=Int.max(maxidx1, maxidx2)} |
228 else raise CTERM "capply: types don't agree" |
224 else raise CTERM "capply: types don't agree" |
229 | capply _ _ = raise CTERM "capply: first arg is not a function" |
225 | capply _ _ = raise CTERM "capply: first arg is not a function" |
230 |
226 |
231 fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1}) |
227 fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1}) |
232 (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = |
228 (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = |
233 Cterm {t=Sign.nodup_vars (lambda t1 t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), |
229 Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2), |
234 T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)} |
230 T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)} |
235 handle TERM _ => raise CTERM "cabs: first arg is not a variable"; |
231 handle TERM _ => raise CTERM "cabs: first arg is not a variable"; |
236 |
232 |
237 (*Matching of cterms*) |
233 (*Matching of cterms*) |
238 fun gen_cterm_match mtch |
234 fun gen_cterm_match mtch |
241 let |
237 let |
242 val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2); |
238 val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2); |
243 val tsig = Sign.tsig_of (Sign.deref sign_ref); |
239 val tsig = Sign.tsig_of (Sign.deref sign_ref); |
244 val (Tinsts, tinsts) = mtch tsig (t1, t2); |
240 val (Tinsts, tinsts) = mtch tsig (t1, t2); |
245 val maxidx = Int.max (maxidx1, maxidx2); |
241 val maxidx = Int.max (maxidx1, maxidx2); |
246 val vars = map dest_Var (term_vars t1); |
242 fun mk_cTinsts (ixn, (S, T)) = |
247 fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T}); |
243 (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)}, |
248 fun mk_ctinsts (ixn, t) = |
244 Ctyp {sign_ref = sign_ref, T = T}); |
249 let val T = typ_subst_TVars Tinsts (valOf (assoc (vars, ixn))) |
245 fun mk_ctinsts (ixn, (T, t)) = |
|
246 let val T = Envir.typ_subst_TVars Tinsts T |
250 in |
247 in |
251 (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, |
248 (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, |
252 Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t}) |
249 Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t}) |
253 end; |
250 end; |
254 in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end; |
251 in (map mk_cTinsts (Vartab.dest Tinsts), |
|
252 map mk_ctinsts (Vartab.dest tinsts)) |
|
253 end; |
255 |
254 |
256 val cterm_match = gen_cterm_match Pattern.match; |
255 val cterm_match = gen_cterm_match Pattern.match; |
257 val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; |
256 val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; |
258 |
257 |
259 (*Incrementing indexes*) |
258 (*Incrementing indexes*) |
415 | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); |
414 | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); |
416 |
415 |
417 fun add_terms_sorts ([], Ss) = Ss |
416 fun add_terms_sorts ([], Ss) = Ss |
418 | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); |
417 | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); |
419 |
418 |
420 fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs); |
419 fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs); |
421 |
420 |
422 fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = |
421 fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = |
423 Vartab.foldl (add_term_sorts o swap o apsnd snd) |
422 Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd)) |
424 (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol); |
423 (Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol); |
425 |
424 |
426 fun add_insts_sorts ((iTs, is), Ss) = |
425 fun add_insts_sorts ((iTs, is), Ss) = |
427 add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); |
426 add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); |
428 |
427 |
429 fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) = |
428 fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) = |
544 |
543 |
545 |
544 |
546 |
545 |
547 (*** Meta rules ***) |
546 (*** Meta rules ***) |
548 |
547 |
549 (*Check that term does not contain same var with different typing/sorting. |
|
550 If this check must be made, recalculate maxidx in hope of preventing its |
|
551 recurrence.*) |
|
552 fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) s = |
|
553 let |
|
554 val prop' = attach_tpairs tpairs prop; |
|
555 val _ = Sign.nodup_vars prop' |
|
556 in Thm {sign_ref = sign_ref, |
|
557 der = der, |
|
558 maxidx = maxidx_of_term prop', |
|
559 shyps = shyps, |
|
560 hyps = hyps, |
|
561 tpairs = tpairs, |
|
562 prop = prop} |
|
563 end handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); |
|
564 |
|
565 |
|
566 (** 'primitive' rules **) |
548 (** 'primitive' rules **) |
567 |
549 |
568 (*discharge all assumptions t from ts*) |
550 (*discharge all assumptions t from ts*) |
569 val disch = gen_rem (op aconv); |
551 val disch = gen_rem (op aconv); |
570 |
552 |
667 let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct |
649 let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct |
668 in case prop of |
650 in case prop of |
669 Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => |
651 Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => |
670 if T<>qary then |
652 if T<>qary then |
671 raise THM("forall_elim: type mismatch", 0, [th]) |
653 raise THM("forall_elim: type mismatch", 0, [th]) |
672 else let val thm = fix_shyps [th] [] |
654 else fix_shyps [th] [] |
673 (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), |
655 (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), |
674 der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, |
656 der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, |
675 maxidx = Int.max(maxidx, maxt), |
657 maxidx = Int.max(maxidx, maxt), |
676 shyps = [], |
658 shyps = [], |
677 hyps = hyps, |
659 hyps = hyps, |
678 tpairs = tpairs, |
660 tpairs = tpairs, |
679 prop = betapply(A,t)}) |
661 prop = betapply(A,t)}) |
680 in if maxt >= 0 andalso maxidx >= 0 |
|
681 then nodup_vars thm "forall_elim" |
|
682 else thm (*no new Vars: no expensive check!*) |
|
683 end |
|
684 | _ => raise THM("forall_elim: not quantified", 0, [th]) |
662 | _ => raise THM("forall_elim: not quantified", 0, [th]) |
685 end |
663 end |
686 handle TERM _ => |
664 handle TERM _ => |
687 raise THM("forall_elim: incompatible signatures", 0, [th]); |
665 raise THM("forall_elim: incompatible signatures", 0, [th]); |
688 |
666 |
729 and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2; |
707 and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2; |
730 fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) |
708 fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) |
731 in case (prop1,prop2) of |
709 in case (prop1,prop2) of |
732 ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => |
710 ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => |
733 if not (u aconv u') then err"middle term" |
711 if not (u aconv u') then err"middle term" |
734 else let val thm = |
712 else |
735 Thm{sign_ref= merge_thm_sgs(th1,th2), |
713 Thm{sign_ref= merge_thm_sgs(th1,th2), |
736 der = Pt.infer_derivs (Pt.transitive u T) der1 der2, |
714 der = Pt.infer_derivs (Pt.transitive u T) der1 der2, |
737 maxidx = Int.max(max1,max2), |
715 maxidx = Int.max(max1,max2), |
738 shyps = Sorts.union_sort (shyps1, shyps2), |
716 shyps = Sorts.union_sort (shyps1, shyps2), |
739 hyps = union_term(hyps1,hyps2), |
717 hyps = union_term(hyps1,hyps2), |
740 tpairs = tpairs1 @ tpairs2, |
718 tpairs = tpairs1 @ tpairs2, |
741 prop = eq$t1$t2} |
719 prop = eq$t1$t2} |
742 in if max1 >= 0 andalso max2 >= 0 |
|
743 then nodup_vars thm "transitive" |
|
744 else thm (*no new Vars: no expensive check!*) |
|
745 end |
|
746 | _ => err"premises" |
720 | _ => err"premises" |
747 end; |
721 end; |
748 |
722 |
749 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] |
723 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] |
750 Fully beta-reduces the term if full=true |
724 Fully beta-reduces the term if full=true |
825 | _ => raise THM("combination: not function type", 0, |
799 | _ => raise THM("combination: not function type", 0, |
826 [th1,th2])) |
800 [th1,th2])) |
827 in case (prop1,prop2) of |
801 in case (prop1,prop2) of |
828 (Const ("==", Type ("fun", [fT, _])) $ f $ g, |
802 (Const ("==", Type ("fun", [fT, _])) $ f $ g, |
829 Const ("==", Type ("fun", [tT, _])) $ t $ u) => |
803 Const ("==", Type ("fun", [tT, _])) $ t $ u) => |
830 let val _ = chktypes fT tT |
804 (chktypes fT tT; |
831 val thm = (*no fix_shyps*) |
805 (*no fix_shyps*) |
832 Thm{sign_ref = merge_thm_sgs(th1,th2), |
806 Thm{sign_ref = merge_thm_sgs(th1,th2), |
833 der = Pt.infer_derivs |
807 der = Pt.infer_derivs |
834 (Pt.combination f g t u fT) der1 der2, |
808 (Pt.combination f g t u fT) der1 der2, |
835 maxidx = Int.max(max1,max2), |
809 maxidx = Int.max(max1,max2), |
836 shyps = Sorts.union_sort(shyps1,shyps2), |
810 shyps = Sorts.union_sort(shyps1,shyps2), |
837 hyps = union_term(hyps1,hyps2), |
811 hyps = union_term(hyps1,hyps2), |
838 tpairs = tpairs1 @ tpairs2, |
812 tpairs = tpairs1 @ tpairs2, |
839 prop = Logic.mk_equals(f$t, g$u)} |
813 prop = Logic.mk_equals(f$t, g$u)}) |
840 in if max1 >= 0 andalso max2 >= 0 |
|
841 then nodup_vars thm "combination" |
|
842 else thm (*no new Vars: no expensive check!*) |
|
843 end |
|
844 | _ => raise THM("combination: premises", 0, [th1,th2]) |
814 | _ => raise THM("combination: premises", 0, [th1,th2]) |
845 end; |
815 end; |
846 |
816 |
847 |
817 |
848 (* Equality introduction |
818 (* Equality introduction |
953 fun prt_typing sg_ref t T = |
923 fun prt_typing sg_ref t T = |
954 let val sg = Sign.deref sg_ref in |
924 let val sg = Sign.deref sg_ref in |
955 Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T] |
925 Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T] |
956 end; |
926 end; |
957 |
927 |
|
928 fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T; |
|
929 |
958 (*For instantiate: process pair of cterms, merge theories*) |
930 (*For instantiate: process pair of cterms, merge theories*) |
959 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = |
931 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = |
960 let |
932 let |
961 val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct |
933 val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct |
962 and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu; |
934 and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu; |
966 else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", |
938 else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", |
967 Pretty.fbrk, prt_typing sign_ref_merged t T, |
939 Pretty.fbrk, prt_typing sign_ref_merged t T, |
968 Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u]) |
940 Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u]) |
969 end; |
941 end; |
970 |
942 |
971 fun add_ctyp ((v,ctyp), (sign_ref',vTs)) = |
943 fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT}, |
972 let val Ctyp {T,sign_ref} = ctyp |
944 Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) = |
973 in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end; |
945 let |
|
946 val sign_ref_merged = Sign.merge_refs |
|
947 (sign_ref, Sign.merge_refs (sign_refT, sign_refU)); |
|
948 val sign = Sign.deref sign_ref_merged |
|
949 in |
|
950 if Type.of_sort (Sign.tsig_of sign) (U, S) then |
|
951 (sign_ref_merged, (T, U) :: vTs) |
|
952 else raise TYPE ("Type not of sort " ^ |
|
953 Sign.string_of_sort sign S, [U], []) |
|
954 end |
|
955 | add_ctyp ((Ctyp {T, sign_ref}, _), _) = |
|
956 raise TYPE (Pretty.string_of (Pretty.block |
|
957 [Pretty.str "instantiate: not a type variable", |
|
958 Pretty.fbrk, prt_type sign_ref T]), [T], []); |
974 |
959 |
975 in |
960 in |
976 |
961 |
977 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
962 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
978 Instantiates distinct Vars by terms of same type. |
963 Instantiates distinct Vars by terms of same type. |
980 fun instantiate ([], []) th = th |
965 fun instantiate ([], []) th = th |
981 | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = |
966 | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = |
982 let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs; |
967 let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs; |
983 val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs; |
968 val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs; |
984 fun subst t = |
969 fun subst t = |
985 subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t); |
970 subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); |
986 val newprop = subst prop; |
971 val newprop = subst prop; |
987 val newdpairs = map (pairself subst) dpairs; |
972 val newdpairs = map (pairself subst) dpairs; |
988 val newth = |
973 val newth = |
989 (Thm{sign_ref = newsign_ref, |
974 (Thm{sign_ref = newsign_ref, |
990 der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, |
975 der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, |
996 prop = newprop}) |
981 prop = newprop}) |
997 in if not(instl_ok(map #1 tpairs)) |
982 in if not(instl_ok(map #1 tpairs)) |
998 then raise THM("instantiate: variables not distinct", 0, [th]) |
983 then raise THM("instantiate: variables not distinct", 0, [th]) |
999 else if not(null(findrep(map #1 vTs))) |
984 else if not(null(findrep(map #1 vTs))) |
1000 then raise THM("instantiate: type variables not distinct", 0, [th]) |
985 then raise THM("instantiate: type variables not distinct", 0, [th]) |
1001 else nodup_vars newth "instantiate" |
986 else newth |
1002 end |
987 end |
1003 handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) |
988 handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) |
1004 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
989 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
1005 |
990 |
1006 end; |
991 end; |
1041 |
1026 |
1042 |
1027 |
1043 (* Replace all TFrees not fixed or in the hyps by new TVars *) |
1028 (* Replace all TFrees not fixed or in the hyps by new TVars *) |
1044 fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1029 fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1045 let |
1030 let |
1046 val tfrees = foldr add_term_tfree_names fixed hyps; |
1031 val tfrees = foldr add_term_tfrees fixed hyps; |
1047 val prop1 = attach_tpairs tpairs prop; |
1032 val prop1 = attach_tpairs tpairs prop; |
1048 val (prop2, al) = Type.varify (prop1, tfrees); |
1033 val (prop2, al) = Type.varify (prop1, tfrees); |
1049 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1034 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1050 in let val thm = (*no fix_shyps*) |
1035 in (*no fix_shyps*) |
1051 Thm{sign_ref = sign_ref, |
1036 (Thm{sign_ref = sign_ref, |
1052 der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, |
1037 der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, |
1053 maxidx = Int.max(0,maxidx), |
1038 maxidx = Int.max(0,maxidx), |
1054 shyps = shyps, |
1039 shyps = shyps, |
1055 hyps = hyps, |
1040 hyps = hyps, |
1056 tpairs = rev (map Logic.dest_equals ts), |
1041 tpairs = rev (map Logic.dest_equals ts), |
1057 prop = prop3} |
1042 prop = prop3}, al) |
1058 in (nodup_vars thm "varifyT", al) end |
|
1059 (* this nodup_vars check can be removed if thms are guaranteed not to contain |
|
1060 duplicate TVars with different sorts *) |
|
1061 end; |
1043 end; |
1062 |
1044 |
1063 val varifyT = #1 o varifyT' []; |
1045 val varifyT = #1 o varifyT' []; |
1064 |
1046 |
1065 (* Replace all TVars by new TFrees *) |
1047 (* Replace all TVars by new TFrees *) |
1322 |
1304 |
1323 (*Faster normalization: skip assumptions that were lifted over*) |
1305 (*Faster normalization: skip assumptions that were lifted over*) |
1324 fun norm_term_skip env 0 t = Envir.norm_term env t |
1306 fun norm_term_skip env 0 t = Envir.norm_term env t |
1325 | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = |
1307 | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = |
1326 let val Envir.Envir{iTs, ...} = env |
1308 let val Envir.Envir{iTs, ...} = env |
1327 val T' = typ_subst_TVars_Vartab iTs T |
1309 val T' = Envir.typ_subst_TVars iTs T |
1328 (*Must instantiate types of parameters because they are flattened; |
1310 (*Must instantiate types of parameters because they are flattened; |
1329 this could be a NEW parameter*) |
1311 this could be a NEW parameter*) |
1330 in all T' $ Abs(a, T', norm_term_skip env n t) end |
1312 in all T' $ Abs(a, T', norm_term_skip env n t) end |
1331 | norm_term_skip env n (Const("==>", _) $ A $ B) = |
1313 | norm_term_skip env n (Const("==>", _) $ A $ B) = |
1332 implies $ A $ norm_term_skip env (n-1) B |
1314 implies $ A $ norm_term_skip env (n-1) B |