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
