(* The `inv` you use in your axiom is not the one you think: *)
# type_of `inv`
val it : hol_type = `:real->real`
(* You'd better give your constant another name, like "elt_inv": *)
# new_constant("elt_inv",`:element->element`);;
val it : unit = ()
# let left_inv = new_axiom `!x . elt_inv(x) prod x = unit`;;
val left_inv : thm = |- !x. elt_inv x prod x = unit
(* You can still use "inv" by overloading it: *)
# make_overloadable "inv" `:A->A`;;
val it : unit = ()
# overload_interface("inv",`elt_inv:element->element`);;
val it : unit = ()
(* Then left_inv is displayed using "inv" instead of "elt_inv": *)
# left_inv;;
val it : thm = |- !x. inv x prod x = unit
(* You can also use `inv` for the input now: *)
# let left_inv = new_axiom `!x . inv(x) prod x = unit`;;
val it : thm = |- !x. inv x prod x = unit
(* And if you still plan to use the original `inv` for real numbers
you should also overload it: *)
# overload_interface("inv",`inv:real->real`);;
val it : unit = ()
--
Vincent Aravantinos
PostDoctoral fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
Le 14 mai 12 à 22:53, Bill Richter a écrit :
Trying to improve my group theory code, I tried to use new_axiom, and
I could not get this to work. Help!
(* this works fine *)
new_type("element",0);;
new_constant("prod",`:element->element->element`);;
new_constant("inv",`:element->element`);;
new_constant("unit",`:element`);;
parse_as_infix("prod",(20, "right"));;
let A1 = new_axiom
`!x y z. (x prod y) prod z = x prod (y prod z)`;;
let left_unit = new_axiom
`!x . unit prod x = x`;;
(* This does not: *)
let left_inv = new_axiom
`!x . inv(x) prod x = unit`;;
(* Exception: Failure "typechecking error (initial type
assignment)". *)
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond.
Discussions
will include endpoint security, mobile security and the latest in
malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
