Re: [Hol-info] hol-online not working

Is HOL light online just HOL Light, or something special in particular? The website for HOL Light can be found at https://www.cl.cam.ac.uk/~jrh13/hol-light/ and the source code is now on GitHub. On Fri, 15 Nov 2019 at 00:38, Miranda, Brando wrote: > Hi, > > Does anyone have a link to HOL light o

Re: [Hol-info] 0 / 0 = 0 ???

Very nice paper. Thanks Umair and Freek for the correction and link. On Wed, 20 Feb 2019 21:08 Umair Siddique > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101&rep=rep1&type=pdf > > http://www.gilith.com/talks/tphols2001-subtypes.pdf > > > - Umair > > On Wed, Feb 20, 2019 at 4:0

Re: [Hol-info] 0 / 0 = 0 ???

sely > reproduce those pure math proofs under the “same” formal system with math > books (except for the subtle differences between ZFC and HOL not affecting > the math theories that I’m working with.) > > —Chun > > Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar < > ramana.

Re: [Hol-info] 0 / 0 = 0 ???

I'd say one of the stronger ways to get "undefined" is to add an element to your type representing undefinedness, e.g., make it (/) : real option -> real option -> real option, where NONE represents "undefined". But then you will have a lot of bookkeeping to deal with... I don't suggest this seriou

Re: [Hol-info] (no subject)

Where is this code from? It looks like an exam question. On Thu, 20 Dec 2018 06:24 幻＠未来 <849678...@qq.com wrote: > > Here is the following code > datatype temp = > C of real > | F of real; > fun temp_to_f t = > case t of >C x => x * (9.0 / 5.0) + 32.

Re: [Hol-info] Choosing an element in an increasing sequence of sets

I think this is false. Here's a proof of the opposite, with the type of f instantiated to a num set generator: val thm = Q.prove( `¬( ∀(f:num->num->bool) a sp. (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ∧ (∀n. f n ⊆ sp) ∧ (BIGUNION (IMAGE f 𝕌(:num)) = sp) ∧ (a ⊆ sp) ⇒ ∃x. a ⊆ f x)`, rw[]

Re: [Hol-info] tacticoe

I would certainly be happy to see work-in-progress commits happen on a branch other than master. I would also be happy to answer any git-related questions or give tips on workflow. On Wed, 27 Jun 2018 at 10:58, Chun Tian (binghe) wrote: > The author (Thibault Gauthier) should learn how to correc

[Hol-info] big records

Dear HOL users, Does anyone know how to use the big record package? I always find I want to turn it off (by increasing the big record size to above the max number of fields in my types) because many things don't work on big records (in particular the simplifier and EVAL) whereas they do work on "s

Re: [Hol-info] Generated machine code of Poly/ML

You could build a binary using polyc. Would that suffice? Or do you need to see the machine code while running the REPL? On 17 May 2018 at 17:13, Mario Xerxes Castelán Castro < marioxcc...@yandex.com> wrote: > Hello. The Poly/ML mailing list appears to be down at the moment. How > can I see the m

Re: [Hol-info] "Gordon Computer"

It doesn't look too bad to me - happy to port them if you like. On 5 April 2018 at 12:36, Lawrence Paulson wrote: > I have just managed to locate Jeff Joyce's "Tamarack-2" files, which he > describes as slightly simplified compared with the original Gordon > computer. They are dated 1989 and the

Re: [Hol-info] Dependency on absolute paths remaining the same

Yes, to do that you need to use --relocbuild, since any executables (heaps) need to be rebuilt if the path changes. Steps: 1. Copy your HOL directory to the new location, omitting any files that match the patterns in tools-poly/rebuild-excludes.txt 2. Run poly --script tools/smart-configure.sml in

Re: [Hol-info] Uninstall HOL

Delete the directory in which you installed it. On 31 Jan 2018 06:01, "Jing Guo" wrote: > Hi, > > Several months ago I installed HOL and recently I want to uninstall it. > However, after some research I still could not find a way, nor it’s > included in the documentation. So I wondered that what

Re: [Hol-info] Share list of terms with later theories

