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
