Re: [Hol-info] EVAL(tac conv rule)

If you use the most recent working version of HOL (get it via git), then your Holmake processes will be multi-core on a per-theory basis (i.e., where the theory-graph of dependencies permits it, Holmake will cause theories to build concurrently). There is currently no support for concurrent

Re: [Hol-info] EVAL(tac conv rule)

One approach would be to define constants that do the abbreviation for you. Then you should recast the theorems/definitions that EVAL is using to also use those new constants. I'm afraid there isn't any code already around that automatically detects repeated sub-terms, so you'd have to write

Re: [Hol-info] Using pattern_matches's custom syntax

Thomas has it right. The behaviour whereby dtcase prints as case is a bug that I will try to get around to fixing at some point. Note that this is all with respect to HOL as you check it out from master on github, not Kananaskis-10. Michael On 28/07/2016, 08:54, "Thomas Tuerk"

Re: [Hol-info] Theory documentation outside of HOL

This is certainly a nice idea. If you do figure out how to do it, please make a pull request. In work that I haven’t polished or committed, I have generalized our graph generation to target arbitrary theory hierarchies, and this generates theory summaries of its own. If that’s all you want,

Re: [Hol-info] Emacs indentation for theory scripts

I think the way to try to do it would be to combine the SML mode and another, custom thing that handled text inside quotations. I might try starting with https://github.com/aaronbieber/fence-edit.el for example. Michael On 3/08/2016, 22:14, "Corey Richardson" wrote:

Re: [Hol-info] HOL4 on Mac OS X using the ML variant shipped with Isabelle

Dear Ken, Thank you for the error report. The warning messages are ugly, and not helpful. As you supposed, the system's behaviour won't have been affected, but it's still not a good look. The bug has now been fixed on the master branch (commits 8f675fb and f44f111 by Anthony Fox). Best

Re: [Hol-info] How to correctly define a binder (as pretty printer)?

The only easy way to do this at the moment would be to - Define a fake constant with the name of the binder you want, but which does nothing. E.g., Define`AE x = x`; - Make it a binder : set_fixity “AE” Binder; - Define your real constant as below:

Re: [Hol-info] How to prove this theorem about relations?

If you want to see the stored rule induction principles, you might use: ThmSetData.all_data "rule_induction"; Or IndDefLib.thy_rule_inductions "list"; where you get to provide the theory name. Michael From: Thomas Tuerk Date: Thursday, 19 January 2017 at 03:22

Re: [Hol-info] How to prove this theorem about relations?

Note that the cases theorem does not capture “leastness”. A coinductive definition of the same relation would give you the same cases theorem. The cases theorem is just giving you the fix-point property. One easy example for thinking about these sorts of things is lists. Imagine you have:

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

Thank you for taking the time to look into this. I agree that a Cygwin poly/ml version is the best route to a Windows build (Moscow ML is simply too slow for serious work). Initially, I’d be happy to not use the Holmake code that depends on Posix. Instead, we could use the Moscow ML approach,

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

There hasn’t been any change in FIRST_ASSUM and FIRST_X_ASSUM. As always, FIRST_ASSUM leaves the assumption in place, and FIRST_X_ASSUM pulls it out. Michael From: Konrad Slind Date: Tuesday, 17 January 2017 at 15:22 To: "Norrish, Michael (Data61, Canberra City)"

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

If you are using the working copy of HOL from the git repository, you should check the release notes in HOLDIR/doc. We document major incompatibilities there. Note also that the last official release was K10. There is a tag for K11 in the repository, and some release notes for it, but it

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

There were really two changes. If it was just a rename, then a find-and-replace (pat_assum -> pat_x_assum) would solve all the problems. However, there was another change to do with the handling of free variables in the pattern. As per the release notes, that change might require the use of

Re: [Hol-info] How to define a new datatype and use it?

