Re: [Hol-info] Abstract algebra in HOL4 and Isabelle/HOL – Re: Abstract algebra in HOL4 – Re: Release notes for HOL4, Kananaskis-14

> I just want to point out that the goalposts have shifted > slightly. The material pointed to by Michael shows that a fair > bit of basic abstract algebra can be cleanly done in HOL's type > theory, which I gather was the original point in question. > > re: Ken's questions. > > 1. The carrier is

Re: [Hol-info] proof replay?

Just for clarification: the HOL4 term parser handled the supplied term without alteration, and intLib.ARITH_CONV is the HOL4 analog of INT_ARITH. On Thu, Jan 28, 2021 at 6:59 PM Konrad Slind wrote: > Also, there seems to be some inefficiency: the posted formula gets proved > quite q

Re: [Hol-info] proof replay?

HOL4 has a notion of persistent theory, so you could spawn many parallel sessions, each delivering a theory with one result, then create a single descendant theory, import all the parent theories, and chain your implications or inequalities there. It also provides integer decision procedures, so

Re: [Hol-info] EVAL when equations have an antecedent

I think so, for example, if "x" is a concrete term, then EVAL "f x" should return a theorem |- f x = c. However, if function f is only defined for x meeting P, then things may be more fiddly. Konrad. On Thu, Jul 30, 2020 at 2:40 PM Mario Xerxes Castelán Castro < marioxcc...@yandex.com> wrote:

Re: [Hol-info] Using @ for multiple selections in HOL Light

If you have |- !p. ?m c. ... as a theorem, then you are set up to use constant specification. Just have to apply SKOLEM_THM to move the existentials out to the top level . Konrad. On Tue, Feb 18, 2020 at 4:33 PM Norrish, Michael (Data61, Acton) < michael.norr...@data61.csiro.au> wrote: > Maybe

Re: [Hol-info] Simplify/normalize propositional logic terms?

A couple of places to look in HOLindex: refuteLib and normalForms structure. On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) wrote: > Hi, > > it can be proven (by DECIDE_TAC) that, > > |- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x > > but is there any conversion function available in HOL4

Re: [Hol-info] How to express a finite_map or alist using a key list and a value list?

See also examples/balanced_bst/balanced_mapTheory, which has a "fromList" construct. That does have the requirement of having the domain type capable of being ordered. Konrad. On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe) wrote: > Hi, > > I wonder what's the most natural/native way to

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

rically, it is this disadvantage of > >> harder proofs that was the reason for making ``0/0=0`` in HOL. It's > >> much easier for automated routines if they don't have to consider > side > >> conditions. > >> > >> Mark. > &g

Re: [Hol-info] Dealing with INFINITE num set ...

