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

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=rep1=pdf > > http://www.gilith.com/talks/tphols2001-subtypes.pdf > > > - Umair > > On Wed, Feb 20, 2019 at 4:02 PM

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 < > ram

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

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) +

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)`,

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

[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

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

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

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

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

[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

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

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 <ramana.ku...@cl.cam.ac.uk> wrote: > Just based on your final question, I suggest: > ?l1 l2. (DELETE_ELEMENT e L = l1 ++ l2) /\ (L = l1 ++ [e] ++ l2) > > On 11 Oct

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

t; exactly the same order and number of appearances? In another words, by > inserting some “e” into (DELETE_ELEMENT e L) I got the original list L? > > Regards, > > Chun Tian > > > Il giorno 02 lug 2017, alle ore 10:23, Ramana Kumar < > ramana.ku

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

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

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

th pointer equality. On 5 October 2017 at 16:15, Heiko Becker <hbec...@mpi-sws.org> 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 1

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

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

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.,

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

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

at featured infinite sums over a base type that didn’t itself include > infinite sums. > >>>> > >>>> Something like > >>>> > >>>> Datatype`CCS = … existing def … (* with or without finite/binary > sums *)` > >>&g

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

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

10 July 2017 at 23:36, Robert Künnemann <rob...@kunnemann.de> 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? Because "y" is

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

[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

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

l >>> which looks perfect: (and no need to prove the 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)) ∧ >>>

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

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

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

a bug in HOL's OpenTheory module? > > Regards, > > Chun > > > > > On 26 April 2017 at 03:57, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > >> Thanks Chun Tian, >> >> I can reproduce the issue. >> >> I tried finding out which the

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

e ore 15:21, Chun Tian (binghe) < > binghe.l...@gmail.com> ha scritto: > > > >> Il giorno 29 apr 2017, alle ore 01:02, Ramana Kumar < > ramana.ku...@cl.cam.ac.uk> ha scritto: > >> > >> Hi Chun, > >> > >> Try with the latest update t

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

porting work, but currently I have > no such need or interest at all. > > > > So I’m going to find out which exact theorem caused the issue first, and > move this theorem (I hope it’s just one) into a whole new script file, then > try to find out which proof step caused the is

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

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

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] >

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)?

it type -D > - > > 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

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

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,

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

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

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

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

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-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

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

[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

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 <ramana.ku...@cl.cam.ac.uk&g

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 <ramana.ku...@cl.cam.ac

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 =

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

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

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,

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

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

ence rule looks a bit suspect. I doubt 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 <ramana.ku...@cl.cam.ac.uk> > wrote: >> >&g

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 <michael.norr...@nicta.com.au> wrote: > Please document somewhere, but yes. > > Michael > >> On 22 Feb 2016, at 09:24, Raman

[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

[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

Re: [Hol-info] word problem

2w 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 <ramana.ku...@cl.cam.ac.uk> wrote: > Hi, > > Does anyone know whether the following goal is true or false? > > How would you prove it? > > If it

[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

Fri, Feb 5, 2016 at 8:52 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> > wrote: > >> ``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

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) <=> (l = []) >

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 >

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

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

Re: [Hol-info] irule vs MP_CANON

in c, (like 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: > >

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

relations between > A and A in HOL. > > Regards, > Nadeem > > On Thu, Nov 19, 2015 at 4:21 PM, Yong Kiam <tanyongk...@gmail.com> wrote: >> >> Or you can type annotate them: >> >> Define`numeq (x:num) y <=> x = y` >> >> which gives numeq w

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

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 <ram...@member.fsf.org> wrote: > there are many options: > > `~A` by metis_tac[] > > `~A` by (strip_tac >> fs[]) > > f

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

[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

Re: [Hol-info] [HOL-INFO] programming mode in HOL4?

Use computeLib.EVAL. On 14 November 2015 at 13:23, shengyu shen wrote: > Dear all: > > I have some experience in ACL2 and COQ, which have a programming mode, in > which I can try running some function. For example, I define a fact > function that compute the factorial of

Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

I have this problem again. Can anyone help? % camlp5 -v Camlp5 version 6.14 (ocaml 4.02.3) hol-light % make \ if test `ocamlc -version | cut -c1-3` = "3.0" ; \ then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \ else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut

Re: [Hol-info] Emacs Macros for HOL Light Proof

You forgot to mention the comprehensive Vim mode for HOL4. (See tools/vim in the HOL4 repository.) On 4 November 2015 at 16:22, Joe Leslie-Hurd wrote: > For those of you who use HOL Light in an Emacs shell, I wrote some > simple Emacs Lisp macros to support interactive proof: >

[Hol-info] What would you like from a HOL workshop?

Dear HOL users and developers, I will endeavour to organise a workshop for HOL, to be co-located with ITP 2016 (France, end of August). Before planning the details, I want to ask you: what kind of workshop would serve you best? Please send me any requests or comments, and together we can use

[Hol-info] EVAL WHILE

To my surprise, EVAL went into a loop on the following term: ``WHILE (\x. x = 0) (\x. x) 1`` I thought in the default setup, EVAL would only evaluate the first argument of a conditional, reducing it to true or false, skipping the other arguments (the then and else branches) until it was known

Re: [Hol-info] map_option

also possible. > > Both types, ie, 'a option set, and 'a set option, are compound monads, and > your function is a monad morphism, which is also used in a certain > construction which can be used to prove that the latter is indeed a > compound monad. > > Cheers, > > Jere

[Hol-info] map_option

Hi all, I think this must be some neat combination of category theory things. Does anyone know which? Or if it's already defined somewhere? val map_option_def = Define` (map_option [] = SOME []) ∧ (map_option (NONE::_) = NONE) ∧ (map_option (SOME x::ls) = case map_option ls of | SOME

[Hol-info] Unicode versions

What is the difference between these functions? Parse.overload_on Parse.Unicode.uoverload_on Parse.Unicode.unicode_version Which ones should be used when? Does more than one need to be used at once? From some of my recent playing around, it seems like unicode_version sometimes but not always

[Hol-info] Final call for abstracts (HOL4 Workshop)

Hi all, A reminder: the deadline for abstracts for the upcoming HOL4 Workshop is less than one week away. All details can be found at the website: https://www.cl.cam.ac.uk/~rk436/hol15/ We look forward to receiving your abstracts, and to seeing you in Berlin for the workshop!

Re: [Hol-info] Question about rewriting in proofs

In both cases it sounds like the problem is that rewriting is rewriting too much - you only want to rewrite a particular occurrence of a term. You might try using ONCE_REWRITE_RULE or Once. If that doesn't work, you can be much more specific about where you apply rewriting by using the rewriting

Re: [Hol-info] Question about rewriting in proofs

Another option is to abbreviate the parts of the term that you don't want to be rewritten. See Q.PAT_ABBREV_TAC for example. On 21 May 2015 at 13:12, Ramana Kumar ram...@member.fsf.org wrote: In both cases it sounds like the problem is that rewriting is rewriting too much - you only want

[Hol-info] HOL Workshop 2015

SECOND CALL FOR ABSTRACTS 2015 International Workshop on HOL4 The HOL Theorem Proving System (HOL'15) hosted by CADE-25 August 2-3, 2015, Berlin, Germany

Re: [Hol-info] Bindings for embedded languages in HOL

There is an example of a nominal datatype in HOL4/examples/unification/triangular/nominal. On Wed, Mar 18, 2015 at 4:10 PM, Petros Papapanagiotou p...@ed.ac.uk wrote: Hello everyone, Having reached the ceiling of what I can achieve by hacking variable bindings and substitutions for embedded

Re: [Hol-info] Viewing HOL proofs

One method is editor integration, which makes the process of viewing the proof less painful than manual copy-paste. In HOL4 there is integration for both Vim ( https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim) and Emacs, which might be a suitable starting point. (These essentially

Re: [Hol-info] Inductive_set definition in HOL4

Qasim Quoting Ramana Kumar ram...@member.fsf.org: Is this something different from what Hol_reln will give you? On Tue, Mar 10, 2015 at 6:33 PM, Muhammad Qasim m_q...@encs.concordia.ca wrote: Hello Everyone, I saw an inductive_set definition in Isabelle. Is there a way to do

[Hol-info] type grammar for munger

I'm having a lot of trouble trying to remove a type abbreviation when using the HOL-TeX munger. I make the munger with a main theory that calls Parse.disable_tyabbrev_printing reln. And if I load this theory in an interactive HOL session and type ``:'a - 'a - bool`` it prints back as I expect. But

[Hol-info] Holmake broken?

I'm having a lot of trouble getting Holmake to work when I have dependencies included (via INCLUDES in my Holmakefile). Has something substantial changed in how I'm supposed to write a Holmakefile? It seems like Holmake is using the INCLUDES from my current directory even when it makes recursive

Re: [Hol-info] Holmake broken?

Related to this: are relative paths allowed in the INCLUDES? and in that case, shouldn't they be relative to the directory containing the Holmakefile? On Wed, Feb 18, 2015 at 11:21 AM, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote: I'm having a lot of trouble getting Holmake to work when I have

Re: [Hol-info] Holmake broken?

in some cases. Michael On 19 Feb 2015, at 4:03 am, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote: Related to this: are relative paths allowed in the INCLUDES? and in that case, shouldn't they be relative to the directory containing the Holmakefile? On Wed, Feb 18, 2015 at 11:21 AM

  1   2   3   >