> 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 e
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
) + 36152178747194683600721967 ⇔ T:
thm
On Thu, Jan 28, 2021 at 6:57 PM Konrad Slind wrote:
> 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
> t
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 t
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:
>
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
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 suc
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 expr
ng). I understand that, historically, 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.
> &g
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)`
by
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
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&rep=rep1&type=pdf
On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
wrote:
> Hi,
>
> in HOL's realTheory, division is d
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)
wrot
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
> possible
... 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 th
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” a
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 "realLib";
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 f
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,
>
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
>
>
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 t
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"
| S
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
https://www.cl.cam.ac.uk/techreports/UCAM
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 EV
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 Paul
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 just subscribed to this
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 some
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 w
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,
> DESCRIPT
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 replaceme
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", "mar
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
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 elements, and I want to express
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: [mike-gordon-update] sad news
To: mi
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)
wrote:
>
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 ("subgoals"^Int.toString
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 variable
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 definitions
> are sorted in
ng used.
>
>
>
> Michael
>
>
>
> *From: *Konrad Slind
> *Date: *Tuesday, 17 January 2017 at 07:41
> *To: *Thomas Tuerk
> *Cc: *HOL-info mailing list
> *Subject: *Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now?
> (and a theorem cannot
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 PAT_X_ASSUM in June. See commit
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 foll
“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,”
http://www.theonion.com/article/gop-st
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,
> Ramana
>
> On 23 Feb
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 managed to make a definition whe
The 8th NASA Formal Methods Symposium
-
http://crisys.cs.umn.edu/nfm2016
June 07 - June 09 2016
McNamara Alumni Center
University of Minnesota
200 Oak Street S.E., Minneapolis, MN 55455
Theme of the Symposium
--
The widespread use and in
As Michael said, higher order is all over the place, even
if first order reasoning is commonplace. One of my favourite
higher order statements is the following encapsulation of
Skolemization:
SKOLEM_THM;
val it =
|- ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x):
thm
Konrad.
On Wed, Nov 18, 201
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 wha
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 wrote:
>
> Petros writes:
>
> | I have g
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
HI Rob,
I think it would be pretty easy. REWR_CONV and its M-N counterpart
HO_REWR_CONV are built from REWR_CONV0 which takes a "part_match"
function which actually determines how the lhs of the rewrite rule is
matched.
Type variables occurring in the hypotheses of the rewrite rule will not be
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 introducto
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
wrote:
> I am sure the technologies are fairly similar. In particular,
> the type of preterms exists in HOL-4 and all kinds of
&g
I am sure the technologies are fairly similar. In particular,
the type of preterms exists in HOL-4 and all kinds of
syntax manipulation can take place there before typechecking
and term construction.
Konrad.
On Thu, Oct 23, 2014 at 6:00 AM, Piotr Trojanek
wrote:
> Dear all,
>
> is it possible
Hi Gergely:
That work was done in the late 1980s. It may be that
Brian Graham still has the proof scripts available. However,
it would probably be very difficult to build a version of HOL
that would run the scripts as-is. An interesting project would
be to re-do the theories using up-to-date tec
014 at 12:07 PM, Konrad Slind wrote:
> 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
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
`(
Hi David,
Adding extra constraints to the definition of listInsert is what I would
suggest. The
typical thing to do is to add the constraints via if-then-else:
f(x) = if
then
else ARB
You will get a constrained function definition and induction theorem. How
these
> 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
> 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
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 th
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: 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 wrote:
> I'm trying to understand Tom Hales's compact descri
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 wrote:
> Dear all,
>
> I am planning to write and publish a brief Hol4
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.
There is a flag implemented so that the simplifier
tracks which rules are successfully applied. See
simpLib.{track,track_rewrites,used_rewrites}
Konrad.
On Fri, Oct 25, 2013 at 3:47 PM, Ramana Kumar wrote:
> There's no easy way to do this, that I know of, but there are several
> difficult
Globals.max_print_depth
On Mon, Jun 24, 2013 at 10:03 AM, Ramana Kumar wrote:
> Is there a notion of print depth for the HOL printer, to avoid printing
> very large terms in full? (Using PolyML.print_depth doesn't seem to do the
> right thing.)
>
>
> -
> 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 wrote:
> I have run into st
> 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 ca
he page :(.
>
> PS: I think this might be easier if we assume that every element in our
> array is the same, however I have no idea how to express assumptions.
>
> Thank you for your help and time.
>
> Yours sincerely,
>
> Jun Jie
>
>
>
>
>
>
> 20
: ‘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 wrote:
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
condition was chosen as being
> easier to work with.
>
> -Cris
>
>
> On Thu, Apr 4, 2013 at 4:00 PM, Konrad Slind wrote:
>
>> Partial functions are annoying, no matter how you approach them.
>>
>> One way to introduce a partial operation in HOL is with
>>
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 algo
Hi Vincent:
Michael has done a thorough job of documenting the simplifier: see
Section 5.5.4 of the Description.
Konrad.
On Sat, Mar 16, 2013 at 7:38 PM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> The HOL4 Description manual has a section on the simplifier. And yes, it
> sh
*
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.
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 wrote:
> Dear Vincent,
>
> I
Hi Vincent,
Peter Homeier has given a thorough treatment of just this problem some
time ago. It can be found in the structure "dep_rewrite". It seems you have
to load it before opening it. There is documentation in
src/1/dep_rewrite.sml
in the distribution.
Cheers,
Konrad.
On Thu, Nov 22, 20
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 i
> Ok, so if I understand this correctly the validity checks are only in
> place to keep you from going down an inference chain that is guarenteed
> to go no where in making progress towards proving your goal. This being
> only an issue when searching for the proof itself in the interactive
> promp
Hi Gottfried,
I didn't read all of your (long) message. However,
I agree with Josef: conservative extension principles for FOL are
well known, even if not discussed in all set theory texts. I just consulted
two (Shoenfield's "Mathematical Logic" and Moschovakis "Notes on
Set Theory"): the former
>
>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 sett
> 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 surpr
>> 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.
> 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
I wrote:
>> It also suffers from the problem that a polymorphic formula
>> assumed in this way can't be instantiated. Asserting an axiom
>> is more powerful. In HOL4 axiom usage can be tracked in a similar
>> way to how assumptions are propagated, so you can get the same
>> effect as using an assum
> HOL Light just prints them in full, I think. Ah well,
> as I already wrote, this way of working does not appeal
> too much to me anyway :-)
>
> Freek
It also suffers from the problem that a polymorphic formula
assumed in this way can't be instantiated. Asserting an axiom
is more powerful. In HO
>> 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
On Mon, Jun 11, 2012 at 1:12 AM, 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.
> I then edit so
Sounds like a bug. Can you send me sources?
Thanks,
Konrad.
On Wed, Jun 6, 2012 at 1:30 PM, Ramana Kumar wrote:
> On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind wrote:
>>
>> Note that Datatype.build_tyinfos is only guaranteed to work on
>> types that Hol_datatype produce
ot for your reply.
> I'm going to take this discussion onto the mailing list rather than the
> issue tracker.
> Further comments and questions below.
>
> On Wed, Jun 6, 2012 at 6:09 PM, Konrad Slind
>
> wrote:
>>
>> Right, that's exactly the situat
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 exam
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 not.
On Wed, Sep 28, 2011 at 11:11 PM, Paul Loewenstein 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.
--
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 1
://www.cs.utexas.edu/users/kaufmann/itp-trusted-extensions-aug-2010/
There is no registration fee. If you are interested in attending,
please send an email to
konrad.sl...@gmail.com
so that we can plan for numbers.
Regards,
Matt Kaufmann and Konrad Slind (co-organizers)
Mike Gordon (local arrangements
Hi Xiaoyu,
There's a "quick-start" document at
http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf
and the HOL4 release has extensive documentation
in the Manual directory.
Konrad.
On Jun 18, 2010, at 12:57 AM, xiaoyu xu wrote:
Dear everyone,
I have installed ML and HOL4 in window
Begin forwarded message:
From: Rita Gatto
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. Rockwell Collins is pursuing a
Hi Amy,
Matrices are an interesting modelling example, since there are
several
viable approaches. For extreme simplicity, I would use functions of
type
num -> num -> 'a
to represent them. That makes many of the basic operations quite easy.
You will also need to include the rows
Hi Behzad,
A 6000 line term is probably making the parser and/or
type inferencer work very hard. It might be better to
build the term using term constructors such as
mk_neg, mk_conj, mk_disj, mk_exists, etc.
Cheers,
Konrad.
On Sep 16, 2009, at 6:56 PM, Behzad Akbarpour wrote:
> Hi everyone;
Hi Lu,
This is easy to code up in HOL. You can strip
the leading foralls, use INST to replace your variable
by a term and then put all the foralls back, except
for the replaced one:
fun MY_SPEC v tm th =
let val (vs,body) = strip_forall(concl th)
val (_,vs') = Lib.pluck (eq
1 - 100 of 127 matches
Mail list logo
