Dear Dr. Michael Norrish, Thank you so much! I have learned a lot from your email.
And I tried the way to remove the overloaded constant count and the one left in the library list is exact what I expected. Unfortunately, I have to solve some problems that appear because some theorems in extra_pred_setTheory could not be recognized by HOL any more. I'm trying to find a way to solve this problem. Also, the previous problem related to MATCH_MP_TAC still exists. 1 I wonder if the theorems proved based on both of extra_pred_setTheory and pred_setTheory have any trouble (I mean the theorems were proved by loading and opening both of these two libraries, which include different definition on a constant, such as count). 2 Could we use them in our process of proving goal? 3 How to solve the problem related to MATCH_MP_TAC? Best Wishes, Liya Quoting Michael Norrish <[email protected]>: > 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
