diff -r 348ce23d2fc2 -r a63605582573 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Apr 21 19:02:54 2005 +0200 +++ b/src/Pure/thm.ML Thu Apr 21 19:12:03 2005 +0200 @@ -26,7 +26,6 @@ val cterm_of : Sign.sg -> term -> cterm val ctyp_of_term : cterm -> ctyp val read_cterm : Sign.sg -> string * typ -> cterm - val cterm_fun : (term -> term) -> (cterm -> cterm) val adjust_maxidx : cterm -> cterm val read_def_cterm : Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> @@ -86,11 +85,11 @@ val implies_intr_hyps : thm -> thm val flexflex_rule : thm -> thm Seq.seq val instantiate : - (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm + (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm val trivial : cterm -> thm val class_triv : Sign.sg -> class -> thm val varifyT : thm -> thm - val varifyT' : string list -> thm -> thm * (string * indexname) list + val varifyT' : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list val freezeT : thm -> thm val dest_state : thm * int -> (term * term) list * term list * term * term @@ -129,9 +128,9 @@ val name_thm : string * thm -> thm val rename_boundvars : term -> term -> thm -> thm val cterm_match : cterm * cterm -> - (indexname * ctyp) list * (cterm * cterm) list + (ctyp * ctyp) list * (cterm * cterm) list val cterm_first_order_match : cterm * cterm -> - (indexname * ctyp) list * (cterm * cterm) list + (ctyp * ctyp) list * (cterm * cterm) list val cterm_incr_indexes : int -> cterm -> cterm val terms_of_tpairs : (term * term) list -> term list end; @@ -187,8 +186,6 @@ in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx} end; -fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t); - exception CTERM of string; @@ -221,8 +218,7 @@ fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = if T = dty then - Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x) - else f $ x, (*no new Vars: no expensive check!*) + Cterm{t = f $ x, sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, maxidx=Int.max(maxidx1, maxidx2)} else raise CTERM "capply: types don't agree" @@ -230,7 +226,7 @@ fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1}) (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = - Cterm {t=Sign.nodup_vars (lambda t1 t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), + Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2), T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)} handle TERM _ => raise CTERM "cabs: first arg is not a variable"; @@ -243,15 +239,18 @@ val tsig = Sign.tsig_of (Sign.deref sign_ref); val (Tinsts, tinsts) = mtch tsig (t1, t2); val maxidx = Int.max (maxidx1, maxidx2); - val vars = map dest_Var (term_vars t1); - fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T}); - fun mk_ctinsts (ixn, t) = - let val T = typ_subst_TVars Tinsts (valOf (assoc (vars, ixn))) + fun mk_cTinsts (ixn, (S, T)) = + (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)}, + Ctyp {sign_ref = sign_ref, T = T}); + fun mk_ctinsts (ixn, (T, t)) = + let val T = Envir.typ_subst_TVars Tinsts T in (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t}) end; - in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end; + in (map mk_cTinsts (Vartab.dest Tinsts), + map mk_ctinsts (Vartab.dest tinsts)) + end; val cterm_match = gen_cterm_match Pattern.match; val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; @@ -417,11 +416,11 @@ fun add_terms_sorts ([], Ss) = Ss | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); -fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs); +fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs); fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = - Vartab.foldl (add_term_sorts o swap o apsnd snd) - (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol); + Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd)) + (Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol); fun add_insts_sorts ((iTs, is), Ss) = add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); @@ -546,23 +545,6 @@ (*** Meta rules ***) -(*Check that term does not contain same var with different typing/sorting. - If this check must be made, recalculate maxidx in hope of preventing its - recurrence.*) -fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) s = - let - val prop' = attach_tpairs tpairs prop; - val _ = Sign.nodup_vars prop' - in Thm {sign_ref = sign_ref, - der = der, - maxidx = maxidx_of_term prop', - shyps = shyps, - hyps = hyps, - tpairs = tpairs, - prop = prop} - end handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); - - (** 'primitive' rules **) (*discharge all assumptions t from ts*) @@ -669,7 +651,7 @@ Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => if T<>qary then raise THM("forall_elim: type mismatch", 0, [th]) - else let val thm = fix_shyps [th] [] + else fix_shyps [th] [] (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, maxidx = Int.max(maxidx, maxt), @@ -677,10 +659,6 @@ hyps = hyps, tpairs = tpairs, prop = betapply(A,t)}) - in if maxt >= 0 andalso maxidx >= 0 - then nodup_vars thm "forall_elim" - else thm (*no new Vars: no expensive check!*) - end | _ => raise THM("forall_elim: not quantified", 0, [th]) end handle TERM _ => @@ -731,7 +709,7 @@ in case (prop1,prop2) of ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => if not (u aconv u') then err"middle term" - else let val thm = + else Thm{sign_ref= merge_thm_sgs(th1,th2), der = Pt.infer_derivs (Pt.transitive u T) der1 der2, maxidx = Int.max(max1,max2), @@ -739,10 +717,6 @@ hyps = union_term(hyps1,hyps2), tpairs = tpairs1 @ tpairs2, prop = eq$t1$t2} - in if max1 >= 0 andalso max2 >= 0 - then nodup_vars thm "transitive" - else thm (*no new Vars: no expensive check!*) - end | _ => err"premises" end; @@ -827,8 +801,8 @@ in case (prop1,prop2) of (Const ("==", Type ("fun", [fT, _])) $ f $ g, Const ("==", Type ("fun", [tT, _])) $ t $ u) => - let val _ = chktypes fT tT - val thm = (*no fix_shyps*) + (chktypes fT tT; + (*no fix_shyps*) Thm{sign_ref = merge_thm_sgs(th1,th2), der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2, @@ -836,11 +810,7 @@ shyps = Sorts.union_sort(shyps1,shyps2), hyps = union_term(hyps1,hyps2), tpairs = tpairs1 @ tpairs2, - prop = Logic.mk_equals(f$t, g$u)} - in if max1 >= 0 andalso max2 >= 0 - then nodup_vars thm "combination" - else thm (*no new Vars: no expensive check!*) - end + prop = Logic.mk_equals(f$t, g$u)}) | _ => raise THM("combination: premises", 0, [th1,th2]) end; @@ -955,6 +925,8 @@ Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T] end; +fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T; + (*For instantiate: process pair of cterms, merge theories*) fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = let @@ -968,9 +940,22 @@ Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u]) end; -fun add_ctyp ((v,ctyp), (sign_ref',vTs)) = - let val Ctyp {T,sign_ref} = ctyp - in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end; +fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT}, + Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) = + let + val sign_ref_merged = Sign.merge_refs + (sign_ref, Sign.merge_refs (sign_refT, sign_refU)); + val sign = Sign.deref sign_ref_merged + in + if Type.of_sort (Sign.tsig_of sign) (U, S) then + (sign_ref_merged, (T, U) :: vTs) + else raise TYPE ("Type not of sort " ^ + Sign.string_of_sort sign S, [U], []) + end + | add_ctyp ((Ctyp {T, sign_ref}, _), _) = + raise TYPE (Pretty.string_of (Pretty.block + [Pretty.str "instantiate: not a type variable", + Pretty.fbrk, prt_type sign_ref T]), [T], []); in @@ -982,7 +967,7 @@ let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs; val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs; fun subst t = - subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t); + subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); val newprop = subst prop; val newdpairs = map (pairself subst) dpairs; val newth = @@ -998,7 +983,7 @@ then raise THM("instantiate: variables not distinct", 0, [th]) else if not(null(findrep(map #1 vTs))) then raise THM("instantiate: type variables not distinct", 0, [th]) - else nodup_vars newth "instantiate" + else newth end handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) | TYPE (msg, _, _) => raise THM (msg, 0, [th]); @@ -1043,21 +1028,18 @@ (* Replace all TFrees not fixed or in the hyps by new TVars *) fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = let - val tfrees = foldr add_term_tfree_names fixed hyps; + val tfrees = foldr add_term_tfrees fixed hyps; val prop1 = attach_tpairs tpairs prop; val (prop2, al) = Type.varify (prop1, tfrees); val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) - in let val thm = (*no fix_shyps*) - Thm{sign_ref = sign_ref, + in (*no fix_shyps*) + (Thm{sign_ref = sign_ref, der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, maxidx = Int.max(0,maxidx), shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), - prop = prop3} - in (nodup_vars thm "varifyT", al) end -(* this nodup_vars check can be removed if thms are guaranteed not to contain -duplicate TVars with different sorts *) + prop = prop3}, al) end; val varifyT = #1 o varifyT' []; @@ -1324,7 +1306,7 @@ fun norm_term_skip env 0 t = Envir.norm_term env t | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = let val Envir.Envir{iTs, ...} = env - val T' = typ_subst_TVars_Vartab iTs T + val T' = Envir.typ_subst_TVars iTs T (*Must instantiate types of parameters because they are flattened; this could be a NEW parameter*) in all T' $ Abs(a, T', norm_term_skip env n t) end