On 18/03/10 01:49, [email protected] wrote:
> 2 Unfortunately, I could not understand the information HOL gives by
> using term_grammar(); as your suggestion. It gives me the message as
> following:
> Overloading:
> < -> real_lt <
> [...]
> count -> extra_pred_set$count pred_set$count
> flr -> NUM_FLOOR
> inf -> prob_extra$inf extra_real$inf real$inf
> inv -> realax$inv relation$inv
> measure -> measure$measure prim_rec$measure
> min -> extra_num$min real$min
> sum -> extra_list$sum real$sum
> ~ -> poly_neg real_neg ~ : grammar
> Could you tell me how to understand this?
Each line is of the form
<symbol> -> <constant> <constant> ... <constant>
This indicates that the <symbol> can resolve to each of the given
constants.
The line for count shows you that count is overloaded to two different
constants called count, one in pred_setTheory, and another in
extra_pred_setTheory. The theorem you are using will be expecting one
of these constants, but the goal you are attempting to prove will be
using the other.
You can probably see this by doing the following:
remove_ovl_mapping "count" {Thy="extra_pred", Name = "count"}
This will adjust the pretty-printing by removing the count from
extra_pred from the grammar.
Then try looking at the goal term and the theorem. I predict that one
will print as extra_pred$count, and the other won't (it will be the
one from pred_set).
The fact that the overloading in this case has two constants whose
semantics is exactly the same means that the overloading is just a
source of confusion rather than convenience.
I suggest you delete the section of
examples/miller/formalize/extra_predScript.sml that is about the count
constant, and try rebuilding.
I will fix the example in the repository. It also has a redundant
BIGINTER constant that I will also delete.
Michael
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
