[Hol-info] Uninterruptible PROVE_TAC []

[Chun Tian (binghe)]

Hi Michael,

with recent commits in HOL’s Git master, I found that I cannot easily interrupt 
the proof searching underly PROVE_TAC (or maybe also METIS_TAC). In another 
words, if I didn’t provide enough lemmas when calling PROVE_TAC [] and have 
caused the proof searching goes into infinite loops, I will *not* be able to 
interrupt HOL any more, by "Meta-H Ctrl-C” in Emacs, unless I do it early 
(still after calling PROVE_TAC but not that late somehow).   Then I have to 
kill HOL process in Emacs, then restart it, replay my proof scripts so far.

Do you have any clue on the root causes?(I also want to know if other HOL 
users met the same issues, by CC to hol-info mailing list)

Regards,

Chun



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] The "limit" of a ``:'num->'a set`` function?

[Chun Tian (binghe)]

Thanks, now I realized that, to have a meaningful “limit" on a sequence of 
sets, such a sequence must be either increasing or decreasing (f n SUBSET f 
(SUC n), or the other direction), then the “limit” is either BIGUNION (IMAGE f 
univ(:num)) or BIGINTER (IMAGE f univ(:num)).

—Chun

> Il giorno 14 set 2018, alle ore 04:53, michael.norr...@data61.csiro.au ha 
> scritto:
> 
> You don't just want something like
> 
>   BIGUNION (IMAGE f univ(:num))
> 
> ?
> 
> Michael
> 
> On 14/9/18, 05:02, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>I want to express the existence of a function (f :’num -> ‘a set) such 
> that, whenever the number n goes to “infinite”, ``f n`` equals to a given set 
> ``X :’a set``.
> 
>This looks like something in limTheory, but I have nothing to do with real 
> numbers here.
> 
>Does anyone know which definition in HOL4’s existing libraries should I 
> look for?
> 
>Regards,
> 
>Chun Tian
> 
> 
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info