Michael: I like the private_db idea. Jeremy: I believe many of the theorems and definitions created by the ind_type machinery are simply _deleted_ before the theory is exported, so they cannot be recovered afterwards. As long as deleted constants are not mentioned in exported theorems (but only in

[Hol-info] Data61 Seeking Research Scientist

One more open position at Data61, this one more suited for early-career academics/researchers. Data61 Seeking Research Scientist = We are looking for a full-time research scientist in formal verification to join us, the Trustworthy Systems group, at Data61, CSIRO.

[Hol-info] Data61 Seeking Proof Engineers

If you're looking for a job using HOL4, the following may be of interest :) Data61 Seeking Proof Engineers == If only there were a place where I could prove theorems for money, change the world, and have fun while doing it... Sounds too good to exist? In the Trustwor

Re: [Hol-info] Small question about sqrt

In your first goal, do either of these work? metis_tac[transcTheory.SQRT_0] rw[] \\ imp_res_tac transcTheory.SQRT_0 On 20 October 2017 at 23:42, Liu Gengyang <2015200...@mail.buct.edu.cn> wrote: > Hi, > > I want to prove the goal: !x. (sqrt x = 0) ==> (x = 0) as below, > > RW_TAC realLib.real_s

Re: [Hol-info] What's the recommended way to delete elements from list?

Oh whoops I misunderstood - it deletes all of them. Never mind. On 11 October 2017 at 22:38, Ramana Kumar wrote: > Just based on your final question, I suggest: > ?l1 l2. (DELETE_ELEMENT e L = l1 ++ l2) /\ (L = l1 ++ [e] ++ l2) > > On 11 October 2017 at 22:34, wrote: > >>

Re: [Hol-info] What's the recommended way to delete elements from list?

ENGTH_DELETE_ELEMENT_LE, but 3 months ago I > just couldn’t prove it! > > However, I still have one more question: how can I express the fact > that all elements in (DELETE_ELEMENT e L) are also elements of L, with > exactly the same order and number of appearances? In ano

Re: [Hol-info] Definitions of partial functions (incl. predicates)

My intuition says that working with total functions (and especially predicates) will be easier. Why? I don't know exactly, but here are some possible reasons: you can just use plain rewriting rather than conditional rewriting, and you don't need to state so many assumptions explicitly on your theor

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

I think it would be good to add this UNIQUE constant to listTheory, if you have time to make a pull request. On 6 October 2017 at 01:49, Chun Tian (binghe) wrote: > Let me close this question (further comments are welcome, of course). > > I actually got another good definition from Robert Beers

Re: [Hol-info] Changing thms used by computeLib

g to do with pointer equality. On 5 October 2017 at 16:15, Heiko Becker wrote: > Hello Ramana, > > yes, the Mk_comb error occurs non-deterministic. Is there a temporary > workaround for this, that I could make use of? > > Cheers, > > Heiko > > On 10/05/2017 12:43

Re: [Hol-info] Changing thms used by computeLib

Hi Heiko, Does it fail every time when you try to run the proofs non-interactively (with Holmake)? I suspect the "Mk_comb" error, if it is non-deterministic, has to do with pointer equality problems, which are in the middle of being fixed. Cheers, Ramana On 5 October 2017 at 13:22, Heiko Becker

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Perhaps it would make more sense to ask people who are using rich type systems what their motivations are :) (On this list it's probably mostly people who are satisfied with simple type theory.) On 15 September 2017 at 11:06, Mario Castelán Castro wrote: > Hello. > > I want ask for your experien

Re: [Hol-info] Is it possible to make Holmake print timing information?

One possible variation on your must_prove might be the following: qmatch_rename_tac {term quotation} >- {tactic} On 28 September 2017 at 18:28, Mario Castelán Castro wrote: > On 27/09/17 05:29, Chun Tian (binghe) wrote: > > Honestly speaking, I like those abbreviated “power” tactics, such that >

Re: [Hol-info] Is it possible to make Holmake print timing information?

In case it's not obvious, the place to make feature requests is here: https://github.com/HOL-Theorem-Prover/HOL/issues Implementation detail: I would guess you could get per-theorem timing by setting the "default prover" to one that does timing, similar to how the --fast option sets it to one that

Re: [Hol-info] Question on rewriting with assumptions

I just wanted to point out, in case you didn't know, that many tactics have lowercase synonyms so you don't have to write them out in all capital letters. For example pop_assum and rewrite_tac. There are also some cheatsheets around online for commonly used tactics, e.g., http://sange.fi/~magnus/c

Re: [Hol-info] How to find existing developments in HOL4?

I think a good approach is to ask the mailing list (as you have done), and to look around in the src and examples directories of the repository. On 11 September 2017 at 12:26, Chun Tian (binghe) wrote: > Well .. I didn’t reply to the mailing list because it contains some > insulting words to thi

Re: [Hol-info] Strange tactics bug when using match_mp_tac

I have a couple of comments/questions on irule: - I think mp_then is supposed to be better still. Am I right? (Or are they serving different purposes?) - I find it annoying that irule produces lots of new subgoals for the hypotheses. Is there a version that doesn't strip all the conjunctions, so

Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects

t itself include > infinite sums. > >>>> > >>>> Something like > >>>> > >>>> Datatype`CCS = … existing def … (* with or without finite/binary > sums *)` > >>>> > >>>> Datatype`bigCCS = SUM (num -&

Re: [Hol-info] On the use of new_axiom() in formal projects

Some very quick answers. Others will probably go into more detail. 1. If you use new_axiom, it becomes your responsibility to ensure that your axiom is consistent. If it is not consistent, the principle of explosion makes any subsequent formalisation vacuous. (If you don't use new_axiom, it can be

Re: [Hol-info] Vimhol key binding for showtypes

r mappings to whatever they want locally. On 10 July 2017 at 23:36, Robert Künnemann wrote: > > On 10/07, Ramana Kumar wrote: > >> A rather trivial thing: I'd like to change the default keybinding for >> showtypes in the Vim mode from "j" to "y". Why?

Re: [Hol-info] A question about ordinals

I have nothing to add here about the proof content, but I thought I'd mention that there are lowercase versions of many tactics which could be easier to type. For example, your proof could start like this: "rpt gen_tac >> mp_tac univ_ord_greater_cardinal". The other style thing I'd say is to prefer

[Hol-info] Vimhol key binding for showtypes

Hi list, A rather trivial thing: I'd like to change the default keybinding for showtypes in the Vim mode from "j" to "y". Why? Because "y" is the second letter of "types", so has some mnemonic value. (And all the other keys are mnemonics.) Whereas "j" has nothing to do with types as far as I can t

Re: [Hol-info] What's the recommended way to delete elements from list?

Sure, that's fine. I probably wouldn't even define such a constant but would instead use ``FILTER ((<>) x) ls`` in place. Stylistically it's usually better to use Define instead of new_definition, and to name defining theorems with a "_def" suffix. I'd also keep the name short like "DELETE" or eve

Re: [Hol-info] Difficulties in proving the termination of a recursive function

well-foundness any more) >>> >>> Current goal: >>> >>> size (CCS_Subst p (rec x p) x) < size (rec x p) ∨ >>> (size (CCS_Subst p (rec x p) x) = size (rec x p)) ∧ >>> CARD (J DELETE x) < CARD J >>>

Re: [Hol-info] Difficulties in proving the termination of a recursive function

Hi Chun, Your relation that works looks like a lexicographic relation, which is something wf_rel_tac should be able to handle automatically. Could you try providing it using the LEX combinator, e.g., wf_rel_tac`inv_image ($< LEX $<) (\x y. (size(FST x), CARD(SND y)))` Actually, looking more close

Re: [Hol-info] Changed order of qualified variables after SPEC_ALL and GEN_ALL

If you're working with a conversion (term -> thm), from which you produce your thm -> thm function via CONV_RULE, then I suggest looking at STRIP_QUANT_CONV. To avoid having to specify the types of variables explicitly, I suggest looking at Q.GEN and Q.SPEC (and Q.ISPEC). To deal with lists of var

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

(ind_type$FCONS a0 >> # (ind_type$FCONS a1 >> # (λn. ind_type$BOTTOM a0 a1) ∧ >> # 'Dertree' a0 ∧ '@temp @ind_typeTest0list' a1) ⇒ >> # '@temp @ind

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

tatype definition into smaller pieces ... > > Regards, > > Chun Tian > > > Il giorno 01 mag 2017, alle ore 07:42, Ramana Kumar < > ramana.ku...@cl.cam.ac.uk> ha scritto: > > > > I think it would help if you could find another "mini" theory that

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

e 3: > thm > 13076 > ref > … > Rule.alpha: not alpha-equivalent > > Full logs in zip is in attach. (the mail is re-sent with compressed > attachments) > > Regards, > > Chun Tian > > > > > > Il giorno 29 apr 2017, alle ore 15:21, Chun Tian (

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

quot; around line 37270: > trans > 5016 > def > while executing trans command: > terms not alpha-equivalent > > Regards, > > Chun Tian > > > Il giorno 25 apr 2017, alle ore 18:50, Chun Tian (binghe) < > binghe.l...@gmail.com> ha scritto: >

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

Hi Chun Tian, It's hard to know exactly what's wrong, but I expect there's a bug in the OpenTheory proof recording facility of HOL4, which is implemented in src/opentheory/postbool/Logging.sml. When you ask Holmake to generate an .ot.art file it first generates a raw .art file by recording all th

Re: [Hol-info] How to eliminate existential quantifier in a goal about list?

Better, in my opinion, is to use e( qexists_tac`0` ); which parses the quotation in the context of the goal, so you don't need to give an explicit type annotation. On 13 April 2017 at 14:11, Thomas Tuerk wrote: > Hi Liu, > > you have realLib open. "0" can be parsed as either a real or a num. >

Re: [Hol-info] A question about EL in listTheory.

Hi Liu, For any n, you can indeed get the nth element of x by using EL. What do you want to do with it? I can try to explain the behaviour you reported, in case it helps. val _= type_abbrev("numlist",``: num list``); val x = ``x: numlist``; val n_element = ``!n. EL n ^x``; This attempted term,

Re: [Hol-info] Problems building HOL from source

No that again looks like malformed products of an incomplete build. Try cleaning the relevant directory. (Or clean everything if you don't mind starting again.) On 3 April 2017 at 17:40, Lars Hupel wrote: > > As for avoiding the error above, you might like to try the fixes-5.6 > branch > > of Po

Re: [Hol-info] Problems building HOL from source

On 3 April 2017 at 13:50, Lars Hupel wrote: > Dear list, > > I've been trying to build a recent commit of HOL (4b08982). > > My environment is Arch Linux x64, Poly/ML 5.6. > > This is the output of "bin/build": > > > Building directory src/holyhammer/hh [03 Apr, 14:01:12] > hh_parse.ml / to

Re: [Hol-info] How to define PAT_X_ASSUM to PAT_ASSUM in K11 final release (and before) and do nothing in K12 (and later version)?

t; - > > val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else > PAT_X_ASSUM; > poly: : error: Value or constructor (PAT_X_ASSUM) has not been declared > Found near if Globals.version < 12 then PAT_ASSUM el

Re: [Hol-info] How to define PAT_X_ASSUM to PAT_ASSUM in K11 final release (and before) and do nothing in K12 (and later version)?

One thing you could try is to use Globals.version, e.g., val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM; On 25 March 2017 at 07:32, Chun Tian (binghe) wrote: > Hi, > > Currently I’m doing several projects in HOL4, and fortunately > Kananaskis-11 was finally released ea

Re: [Hol-info] How to transform an assumption without touching the goal?

How about this? first_x_assum(strip_assume_tac o MATCH_MP th) On 21 January 2017 at 06:39, Chun Tian (binghe) wrote: > Hi, > > suppose currently I have a goal with several assumptions: > > P > - > a0 > a1 > ... > A > > and a theorem th ``A ==> B`` > > Now I want to replace the last as

[Hol-info] QUse.use and exceptions

Hi all, I've noticed that the Vim mode for HOL, in particular this code: https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/vim/vimhol.src#L57 has occasionally stopped passing back raised exceptions to the REPL. >From the UI perspective, this means the user gets no feedback when a comma

Re: [Hol-info] Proving a trivial goal

I didn't know about ELIM_UNCURRY - cool! I would have done rw[GSYM pairTheory.LAMBDA_PROD] (after trying a bunch of things that didn't work..) Also, rw[FORALL_DEF,Once FUN_EQ_THM,pairTheory.UNCURRY] seems to work. As for where this goal came from, I've seen it coming from EVAL_TAC before. On 17

[Hol-info] Using HolyHammer

I thought I would share the approach I have to using HolyHammer currently. I put this in my .hol-config.sml file: load"holyHammer"; fun hh_tac ls g = (Thread.Thread.fork ((fn () => holyHammer.hh ls (list_mk_imp g)), [Thread.Thread.EnableBroadcastInterrupt true]); ALL_TAC g) Now, i

Re: [Hol-info] conservativity of HOL constant and type definitions

Just to answer the question-mark in (2.1), I mechanised a proof that new_type_definition is model-theoretically conservative for standard models and arbitrary base theories. To be clear, the proof assumes the base theory contains "fun", "bool", and "=", and that it has a model that interprets these

Re: [Hol-info] change of email address

I believe you can subscribe with your new address at https://lists.sourceforge.net/lists/listinfo/hol-info. (Of course, the list moderator may be willing to do that on your behalf instead :)) On 1 October 2016 at 12:41, Brian Graham wrote: > My current email address (which this message originate

Re: [Hol-info] A question about the definition of the function in HOL4

Hi Ada, It still looks like you might be mixing up ML and HOL. Are you trying to define an ML function, or a HOL function? In ML, the conjunction of two Boolean expressions can be formed using the "andalso" operator. Now, maybe you already defined /\ like this, and gave it infix status: infix /\

Re: [Hol-info] Certificate issue

Hi Peter, Thank you for the note. You were right, the certificate was expired. It has now been renewed. Sorry for the trouble. I am supposed to receive automated email notices when expiration is coming up. I will now investigate why that did not seem to happen. Cheers, Ramana On 28 June 2016 at

[Hol-info] TAKE_def and DROP_def should not be automatic rewrites

Hi hol-info, I want to ask whether anyone thinks these are good automatic rewrites in listTheory? |- (∀n. TAKE n [] = []) ∧ ∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs |- (∀n. DROP n [] = []) ∧ ∀n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n − 1) xs I find

Re: [Hol-info] A question about the theorem in HOL4?

FST is a function in logic, not in ML. In this case, there does happen to be a similar function, called fst, in ML. Are you trying to specify/prove something in logic? Or are you trying to write an ML program? On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote: > Hi,guys > I am work

Re: [Hol-info] HOL-Light Beginner Questions

I expect it could be because the Boolean constants are spelled "T" and "F" rather than "true" and "false" in the logic, so the latter are being treated as free variables. On 16 June 2016 at 01:09, Heiko Becker wrote: > Hello everyone, > > I am currently learning HOL-Light and therefore working t

[Hol-info] HOL Workshop 2016: Final call

Thinking of submitting an abstract for the HOL workshop this year? They are due tomorrow! It's easy to write one. Don't miss out :) See the call below. --- CALL FOR ABSTRACTS 2016 International Workshop on the HOL Theorem Proving System

Re: [Hol-info] Difficulty with higher order matching

Hi Peter, I'm not sure I can explain why HO_MATCH_MP_TAC is not powerful enough for this kind of match, but I can say what would use instead in this situation. Namely, numLib.LEAST_ELIM_TAC. More generally, I would use DEEP_INTRO_TAC with theorems such as LEAST_ELIM, which is how LEAST_ELIM_TAC is

Re: [Hol-info] Problem installing HOL 4

PolyML 5.6 is supported by the development version of HOL4 (i.e., the head of the master branch), and has been for a while. On 24 May 2016 at 18:39, Chun Tian (binghe) wrote: > Hi all, > > But still, PolyML 5.6 is not supported yet, right? I have to use latest > Poly ML 5.5.x to build HOL4 (Git

[Hol-info] HOL Workshop 2016: 2nd call for abstracts

Don't forgot to submit an abstract for the HOL workshop this year :) The submission deadline is under one month away. See the call below. --- CALL FOR ABSTRACTS 2016 International Workshop on the HOL Theorem Proving System

Re: [Hol-info] What is the advantage of HOL4?

Some strengths of HOL4 (off the top of my head, so maybe not comprehensive): - It is based on simple type theory. See "The seven virtues of simple type theory" . - It is implemented in Standard ML. This is a formally specifi

Re: [Hol-info] Instantiating existentials under existentials

Depending on the body of the existential, you might be better off not mentioning any of the variable names and instead using part_match_exists_tac and a "pattern" that both picks out the `y` and provides the `5`. On 22 March 2016 at 07:12, Ramana Kumar wrote: > Yes there i

Re: [Hol-info] Instantiating existentials under existentials

Yes there is: CONV_TAC(RESORT_EXISTS_CONV(sort_vars["y"])) \\ qexists_tac`5` On 22 March 2016 at 07:08, Magnus Myreen wrote: > Hi hol-info, > > Quick question: is there a tactic for instantiating a nested > existential based on a name? Example: for a goal such as > > ?x y z. ... y ... > > I wa

Re: [Hol-info] A question about a proof with TAKE and DROP?

Also, since the proof appears not to mention CX_def anywhere, it should be possible to generalise the theorem to be about any two lists with the same length (and not mention CX); that might be an easier statement to deal with. On 15 March 2016 at 09:25, Ramana Kumar wrote: > I was able to pr

Re: [Hol-info] A question about a proof with TAKE and DROP?

I was able to prove it as follows, but I needed to prove another lemma about TAKE which really should be in listTheory. open HolKernel boolLib bossLib Parse listTheory rich_listTheory arithmeticTheory val _ = new_theory"ada" val CX_def = Define` (CX [] p q = p) ∧ (CX (x::xs) p q = TAK

Re: [Hol-info] Singletons belong to Borel sets

Have you already proved the two lemmas you suggested already? Namely: all singletons are closed, and all closed sets are Borel? I would suggest proving those two separately first. On 11 March 2016 at 06:41, Muhammad Qasim wrote: > Hello Everyone, > > I want to prove the following, > > `{PosInf}

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

If you want to build HOL with Poly/ML, you should run poly < tools/smart-configure.sml before running bin/build. On 2 March 2016 at 13:18, 康漫 <956066...@qq.com> wrote: > Thank you for your reply! > My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10 > 14:27:30 2014)], where Mos

Re: [Hol-info] a question about rewrite in HOL4

Section 6.2 (The Trace System) of the Description manual describes the trace system. Interactively, the functions traces and set_trace may be of interest. I think the simplifier trace is called "simplifier". On 6 March 2016 at 01:16, Piotr Trojanek wrote: > On Sat, Mar 5, 2016 at 3:04 AM, Micha

Re: [Hol-info] a question about rewrite in HOL4

I think RW_TAC doesn't handle conditional rewrites very well. Try using rw or simp instead. This worked for me: open listTheory val cx_def = Define` (cx [] p q = p) ∧ (cx (x::xs) p q = TAKE x (cx xs p q) ++ DROP x (cx xs q p))` val cx_length = Q.prove( `!l p q . (LENGTH p = LENGTH q)

Re: [Hol-info] HOL breakthrough in American politics

Wonderful! :-) Though one should perhaps reconsider their media engagement strategy when the majority of one's coverage is in The Onion. On 4 Mar 2016 04:51, "Konrad Slind" wrote: >“By expanding on pioneering work in the fields of applied statistics, > higher-order logic, and number theory,

Re: [Hol-info] RESTRICT left over in definition

ubt the > termination condition extractor is setup to deal with pairs in the > concluding equality of a congruence rule. > > Konrad. > > > On Mon, Feb 22, 2016 at 9:36 PM, Ramana Kumar > wrote: >> >> Hi Konrad, >> >> Thanks for looking into this. I ha

Re: [Hol-info] RESTRICT left over in definition

wrote: > Looks horrible. There shouldn't be remaining occurrences of RESTRICT. > Termination-condition extraction should remove them all. > > Can you send me a cut-down version of the problematic function? > > Konrad. > > > On Sun, Feb 21, 2016 at 5:34 AM, Ramana Kuma

Re: [Hol-info] [Hol-developers] dep_rewrite

What needs to be documented? I think I just meant put an "open dep_rewrite" into bossLib. On 22 February 2016 at 11:19, Michael Norrish wrote: > Please document somewhere, but yes. > > Michael > >> On 22 Feb 2016, at 09:24, Ramana Kumar wrote: >> >> So

[Hol-info] RESTRICT left over in definition

I have managed to make a definition where the theorem returned to me by tDefine still contains occurrences of ``RESTRICT new_func (@R. WF R /\ ...)``. Is this to be expected from tricky input equations, or is it a sign of a problem in the recursive function package? Would it be easy to post-proce

[Hol-info] HOL Workshop 2016: call for abstracts

CALL FOR ABSTRACTS 2016 International Workshop on the HOL Theorem Proving System (HOL'16) hosted by ITP-2016 August 25-27, 2016, Nancy, France https://hol-theorem-prover.org/works

Re: [Hol-info] word problem

m - n2w a < n2w m That one seems more likely to be true. But how to prove it? On 9 February 2016 at 10:02, Ramana Kumar wrote: > Hi, > > Does anyone know whether the following goal is true or false? > > How would you prove it? > > If it's false, under what reason

[Hol-info] word problem

Hi, Does anyone know whether the following goal is true or false? How would you prove it? If it's false, under what reasonable additional assumptions would it be true? 0. m < dimword (:α) 1. m < a 2. 0 < m n2w m − n2w a < n2w m Cheers, Ramana -

Re: [Hol-info] About Binary Relations

What's the problem/what is going wrong? On 5 February 2016 at 17:48, Nadeem Iqbal wrote: > Yes, I want the set of first components of the pairs. I replaced S with A, > and used IMAGE FST (A CROSS A), but the problem is not solved. > > > > On Fri, Feb 5, 2016 at 8:52 AM

Re: [Hol-info] About Binary Relations

``S CROSS S`` is a set of pairs. Although ``S`` is usually parsed as a constant, so you might want to use a different letter, or use Parse.hide"S". Do you want the set of first components of the pairs? That would be ``IMAGE FST (S CROSS S)``, and should be equal to ``S``. On 5 February 2016 at 14

Re: [Hol-info] [SPAM] some questions about the use of THEN and THENL in HOL4

The tactic (tac1 THEN tac2) applies tac2 to all subgoals generated by tac1. On 22 December 2015 at 23:05, Ada wrote: > Hey guys, > > I am learning to use HOL4. In listTheory , I found that: > val DROP_0 = store_thm( > "DROP_0", > ``DROP 0 l = l``, > Induct_on `l` THEN SRW_TAC [] []); > I w

Re: [Hol-info] some questions about the proving process in HOL4

--- > LENGTH p = 0 > : proof > - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute); > OK.. > 1 subgoal: > > val it = > TAKE 0 p = p > > 0. LENGTH p = 0 > 1. !l. (LENGTH l = 0) <=

Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

fs[LENGTH_NIL,TAKE_def] On 15 December 2015 at 14:27, Ada wrote: > Hey guys, > > I am learning to use HOL4. There is a function named "TAKE" in HOL4, > which can get the first n elements in a list. > When I was proving one property of TAKE, I find an interesting thing. As > follows: > - g`!p:bo

Re: [Hol-info] Holmake Problem

An opinion I'd like to share: if a package is broken, fixing the package so everyone benefits is a better response than compiling the program from source for yourself. On 5 December 2015 at 03:21, Ian Zimmerman wrote: > On 2015-12-04 13:00 +0330, Ali Abbassi wrote: > > > I am using ubuntu, and I

Re: [Hol-info] some questions about the use of HD and TL in listTheory

HOL syntax for lists uses semicolons (;) to separate list elements, not commas (,). On 30 November 2015 at 18:42, Ada wrote: > Hey guys, > > I am learning to use HOL4. I defined a function named "first" in HOL4. > This function can get the first n elements in a list. As follows: > > - val first_

Re: [Hol-info] irule vs MP_CANON

ke MATCH_MP_TAC, it introduces existentials, which also may > require collecting together some of the ai) which may affect ordering > and exact form of the new subgoals. > > Cheers, > > Jeremy > > > > On 16/11/15 22:28, Ramana Kumar wrote: > > What is the difference betwe

Re: [Hol-info] Definition of Binary Relation in HOL

ards, > Nadeem > > On Thu, Nov 19, 2015 at 4:21 PM, Yong Kiam wrote: >> >> Or you can type annotate them: >> >> Define`numeq (x:num) y <=> x = y` >> >> which gives numeq with type num -> num -> bool >> >> On Thu, Nov 19, 2015 at

Re: [Hol-info] Definition of Binary Relation in HOL

cification. > > On Wed, Nov 18, 2015 at 10:28 PM, Ramana Kumar > wrote: >> >> Which binary relation? What do you mean? >> >> Here's a binary relation that relates natural numbers 1 and 2: >> val a_binary_relation_def = Define`a_binary_relation x y &

Re: [Hol-info] Definition of Binary Relation in HOL

Which binary relation? What do you mean? Here's a binary relation that relates natural numbers 1 and 2: val a_binary_relation_def = Define`a_binary_relation x y <=> (x = 1) /\ (y = 2)`; Here's a binary relation that relates two Booleans iff exactly one of them is true: val another_binary_relation

Re: [Hol-info] proof structure in Coq

I usually use ">>" instead of literally "THEN". Arguably that's still too much "shift". Yes I think you're right about tactician - it's for going back and forth between those styles. On 18 November 2015 at 08:41, Freek Wiedijk wrote: > Hi Ramana, > > >Apparently Coq somewhat recently gained the

[Hol-info] proof structure in Coq

Apparently Coq somewhat recently gained the ability to be explicit about proof structure: http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html (Of course that comes naturally when using tacticals like THEN, THEN1, etc.) --

Re: [Hol-info] is it a bad habit to use "by" mechanism too often?

I think liberal use of explicit subgoals (using "by") can be very good style, because it documents the steps through which you intend the proof to proceed. Once you have finished (part of a proof), it is sometimes possible to shorten it if you so desire. For example, if this works: `l1` by metis_

Re: [Hol-info] how to prove by contradiction

It's also worth mentioning `~A` by PROVE_TAC[] since it can sometimes be faster than metis_tac. On 17 November 2015 at 07:16, Ramana Kumar wrote: > there are many options: > > `~A` by metis_tac[] > > `~A` by (strip_tac >> fs[]) > > first_assum(as

Re: [Hol-info] how to prove by contradiction

there are many options: `~A` by metis_tac[] `~A` by (strip_tac >> fs[]) first_assum(assume_tac o CONTRAPOS) >> res_tac first_x_assum(imp_res_tac o CONTRAPOS) Cases_on`A` >> fs[] `~A` by (spose_not_then strip_assume_tac >> res_tac) `~A` by (CCONTR_TAC >> fs[]) ... On 17 November 2015 at 02:

Re: [Hol-info] how to search my theorems with DB.match

The call should look like: DB.match theories pattern-term where theories is a list of names of theories in which to search for the pattern-term. If you leave the list empty, it searches in all theories in the current hierarchy. I think if you give "-" as a the name, it might search in the current

Re: [Hol-info] what is the meaning of ?-

I believe it is supposed to represent a conjecture, or a goal state. So, something like a theorem that has not been proved yet. On 16 November 2015 at 12:39, shengyu shen wrote: > Dear all: > > I find ?- is used in lots of place in the reference of HOL. It seems to be > something similar to |-

[Hol-info] irule vs MP_CANON

What is the difference between irule and (match_mp_tac o MP_CANON)? I'm more interested in differences in the intended design than in minor details in the implementation. Which is preferred style? Which should get more developer time? Maybe they're actually rather different, but as far as I saw,

Re: [Hol-info] implicitely referring to large set of proven theorems in METIS_TAC

val mythms = [thm1, th2, th3, ..., th20]; fun metis_extra_tac ths = metis_tac (ths@mythms); ... e(metis_extra_tac [...])... On 15 November 2015 at 11:54, shengyu shen wrote: > Dear all: > > assume that I have proven a large number of theorems, for example , 20, > can I make METIS_TAC to use th

  1   2   3   4   >