Dear Yassmeen,
set comprehensions in HOL are a bit cryptic. They are explained in
Section 5.5.1.1 of the Description manual. In short, something like {t |
p} is syntactic sugar that is turned by the parser into GSPEC(\(x1
,...,xn). (t,p)). The trick is figuring out, which variables x1, ... xn
to u
Dear Haito,
what are you trying to do? HOL theories are ML modules. If you type a
value, the Polyml REPL replies the value. However, as your error message
correctly states, modules are not values. So, the error is what I expect
and not a sign that a module is no longer visible.
So, "combinTheory"
Hi Haitao,
it all depends on what exactly you want to do. Sometimes it is as easy
as using GSYM instead of SYM. Of you can use something like DEPTH_CONV
or ONCE_DEPTH_CONV. That's how GSYM is defined in terms of SYM. Or you
could use something more specialised like STRIP_BINDER_CONV or
STRIP_QUANT
Hi,
I believe this is due to how hol-mode copies input from emacs buffers to
HOL. Look at HOL-DIR/tools/hol-mode.el line 802 ff.
(https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/hol-mode.src#L800).
If a chunk of text you want to send exceeds a certain size, it is
written to a temp-file
Hi Chun,
no, it still does not hold. The problem is that case that "a" might be
infinite and while there is for every element 'e' of 'a' an 'n' with 'e
IN f n' you need arbitrary large ones.
A tiny modification of Ramana's counterexample is
f x := count x
sp := UNIV
a := { n | even n }
Cheers
Hi Chun, Waqar,
"Define" does indeed give priority to earlier clauses. Under the hood
pattern compilation takes place. So what is actually is going on for
> val extreal_add_def = Define`
> (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
> (extreal_add PosInf a = PosInf) /\
> (extr
Hi Chun,
the easiest way is using alpha-equivalence. If you really just want to
rename vars, you can state the new form explicitly and use
apha-equivalence via e.g. ALPHA directly. Tools like METIS_TAC should in
theory be able to do it, but in practice try to do too much and
therefore time out, I
Hi,
hard to say, why it does not work without further details. However, one
guess is that types do not match. I would recommend showing the types
when printing the theorem. I expect that P might be of type `'a ->
bool`. In this case you need to instantiate 'a to string first.
Best
Thomas
On 23
are the
same. I have not checked though.
Or are you interested in a proof of the equality? This would be in the
logic and the statement would actually say that both sides are equal,
not that they have the same beta- and eta-normal form.
If you tell me more about what you want to do, I can perha
Dear Shang,
reading your question, I was wondering, whether you really want to use a
WHILE loop. Usually you would rather use recursion in HOL. In higher
order logic you don't have a state that you can modify. Of course you
can mimic a state by passing it around explicitly. This is what the
WHILE
Hi,
I worked with the other formalisation in "src/temporal" by Klaus
Schneider briefly for my master thesis in 2004/2005 supervised by Prof.
Schneider. As far as I remember (ages ago), one of the main points is a
translation of LTL into symbolically represented omega-automata. There
is a paper by
I'm also not using the Poly/ML debugger and don't think this has high
priority. I was just curious and tried it with an old version I had
lying around. With Poly/ML 5.6 and revision
15e37a5df6ea4b6680e57420257ba30b2e45ceac from 12 July 2017 it did still
work. With the same Poly/ML and a current ver
Sorry, I copied my reply to another thread in the wrong message. Please
ignore it. Thomas
On 07.04.2018 08:43, Thomas Tuerk wrote:
>
> Hi,
>
> higher order matching is decidable, but has a very high complexity.
> (see e.g. "An introduction to decidability of higher-orde
Hi,
higher order matching is decidable, but has a very high complexity. (see
e.g. "An introduction to decidability of higher-order matching", Colin
Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order
unification is undecidable, but matching is decidable. As I understand
it, HOL
Hi,
higher order matching is decidable, but has a very high complexity. (see
e.g. "An introduction to decidability of higher-order matching", Colin
Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order
unification is undecidable, but matching is decidable. As I understand
it, HOL
Hi,
just too clarify. Axioms and oracles are different things in HOL 4. In
the context of HOL 4, an "oracle" usually refers to external proof tool
which is trusted by HOL. Its results are "imported" using HOL's "oracle
mechanism" (mk_oracle_thm and related). Oracles are __not__ axiom
schemata. Axi
Dear Sana,
it is easily possible to define own axioms and inference rules. However,
it very easily leads to inconsistencies and is usually not advisable
expect if you really know what you are doing. In most cases the
definitional extension principles provided by HOL suffice and are much
safer to u
Hi,
the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
description manual). AC normalisation would sort multiple occurrences of
the same operant next to each other. Therefore these multiple
occurrences can then be removed by providing 2 idempotency rewrite rules:
f x x = x
f x (f
Hi Heiko,
you need to load the theory before you can open it. Usually you don't
need to take care of it yourself, because tools like Holmake or the
emacs mode take care of it for you. However, for polyscripter you need a
line like
>>__ load "aTheory"
before you can open it. Often you want to loa
S points to B). Switch S to point to B when convenient
> (now the roles of A and B are swapped).
>
> Is this correct?
>
> Thanks.
>
> On 04/02/18 11:56, Thomas Tuerk wrote:
>> Hi,
>>
>> for this workflow, you don't need to change the absolute location.
Hi,
for this workflow, you don't need to change the absolute location. You
can just choose which of the multiple installed HOL versions to use.
Keep the installation in the same place and just choose which one to use
when. The only trouble with this is that you have to rebuild your own
development
I agree with Konrad. We should keep the hol-info mailing list to discussions
about higher order logic and theorem proving.
Thomas
On 30.01.2018 17:13, Konrad Slind wrote:
> Maybe we can stick to higher order logic? This discussion does not
> belong on hol-info.
>
> Thanks,
> Konrad.
>
>
> On Tu
Hi Liu,
you can't instantiate such a variable. The existential quantifier in
your formula is morally a universal one.
(?x. P x) ==> Q
is equivalent to
!x. (P x ==> Q)
Let's make an example and instantiate P and Q as follows:
P x := (x = 5)
Q := F
Then (?x. P x) ==> Q does not hold. "?x. P x"
Hi Liu,
rewriting applies the provided equations left to write. So if if have
(A = A') /\ (B = B') ==> (f A B)
The simplifier (with std_ss) uses the precondition (A = A') /\ (B = B')
as context and adds the rewrite rules
A -> A'
B -> B'
where "->" is an ad-hoc notation for "=" but only applie
nding function) and combine it with
tacticals. You would end up with something like
fun REWRITE1_TAC thm = CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV thm)))
Depending on your circumstances, ONCE_ASM_REWRITE_TAC or similar
existing tactics might do the trick for you as well.
Cheers
Thomas Tuerk
On 25
Hi Chun,
via a subgoal, you can introduce an assumption for a concrete argument.
This should be what you need. I'm thinking of something like
First show that a CCS q exists with "q <> p"
`?q. q <> p` by ...
Then use this new q as an argument)
`(\t. t) q = (\t. p) q` by PROVE_TAC[]
Now you are
Hi Matthias,
I'm not aware of an easy way. Moreover, for me it is unclear how to
count subgoals. I could well imagine that one wants to count only
"interesting ones", i.e. ignore trivial ones like "Cases_on `x:num` >>
ASM_REWRITE_TAC[...]", where the case for "0" is automatically discarded.
One i
Hi,
I always understood "fail" as raising "HOL_ERR". However, I might be
wrong there.
There is QCONV. If a conversion raises UNCHANGED, it calls REFL. So
QCONV (REWRITE_CONV thms)
is what you are after, I believe.
Thomas
On 05.05.2017 22:09, Chun Tian (binghe) wrote:
> Hi,
>
> The HOL System
Hi Dwi,
I would expect that a
ASM_REWRITE_TAC[]
does the trick. It would take the assumptions as a rewrite and use it to
simplify the goal. In this case, it should simplify the goal to "!s0.
Next s0 x = Next s0 x" which is solved thanks to reflexivity. A problem
might be free type variables, i.
Hi Liu,
I don't know EXTENCE_TAC. I would have used EXISTS_TAC. This shound not
depend on whether "a" is a record type or not. So something like:
Q.EXISTS_TAC `EL n A`
It might be worth looking at REFINE_TAC to partially instantiate the
record and quantifier heuristics (QI_ss) to split the quant
Hi Liu,
you have realLib open. "0" can be parsed as either a real or a num.
That's why you get the warning that two resolutions are possible. The
"EXISTS_TAC ``0``" fails, because ``0`` is parsed as a real, while you
need a num. An explicit type annotation does the trick: So use
e (EXISTS_TAC ``0
IGHT1, etc.)
>
> I hope one day I could learn to use the Holyhammer ...
>
> Regards,
>
> Chun
>
>
> On 7 April 2017 at 12:57, Thomas Tuerk <mailto:tho...@tuerk-brechen.de>> wrote:
>
> Hi Chun,
>
> by the way. I always find DB.match and DB
gt; Hi Thomas,
>
> Thank you very much!! Obviously I didn't know those RTC_ALT* and
> RTC_RIGHT* series of theorems before. Now I can prove something new:)
>
> Best regards,
>
> Chun
>
>
> On 7 April 2017 at 12:08, Thomas Tuerk <mailto:tho...@tuerk-brechen.de>>
Hi,
1) They are the same. You can easily proof with induction (see below).
2) Yes you can prove it. You would also do it via some kind of induction
proof. However there is no need, since it is already present in the
relationTheory as RTC_INDUCT_RIGHT1.
Cheers
Thomas
open relationTheory
val
Hi Liu,
unluckily I don't understand what you want to do. Could you explain a
bit more details, please?
Sorting means for me very much simplified that smaller elements appear
before larger ones. However, there is no "before" or "after" for sets.
You can't say something like "a appears before b in
Hi Chun,
use functional extensionality. There are many ways to do it, one is
using the theorem boolTheory.FUN_EQ_THM.
Best
Thomas
On 24.03.2017 21:42, Chun Tian (binghe) wrote:
> Hi again,
>
> If I have a theorem saying two (2-ary) relations are the same:
>
> |- R = R’
>
> Then I can easily pr
Hello,
many thanks. That does the trick and is much nicer than my hack.
@Magnus Myreen: Do you think this is worth adding to the HOL Interaction
manual?
Thank you,
Thomas Tuerk
On 26.01.2017 22:25, Chun Tian (binghe) wrote:
> I took a look into sml-mode.el and the documentation [1], it se
Hello Heiko,
I have the same issue. I just deactivated electric indent mode. So, its
not a proper solution, but for me it does the trick.
(electric-indent-mode -1)
Best
Thomas Tuerk
On 26.01.2017 09:43, Heiko Becker wrote:
> Hello everyone,
>
> I am currently running into some
HOL_ERR
> {message = "unable to find \"min$fun\" in the TypeBase",
> origin_function = "induction_of", origin_structure = "TypeBase"}
> raised
>
>
> On 18 January 2017 at 13:55, Thomas Tuerk <mailto:tho...@tuerk-brechen.de>&g
ct_of ``:'a form``
TypeBase.one_one_of ``:'a form``
...
Best
Thomas
On 18.01.2017 13:22, Chun Tian (binghe) wrote:
> Hi Thomas,
>
> Oh my god ... I've learnt so much from each line of your reply. Thank
> you so much!
>
> Best regards,
>
> Chun
>
Hi Chun,
you are on the right way with the cases theorem. Essentially you need to
rewrite once with it. Then you end up with
∀A a.(atom a = A) ∨ (∃B C. (atom a = dot B C) ∧ subF A B) ⇒ (A = atom a)
Now you need to use the fact that "atom _ = dot B C" does not hold. This
distinctiveness is proved
assumption is removed, while the version
without X keeps it. So in order to get your old proof working, you just
need to replace "PAT_ASSUM" with "PAT_X_ASSUM".
Best
Thomas Tuerk
On 16.01.2017 19:47, Chun Tian (binghe) wrote:
> Hi,
>
> HOL Reference said that, PAT_ASSU
Hi Armaël,
the syntax you use and that is still used in patternMatchesExamples.ML
was the one used before Michaels changes and the recent merge of the
branch you mention.
I'm not too sure myself, how to use the new one and what the new syntax
is exactly. From looking at Michael's commits and the
Hi Ada,
you can't print the definition from the ML REPL. I expect you use
PolyML. In this case look into the file "POLYML_DIR/basis/List.sml".
There you will find the following definition.
fun find _ [] = NONE
| find f (a::b) = if f a then SOME a else find f b
Best
Thomas
On 21.06.2016 11:18,
args" holds, which would be violated by a function "rand". You can
have underspecified functions though or model randomness /
nondeterminism explicitly.
Best
Thomas Tuerk
On 14/06/16 04:48, Ada wrote:
> Hi,guys
> I am working with HOL4. Now, I need a function that c
oly 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
acc
-
Does anyone have an idea library this error message is about? I briefly
started debugging, but have not put much time into it yet? Has anyone
encountered this problem before.
Best
Thomas Tuerk
--
Mob
Hi Ada,
> But I can't specialize the variaty l in CX_IN with "CAN l".
Why can't you specialise it? What methods have you tried? I would have
expected that SPEC or ISPEC do work. A common problem are mismatched
types. Your definitions look polymorphic to me in the type of list
elements. If on
Hi,
there is "GEN_EXISTS_TAC "y" `5`" from bossLib. It is more general than
what was asked for here originally. It also knows about the usual
boolean connectives.
For example, it can instantiate also
?x. P x /\ ?z y. ... y ...
or with negation
?x. (P x /\ (!z y. ... y ...)) ==> Q x
"GEN_EXIST
(TAKE 0 p = p)``,
PROVE_TAC [TAKE_0, LENGTH_NIL])
There are plenty more ways for doing it. The core operation is rewriting
here. So, perhaps have a look at the rewrite tactics and the simplifier.
Best
Thomas Tuerk
On 15.12.2015 13:48, 康漫 wrote:
> Hi,Ramana,Thanks for your r
Hi,
there is also the GoalTree library. In contrast to the GoalStack one,
expanding a tactic gets the tactic twice. Once as a string and once as a
ML function. This allows the GoalTree to keep track of the proof
stucture and print the tactics used for the proof using THEN, THENL,
etc. at the
Hi,
if you don't like stateful tactics, you should also have a look at the
library "DatatypeSimps". Moreover, it often helps me to turn off pretty
printing of case-expressions via
set_trace "pp_cases" 0
You need rewriting of the "list_CASE" and equality of chars. So, your
goal should also be sol
Hi,
I think, it is even simpler:
SIMP_TAC list_ss [rich_listTheory.DROP_APPEND2]
Best
Thomas
On Wed, 2013-02-27 at 22:10 +, Ramana Kumar wrote:
> Thanks! The secret sauce seems to be EL_APPEND2, and possibly whatever
> is in lrw. (And I should use LIST_EQ_REWRITE more often too.)
> This
tion you might be interested in.
Best
Thomas
On Fri, 2012-12-28 at 07:18 -0500, Vincent Aravantinos wrote:
> Hi Thomas,
>
> Le 27/12/12 07:30, Thomas Tuerk a écrit :
> > On Thu, 2012-12-27 at 19:55 +0800, Ramana Kumar wrote:
> >> There might be something in qua
Hi,
the emacs code is in "tools/hol_mode.el"
A documentation how to install it, can be found in
"Manual/Interaction".
I hope this helps,
Thomas Tuerk
Am Sonntag, den 05.02.2012, 09:26 -0800 schrieb Ian Zimmerman:
> The Kananaskis distribution contains a doc/hol-m
55 matches
Mail list logo
