Hello Michael,
I remember from my last time I used hol-light that the following code
from the flyspeck project was quite helpful:
(**
Add printers to HOL-Light to be able to print terms annotated with
their terms.
Snippet obtained from HOL-Light mailing list.
https://sourceforge.net/p/hol/mailman/message/35203735/
Code taken from the Flyspeck project.
**)
let print_varandtype fmt tm =
let hop,args = strip_comb tm in
let s = name_of hop
and ty = type_of hop in
if is_var hop & args = [] then
(pp_print_string fmt "(";
pp_print_string fmt s;
pp_print_string fmt ":";
pp_print_type fmt ty;
pp_print_string fmt ")")
else fail() ;;
let show_types,hide_types =
(fun () -> install_user_printer ("Show Types",print_varandtype)),
(fun () -> try delete_user_printer "Show Types"
with Failure _ -> failwith ("hide_types: "^
"Types are already
hidden."));;
Running it with your example, I get the following output for your theorem:
val crossanticommutative : thm =
|- !(a:real^?219759) (b:real^?219758).
--((b:real^?219758) cross2 (a:real^?219759)) =
(a:real^?219759) cross2 (b:real^?219758)
Consequently
ISPEC `A:real^N` crossanticommutative
works:
val it : thm =
|- !(b:real^?219758). --((b:real^?219758) cross2 (A:real^N)) =
(A:real^N) cross2 (b:real^?219758)
I hope my answer is helpful, please ask for clarifications if necessary.
Best regards,
Heiko
On 01/05/2018 06:11 AM, Michael Beeson wrote:
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
<http://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
------------------------------------------------------------------------------
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
