Hello,
I really appreciate somebody who can help me to solve this problem on
using MATCH_MP_TAC to prove my subgoal:
BIGINTER (IMAGE (\k. {s | FST (f k s) = (x l) k}) (count (SUC n))) IN
events bern
------------------------------------------------------------
the types of all the variables here are shown as following:
BIGINTER
(IMAGE
(\(k :num).
{(s :num -> bool) |
FST ((f :num -> (num -> bool) -> 'b # (num -> bool)) k s) =
(x :num -> num -> 'b) (l :num) k}) (count (SUC (n :num)))) IN
events bern
------------------------------------------------------------
I know there is a theorem in "probability" named
"EVENTS_COUNTABLE_INTER" can be used here.
------------------------------------------------------------
- EVENTS_COUNTABLE_INTER;
> val it =
|- !(p :(('a -> bool) -> bool) # (('a -> bool) -> real))
(c :('a -> bool) -> bool).
prob_space p /\ c SUBSET events p /\ countable c ==>
BIGINTER c IN events p : thm
------------------------------------------------------------
And I had applied it in some proof successfully before. But in this
case, when I tried to use "e(MATCH_MP_TAC EVENTS_COUNTABLE_INTER);" to
prove this subgoal, HOL gives me the message as this:
------------------------------------------------------------
- e(MATCH_MP_TAC EVENTS_COUNTABLE_INTER);
OK..
Exception raised at Tactic.MATCH_MP_TAC:
No match
! Uncaught exception:
! HOL_ERR
------------------------------------------------------------
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
------------------------------------------------------------
Regards,
Liya
------------------------------------------------------------------------------
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
