Hi, Tarek, Thanks for your suggestion! And you are right. The one that you told me its definition is exact what I'm working with.
Unfortunately, after I followed your suggestion, it can not solve this MATCH_MP_TAC problem, although you gave me some new information here. Best Wishes, Liya Quoting Tarek Mhamdi <[email protected]>: > Hi Liya, > > Try to work with this instead > IMAGE (\k. {s | FST (f k s) = (x l) k}) (pred_set$count (SUC n)) > That's the definition of count you are working with > pred_setTheory.count_def: |- !n. count n = {m | m < n} : thm > > -- > Tarek > -------------------------------------------------- > From: <[email protected]> > Sent: Wednesday, March 17, 2010 10:49 AM > To: "Michael Norrish" <[email protected]> > Cc: <[email protected]> > Subject: Re: [Hol-info] A problem on using MATCH_MP_TAC > >> Dear Dr. Michael Norrish, >> >> Thank you for your reply! >> >> 1 I found that if I start a new task and run hol in the new term >> window there, then paste the code (in the file named >> property1_change(xl)_proved.sml as following), it will run smoothly >> without any problem. >> >> However, if I use: >> loadPath := "/home/l/liy_liu/HOL_2" :: !loadPath; >> use "property1_change(xl)_proved.sml"; >> >> and try to run the code this way. Then it is stoped and showed me: >> Exception raised at Tactic.MATCH_MP_TAC: >> No match >> ! Uncaught exception: >> ! HOL_ERR >> [closing file "/home/l/liy_liu/HOL_2/property1_change(xl)_proved.sml"] >> >> Could you tell me what the problem is? >> >> 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: >> ## -> poly$## pair$## >> & -> real_of_num >> () -> one >> * -> poly_mul real_mul * >> ** -> EXP >> + -> poly_add real_add + >> ++ -> APPEND ++ >> - -> real_sub - >> --> -> DFUNSET seq$--> quotient$--> >> < -> real_lt < >> <= -> real_lte <= >> > -> real_gt > >> >= -> real_ge >= >> ALL_EL -> EVERY >> BIGINTER -> extra_pred_set$BIGINTER pred_set$BIGINTER >> BUTLAST -> FRONT >> COMPL -> prob_extra$COMPL pred_set$COMPL >> IS_EL -> MEM >> Id -> = >> REMPTY -> EMPTY_REL >> SIGMA -> SUM_IMAGE >> SOME_EL -> EXISTS >> _ inject_number -> real_of_num nat_elim__magic >> case -> >> list_case option_case one_case sum_case pair_case bool_case num_case >> itself_case literal_case >> case_arrow__magic -> tends_real_real FUNSET case_arrow__magic >> clg -> NUM_CEILING >> 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? >> >> Best Wishes, >> Liya >> >> Quoting Michael Norrish <[email protected]>: >> >>> On 13/03/10 03:14, [email protected] wrote: >>>> ------------------------------------------------------------ >>>> Even I checked the type of "IMAGE (\k. {s | FST (f k s) = (x l) k}) >>>> (count (SUC n))", it shows that it is exact the type of "c" in thereom >>>> EVENTS_COUNTABLE_INTER. More else, I failed to solve this problem by >>>> using "Q.ABBREV_TAC" to make this "IMAGE (\k. {s | FST (f k s) = (x l) >>>> k}) (count (SUC n))" simple. >>>> ------------------------------------------------------------ >>>> - type_of ``IMAGE (\k. {s | FST (f k s) = (x l) k}) (count (SUC n))``; >>>> <<HOL message: more than one resolution of overloading was possible>> >>>> <<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd>> >>>>> val it = ``:('a -> bool) -> bool`` : hol_type >>>> ------------------------------------------------------------ >>> >>> I'd be suspicious of this message. Why are there multiple >>> overloading resolutions possible in the term you give? >>> >>> If you do term_grammar(), what do you see in the overloading section >>> for the strings "count", "SUC", "IMAGE" and "FST"? In particular, >>> does each map to just one constant, and does each map to the >>> constant you expect. >>> >>> Also, are you using the examples/miller probability theory, or the >>> one under src? >>> >>> 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 >>> >> >> >> >> >> ------------------------------------------------------------------------------ >> 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 ------------------------------------------------------------------------------ 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
