Added check for duplicate vars with distinct types/sorts (nodup_Vars)
authornipkow
Tue Feb 13 17:16:06 1996 +0100 (1996-02-13)
changeset 1495b8b54847c77f
parent 1494 22f67e796445
child 1496 c443b2adaf52
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Feb 13 14:13:23 1996 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Feb 13 17:16:06 1996 +0100
     1.3 @@ -615,6 +615,10 @@
     1.4  fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2];
     1.5  
     1.6  
     1.7 +(* check that term does not contain same var with different typing/sorting *)
     1.8 +fun nodup_Vars(thm as Thm{prop,...}) s =
     1.9 +  Sign.nodup_Vars prop handle TYPE(msg,_,_) => raise THM(s^": "^msg,0,[thm]);
    1.10 +
    1.11  
    1.12  (*** Meta rules ***)
    1.13  
    1.14 @@ -703,10 +707,11 @@
    1.15            Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
    1.16              if T<>qary then
    1.17                  raise THM("forall_elim: type mismatch", 0, [th])
    1.18 -            else fix_shyps [th] []
    1.19 -                 (Thm{sign= Sign.merge(sign,signt),
    1.20 -                     maxidx= max[maxidx, maxt],
    1.21 -                     shyps= [], hyps= hyps,  prop= betapply(A,t)})
    1.22 +            else let val thm = fix_shyps [th] []
    1.23 +                      (Thm{sign= Sign.merge(sign,signt),
    1.24 +                           maxidx= max[maxidx, maxt],
    1.25 +                           shyps= [], hyps= hyps,  prop= betapply(A,t)})
    1.26 +                 in nodup_Vars thm "forall_elim"; thm end
    1.27          | _ => raise THM("forall_elim: not quantified", 0, [th])
    1.28    end
    1.29    handle TERM _ =>
    1.30 @@ -827,12 +832,13 @@
    1.31  fun combination th1 th2 =
    1.32    let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1
    1.33        and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2
    1.34 -  in  case (prop1,prop2)  of
    1.35 +  in case (prop1,prop2)  of
    1.36         (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
    1.37 -              (*no fix_shyps*)
    1.38 -              Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2,
    1.39 -                  hyps= hyps1 union hyps2,
    1.40 -                  maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}
    1.41 +          let val thm = (*no fix_shyps*)
    1.42 +             Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2,
    1.43 +                 hyps= hyps1 union hyps2,
    1.44 +                 maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}
    1.45 +          in nodup_Vars thm "combination"; thm end
    1.46       | _ =>  raise THM("combination: premises", 0, [th1,th2])
    1.47    end;
    1.48  
    1.49 @@ -949,16 +955,8 @@
    1.50        then raise THM("instantiate: variables not distinct", 0, [th])
    1.51        else if not(null(findrep(map #1 vTs)))
    1.52        then raise THM("instantiate: type variables not distinct", 0, [th])
    1.53 -      else (*Check types of Vars for agreement*)
    1.54 -      case findrep (map (#1 o dest_Var) (term_vars newprop)) of
    1.55 -          ix::_ => raise THM("instantiate: conflicting types for variable " ^
    1.56 -                             Syntax.string_of_vname ix ^ "\n", 0, [newth])
    1.57 -        | [] =>
    1.58 -             case findrep (map #1 (term_tvars newprop)) of
    1.59 -             ix::_ => raise THM
    1.60 -                    ("instantiate: conflicting sorts for type variable " ^
    1.61 -                     Syntax.string_of_vname ix ^ "\n", 0, [newth])
    1.62 -        | [] => newth
    1.63 +      else nodup_Vars newth "instantiate";
    1.64 +      newth
    1.65    end
    1.66    handle TERM _ =>
    1.67             raise THM("instantiate: incompatible signatures",0,[th])