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
d to what you're trying
> to define.
>
> Note that if you just wanted 2), you can add it directly to the inductive
> relation defining your rules as an additional argument instead of defining a
> brand new relation.
>
>
> On Thu, Jan 12, 2017 at 10:19 AM, Chun Tian (bin
Hi,
HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches the
term argument, applies the theorem tactic to it, and removes this assumption.”
But I found it actually doesn’t remove the assumption in latest Kananaskis 11.
To see this, try the following goal (open listTheory
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
belle.in.tum.de/repos/isabelle/
On 18 January 2017 at 11:54, Makarius wrote:
> On 17/01/17 15:24, Chun Tian (binghe) wrote:
> > Sorry, I re-checked my Isabelle environment and found that the PolyML in
> > Isabelle is actually built by GCC (mingw versions), so my statement
> > a
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
>
nking about these sorts of things is lists.
> Imagine you have:
>
>
>
> isAList l ó l = [] \/ ?h t. l = h::t /\ isAList t
>
>
>
> (where l ranges over a type large enough to encompass lists and lazy lists
> both, and the isAList predicate is identifying the appropriate s
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
Hi,
suppose currently I have a goal with several assumptions:
P
-
a0
a1
...
A
and a theorem th ``A ==> B``
Now I want to replace the last assumption A into B (and remove A), to reach
this new status:
P
-
a0
a1
…
B
I know the usage of POP_ASSUM, ASSUME_TAC, and MP, but
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,
POP_ASSUM ACCEPT_TAC)
>>>>> MATCH_MP_TAC CutRuleSimpl
>>>>> EXISTS_TAC ``(Dot A (Backslash A B))``
>>>>> CONJ_TAC
>>>> | [ MATCH_MP_TAC RightDot
>>>>> CONJ_TAC THEN1 REWRITE_TAC [SeqAxiom]
>>>&
uld
> probably be good to read though...
>
> Michael
>
> On 24 May 2016, at 23:34, Chun Tian (binghe) wrote:
>
>> Hello,
>>
>> (I'm a school student trying to do some course projects using HOL-4)
>>
>> Monica Nesi ever wrote a Cambridge tec
Hi,
suppose I have the following theorem:
th =
|- !x. P x = Q x
How can I convert it into this one?
|- !x. P x ==> Q x
As the first step, I tried "ONCE_REWRITE_RULE [EQ_IMP_THM] th", and got this:
|- !x. (P x ==> Q x) /\ (Q x ==> P x)
But then I don’t know how to benefit from AND1_THM (|- ∀t
hat porting the old code is turning out to be pretty
> straightforward.
>
> Best wishes,
> Michael
>
> On 22/1/17, 21:47, "Chun Tian (binghe)" wrote:
>
>Hello all,
>
>I’d like to report some progress about CCS in latest HOL.
>
>So
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
Hi,
Suppose I have the following definition about a predicate P (with a measure
space m):
val almost_everywhere_def = Define `
almost_everywhere m P = ?N. null_set m N /\ !x. x IN (UNIV DIFF N) ==> P x`;
(I think you can safely think it as `almost_everywhere m P = !x. P x`.)
Now my purpose
ate_restriction ("AE", "almost_everywhere")
>
> Then, you can get the sort of effect you want by writing
>
> ``AE x::m. P``
>
> The m will be a free variable, and the x will be bound in P. If you do a
> dest_term on it, you will get
>
>
Hi,
Currently I’m doing several projects in HOL4, and fortunately Kananaskis-11 was
finally released early this month, and for now I only use K-11 final release
and not chasing and rebuild HOL from Git master any more. On the other side,
I finally learnt to use PAT_X_ASSUM to “pop” any assump
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: Mess
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
Hi,
I have a simple data type based on strings:
val _ = Datatype `Label = name string | coname string`;
Is is possible to set up pretty-printing (or gammar) rules, such that:
1. The term `` `a` `` can be interpreted as `` name “a” ``
2. The term`` -`a` `` can be interpreted as `` coname “a” ``
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
Hi,
I have created some formal theories which builds successfully in all HOL modes
(stdknl, expk and logknl). But when I added the following lines into my
Holmakefile:
ifeq ($(KERNELID),otknl)
all: $(patsubst %Script.sml,%.ot.art,$(wildcard *Script.sml))
endif
the build
be
> able to debug it. It might take me a while to find time for it though.
>
> Cheers,
> Ramana
>
> On 25 April 2017 at 05:38, Chun Tian (binghe) wrote:
> Hi,
>
> I have created some formal theories which builds successfully in all HOL
> modes (stdknl, expk and
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
(λa1'.
> # ∀'Dertree' '@temp @ind_typeTest0list' .
> # (∀a0'.
> # (∃a0 a1.
> # (a0' =
> # (λa0 a1.
> # ind_type$CONSTR 0 a0
> #
r messages
> you sent.
>
> On 29 April 2017 at 23:25, Chun Tian (binghe) wrote:
> Hi Ramana,
>
> Thanks for fixing the issue. I have rebuilt HOL with 672f27ee9 included, now
> previous error in file "Test.art" around line 37270 has disappeared, but we
>
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 commands to install system package “polyml” (currently the
version if 5.6, enough to build HOL):
$ sudo apt-get install polyml
$ sudo aptitude in
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
to HOL (672f27ee9), which I think may fix the
> problem in HOL's OpenTheory Logging module.
>
> Cheers,
> Ramana
>
> On 28 April 2017 at 19:22, Chun Tian (binghe) wrote:
> Hi,
>
> I see you have already consulted in OpenTheory mailing list and Joe Hurd has
&g
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
Hi,
When I use EmitTeX.print_theories_as_tex_doc to export theories into TeX
documents, if the target TeX files already exist, the command reports HOL_ERR:
File ../papers/references already exists.
Exception-
HOL_ERR
{message = "File exists", origin_function = "failwith",
origin_st
);
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
Hi,
We know that EQT_INTRO and EQF_INTRO can be used to convert an existing theorem
into equation with ``= T`` or ``= F`` at right hand side. For instance:
> EQT_INTRO (REFL ``A``);
val it = |- (A = A) ⇔ T: thm
But if I have a theorem returned by EQT_INTRO or EQF_INTRO, how can I go back
to th
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
>
Hi,
I found that, if I call SPEC_ALL on the theorem with qualified variables, and
then call GEN_ALL on the resulting theorem, the order of qualified variables
may get changed:
> GEN_ALL (SPEC_ALL (ASSUME ``!A B C. B + C = A``));
val it =
[.] |- ∀C B A. B + C = A:
thm
most of time, varia
h = ASSUME``∀x y. (f x y ⇔ g y x)``
> val th' = strip_forall_rule f th
> [.] |- ∀x y. f x y ⇒ g y x
>
> On 7 May 2017 at 03:09, Chun Tian (binghe) wrote:
> Hi,
>
> I found that, if I call SPEC_ALL on the theorem with qualified variables, and
> then call GEN_ALL on
Hi,
Recently I found that, GENL and Q.GENL has different generalization orders:
> GENL [``x``, ``y``, ``z``] (SPEC_ALL EQ_TRANS);
val it =
|- ∀x y z. (x = y) ∧ (y = z) ⇒ (x = z):
thm
> Q.GENL [`x`, `y`, `z`] (SPEC_ALL EQ_TRANS);
val it =
|- ∀z y x. (x = y) ∧ (y = z) ⇒ (x = z):
thm
s
), which is automatically handled in the
WF_REL_TAC approach.
Can anyone suggest me some ideas or possible paths to resolve this issue?
or possible ways to prove the WF of arbitrary relations? Since all the
related defintions are long and omitted, I’m not expecting any ready-to-use
scripts.
Regard
> (∀l J p. R (p,J) (label l..p,J)) ∧
>>> (∀rf J p. R (p,J) (relab p rf,J)) ∧ (∀J p. R (p,J) (τ..p,J)) ∧
>>> ∀L J p. R (p,J) (ν L p,J)
>>>
>>> So the goal is nothing but to supply a relation such that, the parameter
>>> pairs in each
--
>> ---
>> load "stringLib";
>>
>> Datatype `term = Var string | App term term | Abs string term`;
>>
>> val FV_def =
>> Define
>> `(FV (Var s) scope = if s IN
n
On 1 July 2017 at 16:28, Chun Tian (binghe) wrote:
> Hi again,
>
> I think it's possible to change the original definition to make the
> cardinality *decrease* instead: previous I use the set J as the set of
> constants that have already been processed, but I can als
> because J is *NOT* assumed to be FINITE.
On 1 July 2017 at 16:51, Chun Tian (binghe) wrote:
> No ... my previous idea doesn't work. I got this goal unprovable:
>
> CARD (J DELETE a) < CARD J
>
> a ∈ J
>
> because J is ass
Hi,
It seems that ListTheory didn’t provide a way to remove elements from list?
What’s the recommended way to do such operation? Should I use FILTER, for
example, like this?
val DELETE_FROM_LIST = new_definition (
"DELETE_FROM_LIST", ``DELETE_FROM_LIST x list = (FILTER (\i. ~(i = x))
list)`
`` in place.
>
> Stylistically it's usually better to use Define instead of new_definition,
> and to name defining theorems with a "_def" suffix. I'd also keep the name
> short like "DELETE" or even "delete".
>
> On 2 Jul 2017 17:
Hi,
Currently I have the following Datatype "(‘a, ‘b) CCS" which supports binary
“sum” operation:
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
...`;
I also have a recursive function for calculating
Hi again ...
Suppose I have the following things:
1. An equivalence relation R (|- equivalence R) for type ‘a
2. A ONE-ONE function f (:num->’a). It’s known that all its values are distinct
according to R.
3. A finite set J of values of the same type.
What theorems could assert the existence of
terday - I see it as a gift to myself:)
Best regards,
Chun
On 5 July 2017 at 12:02, wrote:
> A combination of the partition theorems and FINITE_WEAK_ENUMERATE would be
> my guess…
>
> Michael
>
> On 3/7/17, 22:43, "Chun Tian (binghe)" wrote:
>
> Hi agai
atatype", origin_structure = "Datatype"}
raised
What's the problem here? How can I correctly define such a datatype?
Regards,
Chun
On 3 July 2017 at 13:22, Chun Tian (binghe) wrote:
> Hi,
>
> Currently I have the following Datatype "(‘
be to define a type using (CCS list), and to then quotient
> the resulting type by the equivalence relation that collapses the lists.
>
> Michael
>
> From: "Chun Tian (binghe)"
> Date: Wednesday, 5 July 2017 at 20:37
> To: hol-info
> Subject: Re: [Hol-info] H
Hi,
I’m using the ordinalTheory and cardinalTheory (in
"examples/set-theory/hol_sets”) with the following proposition unprovable:
Suppose I have a ONE_ONE function (f :’a ordinal -> ‘b), and an infinite set
(B: ‘b set), how can I assert the existence of an ordinal ``n`` such that ``(f
n) NOTIN
ad Slind wrote:
> I don't know a lot about this (even though I am responsible for
> ordinalTheory) but
> the Axiom of Infinity in HOL asserts the existence of an infinite set
> without
> saying how big it is. How do you know that B is not the same size as the
> domain of f?
>
&
*my initial proposition IS NOT TRUE unless the infinite set B has the same
type variable with the ordinals ...
On 12 July 2017 at 23:21, Chun Tian (binghe) wrote:
> Hi Konrad,
>
> Simply because the domain of f is the universe of some ordinals. Actually
> I think my initial propos
FULL_SIMP_TAC std_ss [] ],
(* goal 2 (of 2) *)
FULL_SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] \\
PROVE_TAC [] ]);
> Il giorno 12 lug 2017, alle ore 23:32, Chun Tian (binghe)
> ha scritto:
>
> *my initial proposition IS NOT TRUE unless the infinite set B has the
SPEC, since the quotation gets parsed in the context of
> the goal that way.
> For example, I'd replace your first PAT_X_ASSUM line with:
> qpat_x_assum`!g. P`(qspec_then`...`mp_tac)
> (or probably first_x_assum(qspec_then`...`mp_tac), since the pattern match
> there isn't
l I go over the
proof again to replace several tacticals with the ones I learnt from Ramana
Kumar.
--Chun
On 13 July 2017 at 02:50, wrote:
> I’m confused by the Cases_on `x < omega \/ x < omega`. Surely one copy of
> x < omega would be enough.
>
>
>
> Michael
>
>
&g
() in my proof script. My questions:
1. What's the risk for a new_axiom() used on a new constant to break the
consistency of entire HOL Logic?
2. With new_axiom() used, can I still claim that, I have correctly
formalized the proof of that theorem?
3. (optional
ng strict Math notations and theorems from
> related theories, I have full confidence to convince people that it's a
> correct proof.
>
> But I do have used new_axiom() in my proof script. My questions:
>
> 1. What's the risk for a new_axiom() used on a new constant to
ant, you might replace the num
> above with something else. Indeed, you could replace it with ‘a ordinal.
>
>Michael
>
>On 14/7/17, 04:15, "Chun Tian (binghe)" wrote:
>
>Hi Ramana,
>
>Thanks for explanation and hints. Now it’s clea
> general kind, which include, e.g., those that recurse through
> bounded-cardinality powersets -- like the one you need.
>
> Best wishes,
>
> Andrei
>
>
> Message: 1
> Date: Fri, 14 Jul 2017 08:47:38 +0200
> From: "Chun Tian (binghe)"
>
datatype. The one I was working with was quite complicated, but yours
> is much smaller.
>
> Konrad.
>
>
> On Sat, Jul 22, 2017 at 2:58 AM, Chun Tian (binghe)
> wrote:
> Hi Knorad,
>
> Sorry for late response. Thank you very much for providing this sample
> sc
Hi,
If I have two terms s1 and s2 of type ``:string``, then
string_EQ_CONV ``^s1 = ^s2``
returns a theorem like: |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F`` about the
equality the two terms. But if I don’t know the types of s1 and s2, how can I
achieve the same goal by finding a fun
Description should tell you more.
>
> Konrad.
>
>
> On Sat, Jul 22, 2017 at 4:23 PM, Chun Tian (binghe) > wrote:
>
>> Hi,
>>
>> If I have two terms s1 and s2 of type ``:string``, then
>>
>> string_EQ_CONV ``^s1 = ^s2``
>>
>> ret
an arbitrary injective f, does it
> hold for the particular f that you have defined?
>
> (There are plenty of injective functions between equi-numerous sets that are
> not onto…)
>
> Michael
>
> On 23/7/17, 01:07, "Chun Tian (binghe)" wrote:
>
>Hi Konr
Hi,
This is the first time I met the following goal, in which one of the
assumptions should be able to reduce to F (then the goal is resolved):
R (λt. t)
4. (λt. t) = (λt. prefix (label l) t)
The lambda function has the type of ``CCS -> CCS``, which CCS i
new q as an argument)
> `(\t. t) q = (\t. p) q` by PROVE_TAC[]
> Now you are done by BETA reduction and contradicting assumptions.
>
> Best
>
> Thomas
>
>
> On 04.08.2017 20:22, Chun Tian (binghe) wrote:
>> Hi,
>>
>> This is the first time I me
ectively.
>
> Of course, this is a blunt weapon, so you may not wish to use it if other
> assumptions are disrupted too much.
>
> Michael
>
> On 5/8/17, 04:25, "Chun Tian (binghe)" wrote:
>
>Hi,
>
>This is the first time I met the followi
Hi,
I think everyone has his own proof script styles, and there’s no unique way of
indentions fulfilling the favor of everyone. For me, I prefer the following
style:
val DIVIDES_0 = store_thm (
"DIVIDES_0”, ``!x. x divides 0``,
metis_tac [divides_def,MULT_CLAUSES]);
or
val DIVIDES_0 =
That’s so sad … this great person has just retired from University of Cambridge
for one year and several months (if I recall correctly). He never hesitates to
teach or encourage young people, even I as a fresh man in HOL community have
received several e-mails in private from him during the past
My highly subjective opinions: as an end-user, I choose HOL4 over HOL light
because I think and/or found:
1. Standard ML is a better language than OCaml (as a programming language);
2. Poly/ML is a better implementation than OCaml (as a language implementation);
3. HOL4 has a richer and more syst
which is suitable as the
> foundation for further developments.
>
> If you know of an existing formalization of elementary topology in HOL4
> please let me know, so that I can avoid duplicating work.
>
> Regards.
>
> Note: It seems that you forgot to reply to the maili
1 - 100 of 210 matches
Mail list logo
