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
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
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
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) /\
>
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
hough.
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 perhaps help better.
Best
Thomas
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
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
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,
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.
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
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
. 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. You
>> can jus
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
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
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
on) 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.09.2017 20:03,
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
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
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
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,
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
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
)
>
> I hope one day I could learn to use the Holyhammer ...
>
> Regards,
>
> Chun
>
>
> On 7 April 2017 at 12:57, Thomas Tuerk <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wrote:
>
> Hi Chun,
>
> by the way. I always find D
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 <tho...@tuerk-brechen.de
> <mailto:th
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
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
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
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 <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wr
``:'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
>
>
> On 18 January
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
that the 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 <tho...@tue
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,
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
=> (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 reply!
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 solved
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
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-mode subdirectory with a
quick
47 matches
Mail list logo
