Could someone please help me get the following to work?
parse_as_infix("cross2",(20,"right"));;
needs "/Users/beeson/Dropbox/Provers/HOL-Light/Multivariate/vectors.ml";;
(* Properties of scalar cross product *)
let cross2 = new_definition
` x cross2 y = x$1* y$2 - x$2 *y$1`;;
let crossanticommutative = prove(
`!a b. --( b cross2 a) = a cross2 b `,
(REPEAT GEN_TAC)THEN
REWRITE_TAC[cross2;VECTOR_MUL_COMPONENT] THEN
(CONV_TAC REAL_RING)
);; # This works fine.
SPEC `A` crossanticommutative;; # doesn't work, Exception: Failure "SPEC".
ISPEC `A` crossanticommutative;; # doesn't work, Exception: Failure "ISPEC
can't type-instantiate input theorem".
SPEC `A:R^N` crossanticommutative;; #doesn't work, also not with ISPEC.
I believe the types of a and b in crossanticommutative are
real^N, where N is a system-generated type variable, but maybe not, in
view of the failure message for ISPEC.
since
------------------------------------------------------------------------------
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