This can be proved by contradiction, using the fact that the set of numbers less than any given number is finite. val lemB = Q.prove (`!N m. INFINITE N ==> ?n. m <= n /\ n IN N`, spose_not_then strip_assume_tac >> `FINITE (count m)` by metis_tac [FINITE_COUNT] >> `N SUBSET (count m)`

Re: [Hol-info] Dealing with INFINITE num set ...

Rephrasing things might bring clarity: load "pred_setLib"; open pred_setTheory; val set_ss = (arith_ss ++ pred_setLib.PRED_SET_ss); val lem = Q.prove (`~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`, rw_tac set_ss [EQ_IMP_THM,SUBSET_DEF,IN_DEF] >- (`FINITE P \/ ?n. P n

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

It's a deliberate choice. See the discussion in Section 1.2 of http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) wrote: > Hi, > > in HOL's realTheory, division is defined

Re: [Hol-info] Confused about Induct_on

I suspect that the order of quantification in the goal is important, since that controls how the induction predicate is instantiated. So try !Gamma A. Gm Gamma A ==> !Gamma'. since that makes it explicit for the machinery. Konrad. On Tue, Jan 15, 2019 at 1:30 AM Chun Tian (binghe)

Re: [Hol-info] New grammar of defining theorems?

Isn't it clear just from the form? Theorem name quote (ML)--> val name = Q.store_thm(name,quote,ML) Theorem name (ML) --> val name = save_thm(name,ML) On Mon, Jan 7, 2019 at 8:34 PM wrote: > Forward and backward give us nice terminology, thanks! It may also be >

Re: [Hol-info] How to do this kind of induction?

... also meant to mention that "Induct_on" and "completeInduct_on" have online documentation. On Sat, Jan 5, 2019 at 3:20 PM Konrad Slind wrote: > There is discussion of something like this in the Euclid's Theorem > tutorial. You can do Induct_on `j - i` or do the tri

Re: [Hol-info] How to do this kind of induction?

There is discussion of something like this in the Euclid's Theorem tutorial. You can do Induct_on `j - i` or do the trick where you prove ?k. j = i + SUC k, eliminate j, and then induct on k. Konrad. On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe) wrote: > sorry, "i ≤ j” should be “i < j”

Re: [Hol-info] Element assignment in structures

I recommend learning about the syntax of HOL a bit more. Also, as Michael suggested (to you or someone else) maybe write the code up first as an SML program and then translate to HOL. In any case, here are some nonsense definitions that HOL allows. They should help you get further. load

Re: [Hol-info] Element assignment in structures

There seems to be some problems with the syntax. For one, the !ch ... on the right hand side of the definition means that the rhs is boolean, which conflicts with the record values being returned by the if-then-else. Konrad. On Wed, Dec 19, 2018 at 8:04 PM 幻＠未来 <849678...@qq.com> wrote: > The

Re: [Hol-info] assumption matching in SPLIT_LT

Seems like the rw[] is breaking the proof into 3 subgoals, and only on the first one is the pop_assum match_mp_tac succeeding. So the proof is failing before it gets to the THEN_LT. Konrad. On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info < hol-info@lists.sourceforge.net> wrote: > Hi,

Re: [Hol-info] How to (automatically) change the names of quantified variables in a theorem?

See also Conv.RENAME_VARS_CONV On Fri, Aug 3, 2018 at 9:00 AM Chun Tian (binghe) wrote: > Hi Thomas, > > thanks very much, now I see the possibility of changing whatever variable > names I want! (I never knew nor needed ALPHA before, although > alpha-conversion is familiar to me) > > —Chun > >

Re: [Hol-info] INST on a theorem

Hi Dylan, 1. Your "EX" is basically the same as listTheory.EXISTS_DEF (in HOL4). If you are in HOL Light, I am sure there is an analogous definition already available. You should use it, since there are lots of theorems proved about it already and you will save on work. 2. The problem is likely

Re: [Hol-info] Tactic

Here's an old-school solution: fun locate P left [] = NONE | locate P left (h::t) = if P h then SOME (rev left, h, t) else locate P (h::left) t; fun ASM_CONJ_TAC (asl,c) = case locate is_conj [] asl of NONE => raise ERR "ASM_CONJ_TAC" "no conj in assums" |

Re: [Hol-info] modelling sequential devices in higher-order logic

In the way Mike and colleagues modelled hardware, a device is modelled as a predicate over the external wires (ports) of the device. Information hiding is achieved by existential quantification (relational composition). The basics of this are laid out in

Re: [Hol-info] About the experimental kernel

End users should see no difference, but occasionally a proof script generated on top of one kernel won't run on the other. That is due to differences in how renaming is implemented in each kernel. For some specific cases, one kernel performs better than the other. The "standard" kernel runs the

Re: [Hol-info] verifying the Gordon computer

The proofs might still run. I'd be keen to help get them going, if they can be dug up. After Tamarack, Brian Graham verified a hardware-level SECD machine while a student of Graham Birtwistle. Perhaps they have running versions of those proofs. Konrad On Sun, Apr 1, 2018 at 4:39 AM, Lawrence

Re: [Hol-info] Gender-neutral pronouns

Maybe we can stick to higher order logic? This discussion does not belong on hol-info. Thanks, Konrad. On Tue, Jan 30, 2018 at 8:58 AM, Mario Xerxes Castelán Castro wrote: > Hello Bram. Welcome to the mailing list. > > On 30/01/18 05:22, Bram Geron wrote: >> I have only

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

Theorems that need to persist between sessions are most easily stored by name in theories. Maybe some kind of PolyML database magic could also be used, I don't know. As far as DB searches, it wouldn't be hard to implement a refined DB search mechanism that first discarded all theorems that met

Re: [Hol-info] INST

Hi Michael, What I think is happening is that each quoted element is being parsed separately. This means that the type of the x in `x` is a type variable while the type of `2` is :num. Since INST (I think) just fails if the two types aren't identical, you get the displayed behaviour. There may

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

Maybe you are thinking of the snow-watching latern? https://www.cl.cam.ac.uk/archive/mjcg/lantern.html Konrad. On Thu, Dec 14, 2017 at 11:23 AM, Mario Castelán Castro < marioxcc...@yandex.com> wrote: > Hello. > > I recall having read that the HOL4 logo (as found in TUTORIAL, MANUAL, >

Re: [Hol-info] On the order of "variable" substitutions in lists or recursive structures

Hi Chun Tian, There are all kinds of issues with substitutions and applying them to term-like structures. I would probably start by choosing finite maps (finite_mapTheory) as the representation for variable substitutions since they get rid of most if not all the issues with ordering of

Re: [Hol-info] Spurious parent theories

When /bin/hol starts up, it is sitting on top of a somewhat ad hoc collection of theories: > ancestry"-"; val it = ["ConseqConv", "quantHeuristics", "patternMatches", "ind_type", "while", "one", "sum", "option", "pair", "combin", "sat", "normalForms", "relation", "min", "bool",

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

Hi Chun Tian, For your Label type the most appropriate primitive type would be sums (co-products). These are formalized in sumTheory, so you could look at that if you are interested. However, I think you might lose some clarity in your formalization by using them. Cheers, Konrad. On Mon, Oct

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

Hi Chun Tian, The constant ALL_DISTINCT in listTheory is what you are looking for, I think. Konrad. On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) wrote: > Hi, > > (I'm new to HOL's listTheory). Suppose I have a list L which contains > possibly duplicated

[Hol-info] Fwd: [mike-gordon-update] sad news

Sad news for hol-info readers, and many others. Mike was a profound influence, a professional and personal inspiration. He is gone too soon. Konrad. -- Forwarded message -- From: Katriel Cohn-Gordon Date: Tue, Aug 22, 2017 at 12:58 PM Subject:

Re: [Hol-info] How to write a general EQ_CONV ?

EVAL_CONV should do it. It is a general-purpose evaluator that works by deduction. It may even be that string_EQ_CONV is implemented in terms of it. The documentation about computeLib in the Description should tell you more. Konrad. On Sat, Jul 22, 2017 at 4:23 PM, Chun Tian (binghe)

Re: [Hol-info] Counting Subgoals in a Proof

To follow up on Thomas' post, you can easily write a tactical that will do such counting. In the following I print out the number, but you could also store it in a reference cell, as Thomas does. fun COUNT_TAC tac g = let val res as (sg,_) = tac g val _ = print

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

Hi Chun Tian, I'd have to look more closely at your desired function to be able to help. But, it's late and my eyes are giving out. If all you are after is to compute free names, maybe there is a better way. The following is what I would do for defining an operation calculating the free

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

To print theory "foo" as html : DB.html_theory "foo"; Konrad. On Fri, Apr 7, 2017 at 6:50 AM, Chun Tian (binghe) wrote: > yes, I know these signature files, I use them too (when the proofs do not > interest me), but I found that, in signatures, all theorems and

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

sly specific variable names were > being used. > > > > Michael > > > > *From: *Konrad Slind <konrad.sl...@gmail.com> > *Date: *Tuesday, 17 January 2017 at 07:41 > *To: *Thomas Tuerk <tho...@tuerk-brechen.de> > *Cc: *HOL-info mailing list <hol-in

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

I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has caused me a lot of pain. I can see the argument for the renaming, but it has broken a lot of proofs. Konrad. On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk wrote: > Hi Chun, > > PAT_ASSUM was renamed to

Re: [Hol-info] How to show the function body in ML?

I think that function is DB.find (PolyML and therefore HOL4 has separate namespaces due to the module system). You can ask the help system about it: help "find"; which will bring up a menu listing all structures known to the help system that have a "find" function in their signature. As

[Hol-info] HOL breakthrough in American politics

“By expanding on pioneering work in the fields of applied statistics, higher-order logic, and number theory, we’ve arrived at a new branch of mathematics that provides for a multitude of feasible outcomes in which Donald Trump is not the 2016 GOP nominee,”

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

gt; still contains RESTRICT. (In my real example, I also needed to provide > a termination tactic for this call, but in the cut down version > termination is proved automatically, but luckily for me the problem > still showed up.) > > Let me know if you figure it out. > > Cheers, &

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

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 Kumar wrote: > I have

Re: [Hol-info] HOL4 build, deps etc.

Quick and superficial answer: A tool called Holdep computes the dependencies by a quick syntacctic analysis of the ML files in the current directory. It then the dependencies in a sub-directory called .HOLMK. Section 6.3 in the Description part of the Manual gives a detailed description of

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

See (in the HOL4 distribution) examples/lambda/* for quite a lot of lambda calculus based on a nominal-sets approach and examples/fsub for the POPLmark challenge Both by Michael Norrish. Konrad. On Sun, Mar 22, 2015 at 3:04 PM, John Harrison jr...@cl.cam.ac.uk wrote: Petros

[Hol-info] request for literature pointers

I made the following claim in a document: user errors in formally modelling artifacts and expressing properties are far more common than errors in the design and implementation of formal methods tools To me this seems uncontroversial, but it would be nice to be able to point to a paper

Re: [Hol-info] CROSS_applied thm.

I am not sure what the problem is: have you done an open pred_setTheory; ? On my machine, the theorem is there: $hol - HOL-4 [Kananaskis 9 (stdknl, built Wed Oct 22 13:44:55 2014)] For introductory

Re: [Hol-info] HOL Light-style parsing in HOL4

Should have mentioned that you should have a look at src/parse/Preterm.{sig,sml} to start. Konrad. On Thu, Oct 23, 2014 at 4:59 PM, Konrad Slind konrad.sl...@gmail.com wrote: I am sure the technologies are fairly similar. In particular, the type of preterms exists in HOL-4 and all kinds

Re: [Hol-info] MAX ELEMENT OF A LIST

Hi, Problem is that the max computed on the tail of the list let max = Max_List l is an element of an option type, so has the form of NONE or SOME m. However, you are directly comparing max with a number. So the type system is angry at you! Try this instead: val Max_List = Define

Re: [Hol-info] MAX ELEMENT OF A LIST

:07 PM, Konrad Slind konrad.sl...@gmail.comwrote: Hi, Problem is that the max computed on the tail of the list let max = Max_List l is an element of an option type, so has the form of NONE or SOME m. However, you are directly comparing max with a number. So the type system is angry

Re: [Hol-info] Learning HOL Light

Konrad, I should definitely read Description's chapter Derived Inference Rules, which seems to be doing much the same thing as I was attempting in my post. I noticed that Gordon Melham's book is only mentioned much later and is not in your bibliography. Could that be because Gordon wrote the

Re: [Hol-info] Learning HOL Light

Osmosis. The original HOL documentation/code included schematic derivations of the derived rules of inference (didn't that make it into Gordon and Melham?). However, the starting point for that is the rather ad hoc collection of primitive rules and axioms that evolved into the ones currently

Re: [Hol-info] Learning HOL Light

Bill: On p 29 of LOGIC, you write that there are constants Tbool, ∀(α→bool)→bool etc. Why aren't there colons? I would have written that as T:bool and ∀:(α→bool)→bool Are the apparent subscripts supposed to indicate colons, or does HOL4 not use colons for type annotations? Throughout the

Re: [Hol-info] Learning HOL Light

My personal feelings on this foundational aspect are that the actual set of axioms isn't that important provided the usual introduction and elimination rules of predicate calculus can be derived from them. My recollection (don't have citations to hand) is that Church originally wanted the untyped

Re: [Hol-info] Learning HOL Light

RE: type bool. I think BOOL_CASES_AX can be derived from choice. There's a topos-flavoured proof (due to Diaconescu?) in Lambek and Scott, which I think John ported to HOL-Light. Konrad. On Sun, Mar 16, 2014 at 7:25 PM, Bill Richter rich...@math.northwestern.edu wrote: I'm trying to

Re: [Hol-info] Gathering references for a simple tutorial of HOL4

There is already some material of this sort. See http://hol.sourceforge.net/documentation.html If you write more such introductory material, please let us know. Thanks, Konrad. On Wed, Jan 29, 2014 at 7:20 AM, Andrea ag...@leicester.ac.uk wrote: Dear all, I am planning to write and

Re: [Hol-info] More on set comprehensions

Hi Rob, The code for HOL4 set abstractions says that the bound variables of a set abstraction {t | p} are the intersection of the free variables of t and p unless either side has no free vars, in which case the bound variables are those of the other side. Also, if t has no free vars, then fail.

Re: [Hol-info] tactic works only once

Could you perhaps tell me what could possibly be behind the behaviour above? Superficial answer: refs Do you get the same behaviour if you invoke t away from the goalstack? t (top_goal()) = t (top_goal()) Konrad. On Sun, Jun 16, 2013 at 3:03 PM, Ramana Kumar

Re: [Hol-info] Learning HOL Light

I bet the information that p, q, and m have type num is stored somewhere. I know we can infer the type num from the assumptions, but that's not always true. Can you tell me where this type information is stored? Every occurrence of a variable in HOL includes the type of the variable. You can

Re: [Hol-info] Array's in proof

assumptions. Thank you for your help and time. Yours sincerely, Jun Jie 2013/4/15 Konrad Slind konrad.sl...@gmail.com Hi JJ: The definition of replace_smaller is fine, but the rest needs some tweaking. My understanding of system_def is the following (I include replace_smaller

Re: [Hol-info] Array's in proof

l Other representation choices include: - functions of type : ‘a word - ty - partial functions : ‘a word |- ty This could make sense if your “int” type is actually a machine word, e.g. ``:word32`` in HOL. Anthony On 11 Apr 2013, at 18:12, Konrad Slind konrad.sl...@gmail.com wrote

Re: [Hol-info] Array's in proof

Hi J.J. : First you have to choose how arrays are modelled, i.e., which HOL type is going to be used to represent arrays. Choices: - functions of type : num - ty - finite functions : num |- ty - lists: ty list - finite products : ty['dim] Summary of the

Re: [Hol-info] Undefined operations such as division by zero in HOL

to work with. -Cris On Thu, Apr 4, 2013 at 4:00 PM, Konrad Slind konrad.sl...@gmail.comwrote: Partial functions are annoying, no matter how you approach them. One way to introduce a partial operation in HOL is with new_specification. In contrast with new_definition, this allows you

Re: [Hol-info] Undefined operations such as division by zero in HOL

Partial functions are annoying, no matter how you approach them. One way to introduce a partial operation in HOL is with new_specification. In contrast with new_definition, this allows you to introduce a constant with only its relevant properties. Consider, for example, the so-called division

[Hol-info] CFP: HCSS 2013

* The NSA Thirteenth Annual HCSS Conference (2013)* *Call for Presentations* *Introduction* The thirteenth annual HCSS Conference will be held May 7-10, 2013 at the Historic Inns of Annapolis in Annapolis, Maryland. You are invited to submit a proposal to present a talk at this year's conference.

Re: [Hol-info] Improve EXISTS_TAC with by taking hints from the assumption list

FYI. Somewhat related functionality is in Q.REFINE_EXISTS_TAC, which can be used to partially instantiate an existential. But you have to supply a witness, instead of saying find a witness in the assumptions. Konrad. On Thu, Dec 27, 2012 at 5:55 AM, Ramana Kumar ram...@member.fsf.org wrote:

Re: [Hol-info] Hol Light -- Where's the Easy button?

Hi John, No it's not that hard. A calculation-like goal such as CARD {3;4} = 2 is a one-liner in HOL4 and I'd be surprised if that wasn't also true in HOL-Light. In HOL4 the one-liner is an invocation of the simplifier, using the implicit set of rewrites, so RW_TAC (srw_ss()) [] solves

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Generally speaking, I'd say that the automation is too powerful is a problem we'd love [miz3] to have! Great! Right now it's not powerful enough for me. Bill, I'm struggling to understand your point of view. Of course, more automation is a good thing, but presumably in your setting

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Does HOL4 have anything comparable to sets.ml? Yes it will have, and it will probably be spread over many source code files, but I'm afraid I don't know where this is in the HOL4 source. This is a question for HOL4 community, Michael et al. I'm more of a HOL Light and HOL Zero person. The

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Konrad, this is very interesting, because it's so much like sets.ml: There is also a description of sets in HOL4 in the manual. Start at p. 102 of the HOL4 Description document: Yours Michael's Description manual starts pretty much like sets.ml which I cited above. Not surprising.

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Anyway, I've asked myself the same question above, when some HOL person will start to implement a version of sections or locales. My estimate is that when starting today, it would take approx. 5 years to make this become real. Our very first version of Isabelle locales can be seen here (14

Re: [Hol-info] How do I reinitialize HOL in the command window?

On Mon, Jun 11, 2012 at 1:12 AM, gottfried.bar...@gmx.com wrote: I'm using HOL4 in the Windows console. I load a file using the use command, like this: use E:/E_main2/binp/HOL4k7/examples/euclid.sml; On windows I usually run HOL4 under emacs. But of course that's just personal preference.

Re: [Hol-info] How do I reinitialize HOL in the command window?

Send (or post) a minimal failing version and the maintainers can help you. I thought it was me causing problems by loading my own scripts after HOL/examples/euclid.sml, but it wasn't. The failure comes from making the divides constant an infix after its definition. All is fine the first time

Re: [Hol-info] [HOL] TypeBasePure.gen_datatype_info undocumented (#65)

Sounds like a bug. Can you send me sources? Thanks, Konrad. On Wed, Jun 6, 2012 at 1:30 PM, Ramana Kumar ramana.ku...@gmail.com wrote: On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind konrad.sl...@gmail.com wrote: Note that Datatype.build_tyinfos is only guaranteed to work on types

Re: [Hol-info] Announcement: Prooftoys visual proof assistant for higher-order logic

You can also check out src/bool/boolScript.sml in the HOL4 distribution where quite a few theorems are proved about the connectives and quantifiers. Those are forward proofs since tactics don't yet exist at that stage of system build. So they should be easy to adapt to your framework. One

Re: [Hol-info] congruence theorems for partial higher-order functions

Short answer: totalize MAP2 and you can prove the desired congruence without mentioning LENGTH. Long answer : you can prove the congruence without the LENGTH l1 = LENGTH l2 clause for a definition of MAP2 that is explicit about what happens when one of the lists is empty and the other is

Re: [Hol-info] Back to HOL again!

On Wed, Sep 28, 2011 at 11:11 PM, Paul Loewenstein lynto...@gmail.com wrote: I'm back on HOL after more than a decade-long hiatus.  How it's improved! Lots more automation than back in the day. Also lots more theories and examples. Konrad.

Re: [Hol-info] [Hol-developers] Hol example: Simple, functional, sound and complete parsing for all context-free grammars

Hi Tom, That would be fine. If you feel a need to mention untidy proofs, just add a mention in the README file. For lemmas, they can sometimes just be put in auxiliary files that the xScript.sml file depends on. I'm not sure if that's what you are asking ... Konrad. On Tue, Apr 26, 2011 at

[Hol-info] Fwd: Rockwell Collins Automated Analysis

Begin forwarded message: From: Rita Gatto rmga...@rockwellcollins.com Date: April 23, 2010 6:33:07 PM CDT To: sl...@cs.utah.edu Subject: Rockwell Collins Automated Analysis Hello Konrad Once again, RC is expanding and has an opening under Matt Wilding in the Automated Analysis group.

Re: [Hol-info] convert HOL formula to latex

Hi Lu, See the interface at holdir/src/emit/EmitTeX.sig. This allows tex to be generated from HOL terms, definitions, theorems and theories. Snippet: val print_term_as_tex : term - unit val print_type_as_tex : hol_type - unit val print_theorem_as_tex : thm

Re: [Hol-info] FOLD and SETSUM

Hi Naeem, 1. op is not the keyword to use. Instead, use either the dollar notation (thus, $+ or arithmetic$+), or the paren notation (+), which is also supported. 2. FOLD on sets is already defined: it is called ITSET. See the Description (page 102) for a short description. 3. Your

Re: [Hol-info] Question on higher order matching

Hi Peter, Your example is actually a first order matching problem and the first order matcher fails: match_term ``\x:'a. y:'b`` ``\x:num. x + x`` handle e = Raise e; Exception raised at Term.raw_match_term error: variable bound by scope The higher order matcher should fail but returns an

Re: [Hol-info] Uncaught exception: Chr

This exception is probably not directly caused by running out of space. Chr is raised by Char.chr : int - char when applied to an int that doesn't map to a char. Konrad. On Oct 14, 2008, at 3:33 AM, Mike Gordon wrote: Does anyone recognise: ! Uncaught exception: ! Chr as a symptom

Re: [Hol-info] How were type variables added to higher order logic?

This prompted me to go back and check Andrews' book An Introduction to Mathematical Logic and Type Theory:To Truth Through Proof. In there, he presents Q_0, which does not have object language type variables. Variables in the meta language are used instead. I wonder why he decided not to use the

Re: [Hol-info] Defining two mutually recursive funtions

On Feb 6, 2008, at 12:54 PM, [EMAIL PROTECTED] wrote: I am trying to defining two mutually recursive funtions. I have to prove termination. HOL has introduced INL and INR defined in the sumTheory. Their introduction has caused a problem for me. Right. Mutually recursive functions are

[Hol-info] Tools and Techniques for Verification of System Infrastructure (Announce)

may present their research. Detailed information about how to submit an abstract for a poster presentation, and to register for the meeting, will be announced in due course. Organizing Committee: Richard Boulton, Icera Joe Hurd, Galois Konrad Slind, University of Utah For all enquiries