Your options are not all the same. In particular, option 1 gives you a type that can be either a reg1, or a reg2 or a reg3 or a reg4, but only one of those. Your other options are basically the same. Options 2 and 3 are identical (Hol_datatype is an old name for Datatype, and has a slightly

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

EL is indeed the right constant to use: > EVAL ``EL 3 [4;5;6;7;8]``; val it = |- EL 3 [4; 5; 6; 7; 8] = 7: thm I don’t know what you’re trying to express by writing ``!n. EL n x``. The English reading of that term would be “for all n, the nth element of x is true”. (Remember that the

Re: [Hol-info] Pretty printing of strings without double-quotes?

There’s no great way to do this at the moment, because it’s not possible to have all the things that are possible inside string literals (e.g., \n) appear in other contexts. My inclination would be overload n to name, and to overload unary negation to coname, and then you could write n"a"

[Hol-info] Release of HOL4 Kananaskis-11

K11 has been rather long in coming, but I intend to release a Kananaskis-12 within the next few months as the freezing of K11’s feature set actually occurred rather a while ago (June last year), and there has been plenty of work since. # Release notes for HOL4, Kananaskis-11 (Released: 3

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

Note further that a type where you have Datatype‘CCS = C1 … | C2 .. | SUM (num -> CCS)’; does not fall foul of cardinality problems. (You can recurse to the right of a function arrow as above, but not to the left, as would happen in SUM (CCS -> bool).) So, when I wrote “you just can’t have

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

You just can’t have infinite sums inside the existing type for the cardinality reasons. But there’s no reason why you couldn’t have a type that featured infinite sums over a base type that didn’t itself include infinite sums. Something like Datatype`CCS = … existing def … (* with or

Re: [Hol-info] How to define "infinite sums" of custom datatypes?

You can’t define a type that recurses under the set “constructor” (your summ constructor has (CCS set) as an argument). Ignoring the num set argument, you would then have an injective function (the summ constructor itself) from sets of CCS values into single CCS values. This ultimately falls

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

Even if you can’t prove your result for an arbitrary injective f, does it hold for the particular f that you have defined? (There are plenty of injective functions between equi-numerous sets that are not onto…) Michael On 23/7/17, 01:07, "Chun Tian (binghe)" wrote:

Re: [Hol-info] How to reduce these lambda equations to F?

I would use fs[FUN_EQ_THM] to expand the assumptions to !x. x = prefix (label l) x and !x. x = p respectively. Of course, this is a blunt weapon, so you may not wish to use it if other assumptions are disrupted too much. Michael On 5/8/17, 04:25, "Chun Tian (binghe)"

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

You are being caught by the fact that match_mp_tac thm can throw an exception before the tactic is ever applied to a goal. In particular, if the theorem passed to match_mp_tac is not an implication an exception is thrown immediately. You can fix this by handling that possible exception:

Re: [Hol-info] Problem of Installation the latest HOL 4

I’d certainly be happy to adjust smart-configure to be smarter. (I’d be even happier to approve a pull request.) I don’t understand the suggestion about using ldd on libpolyml.so. Do you mean to use it on the poly executable itself? (If I knew where libpolyml.so was, I’d take that to be the

Re: [Hol-info] [ExternalEmail] Re: Issues in kananaskis-11 release source tarball

I have uploaded another tar ball to the sourceforge site. Note that the tarball at github doesn’t have this problem. Michael On 2/5/17, 18:16, "michael.norr...@data61.csiro.au" wrote: Thank you for the bug report! I will upload a corrected

Re: [Hol-info] Documentation for Hol_coreln?

Right. If you have recursive occurrences of R on the RHS, these would correspond to places where the fix-point construction does something with the set parameter (as opposed to ignoring it). Michael On 5/5/17, 02:37, "Chun Tian (binghe)" wrote: I think I got it,

Re: [Hol-info] Problem of Installation the latest HOL 4

Well, as I said, I think it’s quite possible that we don’t need to know this any more. Before polyc was provided, we needed to provide explicit -L paths so that the linker could look in the right places when building executables like Holmake. All this is now handled by polyc I think. In the

Re: [Hol-info] Documentation for Hol_coreln?

As with the cases theorem returned by Hol_reln, the cases theorem is effectively an assertion that the relation is indeed a fix-point. Michael From: "Chun Tian (binghe)" Date: Thursday, 4 May 2017 at 14:07 To: hol-info Subject: [Hol-info]

Re: [Hol-info] Issues in kananaskis-11 release source tarball

Thank you for the bug report! I will upload a corrected tarball shortly. Michael On 2/5/17, 16:11, "Chun Tian (binghe)" wrote: Hi, The kananaskis-11 release source tarball (hol-kananaskis-11.tar.gz) [1] downloadable from HOL’s official site [2] has at

Re: [Hol-info] What is the purpose of labels?

This is a feature that hasn’t really been pursued. There is some code supporting their use (akin to the way Abbr`v` is supported in calls to the simplifier), but it is incomplete and thus unused, and pretty well undocumented. But yes, the idea is to be able to label assumptions to make it

Re: [Hol-info] Converting ordinals from different type variables?

The definition is fine, but will not have the nice properties you want (e.g., monotonicity) if the domain type is bigger than the range. In particular if your domain includes \omega_1 and the range only has countable ordinals, then the result of c2a on \omega_1 will be unspecified. This is

Re: [Hol-info] line wrap length in hol-mode

You need to adjust Globals.linewidth (an int ref). Michael On 17/10/17, 03:57, "Mario Castelán Castro" wrote: Hello. How can I change the column at which the pretty printer will wrap expressions using hol-mode in GNU Emacs? I want it to use the full width of

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

You might define the sublist relation : Sublist [] l = T Sublist _ [] = F Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist (h1::t1) t2 And show that Sublist (DELETE_ELEMENT e l) l This doesn’t capture the idea that the only missing elements are e’s though. This

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

There’s certainly a bug here: I want the superscript T for relations and the superscript -1 for reals, and the two need not mix. I think there’s a straightforward enough solution that will allow “inv” to be used as an input method for both. Michael On 17/10/17, 06:57, "Chun Tian"

Re: [Hol-info] About restricted quantification and algebraic-like structures

On 6/9/17, 03:14, "Mario Castelán Castro" wrote: Sorry; I should have been more clear. Consider this hypothetical situation: I have a proposition “P:σ->bool”. (P is a metavariable ranging over HOL terms with no free variables, σ is a HOL type which

Re: [Hol-info] About restricted quantification and algebraic-like structures

These are good questions. You are right that the ring and topology examples aren’t as usable as one might like. If you want to do real formalisations of abstract algebra, you do want to be able to work with subsets of the whole of the type. See for example the treatment of groups in

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

Eta-expanding as you did is nicer, I think. You might also consider using irule; it is supposed to be an improved match_mp_tac (i.e., does more things), and it doesn’t have the particular problem with exceptions. Indeed, one of its improvements is that it subsumes {MATCH_}ACCEPT_TAC. Michael

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

irule is an “improved” version of match_mp_tac; mp_then is an improved version of imp_res_tac (strictly, imp_res_then). Alternatively, irule applies an introduction rule to the goal (“backwards”); mp_then applies an elimination rule to assumptions. I agree about the stripping of conjunctions.

Re: [Hol-info] Is ``:string ordinal`` uncountable or not?

Strings have the same cardinality as numbers (there is a bijection between them established in string_numTheory), so string ordinal will be the same type (up to isomorphism) as num ordinal. There’s no general way to know what the cardinality of a type is unless you have theorems to hand that

Re: [Hol-info] The use of optionTheory for representing invisible actions in transition systems

I think this is a case of “try it and see”. As per Konrad, it might be more natural to use sums, which is essentially what your original type was. But as both arguments were the same beta parameter, your sum was effectively beta + beta. Switching to a product beta * 2 is clearly equivalent.

Re: [Hol-info] [ExternalEmail] Re: Is ``:string ordinal`` uncountable or not?

Apologies for duplicated paragraphs below… Michael On 10/10/17, 09:27, "michael.norr...@data61.csiro.au" wrote: Strings have the same cardinality as numbers (there is a bijection between them established in string_numTheory), so string ordinal will be the

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

There is no nice way to do this on a per-theorem basis, though I can imagine an option to Holmake that would turn on some sort of logging like this. Can you make a feature request please? You do get per-theory timing information emitted at the end of each script file, and you could see this

Re: [Hol-info] Difficulties in formalizing an informal proof with cardinals (or ordinals)

I think there is still an issue because your existing CCS term may use all of the available ordinals for that type. Then you can never find a least one in that type that is bigger than them all (because there are none left). It seems to me that you have two options. You either prove a result

Re: [Hol-info] Small question about sqrt

Square root is unspecified on numbers < 0, so you don’t know that there is not a negative number whose square root is 0. Michael From: Liu Gengyang <2015200...@mail.buct.edu.cn> Date: Saturday, 21 October 2017 at 00:05 To: hol4_QA Subject: [Hol-info] Small

Re: [Hol-info] The origin of the HOL4 logo

Our manuals’ acknowledgements text includes: The cover design is by Arnold Smith, who used a photograph of a `snow watching lantern' taken by Avra Cohn (in whose garden the original object resides). John Van Tassel composed the \LaTeX\ picture of the lantern. This would have been done

[Hol-info] FW: A problem of derivation

From: "Norrish, Michael (Data61, Acton)" Date: Thursday, 9 November 2017 at 14:15 To: Liu Gengyang <2015200...@mail.buct.edu.cn> Subject: Re: [Hol-info] A problem of derivation Use the theorem SQRT_POW_2. E.g.: Q.prove( `!a b c d.(sqrt(c pow 2 + d pow 2)

Re: [Hol-info] Representation of functions with explicit domain

I’m afraid it depends. There are at least three different options. The obvious one is to use an option type in the range. This makes everything very explicit, but can be quite ugly. Another approach is to just use the normal function space, knowing that you will have the intended domain

Re: [Hol-info] Proof about sorting

There are proofs that quick-sort and merge-sort are correct in the distribution already. Perhaps looking at these examples in src/sort will give you some clues. Michael From: Liu Gengyang <2015200...@mail.buct.edu.cn> Date: Monday, 4 December 2017 at 13:02 To: hol4_QA

Re: [Hol-info] Proof about sorting

I’m pretty confident that your property is a consequence of being SORTED; see SORTED_EQ in sortingTheory for example. You would then need to establish that your function does indeed create lists that are SORTED. Your property0 is also too specific, you shouldn’t require pop = mySort pop.

Re: [Hol-info] How to define term-like multi-recursive structures?

I’m not sure why you say that you can’t add “fix” to the datatype declaration. A line like | fix (CCS list) would be accepted by Datatype. Then the type of the constructor “fix” would be fix : ('a,'b) CCS list -> ('a,'b) CCS In short, I don't understand why you write "the type of ``fix

Re: [Hol-info] build failed with latest HOL

That’s a Poly/ML bug. Please use the 5.7 release available at https://github.com/polyml/polyml/archive/v5.7.tar.gz Michael From: Waqar Ahmad via hol-info Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk> Date: Saturday, 28 October 2017 at 18:13 To: hol-info

Re: [Hol-info] Can the simplifier from simpLib normalize symmetric relations?

Passing the theorem EQ_SYM_EQ will normalise this sort of thing: > EQ_SYM_EQ; val it = |- ∀x y. x = y ⇔ y = x: thm > SIMP_CONV (srw_ss()) [EQ_SYM_EQ] “a = b ∧ x = z ⇔ b = a ∧ x = z”; <> val it = |- (a = b ∧ x = z ⇔ b = a ∧ x = z) ⇔ T: thm Michael On 29/10/17, 02:58, "Mario Castelán

Re: [Hol-info] How to define term-like multi-recursive structures?

You would have to define every function in terms of “fix” and then come up with a clause for the new constant using “Fix” as well (or prove a new “axiom” for the type). You would also need to prove new induction and cases theorems. But yes, this “cheap approach” might be doable. Michael On

Re: [Hol-info] Can the simplifier from simpLib normalize symmetric relations?

In these situations, the simplifier detects the potential loop and only rewrites if the resulting term is smaller than the original in some well-founded order. Michael On 31/10/17, 04:30, "Mario Castelán Castro" wrote: On 29/10/17 16:18,

Re: [Hol-info] Extension of Co-algebraic Datatype

I think you may be able to make your needs more precise by explicitly considering what your co-algebra would be. In particular, write down the type of the “general” destructor myType -> F(myType) For lazy lists, this is α llist -> (α # α llist) option For the co-algebraic numbers it’s

Re: [Hol-info] Extension of Co-algebraic Datatype

If you want the coinductively defined streams predicate over lllist, you can write > CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a > s)`; <> <> val it = (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s), ⊢ ∀A streams'. (∀a0. streams' a0 ⇒ ∃a

Re: [Hol-info] Comparing two Linear Temporal Logic (LTL) formalizations in HOL4

The paper describing the work in examples/logic/ltl will appear at ITP this year. Because there's a slight CakeML angle to it, it's available from cakeml.org at https://cakeml.org/itp18.pdf. You are right that this work could be described as a deep embedding. Deep embeddings usually have the

Re: [Hol-info] Reverse Function on LazyLists

As reverse on llist only really works when the argument is finite, the easiest definition would be Lrev ll = fromList (REVERSE (toList ll)) You could lift this to infinite lists by having ~LFINITE ll ==> (Lrev ll = infinite-list-of something) Or similar. As it happens, I believe such a

Re: [Hol-info] HOL 4 Kananaskis 11 Installation Problem

Subscript is the standard exception raised if you attempt to do things like List.nth([1,2,3], 3) or String.sub("foo bar", 9) I guess that Holmake is trying to do one of the above sorts of things. What happens if you move the Holmakefile in tools/set_mtime out of the way and call

Re: [Hol-info] Extension of Co-algebraic Datatype

There is no documentation I’m afraid, except that the interface and behaviour is basically exactly the same as for IndDefLib, which is described in the DESCRIPTION manual. Michael From: Waqar Ahmad <12phdwah...@seecs.edu.pk> Date: Wednesday, 16 May 2018 at 06:11 To: "Norrish, Michael (Data61,

Re: [Hol-info] big records

If you understand what the package is doing (and I admit that this is not easy), then the behaviour of the simplifier on big records is in turn fairly understandable. The advantage of the package is not suffering a quadratic blow-up in elapsed time and theorem sizes (in turn leading to

[Hol-info] Kananaskis-12 release of HOL4

Release notes for HOL4, Kananaskis-12 = (Released: 20 June 2018) We are pleased to announce the Kananaskis-12 release of HOL 4. We would like to dedicate this release to the memory of Mike Gordon (1948–2017), HOL’s first developer and the leader of the

Re: [Hol-info] On equivalence of two definitions of PERMUTES

The two definitions are not equivalent. The BIJ overload permits functions to be designated permutations that the definition does not. BIJ can be used to identify bijections between different types so it can't/shouldn't require anything much of functions outside their domain. I think one's

Re: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12

This looks like a regression. Can you turn this into an issue on github please? Michael From: Waqar Ahmad via hol-info Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk> Date: Tuesday, 3 July 2018 at 01:41 To: hol-info Subject: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12 Hi all, I

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

As I said earlier, the breakage is certainly caused by the way in which the REPL executable now includes a custom lexer (for handling the various backquote ```` syntaxes), and is not the standard Poly REPL. This is exactly the change that was implemented in the heaps-reworked branch. Having

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

It looks as if it came from polyml/basis/FinalPolyML.sml Michael On 29/4/18, 20:23, "Chun Tian" wrote: Thanks for the detailed explanation. Just one more question: do you know which code file in Poly/ML sources corresponds to tools-poly/holrepl.ML?

Re: [Hol-info] How to define term-like multi-recursive structures?

Using alists rather than finite-maps will have the issue that fix [(X, a + Y); (Y, b + X)] X will be seen as different to fix [(Y, b + X); (X, a + Y)] X when you might prefer them to be syntactically identical, but there are so many “structural congruences” in this syntax that having to

Re: [Hol-info] LRTC (Reflexive Transitive Closure with a List)

I’m afraid I can’t now remember if someone has already pointed this out, but I think you probably should use the theory of “paths” for this sort of thing. See the description in the DESCRIPTION manual, and the theory itself in src/path Michael From: "Chun Tian (binghe)"

Re: [Hol-info] Spurious parent theories

We don’t track logical dependencies. Rather, we record what theories have been loaded. This loading is “irreversible”, so using the default setup will force you to have all those theories as ancestors. Both the command-line --holstate= and Holmakefile HOLHEAP= methods seem fine to me. Using

Re: [Hol-info] res_quanLib and res_quanTools are exact duplicates

Agreed: let’s keep Lib and ditch Tools. Thanks, Michael On 21/10/17, 03:12, "Mario Castelán Castro" wrote: res_quanLib and res_quanTools are exact duplicates. Is there some reason to have both of these structures instead of just one? If not, then which one

Re: [Hol-info] How to build only hol.bare?

The way to do this sort of thing is to specify the sequence of directories you want built with the --seq=fname command line option. Sequence files can #include other files. See the documentation in the top-level file tools/build-sequence If you are hacking HOL frequently, please read

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

There is generic machinery for adding values of various forms to theories so that future theories and ML code can see them. The smoothest instantiation is in ThmSetData (in src/1) which allows storage of sets of theorems in a “2D matrix” indexed by theory-name and set-name. For example, the

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

That level of generality is already possible, and has always been a desideratum for the design. (The grammar update information stored is about that complicated for example; consider the types that occur in a call to add_rule.) The painful part is that you have to write functions to encode and

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

If people wanting to store these “uninteresting” theorems are happy to wrap and unwrap the OMITs, this would be one approach. I had been thinking of adding a save_private_thm(name, privatedbname, thm) entrypoint to Theory.sml. You’d want multiple possible “private dbs”, so there would

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

I was thinking along these lines, yeah. Such theorems could also be stopped from appearing in the Theory.sig file. Michael On 12/1/18, 07:31, "Konrad Slind" wrote: Theorems that need to persist between sessions are most easily stored by name in theories.

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

In fact, bin/build cleanForReloc will purge a directory tree of the files in rebuild-excludes.txt, so it might be easier to copy a tree and then “clean” it. This workflow should be documented before the next release. Best wishes, Michael From: Ramana Kumar Date:

Re: [Hol-info] Using polyscripter with user-written theories

Thanks for the question Heiko. I think Thomas’s answer is the best that can be done at the moment, but now that I’m aware of the problem, I will adjust polyscripter to pay attention to `INCLUDES =` lines in a Holmakefile, and perhaps also `-I` command-line options passed to polyscripter. With

Re: [Hol-info] [ExternalEmail] Re: Using polyscripter with user-written theories

Just to confirm that polyscripter as of 0146fefd73f now does pay attention to INCLUDES and PRE_INCLUDES lines in Holmakefiles. Michael On 19/2/18, 11:51, "michael.norr...@data61.csiro.au" wrote: Thanks for the question Heiko. I think Thomas’s

Re: [Hol-info] The origin of the HOL4 logo

I’m pretty sure I derived the small logo GIF file from the eps file in the HOL repo using some image manipulation process, and perhaps some bitmap tweaking. The photo may be the one linked to earlier at the URL under cl.cam.ac.uk/~mjcg. Michael On 19/12/17, 13:13, "Mario Castelán Castro"

Re: [Hol-info] Undefined references building “description.pdf”

Thanks for the bug report. The error is due to this: ! pdfTeX error (font expansion): auto expansion is only possible with scalable fonts. \AtBegShi@Output ...ipout \box \AtBeginShipoutBox \fi \fi I will try to look into what is going on at

[Hol-info] PhD opportunities at the ANU

++ The Logic and Computation Group at the Research School of Computer Science, The Australian National University has a number of PhD scholarship available for bright, enthusiastic doctoral students in the following subjects: - Logic

Re: [Hol-info] Partial Function on lazy list

The function is already ready for use with any P; the final until_thm looks like val until_thm = ⊢ (until P [||] = [||]) ∧ (until P (h:::t) = if P h then [|h|] else h:::until P t): thm meaning that one can write things like until (\x. x MOD 3 = 0) ll for example. This seems like a

Re: [Hol-info] Partial Function on lazy list

You need to define a helper function that has as its state not only the llist that is being consumed but also a Boolean indicating whether or not to stop (because a P-satisfying element has been seen). - - val until0_def = new_specification ("until0_def", ["until0"], ISPEC ``λbll. if

Re: [Hol-info] Using Assumptions

Mario is right if you are happy to write the whole assumption out (as he describes), or if you have your hands on the relevant term some other way. If you also want the benefit of parsing a string into a term in the context of the current goal, you might also want to try QTY_TAC bool

Re: [Hol-info] Assumptions of goal usage

Yes. Use tactics like drule, dxrule and others in this family. See https://hol-theorem-prover.org/kananaskis-12-helpdocs/help/Docfiles/HTML/Tactic.drule.html Alternatively, write in a declarative style: `e` by metis_tac[th] >> `f` by metis_tac[] >> Michael From: Dylan Melville

Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

Make the assumption the left-hand-side of an implication (moving it out of the assumptions), rewrite with the identity that says that ((P /\ Q) ==> R) <=> (P ==> (Q ==> R)) and then move all the implications’ left-hand-sides back into the assumptions. In HOL4 you could use something like

Re: [Hol-info] Lazy list: Stream in coinduction

Don’t use abbreviations before starting your proof: it’s muddling your quantifications. Instead, use !s. (?s0. s = StreamD s0) /\ P s ==> streams A s as your goal and follow with ho_match_mp_tac streams_coind >> dsimp[] You will then end up with ∀s0. P (StreamD s0) ⇒ ∃a

Re: [Hol-info] QuoteFilter with precise positions

The quotation filter doesn't really do any tokenization other than to spot occurrences of the magic term and quotation delimiters: ` .. ` (a quotation) ‘ .. ’ (also a quotation, but with non-identical delimiters) ``:ty`` (an application of the type parser to a quotation) “:ty”(

Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

The assumption of the rewrite theorem is not present in the assumptions of the goal and so you get an invalid tactic. Strictly speaking this is not REWRITE_TAC failing but e. Indeed, you should find that REWRITE_TAC [second_b13_complete] applied to the goal works just fine. Michael From:

Re: [Hol-info] QuoteFilter with precise positions

Two minor followups: - there is evidently a bug in the position information when the leading delimiter is a Unicode quote mark (the number of bytes gets counted rather than the number of "characters"); - the unquote filter is built by the process of "configuring" the system before building;

Re: [Hol-info] Partial Order for Set Supremum

It looks to me as if the assumption !x y. P x /\ P y ==> x <= y Is false for all sets with cardinality greater than 1. (If <= is over the reals, and P encodes a set with more than one element, then one or other will be strictly less than the other. Then, it’s easy to specialise the above

Re: [Hol-info] QuoteFilter with precise positions

On 5/9/18, 23:14, "Makarius" wrote: On 28/08/18 03:00, michael.norr...@data61.csiro.au wrote: >> >> - there is evidently a bug in the position information when the leading delimiter is a Unicode quote mark (the number of bytes gets counted rather than the number of

Re: [Hol-info] Reference cells in HOL4

I'd be happy to see (1) made as a pull request. (Doing it this way gets the Travis CI to automatically check it (at least to some extent).) I agree that (2) is a useful distinction to make. Michael On 30/8/18, 23:27, "Fabian Immler" wrote: Dear HOL4 Developers, In a recent

Re: [Hol-info] Inquiry: Introducing new types as predicates

HOL’s core principle of type definition *is* based on predicates, inasmuch as a new type is constructed by appealing to a non-empty predicate over an existing type to represent the new type. But I guess this doesn’t quite give you the “style” you want. Are you aware of the predicate sub-typing

Re: [Hol-info] HOL Help for Axiom.

Indeed. There is no need to distinguish axioms and axiom schemata (as Thomas said, oracles are not the latter). This is because of the INST and INST_TYPE rules of inference. In a system with schemata, instantiation (or matching) is the way you check whether or not you have an oracle, and you

Re: [Hol-info] "Gordon Computer"

Thanks for digging out this material Larry! I’d be very happy to see it added to our examples directory. Ramana, let me know if you want to make the initial commits. I suggest we can have an examples/hardware with an appropriate README. Best, Michael From: Lawrence Paulson

Re: [Hol-info] About the experimental kernel

Term.lazy_beta_conv, which is in turn called by Thm.Beta and Thm.Specialize. Michael On 12/4/18, 09:50, "Jeremy Dawson" wrote: On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote: > for explicit lazy beta > conversions (with an internal

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

I've never used the Poly/ML debugger. The HOL4 REPL is a custom piece of code (handling the lexing of “...” forms, for example), so I guess this interferes with what the debugger wants to do. If you wanted to use the debugger, you might be able to get things to work by manually use-ing the HOL

Re: [Hol-info] Unexpected failure to considerate equality of lambda terms in Metis and MESON

I'm afraid there is no solution to this problem whereby automatic tools will make lots of progress. First order reasoners such as PROVE_TAC and METIS_TAC try to do a little in this area (converting lambda-expressions to terms involving combinators for example), but this only goes so far, and

[Hol-info] PhD Scholarships at the Australian National University

The Logic and Computation Group at the Research School of Computer Science, The Australian National University has a number of PhD scholarship available for bright, enthusiastic doctoral students in the following fields: - Logic and Linguistics (Ekaterina Lebedeva) - Logic in Computer Science

  1   2   >