Falling script can be run after loading vectors.ml
# let lemma300 = VECTOR_ARITH `!x:real^2 y:real^2 z:real^2. (x + y = z)
<=> (y = z-x)`;;
val lemma300 : thm = |- !x y z. x + y = z <=> y = z - x
# let test = ASSUME `!a:real^2 b:real^2 c:real^2 d:real^2 . tarea(d,a,b) +
tarea(c,a,d) = tarea(a,b,c)`;;
val test : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
|- !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
# REWRITE_RULE[lemma300] test;;
val it : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
|- !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
#
I was expecting
tarea(c,a,d) = tarea(a,b,c)-tarea(d,a,b) in the conclusion
(and maybe in the assumptions too). Note that no type variables
are involved, so whatever the problem is here, it has nothing to do
with type variables.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
