d would be greatly appreciated.
- -
Charles Gretton & Michael Norrish
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Do you see the same output in the example as per the Tutorial? If you have
∃x’. x = 0 ∨ x’ = 0
then I’d be very surprised if qexists_tac `0` failed.
Best wishes,
Michael
On 21 Mar 2022, at 03:47, Brian Milnes
mailto:briangmil...@gmail.com>> wrote:
Folks,
What is wrong with the Euclid exa
The right strategy when confronted like a goal such as
LENGTH (APP [] l2) = LENGTH [] + LENGTH l2
is to look at the sub-terms that contain patterns that “should” be simpler.
When I look at the above, I see
APP [] l2
and
LENGTH []
You have equational theorems to hand that have terms mat
I agree that the second conjuncts of each are probably annoying. I'd keep just
the first conjuncts and think about adding
0 < n ==> TAKE n (x::xs) = x::TAKE (n - 1) xs
as well as the analogous one for DROP.
There is as yet no way to remove specific theorems, but there should be (and
there'
Indeed. As Ramana suggested, you should use DEEP_INTRO_TAC in situations like
this.
Michael
On 9 Jun 2016, at 21:05, Rob Arthan
mailto:r...@lemma-one.com>> wrote:
On 9 Jun 2016, at 00:15, Ramana Kumar
mailto:ramana.ku...@cl.cam.ac.uk>> wrote:
Hi Peter,
I'm not sure I can explain why HO_MA
I think modern machinery would probably make a mechanisation that old seem
extremely long-winded and painful. Even if you found the material, which seems
unlikely, it might not be that helpful. Papers describing it would probably be
good to read though...
Michael
On 24 May 2016, at 23:34, Ch
On Tue, May 31, 2016 at 7:57 PM, Michael Norrish
mailto:michael.norr...@nicta.com.au>> wrote:
Dear Peter,
If you use the Emacs mode to select regions and paste them into a *HOL* buffer
(with M-h M-r), then if you precede that command with two C-u "prefixes", you
get the toggl
Dear Peter,
If you use the Emacs mode to select regions and paste them into a *HOL* buffer
(with M-h M-r), then if you precede that command with two C-u "prefixes", you
get the toggling of quiet-declarations before and after.
So, when I'm opening many theories all at once, I select the relevant
For the curious, I believe the relevant reference is
• Lawrence Paulson. A higher-order implementation of rewriting. Science of
Computer Programming, 3(2):119–149, August 1983.
Michael
On 29 May 2016, at 01:08, Rob Arthan
mailto:r...@lemma-one.com>> wrote:
I was trying to find a reference fo
It depends on what term-structure you expect to see as the argument to exp.
If, for example, you were only going to see integer literals there, you could
just use realSyntax.int_of_term:
> realSyntax.int_of_term ``4:real``;
val it = 4i: Arbint.int
> realSyntax.int_of_term ``-5:real`
It looks to me as if you have a very old libpoly installed in /usr/local/lib
(or perhaps somewhere else on your LD_LIBRARY_PATH). I'd guess that you need
to purge those files (and make sure that the 5.6 library files end up there as
well).
Michael
> On 24 May 2016, at 14:50, Thomas Tuerk wro
> On 21 Mar 2016, at 01:18, Ada wrote:
>
> Hi,guys
> I am working with HOL4.
> > val it =
> TAKE n (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
> DROP n (TAKE n (CX l q p) ++ DROP n (CX l p q)) =
> CX l p q
>
> ...
> - e (SRW_TAC [numS
s.sourceforge.net>
You can reach the person managing the list at
hol-info-ow...@lists.sourceforge.net<mailto:hol-info-ow...@lists.sourceforge.net>
When replying, please edit your Subject line so it is more specific
than "Re: Contents of hol-info digest..."
Today's Topics:
1. Re: H
> On 5 Mar 2016, at 09:01, Ramana Kumar wrote:
>
> I think RW_TAC doesn't handle conditional rewrites very well. Try using rw or
> simp instead.
>
RW_TAC handles conditional rewrites in exactly the same way as simp and rw.
If I try RW_TAC list_ss [cx_length] with the repository version of HOL,
I agree: your theorem is hard to prove because you don't have enough
information about FA etc. Can you prove that
mux_list_imp a b sel y ==> (LENGTH y = something)
If you can't, why not adjust mux_list_imp's definition so that you can?
Similarly, it would seem reasonable to have the same pro
Please document somewhere, but yes.
Michael
> On 22 Feb 2016, at 09:24, Ramana Kumar wrote:
>
> So, yes?
>
> On 2 February 2016 at 15:51, Ramana Kumar wrote:
>> On 2 February 2016 at 15:04, Michael Norrish
>> wrote:
>>>
>>> Don't know.
>&g
I guess you are using MoscowML (perhaps because you are on Windows). Is this
right?
Unfortunately, the src/floating-point directory requires Poly/ML, and for the
moment that requires unix of some form.
If you want to use this directory, I'm afraid you must use Unix. If you are
committed to a
The x and y should be universally quantified in Ramana's suggestion:
relations A = { R | !x y. R x y ==> x IN A /\ y IN A }
Michael
> On 21 Nov 2015, at 01:46, Ramana Kumar wrote:
>
> maybe this?
> val relns_def = Define`relns A = { R | R x y ==> x IN A /\ y IN A }`
>
> On 20 November 2015 at
Some of the definitions are higher-order. For example, the universal
quantifier has to be higher order because it's a function that takes a
predicate as an argument.
Even functions like MAP are higher-order because they take functions as
arguments. Often metis is capable of proving useful fac
I just tried it with integers and naturals and both worked:
> EVAL ``WHILE (\x. x = 0n) (\x. x) 1``;
val it =
|- WHILE (λx. x = 0) (λx. x) 1 = 1:
thm
> load "intLib";
<>
val it = (): unit
> show_types := true;
val it = (): unit
> EVAL ``WHILE (\x. x = 0) (\x. x) 1``;
<>
val it =
|- WHILE
There's a little in posetTheory (sources for which are in src/pair/src).
Michael
> On 11 Oct 2015, at 21:00, Ramana Kumar wrote:
>
> Is there any theory about partial orders in HOL4?
>
> I have been party to some work on the partial order of lazy lists under the
> prefix relation (in particular
I'm not sure what you are using when you refer to UPPAAL 4.
Guessing wildly: one way to combine constraints might be to put a conjunction
(/\) between them...
Michael
On 14 Aug 2015, at 23:34, Adnan Rashid Raja
mailto:adnanraja...@yahoo.com>> wrote:
Dear all,
Can anyone please tell me, how w
Initially I thought maybe I do not have the right
> access to the directory and reinstalled it in another drive, but it did not
> work. None of the installations is in the home directory (I’m a Mac user).
>
> Thanks,
> Narges
>
>> On May 8, 2015, at 8:51 AM, Michael Norrish
should cause a .HOLMK directory to be needed.
Michael
> On 8 May 2015, at 16:31, Narges Khakpour wrote:
>
> I am using Poly/ML. This error is raised when I load some specific theories
> like wordsTheory.
>
> Narges
>
>> On May 8, 2015, at 1:58 AM, Michael Norrish
>
Are you using Poly/ML or Moscow ML?
Michael
> On 7 May 2015, at 20:17, Narges kh wrote:
>
> Hello,
>
> When I load a theory in HOL4, I *occasionally* receive the following error
> message:
>
> "Loading wordsTheory
> Couldn't make .HOLMK directory: Permission denied
> Exception- Fail "Couldn't m
The line you saw is just internal logging of the Metis search for a proof. It
can be nice to see that it is still doing something by watching that output.
(Normally, you should just give up if there is too much logging and the goal is
not proved very quickly.)
Michael
On 12 Apr 2015, at 10:3
ou for your guidelines!
>
> -- Piotr
>
> On Fri, Oct 24, 2014 at 12:31 AM, Michael Norrish
> wrote:
>> On 23/10/14 22:00, Piotr Trojanek wrote:
>>> Dear all,
>>
>>> is it possible to use HOL4 parser in a similar way to `parse_preterm`
>>> fro
There’s no direct support for this in the system, though I’d certainly like to
extend Induct so that it supported this.
For the moment, you have to set things up by hand. E.g., arrange for the goal
to look like
!n. EVEN n ==> !m. (n = SUC m) ==> ~EVEN m
before then calling Induct_on `EVEN
The grammar is determined in the same way as when grammars are merged by the
action of loading a bunch of ancestor theories. The safest way to disable reln
in your situation would probably to have a theory that removes the abbreviation
and then is the only thing loaded by the munger. (How do you
r/bar/foo, then dir/bar, it
> works. But Holmake is supposed to do this recursive calling itself in
> dependencies correctly from a single call at the tip.
>
> On Thu, Feb 19, 2015 at 3:48 AM, Michael Norrish <mailto:michael.norr...@nicta.com.au>> wrote:
>
> I’d be kee
I’d be keen to see (preferably relatively small) test-cases for breakages along
these lines. Holmake has changed fairly dramatically in its dependency
analysis over the last few commits to the repository version, and as per the
hol-builds mailing list (to which you should subscribe if you are w
have got better. However, I'm
> using the latest commit and it seems that things are no better and possibly
> worse. I can point you to files that regularly push me out of memory if that
> would be helpful.
>
> On Tue, Feb 3, 2015 at 9:57 PM, Michael Norrish <mailto:micha
memory if that
> would be helpful.
>
> On Tue, Feb 3, 2015 at 9:57 PM, Michael Norrish <mailto:michael.norr...@nicta.com.au>> wrote:
>
> My most recent commit to the repository may fix this problem. We believe
> that
> the issue was with Holdep
My most recent commit to the repository may fix this problem. We believe that
the issue was with Holdep's analysis. That analysis has just changed
significantly. I'd be interested to hear if the problems get better or worse
now.
Michael
On 03/02/15 22:45, Ramana Kumar wrote:
> I often run int
You need to use completeInduct_on, as in
completeInduct_on `m + n`
Best,
Michael
On 12/12/14 09:30, Muhammad Qasim wrote:
> Hello,
>
> I am looking for an alternative of WF_INDUCT_TAC for HOL4. I would be
> greatful if someone can provide good advice. I found a link for this
> tactic but the
As Konrad said, we have two flavours of rewriter. The FREEZE_THEN thm_tactical
can also be used to automate the "trick" whereby free variables get "frozen" in
assumptions. See
http://hol.sourceforge.net/kananaskis-10-helpdocs/help/Docfiles/HTML/Tactic.FREEZE_THEN.html
for documentation. This
Wow; I've never seen anything like this before.
Can you describe what setup you have please? What OS, what SML implementation
etc?
Thanks,
Michael
On 03/12/14 13:26, David Sanán wrote:
> Hi all,
> I recently changed my computer at home and reinstalled everything, including
> HOL4.But after the
ers, whether or not they’re
subscribed. However, now that you’ve prompted me to think about it at all, I
think I can adjust this to be a little less of a barrier.
Thanks,
Michael
> On Mon, Dec 1, 2014 at 7:46 AM, Michael Norrish <mailto:michael.norr...@nicta.com.au>> wrote:
>
How are you using the induction theorem?
I think the safest way would be to write
HO_MATCH_MP_TAC ITSET_IND
If that's what you're doing and you're getting the bad free variable, then I'd
adjust the above to
HO_MATCH_MP_TAC (GEN_ALL ITSET_IND)
I hope this helps,
Michael
On 29/11/14 01
We are pleased to announce the release of the latest version of the HOL4
theorem-proving system.
Download it now from http://hol.sourceforge.net
Michael
--
Release Notes for HOL4, Kananaskis-10
Contents
* New features
* Bugs fixed
* New theories
* New tools
* Examples
*
On 04/11/14 13:33, ＂f~鳓ぁぇ wrote:
> Hi,
> I want to prove a goal like this:
> `case "d" of "u" =>1 |"s" =>2|"d"
> =>3
> |"p" =>4`
> Is there a tactic which can match "d" with the branch "d" and then execute
> this
> branch.
SIMP_TAC (srw_ss()) []
or
On 23/10/14 22:00, Piotr Trojanek wrote:
> Dear all,
> is it possible to use HOL4 parser in a similar way to `parse_preterm`
> from HOL Light?
> In HOL Light one can easily build a parser for HOL terms embedded in a
> custom language (see hol_light/Examples/prog.ml). In HOL4 it seems
> only possi
> On 24 Oct 2014, at 04:59, Ramana Kumar wrote:
> (Userprinters are very difficult to use with the munger, so I would like to
> avoid them if possible.)
Why is this? Note that printing of if-then-else and monad syntax is done by a
user printer in core HOL, and those examples work fine in t
The commands that set them up as syntax should also set up the standard TeX
override map to do this. For example, boolScript.sml includes the following
lines to set up if-then-else:
val _ = TeX_notation {hol = "if", TeX = ("\\HOLKeyword{if}", 2)}
val _ = TeX_notation {hol = "then", TeX
I think the commits you pushed to the repository (a83e2652 and 0802f86b) are
fine fixes for this.
Michael
On 29 Sep 2014, at 2:13 am, Ramana Kumar wrote:
> Hi all,
>
> I'm having trouble figuring out how to add theorems that include string
> literals into my LaTeX document, when the strings m
This is the HOL4 answer to the question.
If you know the name and theory of the constant, then
prim_mk_const {Thy = thy, Name = name}
will give you back the constant “as defined”. So that
type_of (prim_mk_const {Thy = "min", Name = "="})
gives back
val it = ``:α -> α -> bool``: h
On 09/09/14 15:07, Jiaqi Tan wrote:
> I tried to clear the assumption list by appending "THEN (POP_ASSUM (K
> ALL_TAC))"
> to my current list of tactics, but it doesn't clear any of the assumptions. I
> tried using "THEN (POP_ASSUM MP_TAC)" (in place of "K ALL_TAC") as well, and
> it
> only adds
The standard issue with problems like these is a difference in types. Have you
tried examining the goal with show_types on?
Do
show_types := true;
and reprint the goal? Do you really have an instance of A ==> A?
You can also do the following:
match_term ``A ==> A`` (#2 (top_goal());
tha
At the moment, the --quiet option changes Holmake's behaviour, not that of the
executing script file.
For now, I'd suggest
Holmake | grep -v "^Saved.theorem"
Michael
On 29/07/14 19:02, Ramana Kumar wrote:
> Is there some way to turn off the "Saved theorem" etc. messages during a build
> of
al treatment of
> string literals supersede user printers somehow, or have I done something
> wrong?
>
> Maybe Literal.string_literalpp should be overridable?
>
>
> On Fri, Jul 25, 2014 at 7:32 AM, Michael Norrish <mailto:michael.norr...@nicta.com.au>> wrote:
>
>
I can't think of an easy solution for this other than a custom user-level
pretty-printer. You should probably make a feature request so that the TeX
technology can do this itself. (And then think about implementing the feature
request yourself :)
Perhaps the classier implementation route would b
hat we
> would want is general mechanisms for overriding the printer's behaviour that
> don't have to anticipate why we want to do it.
>
> If I understand correctly, what is missing is some way to give preference to
> an
> overload over a listform.
>
>
> On Fr
st as "NIL" I would be fine.
> But I haven't been able to do that. How do you get the pretty-printer to stop
> using the add_listform rule for NIL while retaining it for non-empty lists?
> I tried prefer_form_with_tok but it didn't work.
> On Thu, Jul 24, 2014 a
The latter is how I've done this in the past.
Michael
> On 24 Jul 2014, at 22:16, "Ramana Kumar" wrote:
>
> HOL's pretty-printer usually prints the empty list as "[]", which I believe
> is produced by two separate tokens (one for each bracket) via a "listform"
> parsing/printing rule.
>
> In L
On 23/06/14 02:49, Ramana Kumar wrote:
> Is there a nice way to add user printers to pretty-print lists of different
> types differently?
>
> We've tried using add_user_printer on the pattern ``ls:foo list``, but this
> seems to apply the user printer on other kinds of lists as well.
>
> Looking at
The latest Git checkout seems to work exactly as
> you suggest (thanks). Originally I had been using the version downloaded from
> the main website (not sure if this has been updated since), which did not
> seem to format the datatype declarations so well.
>
> Thanks,
> Matthe
The default method to do this hasn't changed, and the repository version of HOL
will print type declarations with the new style. Thus the command
$ ~/HOL/bin/mkmunge
$ ./munge.exe < foo.htex > foo.tex
$ pdflatex foo.tex
will produce the attached foo.pdf, when given the file foo.htex
Note that any relation A satisfying
!u v z. A u v /\ A u z ==> (u = z)
must be a subset of the identity relation. Specialise the above with x, y, y
and you get
A x y /\ A x y ==> x = y
Michael
On 30/05/14 02:39, David Sanan wrote:
> Hi all,
> I am trying to prove this simple property over
Best practice would probably be to write
`!n. n <= C’ ==> n <> w` by METIS_TAC[]
You can also look at things like Q.SUBGOAL_THEN
Michael
On 13 May 2014, at 6:01 pm, masoume tajvidi wrote:
> Hi ,
> I have a subgoal like this:
>
> F
>
> 0. (
Some options:
METIS_TAC[]
works because first-ordering reasoning with equality is certainly
able to find simple substitutions like this one
SRW_TAC[][]
works because SRW_TAC[][] eliminates simple equalities in the
assumptions, whether they are oriented var = expression or
1. The simplest way would be to put your overloads and abbreviations into a
base theory that your subsequent theories all import. If you must have these
parser changes in a lib file, then this is possible, but you should change the
commands so that they are all "temp" versions. I.e., instead o
On 13/02/14 04:46, Vincent Aravantinos wrote:
> Then considering leaving the goal unchanged, well it is a matter of taste... I
> know it is the standard to leave the goal unchanged. But I personally met many
> buggy situations that I hardly detected because HOL {4,Light} was just
> allowing
> a r
On 4 Jan 2014, at 6:17 pm, Bill Richter wrote:
> To see this, think of a mathematical function f: X ---> Y between sets and a
> subset A of X. Then we speak of the image f(A), which is a subset of Y,
> defined by
>
> f(A) = {f(a) | a ∈ A}.
>
> But what does that mean? I claim it's just a shor
p too.
> Wishes of a happy new year,
>
> Andrea
>
>> On 26/12/13 20:46, Michael Norrish wrote:
>> Please do. If you'd like to, I would be happy to take a pull request so
>> that your sources could go into our main github repository.
>>
>> Micha
Please do. If you'd like to, I would be happy to take a pull request so that
your sources could go into our main github repository.
Michael
On 27 Dec 2013, at 8:26, "Domenico D. D. Masini"
mailto:domenico.mas...@gmail.com>> wrote:
Hello,
I'm studying HOL since some months. I'm not a professi
On 18/12/13 14:56, Bill Richter wrote:
> I tried something like this when you first posted, but I didn't think to use
> dest_comb. Do you have any general tips on how to recognize a term as say a
> combination (which worked here) on an abstraction (not here)?
Try using a match-expression:
ma
Ramana is right: this is a documentation bug.
Michael
On 6 Dec 2013, at 4:27, "Ramana Kumar"
mailto:ram...@member.fsf.org>> wrote:
Hmm... this could be a throwback to a time when the hypotheses were represented
by a list... if so the documentation should be updated. I'm not entirely sure
thou
It’s a general requirement that filenames and structure names linkup, so you
will need to call your file S.sml if it defines a top-level structure called S.
(Or you can rename your structure to be bla.) You can, of course, have
structures named whatever you like within the top-level structure.
An LTL formula is true of a stream of states. A stream of states might usually
be modelled as a function from numbers to states. However, in the development
you're referring to, the states are just numbers, so that the first state of the
stream is number 0, the next is number 1 etc. Moreover, th
This has been fixed. The new documentation and error message behaviour will be
in the next release (expect it soon).
See https://github.com/mn200/HOL/issues/128
Thanks again,
Michael
On 10/08/13 23:45, Rob Arthan wrote:
> I think the section on new_type_definition in the HOL 4 reference manual
Thanks for the bug report!
I've put it into our issue tracker at https://github.com/mn200/HOL/issues/128
Michael
On 10/08/13 23:45, Rob Arthan wrote:
> I think the section on new_type_definition in the HOL 4 reference manual
> should
> say that it fails if the theorem in the parameter has free
There's a chunk of stuff in examples/set-theory/hol_sets/cardinalTheory,
including, for example, the fact that k x k = k.
Michael
On 09/08/2013, at 17:15, "Ramana Kumar" wrote:
> HOL Light has a decent body of theory about cardinality inequalities and
> arithmetic for sets-as-predicates.
> F
Cute!
Michael
On 28/06/2013, at 23:36, Tjark Weber wrote:
> Hi,
>
> I've used Gource [1] to visualize the development history (as recorded
> in public repository logs) of Coq, HOL4 and Isabelle. Enjoy!
>
> 14 years of Coq development:
> http://youtu.be/qyM4D6-623A
>
> 14 years of HOL4 develo
Due to author request, we have extended the final submission deadline until
Monday, 17 June.
Thanks for submitting to CPP 2013!
--
Michael
---
3rd International Conference on Certified Programs and Proofs (CPP2013)
) &
Michael Norrish (NICTA)
:General Chair:
Peter Schachte, *University of Melbourne*
:Website:
http://cpp2013.forge.nicta.com.au
Program Committee
^
= ===
Derek Dreyer MPI-SWS
William Fa
among the targets. One author of each
accepted paper is expected to present it at the conference.
Organisation
:Program Co-Chairs:
Georges Gonthier (Microsoft Research Cambridge) &
Michael Norrish (NICTA)
:General Chair:
Peter Schachte, *University of Melbourne*
:Web
How do you "open it using hol.bat"?
There are a few ways to feed files to HOL. One way is with a command line
redirect:
$ hol < myfile
Another is by calling use within HOL:
> use "myfile";
However, the best way is to set the file up so that its can be compiled with
Holmake. For thi
On 09/04/13 14:40, Albert Y. C. Lai wrote:
> This can be written in Haskell as:
>do {
> q0 <- x/y;
> q1 <- b/c;
> return (q0 + q1)
>}
If you have defined / to return options as Albert suggests, the above can be
mimicked with HOL4's support for monad syntax.
You'd need to
On 10/04/13 05:46, Cris Perdue wrote:
> I think this systematizes the approach that leads to using x != 0 ==> recip x
> *
> x = 1 as a specification for reciprocal, or Konrad's example with DIV and MOD.
> Hopefully I am not missing something here.
Taking definedness to the level Freek is discuss
There are manual examples in llistScript.sml and lbtreeScript.sml (both in
src/llist). The predicate lrep_ok which characterises the subset of the
representing type for "lazy lists" is coinductive. There are inversion and
induction theorems proved for this constant. Something pretty similar is do
Belatedly: the constant behind HOL4's set comprehensions, GSPEC, is really just
a version of IMAGE, so if you can think of a monotonicity theorem for IMAGE,
that should be something you could transform to be suitable for GSPEC too.
Michael
On 04/04/13 00:56, Ramana Kumar wrote:
> I found a way ar
Gonthier (Microsoft Research Cambridge) &
Michael Norrish (NICTA)
:General Chair:
Peter Schachte, *University of Melbourne*
Program Committee
^
= ===
Derek Dreyer Max Planck Institute
William Fa
I'm not sure I necessarily understand all of your question, but it seems
as if you are hoping to prove the
(x * y = 0) <=> (x = 0) \/ (y = 0)
property for multiplication in your linear space. Your vectors are
lists of coefficients, so that x = 0 really means that the list x
consists only of z
The HOL4 Description manual has a section on the simplifier. And yes, it
should preserve the probability of goals because at the top level, it is only
capable of replacing equals with equals.
Michael
On 17/03/2013, at 10:46, Vincent Aravantinos
wrote:
> Hi list,
>
> I have two questions a
On 08/02/13 10:43, Michael Norrish wrote:
> On 08/02/13 09:09, Ramana Kumar wrote:
>> There is a polyml package in the Ubuntu package repositories, but I think it
>> is
>> probably quite old (around version 5.2). Still, it would be usable.
>
> Unfortunately, Kananas
On 08/02/13 09:09, Ramana Kumar wrote:
> There is a polyml package in the Ubuntu package repositories, but I think it
> is
> probably quite old (around version 5.2). Still, it would be usable.
Unfortunately, Kananaskis-8, as released, doesn't work with polyml5.2.
I'd recommend upgrading to a mor
Did you let build run until you saw the message "HOL built successfully"? It
takes a while. My guess is that you closed your terminal before HOL was
actually built.
Michael
On 06/02/2013, at 7:17, "J. J. W." wrote:
> Dear all,
>
> I am using Mint 13 and already have installed PolyML 5.5 su
This is fixed in the repository, as of commit d7be44f. You may find that
set_trace "pp_array_types" 0
will give you an acceptable workaround if you can't upgrade.
Michael
On 26/01/2013, at 1:17, hamed nemati wrote:
>
> Hi all,
>
> I would appreciate if someone could help me to find ou
On 26/01/13 1:17 AM, hamed nemati wrote:
> I would appreciate if someone could help me to find out how I can force
> the Hol4 to print its output in a user defined format. For example,
> using the following code snippet:
> type_abbrev("u8", ``:bool[8]``);
> val user_plus_def = Define `(user_pl
On 16/01/13 19:49, Yuntao Peng wrote:
> Now there is a goals I want to prove [...]
> Thanks to the listTheory is base on real, so I can not use its theorem.
I’m not sure what you mean by this last sentence. Certainly, the theory of
lists (listTheory) is not tied to real numbers at all.
Also, as
Note that Ramana's proof will only work if you first
open lcsymtacs
Michael
On 17/01/13 01:40, Ramana Kumar wrote:
> By the way, your listAdd function is almost equal to ``list$MAP2
> complex_add``,
> and if you used that, you could use rich_listTheory.LENGTH_MAP2.
>
> To prove your goal, ju
On 15/01/13 20:13, Bill Richter wrote:
> In HOL Light vectors, there's something like type quantification,
> and I thought that wasn't possible in HOL.
> First, I could not find an HOL4 analogue of HOL Light vectors. The
> basic idea seems to be that to define the type operator ^ which
> yields t
On 28/12/2012, at 23:07, Vincent Aravantinos
wrote:
> Le 27/12/12 06:55, Ramana Kumar a écrit :
>> Do you have a clone of the HOL4 git repository? You could make a pull
>> request on github after adding HINT_EXISTS_TAC in an appropriate place.
>
> I'd totally be ready to do this, but I would l
HOL4’s SATISFY_ss (from SatisfySimps) should solve this problem (particularly
now that Thomas Türk has fixed a bug in its code).
Michael
On 27/12/2012, at 11:42, Ramana Kumar wrote:
> For what it's worth, my usual move in this situation is to do
>
> qmatch_assum_abbrev_tac 'P t' >>
> qexists_
On 18/12/12 6:04 PM, Bill Richter wrote:
> But I really don't understand why Michael's STRIP_TAC works. P 48 of the
> tutorial says
> STRIP_TAC has the effect of DISCH_TAC, GEN_TAC or CONJ_TAC.
> At the time we use it, we have only the goal
> `(?s. s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m
On 17/12/12 03:19, Petros Papapanagiotou wrote:
> Hello Bill,
> On 13/12/2012 10:32, Bill Richter wrote:
>> Let's try to port this proof to HOL Light up to qDef:
>> g `addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q`;;
>> e(SIMP_TAC[addN]);;
>> e(DISCH_THEN(X_CHOOSE_TAC `s: num->num`));;
>> e(SUBGOA
Note that this approach will fail if the term to be rewritten is under a
variable binding.
MP_REWRITE_TAC REAL_DIV_REFL ([], ``!x. x <> 0 ==> P (x/x)``)
gives back an unprovable x <> 0 as a new subgoal, and also fails to simplify the
bound x/x in the “original” branch. (Put `x*x + 1` in `x` if
On 19/11/12 11:01, Michael Norrish wrote:
> Ignoring abbreviations, you could use
> fun simpterm q =
> ASSUM_LIST (fn ths => Q_TAC (ASSUME_TAC o SIMP_CONV (srw_ss()) ths) q)
> This simplifies the term corresponding to assumption q and gives you back the
> resulting assu
On 19/11/12 03:46, Ramana Kumar wrote:
> Thanks for those.
> I just used
> IMP_RES_THEN (assume_tac o SIMP_RULE(srw_ss())[])
> (METIS_PROVE[]``Abbrev(x=y)==>(x.out = y.out)``)
> which worked great for getting an equation for the x.out of every x, but I'm
> not
> sure if I can get it for just one
On 16/11/12 12:28 PM, John Harrison wrote:
> Michael wrote:
> | As Ramana said, I recently proved this (every set can be well-ordered) as
> | part of my development of the ordinal numbers. I needed Scott Owens'
> | earlier proof of Zorn's Lemma. My proof is in
> | examples/set-theory/hol_sets, i
1 - 100 of 253 matches
Mail list logo
