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
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 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
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
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
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
> 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
> 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
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
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
`(
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 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
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
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 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
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 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
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
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
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
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
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
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
“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
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
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
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
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
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 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
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:
>
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
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
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
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,
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
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 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
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
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
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
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
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
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
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
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
>
>
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,
>
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
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 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
... 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
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
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
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
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
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
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
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
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
>> I would also like to know if there is any way of defining the
>> reflexive-transitive closure of a relation in a better way (i.e., so
>> that HOL knows what it is and there is no need to prove, for example,
>> that WiresRTC(WiresRTC(a)) = WiresRTC(a)).
>>
RTC is defined in relationTheory, and y
Hi Juan,
Although it is useful, RW_TAC is not the only reasoning tool to
use in HOL, as you are finding. In your example, if you want to
get to a state
> seq IN
> setSeqLast
>(setSeqConcat
> (setSetConcat
>(seqSetConcat (CombBlk {CA (SignalLink (P_s c') s
Juan Perna wrote:
> Hello,
>
> I am needing to transform a goal of the form: "?x.!y. (P x y)" into
> "!y.?x. (P x y)" but I haven't been able to find anything like that in
> the "bool" theory (or anywhere else). I looked for it using:
>
> DB.match ["-"] ``!P. (!x.?y. P) ==> (?y.!x. P)``;
>
Hi Juan,
Seems to be something about the way the goal is stated.
You've got
>> `!a. smPred a ==>
>> !sec c. (a = (c,seq)) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`
If this is restated as
!a. smPred a ==> ?hwa. seqLast (SND a) = Link hwa Empty
then the IHs end up looking like what
This is a situation where type abbreviations probably won't
help you, since you have to mention all the type variables
when writing the abbreviation (just like in ML).
Antiquotations might help. At the ML level you could write
val my_type = ``:('a,'b,'c,'d,'e,'f,'g,'h)my_type``
and then later
ndees 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 enqu
On Dec 27, 2007, at 9:59 AM, [EMAIL PROTECTED] wrote:
> Hi,
>
> pred_setTheory.BIGINTER seems to be a generalized UNION defintion if
> I'm understanding it correctly. for example, suppose..
No, it's a generalized intersection. Here's a version of your example.
We want to show
> BIGINTER {{1
On Dec 22, 2007, at 12:21 PM, [EMAIL PROTECTED] wrote:
> val F_defn = Hol_defn "F"
> `F (x:real) = if x <= 0 then 0 else x + F(x - 0.5)`;
>
>
The "x.y" syntax is used for record field selection in HOL-4.
I got the example to be accepted by using 1/2 instead
of 0.5:
Hol_defn
"Fn"
CALL FOR POSTERS
Tools and Techniques for Verification of System Infrastructure (TTVSI)
http://www.ttvsi.org/
TTVSI is a meeting organized to honour Professor Michael Gordon, a
longtime leader in the field of formal verification. On the occasion
of Professor Gordon's 60th birthday, a two day
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 mod
CALL FOR PARTICIPATION, REGISTRATION, and POSTERS
Tools and Techniques for Verification of System Infrastructure (TTVSI)
http://www.ttvsi.org/
Today's increasingly computer-based society is dependent on the
correctness and reliability of crucial infrastructure, such as
programming languages,
[ Early registration deadline is today. ]
Tools and Techniques for Verification of System Infrastructure (TTVSI)
http://www.ttvsi.org/
Today's increasingly computer-based society is dependent on the
correctness and reliability of crucial infrastructure, such as
programming languages, compi
[ Final Registration Deadline is Friday ]
Tools and Techniques for Verification of System Infrastructure (TTVSI)
http://www.ttvsi.org/
Today's increasingly computer-based society is dependent on the
correctness and reliability of crucial infrastructure, such as
programming languages, compil
On Apr 4, 2008, at 9:51 AM, Augusto Ribeiro wrote:
> Dear All,
>
> Sorry for the extensive background if you prefer please go straight
> to the PROBLEM that is a bit below in the mail.
>
> > BACKGROUND <
>
> I'm trying to use HOL to prove termination of recursive functions
Hi Augusto:
1. One way to control rewriting is to attach a tag to the
rewrite rule that will set a limit on how many times it is
expanded.
RW_TAC arith_ss [Once half]
2. You will need to use induction to prove your goal. You can
use math. induction via
If you now want to see how annoying proof with HOL can be, try to
prove
half (x + 4) = half x + 2
This doesn't need an induction.
Not so annoying: the following works.
RW_TAC arith_ss [Ntimes half 2]
Konrad.
On Apr 7, 2008, at 8:01 PM, Michael Norrish wrote:
val half = Define `half(x)
Hi,
I have a student wanting to translate Michael Norrish's
DPLL example to HOL-Light. Part of that involves
replacing HOL-4's use of the Binarymap structure
with the appropriate thing in HOL-Light. It seemed
like instantiating OCaml's Map functor was the right
approach, but we weren't able to e
> I'm interested in proving termination of nested functions and I
> have some questions:
>
> 1- First I noticed that HOL is able to prove the termination of
> this definition
>automatically:
>
>Define `(ack 0 y = 1 + y)
>/\ (ack (SUC u) 0 = ack u (SUC 0))
>/\ (ack (SUC
Hi Ewa,
When reasoning about recursively defined functions,
you are probably going to have to do an induction,
and also expand out the definition(s) of the functions.
But in the example you have given, it may not even be
necessary to do that. I would separately prove
that function "i" is the i
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 th
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 s
Hi Vladimir,
* It could be that types are different in lemma5_8 and
in your goal. If you try
MATCH_MP_TAC lemma5_8
and it fails, this is probably the case. Then you
should set
show_types := true
and have a look at the types in the goal and the theorem.
* Try METIS_TA
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
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 descriptio
Hi Lu,
See the interface at /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 -> un
Hi Lu,
That message comes from the parser, when
unconstrained type variables remain after
type inference. So it seems that you are making
an invocation
match_term `` ...`` `` ... ``;
where one or both of the terms involved are
being parsed. If you don't want to see any
messages you can
Hi Lu,
If I do the following (MoscowML based HOL),
- app load ["wordsLib","pred_setLib"];
- g `DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
{a | a >= 0x0w /\ a < 0x1000w}`;
- time e
(RW_TAC (srw_ss()) [pred_setTheory.DISJOINT_DEF,
pred_setTheory.EXTENS
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
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 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
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 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
://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 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
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.
--
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.
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
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
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
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
>> 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
1 - 100 of 127 matches
Mail list logo
