Hi Konrad,
Thanks for your comments. I know a little about sum types but never go chances
to use it. I’m going to keep my current Action type (based on optionTheory) and
not touch the Label type.
Regards,
Chun Tian
> Il giorno 09 ott 2017, alle ore 15:44, Konrad Slind
> ha scritto:
&
gh to be
uncountable?)
Regards,
Chun Tian
[1] Norrish, M., Huffman, B.: Ordinals in HOL: Transfinite Arithmetic up to
(and Beyond) w1. (2013).
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
C
e types, or simple sum or prod types based on new types
(i.e. defined by Datatype or type bijections, etc).
Regards,
Chun Tian
> Il giorno 10 ott 2017, alle ore 00:32,
> ha scritto:
>
> I think this is a case of “try it and see”.
>
> As per Konrad, it might be more natural to u
“e” into
(DELETE_ELEMENT e L) I got the original list L?
Regards,
Chun Tian
> Il giorno 02 lug 2017, alle ore 10:23, Ramana Kumar
> ha scritto:
>
> Sure, that's fine. I probably wouldn't even define such a constant but would
> instead use ``FILTER ((<>) x) ls``
me summarize them again:
1. How to express the cardinality of a set as “cardinal numbers” in HOL?
2. How to find a larger ordinal for a set of custom-defined datatype, when
their type variables are related?
Best regards,
Chun Tian
[1]
https://github.com/binghe/informatica-public/blob/master/thesi
m N. m < n ∧ n ≤ N ⇒ ¬(lts m (Klop a N) ≈ lts n (Klop a N))
And all my proof scripts can be found at [1]. These’re new developments,
they’re not in HOL’s example/CCS folder.
[1] https://github.com/binghe/informatica-public/tree/master/thesis
> Il giorno 12 ott 2017, alle ore 11:51, Chun
My structure can contain (‘a ordinals) as part of it, and I have a function,
given any ordinal N, for all n < N, f(n) is a different value of my structure
(which contains ordinal too). Its cardinality must be very huge, and that’s the
only thing I know.
—Chun
> Il giorno 12 ott 2017, alle ore
Well, after reading a paper [1] on Isabelle’s cardinals, I started to think:
maybe what’s “missing" in HOL4 is a theory of “Cardinal Arithmetic” - the
current cardinalTheory can only express the relative cardinality between two
sets (cardleq). Michael’s work [2] was mainly on ordinals and ordi
⁺ = (c2a α)⁺) ∧
∀α. 0o < α ∧ islimit α ⇒ (c2a α = sup (IMAGE c2a (preds α))):
thm
Is my definition correct? (especially for the “lf” part using “sup”) And if
so, what properties can I expect from this function? Is it at least monotone?
i.e.
∀m n. m ≤ n ⇒ c2a m ≤ c2a n
Reg
I’m using HOL built from latest Git “master” branch; you’re using HOL
Kananaskis-11 release.
—Chun
> Il giorno 16 ott 2017, alle ore 17:01, Mario Castelán Castro
> ha scritto:
>
> On 16/10/17 09:35, Chun Tian (binghe) wrote:
>> I'm fine with constant overloading. But
/\ ALL_IDENTICAL
t))`;
But the definition is ugly and a little long. Any suggestion on a better
definition? Thanks.
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant
Thanks, I’m going to use: ALL_IDENTICAL t = ?x. !y. MEM y t ==> y = x
> Il giorno 19 ott 2017, alle ore 22:57, Mario Castelán Castro
> ha scritto:
>
> If you want to allow the empty list then:
>
> “∀x y. MEM x l ∧ MEM y l ⇒ x = y”
>
> or:
>
> “∃x. set l ⊆ x”.
>
> or:
>
> “∃x. MEM y l ⇒ y =
probably should use the theory of “paths” for this sort of thing.
>
> See the description in the DESCRIPTION manual, and the theory itself in
> src/path
>
> Michael
>
> From: "Chun Tian (binghe)"
> Date: Thursday, 5 October 2017 at 23:35
> To: hol-info
>
f Ps also contains variables, the resulting term
may not be unique any more.)
How can expression this property (e.g. in listTheory)? What’s the name of this
phenomena? and what’s the idea in its proof?
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP usin
Hi Konrad,
Thank you very much! I’m learning finite_mapTheory now.
Regards,
Chun
> Il giorno 23 ott 2017, alle ore 20:42, Konrad Slind
> ha scritto:
>
> Hi Chun Tian,
>
> There are all kinds of issues with substitutions and applying them to
> term-like
> stru
HOL doesn’t rebuild everything when you re-run “bin/build”: it only rebuilds
changed theories and all dependencies. Sometimes you need to re-run “poly <
tools/smart-configure.sml” and rebuild everything, other times you need to
clean everything “bin/build cleanAll” to fix the building process.
> Il giorno 25 ott 2017, alle ore 21:37, Mario Castelán Castro
> ha scritto:
>
> On 25/10/17 14:29, Chun Tian wrote:
>> HOL doesn’t rebuild everything when you re-run “bin/build”: it only rebuilds
>> changed theories and all dependencies. Sometimes you need to re-run
ls) X
And in all theorems I only use “Fix”. Is this possible (as a cheap solution)
for resolving the “structural congruences” issue?
Regards,
Chun Tian
[1] Homeier, P.V.: Higher Order Quotients in Higher Order Logic. preparation;
draft available at http://www cis …. (1969).
> Il giorno 27
> Il giorno 27 ott 2017, alle ore 17:35, Chun Tian ha
> scritto:
>
> Thanks for your comments.
>
> If I quotient [1] the original CCS datatype into another one, I could expect
> to have the a “fix” constructor with a finite map, right?
>
> On the the other side
ure merged into the BNF_datatype.
Anyway, this is long-term plan, I don’t make any promise. And thanks so much
for all the help I got from HOL community!
Regards,
Chun Tian
[1] Traytel, D., Popescu, A.: Foundational, compositional (co) datatypes for
higher-order logic: Category theory applied
Hi,
I didn't follow the entire discussions about “Gordon computer”, but if you just
want to run HOL88, that’s easy.
All you need to do is an Ubuntu 16.04 Linux environment (or Debian GNU/Linux),
and install the “hol88” (and other hol88-*) packages [1, 2]. Latest version is
“2.02.19940316”.
Bu
I also observed the same: it was working but now it doesn’t work.
Without that debugger I couldn't have finished my thesis work in which there’s
a huge recursive SML function of 400+ lines [1] to compute the transitions from
any CCS term and returns a theorem.
—Chun
[1]
https://github.com/HOL
Hi Michael,
I… took some time trying to find out the revision which breaks the debugging
facility. After many rounds of binary searching, I found that, until the
following revision
e5fc0f365922cfd11ec32c4531983d20892777a6 (Improving naming of
bit-vector signed division constants…) on S
s might be
> done on the Poly/ML mailing list. Such tweaking would almost certainly have
> to be done against the code in tools-poly/holrepl.ML, which is basically a
> slightly adjusted copy of code from the Poly/ML sources.
>
> Michael
>
> On 29/4/18, 02:56, "Chun Ti
Hi,
I saw how the new LTL formalization (in `examples/logic/ltl`) by Simon Jantsch
suddenly appeared in the past months and because more and more complete also
with help of HOL maintainers. But there’s already an older LTL formalization
(in `src/temporal`) since long time ago, done by Klaus Sch
Hi,
not only SBCL but all Common Lisp platforms must implement DISASSEMBLE [1] as
it’s part of the standard (although outputs are platform-dependent). In ML
world, such facility must be platform dependent, if it exists.
[1]
http://www.lispworks.com/documentation/HyperSpec/Body/f_disass.htm#dis
I’m not going to answer these questions in HOL mailing list. You need to
subscribe to Poly/ML mailing list and ask there.
—Chun
> Il giorno 19 mag 2018, alle ore 17:27, Mario Xerxes Castelán Castro
> ha scritto:
>
> On 18/05/18 16:40, Chun Tian wrote:
>
>> Hi,
>>
e thing.
>
> It's also obviously useful to have a type corresponding to the syntax if you
> are going to define computable functions to traverse over it and transform it
> into automata (as is done in our work).
>
> Michael
>
> On 19/5/18, 00:42, "Chun Tian"
ls before making a decision on which
one to base upon.
Regards,
Chun Tian
> Il giorno 21 mag 2018, alle ore 19:30, Thomas Tuerk
> ha scritto:
>
> Hi,
>
> I worked with the other formalisation in "src/temporal" by Klaus Schneider
> briefly for my master thesis in
; Building directory tools/set_mtime [22 May, 22:24:34]
> Holmake failed with exception: Subscript
> Build failed in directory /home/adarbari/HOL/tools/set_mtime (exited with
> code 1)
>
>
>
> --
>
> Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)
> Founder & CEO
>
ile in tools/set_mtime out of the way
> and call
>
> Holmake --poly_not_hol --no_sigobj --qof
>
> in that directory?
>
> Michael
>
>
> On 23/5/18, 07:53, "Chun Tian" wrote:
>
> I’m not 100% sure, but the keyword “Subscript” seems related to
Hi,
I saw the following definition in the current pending request (vector theory
#513):
val INVERSE_DEF = Define `INVERSE f = \y. @x. f x = y`;
But isn’t this too common to be already somewhere in HOL’s theory library? If
so, where is it?
Regards,
Chun
signature.asc
Description:
Hi,
(I’m trying to convert the current pending PR into acceptable code changes)
in pred_setTheory, I saw there’s a definition of PERMUTES (permutation
functions over a set) as overloading of BIJ (bijections):
val _ = overload_on("PERMUTES", ``\f s. BIJ f s s``);
val _ = set_fixity "PERMUTES" (I
s one wants to prove. In
> particular, the definition approach only lets one function serve as a
> particular permutation. The BIJ-overload approach will let many functions be
> the "same" permutation.
>
> Michael
>
> On 28/5/18, 19:01, "Chun Tian"
Hi,
you should reply something meaningful unless you don’t know what’s your *real*
problem (and what others are talking about).
"ML for the working programmer” is a book teaching you how to writing program
in Standard ML, you’ll learn how to manipulate ML lists in that book. If you
want to us
Besides, I don’t think your original goal is true: the variable L is free in
LHS, but bound in RHS, as shown in different colors.
Chun
Inviato da iPhone
> Il giorno 26 ott 2019, alle ore 17:18, Yassmeen Derhalli
> ha scritto:
>
>
> Dear Thomas,
>
> Thank you so much for your elaborated re
Hi all,
But still, PolyML 5.6 is not supported yet, right? I have to use latest
Poly ML 5.5.x to build HOL4 (Git master) on Mac OS X.
Regards,
Chun Tian (binghe)
University of Bologna
On 24 May 2016 at 07:29, Thomas Tuerk wrote:
> Hi Michael,
>
> thanks. That did the trick. The new
after a full clean up of my HOL working directory, with all .HOLMK and
.hollogs directories deleted (otherwise I still can't build), I finally
managed to build latest HOL with PolyML 5.6, for the first time.
Thanks again.
Regards,
Chun Tian (binghe)
University of Bologna, Italy
On 24 May
r if the related HOL
theory scripts are still available somewhere on Internet?
Regards,
--
Chun Tian (binghe)
University of Bologna, Italy
[1] http://128.232.0.20/techreports/UCAM-CL-TR-278.pdf
--
Mobile security can be
tion
that I could define using HOL’s Define, but in HOL named like Ax,
RightSlash, … are just names of theorems, and there’s no concept of “proof”
defined so far, so I have no way to express the degree of a proof itself !!
I’m stuck here
Hi Yong,
thank you very much! Now I understand the situation much better:)
Regards,
Chun Tian
> Il giorno 12/gen/2017, alle ore 17:28, Yong Kiam ha
> scritto:
>
> Hi,
>
> I formalized cut elimination for a version of ordered logic (related to the
> Lambek calculus)
? (it’s actually part of the HOL-ACL2 bridge, defined in
“examples/acl2/ml/fmap_encodeScript.sml”)
Best regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on
by comparing the proof of probability theorems between K10
and K11, while PAT_X_ASSUM is not mentioned in the manual at all. How to
proceed? I write a reference page for it?
Regards,
Chun
> Il giorno 16/gen/2017, alle ore 19:47, Chun Tian (binghe)
> ha scritto:
>
> Hi,
>
; though, so thank you very much for writing those!
>
> Michael
>
> On 17/1/17, 05:47, "Chun Tian (binghe)" wrote:
>
> Hi,
>
> HOL Reference said that, PAT_ASSUM "Finds the first assumption that
> matches the term argument, applies the theorem tactic
Sorry, I re-checked my Isabelle environment and found that the PolyML in
Isabelle is actually built by GCC (mingw versions), so my statement about
"PolyML cannot be built in ..." was completely wrong. The rest ideas should
still hold.
On 17 January 2017 at 13:36, Chun Tian (binghe)
wr
Atoms) (at_ : Atoms),
subFormula A (At at_) -> A = At at_.
intros Atoms A at_ H.
inversion H.
reflexivity.
Qed.
Need help ...
Regards,
Chun Tian (binghe)
University of Bologna (Italy)
--
Check out the vi
inting out the hidden Mercurial repository of
Isabelle [1] ^_^ Now I can see how "active" it is for a "not dying" theorem
prover: stable 10-20 code commits on everyday basis, and new theories keep
going into core Isabelle libraries.
Regards,
Chun Tian
[1] hg clone http://isa
val form_ss = DatatypeSimps.type_rewrites_ss [``:'a form``]
>
> val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,
>
> ONCE_REWRITE_TAC [subF_cases] THEN
> SIMP_TAC (std_ss++form_ss) [])
>
>
> I hope this helps
>
> Thomas
>
> On
; are collected. It is used by tools like the case or induct tactics. So,
> some other nice way of getting such theorems is
>
> TypeBase.fetch ``:'a form``
>
> or specialized ones via
>
> TypeBase.distinct_of ``:'a form``
> TypeBase.one_one_of ``:'a form``
>
sig"
> defines a map "rule_induction_map" that contains these induction theorems.
>
> If you want to get your hands on the strong induction theorem, I would
> use DB.fetch, i.e.
>
> DB.fetch "-" "R_strongind"
>
> Cheers
>
> Thomas
>
orem could help us to prove things like:
If ... (e.g. x is John), then x is a Man.
Also recall in Wikipedia's "Coinduction" page [1], it says "As a definition
or specification, coinduction describes how an object may be "observed",
"broken down" or "dest
on theorem too
but no need to return it explicitly, like the R_strongind theorem.
On 20 January 2017 at 12:07, Chun Tian (binghe)
wrote:
> Hi Michael,
>
> It took me some time to think about your words and learn co-induction. I'm
> no expert, but I don't agree with the o
List, then l is List.
>
> In fact the only subset satisfying these (which is therefore both the
> least and the greatest) is the set of all lists.
>
> Think instead about
>
> Hol_reln `P (SUC n) ==> P n` ; (* no numbers *)
> Hol_coreln `Q (SUC n) ==> Q n` ; (* all
nciple.
>
> Q.prove (
> `!n. Q n`,
> rw [] >> irule Q_coind >> qexists_tac `\x. T` >> rw []);
>
> Scott
>
>> On 2017/01/20, at 17:10, Chun Tian (binghe) wrote:
>>
>> Hi,
>>
>> Well, I tried your definitions about P and Q, th
MP, but how can I combine these
tools into a single tactic to execute? (or there’s another more straight way to
achieve the same purpose?)
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGM
Hi Ramana,
Thank you, it’s perfect. (I replaced FIRST_X_ASSUM with POP_ASSUM in my case)
Regards,
Chun
> Il giorno 20 gen 2017, alle ore 22:25, Ramana Kumar
> ha scritto:
>
> How about this? first_x_assum(strip_assume_tac o MATCH_MP th)
>
> On 21 January 2017 at 06:39,
equent E Delta A) rule derlist; H2]) =
MAX (MAX (degreeFormula A) (degreeProof (Der (Sequent E Delta A) rule
derlist)))
(degreeProof H2))`;
All my code written so far can be found here [5, 6]. I haven’t fully finished
the formal proof of Cut Elimination theorem, that wil
becomes HOL. And these proof scripts are NOT my original work, they all
belong to Professor Monica Nesi. I just do the porting.
Regards,
Chun Tian
[1] https://github.com/binghe/informatica-public/blob/master/CCS/CCSScript.sml
[2] http://homepages.inf.ed.ac.uk/perdita/cwb/
> Il giorno 04 giu 2
nefit from AND1_THM (|- ∀t1 t2. t1 ∧ t2 ⇒ t1),
or there’s a better method to do the whole thing?
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech comm
Hi Michael,
Thank you very much! Then I’ll create a PR once the work at my side is done.
Best regards,
Chun
> Il giorno 22 gen 2017, alle ore 23:16,
> ha scritto:
>
> Hi Chun Tian,
>
> I agree that a CCS example would be very appealing.
>
> I’m also very happy t
e conjunctions. (This has the
> issue that it might disturb other universal quantifications within the P or
> Q…)
>
> Michael
>
> On 23/1/17, 09:08, "Chun Tian (binghe)" wrote:
>
>Hi,
>
>suppose I have the following theorem:
>
&
I took a look into sml-mode.el and the documentation [1], it seems that the
following Emacs configuration could disable the auto-indent triggered by return
key:
(defun my-sml-mode-hook ()
"Local defaults for SML mode"
(setq electric-indent-chars '()))
(add-hook 'sml-mode-hook 'my-sml-mode-h
x))
--> (X x)`;
Can anyone suggest a correct way to define the “AE” syntax?
P. S. furthermore, is it possible to define a pretty printer for the last
definition “converge_AE p X_n X”, to make it printing into the following form?
X_n --> X (p-a.e.)
Best Regards,
C
n x. (S' n x − expectation p (S' n)) / &n) --> (λx. 0) (in p)``:
term
> SLLN_general_def;
val it =
``∀p X S' mu.
indep_real_rvs p X 𝕌(:num) ∧ (∀n. distribution p (X n) = mu) ∧
(∀n. expectation p (X n) < PosInf) ∧
(∀x. S' n x = SIGMA
files:
(* This is for Kananaskis 11 only, remove it for K12. *)
val PAT_X_ASSUM = PAT_ASSUM;
The question is, at PolyML (and MosML) level, how to write code to re-define
PAT_X_ASSUM only in K11 final release (and before)? Or there’s another better
solution to this entire problem?
Regards,
Chun
Hi again,
If I have a theorem saying two (2-ary) relations are the same:
|- R = R’
Then I can easily prove the following theorem using REWRITE_TAC:
|- !x y. R x y = R’ x y
But if I had the second one first, how to prove the previous one?
Regards,
Chun Tian
signature.asc
Description
ing
> 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 prove the following
m
> Il giorno 24 mar 2017, alle ore 21:50, Thomas Tuerk
> ha scritto:
>
> 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) wr
PAT_X_ASSUM
Static Errors
> Il giorno 25 mar 2017, alle ore 04:02, Ramana Kumar
> ha scritto:
>
> One thing you could try is to use Globals.version, e.g.,
> val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM;
>
> On 25 March 2017 at 07:32, Chun Tia
hat I can't
> think of at the moment. (There's a trickier way using "use"...)
>
> On 25 March 2017 at 21:00, Chun Tian (binghe) wrote:
> Hi… thanks, but it doesn’t work in HOL K11 final (where PAT_X_ASSUM is not
> defined):
>
> -
Thanks! Now it’s much easier to understand:) —Chun
> Il giorno 27 mar 2017, alle ore 13:46, Brian Campbell
> ha scritto:
>
> On 25/03/17 12:19, Ramana Kumar wrote:
>> OK... You could check directly whether "PAT_X_ASSUM" is bound in the
>> PolyML global namespace, and enter it if necessary:
>>
ove the
following theorem RTC_INDUCT2 in relationTheory? (which looks like RTC2_ind
generated in above definition)
val RTC_INDUCT2 = store_thm(
"RTC_INDUCT2",
``!R P. (!x. P x x) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
(!x (y:'a). RTC R x y ==> P x y)``,
y)` suffices_by (
> SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
> THEN
>
> GEN_TAC THEN CONJ_TAC THENL [
> Induct_on `RTC2` THEN
> METIS_TAC [RTC_RULES_RIGHT1],
>
> MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
> METIS_TAC[RTC2_rules]
> ]);
>
&g
ou can for
> example try
>
> DB.print_match [] ``RTC``
> DB.print_match [] ``RTC _ x x``
> DB.print_find "RTC"
> to find interesting theorems about RTC.
>
> Cheers
>
> Thomas
>
>
> On 07.04.2017 12:51, Chun Tian (binghe) wrote:
>
> Hi Thomas,
>
> Th
t; file.
>
> https://hol-theorem-prover.org/kananaskis-10-helpdocs/
> help/src-sml/htmlsigs/relationTheory.html#LinearOrder-val
>
> Best
>
> Thomas
>
> On 07.04.2017 13:07, Chun Tian (binghe) wrote:
>
> Thanks again, this is really convenient.
>
> Actually a la
Ah ... thank you very much!
Chun
> Il giorno 07 apr 2017, alle ore 16:43, Konrad Slind
> ha scritto:
>
> To print theory "foo" as html :
>
>DB.html_theory "foo";
>
> Konrad.
>
>
>> On Fri, Apr 7, 2017 at 6:50 AM, Chun Tian (bin
,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm
contexts. My inclination would be overload n to name, and
> to overload unary negation to coname, and then you could write
>
> n"a" and -"a"
>
> Michael
>
>
> On 24/4/17, 02:15, "Chun Tian (binghe)" wrote:
>
> Hi,
>
> I
Conv
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.or
again. (otherwise it’s not worth wasting your valuable time
looking into long proof scripts)
Regards,
Chun
> Il giorno 25 apr 2017, alle ore 10:04, Ramana Kumar
> ha scritto:
>
> Hi Chun Tian,
>
> It's hard to know exactly what's wrong, but I expect there's
ory failed:
error in file "Test.art" around line 37270:
trans
5016
def
while executing trans command:
terms not alpha-equivalent
Regards,
Chun Tian
> Il giorno 25 apr 2017, alle ore 18:50, Chun Tian (binghe)
> ha scritto:
>
> Hi Ramana,
>
> Thanks for your de
dicating a bug in HOL's OpenTheory module?
Regards,
Chun
On 26 April 2017 at 03:57, Ramana Kumar wrote:
> Thanks Chun Tian,
>
> I can reproduce the issue.
>
> I tried finding out which theorems were causing the failure. They're
> rather ugly (I will paste at the e
to smaller pieces ...
Regards,
Chun Tian
> Il giorno 01 mag 2017, alle ore 07:42, Ramana Kumar
> ha scritto:
>
> I think it would help if you could find another "mini" theory that exhibits
> the same issue... it's hard to tell what's wrong just from the erro
iu/hol/bin/Holmake” into somewhere already part of PATH (e.g.
"/home/liu/bin”)
5. To use HOL4 for theory creations. I suggest the toolchain of Emacs +
sml-mode.el . For details, see "an 8-page guide to HOL interaction and basic
proof using Emacs” [2]
Regards,
Chun Tian
[1] git clone htt
The way you startup HOL is correct. But something unknown is wrong here. In
this case, you should execute "bin/build cleanAll" and rebuild HOL. Or maybe
just delete the whole “hol” directory and re-do everything again.
> Il giorno 01 mag 2017, alle ore 15:17, Liu Gengyang
> <2015200...@mail.buc
/libpolymain.a .
Regards,
Chun
> Il giorno 01 mag 2017, alle ore 15:15, Chun Tian (binghe)
> ha scritto:
>
> Hi Liu,
>
> I hope my experiences could help a little:
>
> 1. In Ubuntu 16.04, there’s no need to build PolyML from source, you can use
> one of the following
Hi,
The kananaskis-11 release source tarball (hol-kananaskis-11.tar.gz) [1]
downloadable from HOL’s official site [2] has at least one missing file:
bin/hol.ML. As a result, even the building process succeeds, HOL cannot startup
… I think everyone who is trying to build HOL from the source tar
rt" around line 3:
thm
13076
ref
…
Rule.alpha: not alpha-equivalent
Full logs are in attach.
Regards,
Chun Tian
Test.ot.art
Description: Binary data
> Il giorno 29 apr 2017, alle ore 01:02, Ramana Kumar
> ha scritto:
>
> Hi Chun,
>
> Try with the latest update
it.
This file should include a line of the form
val polymllibdir = "path-to-dir-containing-libpolymain.a";
> Il giorno 02 mag 2017, alle ore 17:51, Ian Zimmerman ha
> scritto:
>
> On 2017-05-02 15:55, Chun Tian (binghe) wrote:
>
>> I forgot one thing: In moder
)
>
> Does ldd say more useful things on the Linux systems where this appears to be
> an issue?
>
> Having said all this, it’s also possible that using polyc everywhere makes it
> unnecessary for HOL itself to know anything about this directory. I’ll have
> to check this.
contains
libpolymain.a.
> Il giorno 02 mag 2017, alle ore 22:04, Chun Tian (binghe)
> ha scritto:
>
> Hi,
>
> I’m afraid that “ldd” command won’t give anything useful. On Ubuntu 16.04
> (x86_64), ldd gives the following outputs on “libpolyml.so” (the pointer
> addr
)
> libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x7fa5a7fa1000)
> libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6
> (0x7fa5a7ca1000)
> libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1
> (0x7fa5a7a8b000)
> libc.so.6 => /lib/
Hi,
Currently the "Hol_coreln" command in HOL4 seems undocumented. I wonder, is
there any related paper or notes when this facility was added?
I mainly want to know the purpose of the "cases" theorem returned by
Hol_coreln (beside looking at source code).
Thanks,
-
case, such that R is the fixed point of F, e.g. F (R) = R ?
Regards,
Chun
On 4 May 2017 at 14:17, wrote:
> As with the cases theorem returned by Hol_reln, the cases theorem is
> effectively an assertion that the relation is indeed a fix-point.
>
>
>
> Michael
>
&
I think I got it, it’s F(R) = {(0,0)} in this case ...
> Il giorno 04 mag 2017, alle ore 14:53, Chun Tian (binghe)
> ha scritto:
>
> Hi Michael,
>
> Thanks for quick response. I want to further ask, if I have the following
> mini relation:
>
> val (R_rules, R_c
ere.
>
> 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 REFERENCE sai
"failwith",
origin_structure = "??"} raised
This doesn’t make any sense, I think, as other commands like DB.html_theory ()
does allow overwriting files.
Is there any hidden option that allows me to call
EmitTeX.print_theories_as_tex_doc without deleting existing files first?
Regard
);
failwith "File exists”)
meanwhile I can use OS.FileSys.remove () to delete old files before calling
EmitTeX.print_theories_as_tex_doc () as I want. So there’s no issue at all.
Regards,
Chun
> Il giorno 06 mag 2017, alle ore 15:28, Chun Tian (bingh
to the input theorem?
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.o
Sorry … I found nothing in boolTheory, but by guessing theorem names EQT_ELIM
and EQF_ELIM are available...
> Il giorno 06 mag 2017, alle ore 23:17, Chun Tian (binghe)
> ha scritto:
>
> Hi,
>
> We know that EQT_INTRO and EQF_INTRO can be used to convert an existing
>
1 - 100 of 246 matches
Mail list logo
