Re: [Hol-info] hol-online not working

[Ramana Kumar]

Is HOL light online just HOL Light, or something special in particular? The
website for HOL Light can be found at
https://www.cl.cam.ac.uk/~jrh13/hol-light/ and the source code is now on
GitHub.

On Fri, 15 Nov 2019 at 00:38, Miranda, Brando  wrote:

> Hi,
>
> Does anyone have a link to HOL light online that works?
>
> https://code.google.com/archive/p/hol-online/
>
> thanks!
>
> -
> Brando Miranda
> PhD Student
> Computer Science at University of Illinois at Urbana-Champaign (UIUC)
> Alfred P. Sloan Scholar | SURGE Fellow | Saburo Muroga Endowed Fellow
> miran...@illinois.edu
>
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Ramana Kumar]

Very nice paper. Thanks Umair and Freek for the correction and link.

On Wed, 20 Feb 2019 21:08 Umair Siddique 
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101=rep1=pdf
>
> http://www.gilith.com/talks/tphols2001-subtypes.pdf
>
>
> - Umair
>
> On Wed, Feb 20, 2019 at 4:02 PM Freek Wiedijk  wrote:
>
>> Hi Ramana,
>>
>> >I think this is exactly what is impossible to do in HOL:
>> >it is a logic of total functions.
>>
>> I think that in PVS you _can_ do something like that, right?
>> Using the predicate subtypes.  Even though PVS _also_
>> only has total functions.
>>
>> And I _think_ there was a paper once about how to mimic
>> predicate subtypes in HOL.  Does anyone remember the
>> reference?
>>
>> Freek
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Ramana Kumar]

> So I think the key is to make sure that “undefined” thing really
undefined, such that whenever it appears, the proof cannot proceed any more

I think this is exactly what is impossible to do in HOL: it is a logic of
total functions.

On Wed, 20 Feb 2019 at 15:26, Chun Tian (binghe) 
wrote:

> Well, as the purpose of optionTheory is to augment any type with one more
> value, for (at least) extreals, it would be equivalent to have that
> “undefined” thing defined as part of the datatype definition:
>
> val extreal_def = Datatype
>`extreal = NegInf | PosInf | Normal real | Undefined`;
>
> However, once “Undefined” is actually defined, it’s then a disaster to
> affect almost all arithmetic laws. For a number which is either PosInf nor
> NegInf, now we can’t say it must be a (Normal x) any more, and many
> theorems will be broken.  To fix it, we have to treat this “Undefined” as
> something like those NaNs in IEEE 754 standard and define their orders and
> arithmetic laws, then all these work are unnecessary for formalization of
> pure math theorems.
>
> So I think the key is to make sure that “undefined” thing really
> undefined, such that whenever it appears, the proof cannot proceed any
> more, except for syntactic rewriting, which is inevitable in HOL.   Keeping
> ``0 / 0 = 0`` as before, could be another option, but I have concerns to
> convince mathematicians to accept this fact since I aim at precisely
> reproduce those pure math proofs under the “same” formal system with math
> books (except for the subtle differences between ZFC and HOL not affecting
> the math theories that I’m working with.)
>
> —Chun
>
> Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> I'd say one of the stronger ways to get "undefined" is to add an element
> to your type representing undefinedness, e.g., make it (/) : real option ->
> real option -> real option, where NONE represents "undefined". But then you
> will have a lot of bookkeeping to deal with...
> I don't suggest this seriously in the case of division -- I would rather
> suggest accepting the usual treatment of these partial functions as a small
> price for the benefits of working in a logic of (only) total functions.
>
> On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson  wrote:
>
>> None of these attempts make any sense. In HOL and similar systems
>> (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be
>> undefined in any strong sense. Fortunately, it’s consistent and harmless to
>> put x/0 = 0.
>>
>> Larry Paulson
>>
>>
>> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote:
>> >
>> > I run some experiments so to check if it is violating any fundamental
>> rule.
>> > So far it went good.
>>
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Ramana Kumar]

I'd say one of the stronger ways to get "undefined" is to add an element to
your type representing undefinedness, e.g., make it (/) : real option ->
real option -> real option, where NONE represents "undefined". But then you
will have a lot of bookkeeping to deal with...
I don't suggest this seriously in the case of division -- I would rather
suggest accepting the usual treatment of these partial functions as a small
price for the benefits of working in a logic of (only) total functions.

On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson  wrote:

> None of these attempts make any sense. In HOL and similar systems
> (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be
> undefined in any strong sense. Fortunately, it’s consistent and harmless to
> put x/0 = 0.
>
> Larry Paulson
>
>
> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote:
> >
> > I run some experiments so to check if it is violating any fundamental
> rule.
> > So far it went good.
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] (no subject)

[Ramana Kumar]

Where is this code from? It looks like an exam question.

On Thu, 20 Dec 2018 06:24 幻＠未来 <849678...@qq.com wrote:

>
> Here is the following code
> datatype temp =
>  C of real
>  | F of real;
>  fun temp_to_f t =
> case t of
>C x => x * (9.0 / 5.0) + 32.0
>   | F x => x;
> What is the function of the function temp_to_f ? How to use this function 
> specifically?
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Ramana Kumar]

I think this is false. Here's a proof of the opposite, with the type of f
instantiated to a num set generator:

val thm = Q.prove(
`¬(
  ∀(f:num->num->bool) a sp.
  (f 0 = ∅) ∧
  (∀n. f n ⊆ f (SUC n)) ∧
  (∀n. f n ⊆ sp) ∧
  (BIGUNION (IMAGE f 핌(:num)) = sp) ∧
  (a ⊆ sp) ⇒
 ∃x. a ⊆ f x)`,
  rw[]
  \\ qexists_tac`count`
  \\ qexists_tac`UNIV`
  \\ rw[SUBSET_DEF, PULL_EXISTS]
  >- metis_tac[]
  >- (
rw[Once EXTENSION]
\\ qexists_tac`count (SUC x)`
\\ rw[] )
  >- (
rw[EXTENSION]
\\ qexists_tac`SUC x`
\\ rw[] ));


On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) 
wrote:

> sorry, I also have this necessary assumption:
>
>  5.  BIGUNION (IMAGE f 핌(:num)) = sp
>
> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > I ran into the following goal in the proof of a big theorem:
> >
> >   ∃x. a ⊆ f x
> >   
> > 3.  f 0 = ∅
> > 4.  ∀n. f n ⊆ f (SUC n)
> >20.  ∀n. f n ⊆ sp
> >21.  a ⊆ sp
> >
> > I have an increasing sequence of sets (f n) from empty to the whole
> space (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I
> can always choose a big enough index x such that (f x) will contain “a”.
> But how can I make this argument formal?
> >
> > thanks,
> >
> > Chun
> >
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] tacticoe

[Ramana Kumar]

I would certainly be happy to see work-in-progress commits happen on a
branch other than master.
I would also be happy to answer any git-related questions or give tips on
workflow.

On Wed, 27 Jun 2018 at 10:58, Chun Tian (binghe) 
wrote:

> The author (Thibault Gauthier) should learn how to correctly use Git
> *first*, before committing directly to ‘master’.
>
> —Chun
>
>
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] big records

[Ramana Kumar]

Dear HOL users,

Does anyone know how to use the big record package? I always find I want to
turn it off (by increasing the big record size to above the max number of
fields in my types) because many things don't work on big records (in
particular the simplifier and EVAL) whereas they do work on "small" records.

Would it be OK to disable the big record package by default (e.g., set the
size limit to "infinity" by default)? Or would it be easy to make the above
tooling work for big records too? What are the advantages of big records
anyway?

Cheers,
Ramana
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Generated machine code of Poly/ML

[Ramana Kumar]

You could build a binary using polyc. Would that suffice? Or do you need to
see the machine code while running the REPL?

On 17 May 2018 at 17:13, Mario Xerxes Castelán Castro <
marioxcc...@yandex.com> wrote:

> Hello. The Poly/ML mailing list appears to be down at the moment. How
> can I see the machine code generated by Poly/ML?
>
>
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] "Gordon Computer"

[Ramana Kumar]

It doesn't look too bad to me - happy to port them if you like.

On 5 April 2018 at 12:36, Lawrence Paulson  wrote:

> I have just managed to locate Jeff Joyce's "Tamarack-2" files, which he
> describes as slightly simplified compared with the original Gordon
> computer. They are dated 1989 and the comments suggest that they are for
> HOL88. I guess they will bring back the memories for some people. But it
> would probably take a lot of work to get them to run in a modern version of
> HOL.
>
> http://www.cl.cam.ac.uk/~lp15/tmp/tamarack2.zip
>
> Larry
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Dependency on absolute paths remaining the same

[Ramana Kumar]

Yes, to do that you need to use --relocbuild, since any executables (heaps)
need to be rebuilt if the path changes.

Steps:
1. Copy your HOL directory to the new location, omitting any files that
match the patterns in tools-poly/rebuild-excludes.txt
2. Run poly --script tools/smart-configure.sml in the new location
3. Run bin/build --relocbuild in the new location

If there are additional developments outside of HOL that you want to build
using the newly located HOL, you may also need to use Holmake's
--relocbuild argument when rebuilding them initially (and also see
--nolmbc).

On 4 February 2018 at 17:16, Mario Xerxes Castelán Castro <
marioxcc...@yandex.com> wrote:

> Hello.
>
> Is it possible to use HOL4 in such a way that it continues working
> despite moving the directory to a different absolute path? The option
> “--relocbuild” of “bin/build” seems to be related. Is it documented
> anywhere? (I did not find anything in the manual)
>
> Thanks.
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Uninstall HOL

[Ramana Kumar]

Delete the directory in which you installed it.

On 31 Jan 2018 06:01, "Jing Guo"  wrote:

> Hi,
>
> Several months ago I installed HOL and recently I want to uninstall it.
> However, after some research I still could not find a way, nor it’s
> included in the documentation. So I wondered that what’s the recommended
> way to do it?
>
> Thanks!
>
> ---
> Jing
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Data61 Seeking Research Scientist

[Ramana Kumar]

One more open position at Data61, this one more suited for early-career
academics/researchers.

Data61 Seeking Research Scientist
=

We are looking for a full-time research scientist in formal verification to
join us, the Trustworthy Systems group, at Data61, CSIRO. Our highly
international team is located on the UNSW campus, close to the beautiful
beaches of sunny Sydney, Australia, one of the world's most liveable cities.

Our vision is a world in which computer users can choose all three: correct,
secure, and fast. We believe that most current approaches to building
systems
are fundamentally flawed. We aim to demonstrate a better way. Our approach
is
rooted in foundational, formal verification using theorem provers (e.g.,
Isabelle, HOL4), and high-performance system design. If you find this vision
appealing, and have ideas about how to pursue it, we want to hear from you.

Our team brings together a unique combination of expertise in systems,
security, formal verification, and programming languages. We are the
creators
of seL4, the world's first operating system microkernel with a
machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme
performance
and foundational binary-level correctness and security proofs. We are also
involved in CakeML, the most realistic verified compiler for a functional
programming language, and a promising approach to scaling full verification
up to applications code.

We are building on these successes in various directions, including
concurrency (formal reasoning and implementation), timing (real-time
guarantees and timing channels), and whole-system verification using
component systems (e.g., CAmKES) and code+proof co-generation.

We publish in top conferences, and are involved in multiple international
research collaborations. You will have the opportunity to teach at UNSW
should you wish to take it. We have a flexible, friendly, and intellectually
stimulating work environment.

We value diversity in all forms and welcome applications from people of all
ages, including people with disabilities, and those who identify as LGBTIQ.
See https://ts.data61.csiro.au/diversity/ for more information.

The salary range for this position is AUD 95-103K (plus superannuation),
depending on experience and qualifications.

Apply online here:
https://jobs.csiro.au/job/Sydney%2C-NSW-Research-Scientist-in-Formal-Verification/438798200/

Your application should include a cover letter, CV, short research
statement,
and contact information for two references.

This round of applications closes 21 November 2017.
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Data61 Seeking Proof Engineers

[Ramana Kumar]

If you're looking for a job using HOL4, the following may be of interest :)

Data61 Seeking Proof Engineers
==

If only there were a place where I could prove theorems for money, change
the
world, and have fun while doing it...

Sounds too good to exist?

In the Trustworthy Systems team at Data61 that's what we do for a living. We
are the creators of seL4, the world's first fully formally verified
operating
system kernel with extreme performance and strong security & correctness
proofs. Our highly international team is located on the UNSW campus, close
to
the beautiful beaches of sunny Sydney, Australia, one of the world's most
liveable cities.

We are looking for two motivated proof engineers who want to join our team,
move things forward, and have global impact. We are expanding our team,
because seL4 is going places. There are active projects around the world in

  - Automotive - because cars have been hacked enough
  - Aviation - for more security and safety for autonomous vehicles
  - Defence - protecting confidential information
  - Connected consumer devices - with security built in from the start
  - Spaceflight, autonomous and crewed - because awesome

To make these projects successful, we need to scale formal verification.
You would

  - work on industrial-scale formal proofs in Isabelle/HOL and HOL4
  - develop formally verified infrastructure for building secure systems
on top of seL4
  - contribute to improved proof automation and better reasoning techniques
  - apply formal proof to real-world systems and tools

To apply for this position, you should possess a significant subset of the
following skills.

  - functional programming in a language like Haskell, ML, or OCaml
  - first-order or higher-order formal logic
  - basic experience in C
  - ability and desire to quickly learn new techniques
  - undergraduate degree in Computer Science, Mathematics, or similar
  - ability and desire to work in a larger team

We are hiring at two levels, so if you are more qualified or experienced
than
the above would suggest, you can come in as a senior proof engineer.

If you additionally have experience

  - in software verification with an interactive theorem prover such as
Isabelle/HOL, HOL4, or Coq, and/or
  - with operating systems and microkernels, and/or
  - in verified applications technology such as CakeML

you should definitely apply!

If you have the right skills and background, we can provide training on the
job. Continual learning is a central component of everything we do. You will
work with a unique world-leading combination of OS and formal methods
experts, students at undergraduate and PhD level, engineers, and researchers
from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun,
creative, and welcoming workplace with flexible hours & work arrangements.

We value diversity in all forms and welcome applications from people of all
ages, including people with disabilities, and those who identify as LGBTIQ.
See https://ts.data61.csiro.au/diversity/ for more information.

Salary ranges for this position (in AUD) (plus superannuation):
- Junior: 61-78K, 80-91K
- Senior: 95-103K, 109-128K
depending on experience and qualifications.

Apply online at the following links:
- https://jobs.csiro.au/job/Sydney,-NSW-Proof-Engineer/438797400/
- https://jobs.csiro.au/job/Sydney,-NSW-Senior-Proof-Engineer/438798100/

Your application should include a cover letter, CV, undergraduate transcript
(if applicable), and contact information for two references.

This round of applications closes 21 November 2017.

The seL4 code and proof, and the CakeML project, are open source.
Check them out at https://seL4.systems and https://cakeml.org

More information about Data61's Trustworthy Systems team at
https://ts.data61.csiro.au

Still studying? We also have internship opportunities!
https://ts.data61.csiro.au/students/
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Small question about sqrt

[Ramana Kumar]

In your first goal, do either of these work?

metis_tac[transcTheory.SQRT_0]

rw[] \\ imp_res_tac transcTheory.SQRT_0

On 20 October 2017 at 23:42, Liu Gengyang <2015200...@mail.buct.edu.cn>
wrote:

> Hi,
>
> I want to prove the goal: !x. (sqrt x = 0) ==> (x = 0) as below,
>
> RW_TAC realLib.real_ss [] >>
> `sqrt 0 = 0` by RW_TAC realLib.real_ss [transcTheory.SQRT_0]
>
> The result is:
> x = 0
> 
>   0.  sqrt x = 0
>   1.  sqrt 0 = 0
>
> I think it is obvious, but I can'n prove it by rewrite or simplify tactic.
>
> However, if the goal is: !x. x>=0 /\ (sqrt x = 0) ==> (x = 0), I can prove
> it as below:
>
> RW_TAC std_ss [] >>
> `sqrt x pow 2 = 0 pow 2` by RW_TAC std_ss [] >>
> `0 <= x` by RW_TAC std_ss [realTheory.real_ge] >-
> RW_TAC std_ss [GSYM realTheory.real_ge] >>
> FULL_SIMP_TAC realLib.real_ss [transcTheory.SQRT_POW_2]
>
> So, what the problem about the first goal?
>
> Regards，
>
> Liu
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] What's the recommended way to delete elements from list?

[Ramana Kumar]

Oh whoops I misunderstood - it deletes all of them. Never mind.

On 11 October 2017 at 22:38, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:

> Just based on your final question, I suggest:
> ?l1 l2. (DELETE_ELEMENT e L = l1 ++ l2) /\ (L = l1 ++ [e] ++ l2)
>
> On 11 October 2017 at 22:34, <michael.norr...@data61.csiro.au> wrote:
>
>> You might define the sublist relation :
>>
>>   Sublist [] l = T
>>   Sublist _ [] = F
>>   Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist
>> (h1::t1) t2
>>
>> And show that
>>
>>   Sublist (DELETE_ELEMENT e l) l
>>
>> This doesn’t capture the idea that the only missing elements are e’s
>> though.  This definition of Sublist might not be the easiest to work with…
>>
>> Michael
>>
>> On 11/10/17, 22:31, "Chun Tian" <binghe.l...@gmail.com> wrote:
>>
>> Hi,
>>
>> I’d like to close an old question.  3 months ago I was trying to
>> define the free names in CCS process but failed to deal with list
>> deletions.   Today I found another way to delete elements from list,
>> inspired by DROP:
>>
>> val DELETE_ELEMENT_def = Define `
>>(DELETE_ELEMENT e [] = []) /\
>>(DELETE_ELEMENT e (x::l) = if (e = x) then DELETE_ELEMENT e l
>>  else x::DELETE_ELEMENT e l)`;
>>
>> And the previous definition suggested by Ramana based on FILTER now
>> becomes a theorem as alternative definition:
>>
>>[DELETE_ELEMENT_FILTER]  Theorem
>>
>>   |- ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L
>>
>> I found it’s easier to use the recursive definition, because many
>> useful results can be proved easily by induction on the list. For example:
>>
>>[EVERY_DELETE_ELEMENT]  Theorem
>>
>>   |- ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P L
>>
>>[LENGTH_DELETE_ELEMENT_LE]  Theorem
>>
>>   |- ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L
>>
>>[LENGTH_DELETE_ELEMENT_LEQ]  Theorem
>>
>>   |- ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L
>>
>>[NOT_MEM_DELETE_ELEMENT]  Theorem
>>
>>   |- ∀e L. ¬MEM e (DELETE_ELEMENT e L)
>>
>> What I actually needed is LENGTH_DELETE_ELEMENT_LE, but 3 months ago
>> I just couldn’t prove it!
>>
>> However, I still have one more question: how can I express the fact
>> that all elements in (DELETE_ELEMENT e L) are also elements of L, with
>> exactly the same order and number of appearances?   In another words, by
>> inserting some “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 <
>> ramana.ku...@cl.cam.ac.uk> ha scritto:
>> >
>> > Sure, that's fine. I probably wouldn't even define such a constant
>> but would instead use ``FILTER ((<>) x) ls`` 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:04, "Chun Tian (binghe)" <binghe.l...@gmail.com>
>> wrote:
>> > 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)``);
>> >
>> > Regards,
>> >
>> > Chun
>> >
>> >
>> > 
>> --
>> > Check out the vibrant tech community on one of the world's most
>> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>> > ___
>> > hol-info mailing list
>> > hol-info@lists.sourceforge.net
>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>> >
>>
>>
>>
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] What's the recommended way to delete elements from list?

[Ramana Kumar]

Just based on your final question, I suggest:
?l1 l2. (DELETE_ELEMENT e L = l1 ++ l2) /\ (L = l1 ++ [e] ++ l2)

On 11 October 2017 at 22:34, <michael.norr...@data61.csiro.au> wrote:

> You might define the sublist relation :
>
>   Sublist [] l = T
>   Sublist _ [] = F
>   Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist
> (h1::t1) t2
>
> And show that
>
>   Sublist (DELETE_ELEMENT e l) l
>
> This doesn’t capture the idea that the only missing elements are e’s
> though.  This definition of Sublist might not be the easiest to work with…
>
> Michael
>
> On 11/10/17, 22:31, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> Hi,
>
> I’d like to close an old question.  3 months ago I was trying to
> define the free names in CCS process but failed to deal with list
> deletions.   Today I found another way to delete elements from list,
> inspired by DROP:
>
> val DELETE_ELEMENT_def = Define `
>(DELETE_ELEMENT e [] = []) /\
>(DELETE_ELEMENT e (x::l) = if (e = x) then DELETE_ELEMENT e l
>  else x::DELETE_ELEMENT e l)`;
>
> And the previous definition suggested by Ramana based on FILTER now
> becomes a theorem as alternative definition:
>
>[DELETE_ELEMENT_FILTER]  Theorem
>
>   |- ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L
>
> I found it’s easier to use the recursive definition, because many
> useful results can be proved easily by induction on the list. For example:
>
>[EVERY_DELETE_ELEMENT]  Theorem
>
>   |- ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P L
>
>[LENGTH_DELETE_ELEMENT_LE]  Theorem
>
>   |- ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L
>
>[LENGTH_DELETE_ELEMENT_LEQ]  Theorem
>
>   |- ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L
>
>[NOT_MEM_DELETE_ELEMENT]  Theorem
>
>   |- ∀e L. ¬MEM e (DELETE_ELEMENT e L)
>
> What I actually needed is LENGTH_DELETE_ELEMENT_LE, but 3 months ago I
> just couldn’t prove it!
>
> However, I still have one more question: how can I express the fact
> that all elements in (DELETE_ELEMENT e L) are also elements of L, with
> exactly the same order and number of appearances?   In another words, by
> inserting some “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 <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
> >
> > Sure, that's fine. I probably wouldn't even define such a constant
> but would instead use ``FILTER ((<>) x) ls`` 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:04, "Chun Tian (binghe)" <binghe.l...@gmail.com>
> wrote:
> > 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)``);
> >
> > Regards,
> >
> > Chun
> >
> >
> > 
> --
> > Check out the vibrant tech community on one of the world's most
> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> > ___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Definitions of partial functions (incl. predicates)

[Ramana Kumar]

My intuition says that working with total functions (and especially
predicates) will be easier.
Why? I don't know exactly, but here are some possible reasons:
you can just use plain rewriting rather than conditional rewriting,
and you don't need to state so many assumptions explicitly on your
theorems.

I also want to make a point against the supposed elegance of partial
definitions. My understanding is that it seems more elegant to not
specify a function on inputs that are supposed to be "invalid" for
that function, because then you know your proofs don't depend on how
the function behaves on those inputs. In theory you could substitute
any function which agrees only on the valid inputs. However,
practically, I've never seen this work out. Nobody takes a proof on
an underspecified function and transports it to another setting with
another function that's the same on valid inputs, at least not
without doing substantial work. But often people do run into annoying
problems due to underspecification.


On 6 October 2017 at 06:04, Mario Castelán Castro 
wrote:

> Hello.
>
> What is the preferred way to define functions only for some values? For
> example, as in arithmetic$DIV in HOL?:
>
>   ⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)
>
> Here nothing is asserted for the value of DIV for n = 0, thus it is
> “undefined” in some sense. I know that this can be done with
> “new_specification” but proving _trivial_ existence theorems seems like
> something that should be automatized.
>
> I am writing a formalization of elementary topology[1]. I have to define
> the concept of the interior, closure, etc. Currently I use total
> definitions. I am thinking that it may be more elegant to use a partial
> definition like the above.
>
> For example, currently I have the definition:
>
> interior To X r ⇔
>   is_topo To ∧ X ⊆ space To ∧ r ∈ space To ∧
>   ∃Y. r ∈ Y ∧ Y ⊆ X ∧ Y open_in To
>
> I want to change this to:
>
> is_topo To ∧ X ⊆ space To ⇒
>   interior To X = ⋃ {Y | Y ⊆ X ∧ Y open_in To}
>
> Is there some expected difficulty with this under-specification?
>
> Thanks.
>
> [1]  (work in progress).
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Ramana Kumar]

I think it would be good to add this UNIQUE constant to listTheory, if you
have time to make a pull request.

On 6 October 2017 at 01:49, Chun Tian (binghe) 
wrote:

> Let me close this question (further comments are welcome, of course).
>
> I actually got another good definition from Robert Beers in a private
> email:
>
>[UNIQUE_DEF]  Definition
>
>   |- ∀x L.
>UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2
>
> This form is very useful for me, because "¬MEM x L1 ∧ ¬MEM x L2” is
> exactly what I needed from the uniqueness. Then I tried to prove the
> following two alternative definitions using above definition, with success:
>
>[UNIQUE_ALT]  Theorem
>
>   |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])
>
>[UNIQUE_ALT_COUNT]  Theorem
>
>   |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)
>
> where LIST_ELEM_COUNT is a constant defined in rich_listTheory:
>
> [LIST_ELEM_COUNT_DEF]  Definition
>
>   |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)
>
> From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other
> direction is more difficult. I attached my proof scripts in case anyone
> needs it. But I’m new to listTheory, my scripts are very ugly, sorry for
> that (they will become better once I’ve learnt more).
>
> Regards,
>
> Chun Tian
>
>
>
> > Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > (I'm new to HOL's listTheory). Suppose I have a list L which contains
> possibly duplicated elements, and I want to express certain element X is
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> >
> > Regards,
> >
> > Chun Tian
> >
> > --
> > Chun Tian (binghe)
> > University of Bologna (Italy)
> >
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Changing thms used by computeLib

[Ramana Kumar]

Unfortunately I don't know anything better than "run it again".

You could also maybe try an older HOL commit (maybe prior to
d52c7d66716ddd253b6fd40bd3d38b29a238c392) and see if that's any more
reliable.

This is all speculation on my part though. The problem could have nothing
to do with pointer equality.

On 5 October 2017 at 16:15, Heiko Becker <hbec...@mpi-sws.org> wrote:

> Hello Ramana,
>
> yes, the Mk_comb error occurs non-deterministic. Is there a temporary
> workaround for this, that I could make use of?
>
> Cheers,
>
> Heiko
>
> On 10/05/2017 12:43 PM, Ramana Kumar wrote:
>
> Hi Heiko,
>
> Does it fail every time when you try to run the proofs non-interactively
> (with Holmake)?
>
> I suspect the "Mk_comb" error, if it is non-deterministic, has to do with
> pointer equality problems, which are in the middle of being fixed.
>
> Cheers,
> Ramana
>
> On 5 October 2017 at 13:22, Heiko Becker <hbec...@mpi-sws.org> wrote:
>
>> Hello,
>>
>> I have some proofs that I could previously solve by running EVAL_TAC,
>> after modifying computeLib.the_compset with
>>
>>
>> val _ = computeLib.del_funs [sptreeTheory.subspt_def]
>> val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
>> sptreeTheory.subspt_eq]
>>
>>
>> As it turns out, the proofs still run fine when interactively run in an
>> HOL4 emacs session, but the proofs fail when run on the command line.
>>
>> The failure either is
>>
>> HOL_ERR {message = "", origin_function = "Mk_comb", origin_structure = "T$
>> m"}
>>  Uncaught exception: HOL_ERR {message = "", origin_function = "Mk_comb",
>> origin_structure = "Thm"}
>>
>> or
>>
>>  (∀k.
>> k = 1 ∨ k = 0 ⇒
>> lookup k (BS (BN LN (LS ())) () (LS ())) =
>> lookup k (BS LN () (LS (
>>
>> Previously it sufficed to have a file myComputeLib.sml declaring the
>> structure myComputeLib and adding the two val statements above there and
>> loading that file when doing the proof with "open". When trying to debug
>> this issue, I moved the val statements in a separate tactic, declaring
>>
>>   val my_eval_tac =
>>  let
>>val _ = computeLib.del_funs [sptreeTheory.subspt_def]
>>val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
>> sptreeTheory.subspt_eq]
>>  in
>>   EVAL_TAC
>>  end;
>>
>>
>> but that did not solve my problem either.
>>
>> Can someone help me resolve this or give me a hint on how to debug this
>> issue?
>>
>> Thanks,
>>
>> Heiko
>>
>>
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

[Ramana Kumar]

Perhaps it would make more sense to ask people who are using rich type
systems what their motivations are :)
(On this list it's probably mostly people who are satisfied with simple
type theory.)

On 15 September 2017 at 11:06, Mario Castelán Castro  wrote:

> Hello.
>
> I want ask for your experience and opinion of proof assistants with
> “rich” type systems (allowing types dependent on terms and “proofs as
> terms, propositions as types”) like Agda and Coq. Specifically, how
> practical are these systems for pure mathematics, compared to HOL4 and
> HOL Light? Is there a significant advantage of these systems for pure
> mathematics compared to higher order logic?
>
> Systems with types dependent on terms promise many expressibility
> built-it into the logic. My impression is that this is unnecessary and
> generates more problems than what it solves. When one tries to make the
> logic as rich as possible instead of as simple as possible, containing
> everything that could be desired built-in, the result is an enormously
> complex logic (with the implications that the logical kernel, if any,
> will be more difficult to verify either by ordinary code review or
> formally). In the case of Coq, it is my understanding that the logical
> foundation even changes regularly with new releases.
>
> Yet a system that has everything that could be wanted from it is an
> unachievable goal. Users or interested parties eventually find something
> missing so a process of endless revision of the foundations begins.
>
> This does not seem to happen with foundations based on set theory. ZFC
> (possibly augmented with proper classes and large cardinals) seems to be
> both sufficient for all mathematics and written in stone (in the sense
> that we are not continuously revising the foundations continuously).
>
> What is thus the motivation for the search for logical foundations and
> systems based on “rich” type theory (beyond higher order logic)? Setting
> aside philosophical interest in type theories (intuitionism), is there
> some advantage to them as foundations or practical systems beyond the
> built-in syntactic sugar? I am missing something?
>
> Thanks.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Is it possible to make Holmake print timing information?

[Ramana Kumar]

In case it's not obvious, the place to make feature requests is here:
https://github.com/HOL-Theorem-Prover/HOL/issues

Implementation detail: I would guess you could get per-theorem timing by
setting the "default prover" to one that does timing, similar to how the
--fast option sets it to one that skips the proof.

On 27 September 2017 at 11:12,  wrote:

> There is no nice way to do this on a per-theorem basis, though I can
> imagine an option to Holmake that would turn on some sort of logging like
> this. Can you make a feature request please?
>
> You do get per-theory timing information emitted at the end of each script
> file, and you could see this logging information in the .hollogs file
> corresponding to your script.
>
> Michael
>
> On 27/9/17, 15:39, "Mario Castelán Castro"  wrote:
>
> Hello.
>
> I want to know how much time each theorem takes to prove when
> processing
> a script file with Holmake. Does Holmake has an option for this? I
> tried
> “--d” already.
>
> Thanks in advance.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Question on rewriting with assumptions

[Ramana Kumar]

I just wanted to point out, in case you didn't know, that many tactics have
lowercase synonyms so you don't have to write them out in all capital
letters. For example pop_assum and rewrite_tac.

There are also some cheatsheets around online for commonly used tactics,
e.g., http://sange.fi/~magnus/cheatsheet.txt and
https://gist.github.com/xrchz/71048e26e42f7f195d1726a855a4d2ff. Maybe these
should be linked from the main website (and probably merged)...

On 26 September 2017 at 04:42, Mario Castelán Castro  wrote:

> Hello Chun Tian.
>
> On 25/09/17 17:12, Chun Tian (binghe) wrote:
> > To prevent "explicit" lambda expressions in this case, what I've learnt
> > from Joe Hurd is the following simple helper ML function:
> >
> > fun wrap a = [a];
> >
> > then your "POP_ASSUM (fn thm => REWRITE_TAC [thm])" becomes "POP_ASSUM
> > (REWRITE_TAC o wrap)".
>
> Thanks you. This does nicely what I wanted.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to find existing developments in HOL4?

[Ramana Kumar]

I think a good approach is to ask the mailing list (as you have done), and
to look around in the src and examples directories of the repository.

On 11 September 2017 at 12:26, Chun Tian (binghe) 
wrote:

> Well .. I didn’t reply to the mailing list because it contains some
> insulting words to third-party products. But since you forwarded it
> already, I’m fine with that.
>
> I didn’t know you were looking for formalizations of pure mathematics
> theories, but here is my another little experience:
>
> 1. Go to "Formalizing 100 Theorems” web site [1] and find a theorem in
> your targeting area.
> 2. Choose one of the formalization under that theorem (if there is), based
> on the theorem prover you know how to use.
> 3. We can imagine the formalization of that theorem must depends or ships
> with a large piece (if not the whole) of underlying math theory.
>
> The only sad thing is, this web site didn’t mention any work done in HOL4
> (and its predecessors). While the closest one is HOL light, of course. I
> think migrating theories to HOL4 from other theorem provers is not always
> straightforward but still doesn’t create much academic value, unless you
> can push the related theories to a higher level.
>
> Regards,
>
> Chun Tian
>
> [1] http://www.cs.ru.nl/~freek/100/
>
> > Il giorno 10 set 2017, alle ore 21:31, Mario Castelán Castro <
> marioxcc...@yandex.com> ha scritto:
> >
> >> Why did you ignore Google web search (www.google.com) and Google
> scholar search (scholar.google.com)?   DuckDuckGo is built-in supported
> by some open source products, but I think it’s generally a garbage.
> >
> > Google has a lot of private data about people. They can do, and do, many
> > bad things with this data. I can not stop Google surveillance, but I do
> > not want to make their task easier. Anyway, Startpage is an independent
> > proxy for Google Search therefore the results should be similar to what
> > Google Search would provide directly. In my experience DuckDuckGo has
> > served well enough. It is my main search engine.
> >
> > Unfortunately, I still use Google Scholar because I have not found a
> > good general purpose alternative. I use PubMed when I need to search for
> > publications in medicine, but for mathematics/logic I do not know of any
> > good alternative. Suggestions would be very welcome.
> >
> >> My experience: “HOL4” is a bad key word, because mostly what you may
> found is a formalization done in old HOL versions. Instead, “formalization”
> + “higher order logic” + domain keywords should be enough.
> >
> > Thanks! This gives much better results for my aforementioned benchmark
> > test about prime numbers. ☺
> >
> > There seems to be no signification formalization of elementary topology
> > in HOL4. I am aware that there is some topology in “/src/real” in the
> > HOl4 distribution, but it is very limited. Searching with DuckDuckGo,
> > Startpage and Google Scholar for “formalization "higher order logic"
> > topology” does not turn anything relevant. As my first development with
> > a proof assistant I am formalizing some theorems of elementary topology
> > in HOL4. I plan to develop and publish a theory 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 mailing list.
> >
> > On 10/09/17 13:34, Chun Tian (binghe) wrote:
> >> Hi,
> >>
> >> Why did you ignore Google web search (www.google.com) and Google
> scholar search (scholar.google.com)?   DuckDuckGo is built-in supported
> by some open source products, but I think it’s generally a garbage.
> >>
> >> My experience: “HOL4” is a bad key word, because mostly what you may
> found is a formalization done in old HOL versions. Instead, “formalization”
> + “higher order logic” + domain keywords should be enough.
> >>
> >> Regards,
> >>
> >> Chun Tian
> > --
> > Do not eat animals; respect them as you respect people.
> > https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
> >
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Strange tactics bug when using match_mp_tac

[Ramana Kumar]

I have a couple of comments/questions on irule:

- I think mp_then is supposed to be better still. Am I right? (Or are they
serving different purposes?)

- I find it annoying that irule produces lots of new subgoals for the
hypotheses. Is there a version that doesn't strip all the conjunctions, so
they can be worked on together?

On 24 August 2017 at 09:22,  wrote:

> Eta-expanding as you did is nicer, I think.
>
> You might also consider using irule; it is supposed to be an improved
> match_mp_tac (i.e., does more things), and it doesn’t have the particular
> problem with exceptions.  Indeed, one of its improvements is that it
> subsumes {MATCH_}ACCEPT_TAC.
>
> Michael
>
> On 23/8/17, 17:28, "Heiko Becker"  wrote:
>
> Thank you for the fix. With this I could come up with a solution that I
> find ok for the moment:
>
> val my_match_mp_tac = (fn thm => (fn gs => match_mp_tac thm gs))
>
> This allows to at least not have the HOL_ERR handling, but I guess it
> depends what one finds nicer.
>
>
> Heiko
>
> On 08/23/2017 09:03 AM, michael.norr...@data61.csiro.au wrote:
> > You are being caught by the fact that match_mp_tac thm can throw an
> exception before the tactic is ever applied to a goal.  In particular, if
> the theorem passed to match_mp_tac is not an implication an exception is
> thrown immediately.
> >
> > You can fix this by handling that possible exception:
> >
> > fun simple_apply thm = ACCEPT_TAC thm ORELSE (match_mp_tac thm
> handle HOL_ERR _ => ALL_TAC)
> >
> > This arguably a poor design for match_mp_tac, and should perhaps be
> changed.
> >
> > Michael
> >
> >
> >
> > On 23/8/17, 16:55, "Heiko Becker"  wrote:
> >
> >  Hello everyone,
> >
> >  while working on some custom tactics, I noticed some strange
> behavior
> >  related to combining tactics with match_mp_tac and the ORELSE
> tactical:
> >
> >  I am trying to write a tactic takes a theorem and first tries
> out
> >  whether it is already a proof of the current goal with
> ACCEPT_TAC.
> >  If this does not succeed, the tactic should try matching the
> theorem
> >  with match_mp_tac.
> >
> >  Here is what I have come up with:
> >
> >   fun simple_apply thm = (ACCEPT_TAC thm) ORELSE
> (match_mp_tac thm);
> >
> >  I have defined a test tactic, to see whether ACCEPT_TAC works
> as I
> >  expect it to work:
> >
> >   fun dumb_apply thm = (ACCEPT_TAC thm) ORELSE (FAIL_TAC
> "Unreachable");
> >
> >  Strangely the simple_apply tactic does not work in cases, where
> the
> >  dumb_apply tactic works:
> >
> >   val test_thm = Q.prove (
> > ` !(n:num) (P:num -> bool).
> >  P n ==>
> >  P n`,
> > rpt gen_tac
> > DISCH_THEN ASSUME_TAC
> > qpat_x_assum `P n` (fn thm => simple_apply thm) (* Fails
> with "No
> >  parse of quotation leads to success" *)
> > qpat_x_assum `P n` (fn thm => dumb_apply thm)  (* Proves
> the goal *)
> > );
> >
> >
> >  Can someone explain to me what I did wrong with the
> simple_apply tactic?
> >
> >
> >  Thanks,
> >
> >
> >  Heiko
> >
> >  
> --
> >  Check out the vibrant tech community on one of the world's most
> >  engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> >  ___
> >  hol-info mailing list
> >  hol-info@lists.sourceforge.net
> >  https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects

[Ramana Kumar]

gt;>>   ('a,'b,'c) prog
> >>>
> >>> and one of the constructors has type
> >>>
> >>>   ('a -> ('a,'b,'c) prog) -> ('a,'b,'c) prog
> >>>
> >>> which seems close to what you want.
> >>>
> >>> Konrad.
> >>>
> >>>
> >>> On Fri, Jul 14, 2017 at 1:47 AM, Chun Tian (binghe) <
> binghe.l...@gmail.com> wrote:
> >>> Hi Michael,
> >>>
> >>> Great, thanks! Then I guess the only remain issue in my project is to
> define this datatype by hand. I’ll make a deeper reading in Tom Melham’s
> paper [1] and see how such job can be done. If there're other relevant
> materials, please let me know (at least the title).
> >>>
> >>> Regards,
> >>>
> >>> Chun Tian
> >>>
> >>> [1] Melham, Tom. Automating recursive type definitions in higher order
> logic. 1989.
> >>>
> >>>> Il giorno 14 lug 2017, alle ore 08:24, <Michael.Norrish@data61.csiro.
> au> <michael.norr...@data61.csiro.au> ha scritto:
> >>>>
> >>>> Note further that a type where you have
> >>>>
> >>>> Datatype‘CCS = C1 … | C2 .. | SUM (num -> CCS)’;
> >>>>
> >>>> does not fall foul of cardinality problems.  (You can recurse to the
> right of a function arrow as above, but not to the left, as would happen in
> SUM (CCS -> bool).)
> >>>>
> >>>> So, when I wrote “you just can’t have infinite sums”, I was
> over-stating.  If you see num -> CCS as enough of an infinite sum, then
> you’re OK. (And you could certainly also have “SUM : ('a ordinal -> CCS) ->
> CCS”.)
> >>>>
> >>>> Unfortunately, HOL4’s Datatype principle doesn’t allow the definition
> above as I’ve written it, but such types can be defined by hand with
> sufficient patience.
> >>>>
> >>>> Michael
> >>>>
> >>>> On 14/7/17, 14:47, "michael.norr...@data61.csiro.au" <
> michael.norr...@data61.csiro.au> wrote:
> >>>>
> >>>>   You just can’t have infinite sums inside the existing type for the
> cardinality reasons.  But there’s no reason why you couldn’t have a type
> that featured infinite sums over a base type that didn’t itself include
> infinite sums.
> >>>>
> >>>>   Something like
> >>>>
> >>>> Datatype`CCS = … existing def … (* with or without finite/binary
> sums *)`
> >>>>
> >>>> Datatype`bigCCS = SUM (num -> CCS)`
> >>>>
> >>>>   Depending on the degree of branching you want, 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)" <binghe.l...@gmail.com>
> wrote:
> >>>>
> >>>>   Hi Ramana,
> >>>>
> >>>>   Thanks for explanation and hints.  Now it’s clear to me that, I
> *must* remove the new_axiom() from the project, even if this means I have
> to bring some “ugly” solutions.
> >>>>
> >>>>   Now I see ord_RECURSION is a universal tool for defining
> recursive functions on ordinals, for this part I have no doubts any more.
> But my datatype is discrete, no order, no accumulation, currently I can’t
> see a function (lf :’a ordinal -> ‘b set -> ‘b) which can be supplied to
> ord_RECURSION ..
> >>>>
> >>>>   Currently I’m trying to something else in the datatype, and I
> have to replay all theorems in the project to see the side effects.
> Meanwhile I would like to hear from other HOL users for possible solutions
> on the infinite sum problem which looks quite a common need ..
> >>>>
> >>>>   Regards,
> >>>>
> >>>>   Chun
> >>>>
> >>>>> Il giorno 13 lug 2017, alle ore 14:35, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
> >>>>>
> >>>>> Some very quick answers. Others will probably go into more detail.
> >>>>>
> >>>>> 1. If you use new_axiom, it becomes your responsibility to ensure
> that your axiom is consistent. If it is not consistent, the principle of
> explosion makes any subsequent formalisation vacuous. (If you don't use
> new_axiom, it can be shown that any formalisation is consistent as long as
>

Re: [Hol-info] On the use of new_axiom() in formal projects

[Ramana Kumar]

Some very quick answers. Others will probably go into more detail.

1. If you use new_axiom, it becomes your responsibility to ensure that your
axiom is consistent. If it is not consistent, the principle of explosion
makes any subsequent formalisation vacuous. (If you don't use new_axiom, it
can be shown that any formalisation is consistent as long as set theory is
consistent.)

2. Yes. But you should probably detail why you claim that the axiom is
consistent and that you wrote it down correctly. It also makes it less
appealing for others to build on your work subsequently.

3. Yes. Prove the existence of functions defined on ordinals, specialise
that existence theorem with your desired definition, then use
new_specification. Maybe the required theorem exists already? Does
ord_RECURSION do it? See how ordADD is defined. (I haven't looked at this
in detail.)

On 13 July 2017 at 21:10, Chun Tian (binghe)  wrote:

> Hi,
>
> (Thank you for your patience for reading this long mail with the question
> at the end)
>
> Recently I kept working on the formal proof of an important (and elegant)
> theorem in CCS, in which the proof requires the construction of a recursive
> function defined on ordinals (returning infinite sums of CCS processes).
> Here is the informal definition:
>
> 1. Klop a 0o := nil
> 2. Klop a (ordSUC n) := Klop a n + (prefix a (Klop a n))
> 3. islimit n ==>
>Klop a n := SUM (Klop a m) for all ordinals m < n
>
> (here the "+" operator is overloaded, it's the "sum" of an custom datatype
> (CCS) defined by HOL's Define command. "prefix" is another operator, both
> are 2-ary)
>
> I think it's a well-defined function, because the ordinal arguments
> strictly becomes smaller in each recursive call. But I don't know how to
> formall prove it, and of course HOL's Define package doesn't support
> ordinals at all.
>
> On the other side, my datatype doesn't support infinite sums at all, and
> it seems no hope for me to successfully defined it, after Michael has
> replied my easier email and explained the cardinality issues for such
> nested types.
>
> So I got two issues here: 1) no way to define infinite sums, 2) no way to
> define resursive functions on ordinals.  But I found a "solution" to bypass
> both issues: instead of trying to express infinite sums, I turn to focus on
> the behavior of the infinite sums and define the behavior directly as an
> axiom.  In CCS, if a process p transits to p', then p + q + ... (infinite
> other process) still transit to p'. Thus I wrote the following "cases"
> theorem (which looks quite like the 3rd return values by Hol_reln) talking
> about a new constant "Klop"
>
> val _ = new_constant ("Klop", ``:'b Label -> 'c ordinal -> ('a, 'b) CCS``);
>
> |- (!a. Klop a 0o = nil) ∧
>(!a n u E.
>   Klop a n⁺ --u-> E <==>
>   u = label a ∧ E = Klop a n ∨ Klop a n --u-> E) ∧
> !a n u E.
>  islimit n ==> (Klop a n --u-> E <==> !m. m < n ∧ Klop a m --u-> E)
>
> I used new_axiom() to make above definion accepted by HOL. I don't know
> how to "prove" it, don't even know what to prove, because it's just a
> definition on a new logical constant (acts as a black-box function), while
> it's behaviour is exactly the same as if I have infinite sums in my
> datatype and HOL has the ability to define recursive function on ordinals.
>
> From now on, I need no other axioms at all. Then I can prove the following
> "rules" theorems which looks like the first return value of Hol_reln:
>
> |- (!a n. Klop a n⁺ --label a-> Klop a n) ∧
>!a n m u E. islimit n ∧ m < n ∧ Klop a m --u-> E ==> Klop a n --u-> E
>
> Then I can use transfinite inductino to prove a lot of other properties of
> the function ``Klop a``. And with a lot of work, finally I have proved the
> following elegant theorem in Concurrent Theory:
>
> Thm. (Coarsest congruence contained in weak equivalence)
>|- !g h. g ≈ʳ h <==> !r. g + r ≈ h + r
>
> ("≈ʳ" is observation congruence, or rooted weak bisimulation equivalence.
> "≈" is weak bisimulation equivalence)
>
> Every lemma or proof step corresponds to the original paper [1] with
> improvements or simplification. And if you let me to write down the
> informal proof (from the formal proof) using 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 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. (optionall) is there any hope to prevent using new_axiom() in my case?
>
> Best regards,
>
> Chun Tian
>
> [1] van Glabbeek, Rob J. "A characterisation of weak bisimulation
> congruence." Lecture notes in computer science 3838 (2005): 26.
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
> 

Re: [Hol-info] Vimhol key binding for showtypes

[Ramana Kumar]

I think 't' for 'terms' takes precedence in my head: I am rarely thinking
about quotations. There could be an argument for using 'q' for quiet mode
(instead of 'u'). But anyway, I'll make the j->y change now. Of course
anyone can easily change their mappings to whatever they want locally.

On 10 July 2017 at 23:36, Robert Künnemann <rob...@kunnemann.de> wrote:

>
> On 10/07, Ramana Kumar wrote:
>
>> A rather trivial thing: I'd like to change the default keybinding for
>> showtypes in the Vim mode from "j" to "y". Why? Because "y" is the second
>> letter of "types", so has some mnemonic value. (And all the other keys are
>> mnemonics.) Whereas "j" has nothing to do with types as far as I can tell.
>> On the keyboard, they're about as close together, so the main cost is on
>> those who've already learned the one shortcut to learn another. Strong
>> objections?
>>
>
> No, I'd be fine with it. But wouldn't it be even easier to memorize if
> hq and hQ were for quotations and then the t would be free, so ht could
> stand for types?
>
> Cheers, Robert
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A question about ordinals

[Ramana Kumar]

I have nothing to add here about the proof content, but I thought I'd
mention that there are lowercase versions of many tactics which could be
easier to type.
For example, your proof could start like this: "rpt gen_tac >> mp_tac
univ_ord_greater_cardinal".
The other style thing I'd say is to prefer qpat_x_assum over pat_x_assum,
and qspec_then over (Q.)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 doing much)

On 13 July 2017 at 09:26, Chun Tian (binghe)  wrote:

> Found a proof:
>
> open cardinalTheory ordinalTheory sumTheory;
>
> val ONE_ONE_IMP_EXISTS = store_thm ((* NEW *)
>"ONE_ONE_IMP_EXISTS",
>   ``!(A :'a set) (f :'a ordinal -> 'a). ONE_ONE f ==> ?n. !x. x IN A ==> x
> <> f n``,
> REPEAT GEN_TAC
>  >> MP_TAC univ_ord_greater_cardinal
>  >> RW_TAC std_ss [ONE_ONE_DEF, cardleq_def, INJ_DEF, IN_UNIV]
>  >> CCONTR_TAC
>  >> PAT_X_ASSUM ``!g. P``
> (MP_TAC o (Q.SPEC `\n. if n < omega then INL (@m.  = n) else INR
> (f n)`))
>  >> BETA_TAC
>  >> REPEAT STRIP_TAC
>  >> Cases_on `x < omega \/ x < omega` (* 2 sub-goals here *)
>  >| [ (* goal 1 (of 2) *)
>   FULL_SIMP_TAC std_ss [] \\
>   PAT_X_ASSUM ``(@m.  = x) = @m.  = y`` MP_TAC \\
>   REWRITE_TAC [] \\
>   NTAC 2 SELECT_ELIM_TAC \\
>   REPEAT STRIP_TAC >| (* 3 sub-goals here *)
>   [ (* goal 1.1 (of 3) *)
> PAT_X_ASSUM ``y < omega`` (ASSUME_TAC o (REWRITE_RULE [lt_omega]))
> \\
> PROVE_TAC [],
> (* goal 1.2 (of 3) *)
> PAT_X_ASSUM ``x < omega`` (ASSUME_TAC o (REWRITE_RULE [lt_omega]))
> \\
> PROVE_TAC [],
> (* goal 1.3 (of 3) *)
> 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) <
> binghe.l...@gmail.com> ha scritto:
> >
> > *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 proposition unless the infinite set B has the
> same type variable with the ordinals: ('a ordinal) and ('a set). Now
> there's a theorem in ordinalTheory saying that:
> >
> >[univ_ord_greater_cardinal]  Theorem
> >
> >   |- 핌(:'a inf) ≺ 핌(:'a ordinal)
> >
> > where (:'a inf) means the sum type: ``:num + 'a``.  Reading from right
> to left, it says there's no injection from 핌(:'a ordinal) to 핌(:'a inf).
> In another words, for all mappings g, there're x, y IN 핌(:'a ordinal) such
> that g(x) = g(y) but x <> y.
> >
> > If my original goal is not true, i.e. for all x IN 핌(:'a ordinal), f(x)
> in B. then the following mapping:
> >
> > g(x) = if x < omega then INL (@n. n = ) else INR f(x)
> >
> > will map each ('a ordinal) ordinals into B UNION univ(:num),   and the
> part from non-limit ordinals to univ(:num) is actually a bijection.   Now
> the result I got from univ_ord_greater_cardinal and the assumption (ONE_ONE
> f) are conflict, thus my original goal must be true.
> >
> > Do you agree?
> >
> > Regards,
> >
> > Chun
> >
> >
> > On 12 July 2017 at 22:53, Konrad 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?
> >
> > Konrad.
> >
> >
> > On Wed, Jul 12, 2017 at 12:50 PM, Chun Tian (binghe) <
> binghe.l...@gmail.com> wrote:
> > 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 B``?
> >
> > Regards,
> >
> > Chun Tian
> >
> >
> > 
> --
> > Check out the vibrant tech community on one of the world's most
> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> > ___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
> >
> >
> >
> > --
> > Chun Tian (binghe)
> > University of Bologna (Italy)
> >
> >
> >
> >
> > --
> > Chun Tian (binghe)
> > University of Bologna (Italy)
> >
>
>
> 
> --
> Check out the vibrant tech community on one of the world's 

[Hol-info] Vimhol key binding for showtypes

[Ramana Kumar]

Hi list,

A rather trivial thing: I'd like to change the default keybinding for
showtypes in the Vim mode from "j" to "y". Why? Because "y" is the second
letter of "types", so has some mnemonic value. (And all the other keys are
mnemonics.) Whereas "j" has nothing to do with types as far as I can tell.
On the keyboard, they're about as close together, so the main cost is on
those who've already learned the one shortcut to learn another. Strong
objections?

Cheers,
Ramana
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Difficulties in proving the termination of a recursive function

[Ramana Kumar]

You could make the definition with J as a list instead of a set. (Then you
can define a set version in terms of that using SET_TO_LIST if you want.)

Or you could do something like `FN p J = if FINITE J then case p of ...
else ARB`. But that's probably more trouble than using a list.

On 2 July 2017 at 00:52, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:

> > because J is *NOT* assumed to be FINITE.
>
> On 1 July 2017 at 16:51, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
>
>> No ... my previous idea doesn't work. I got this goal unprovable:
>>
>> CARD (J DELETE a) < CARD J
>> 
>>   a ∈ J
>>
>> because J is assumed to be FINITE.
>>
>> I think I still need to know how to put the cardinality bound into the
>> relation for WF_REL_TAC ...
>>
>> Regards,
>>
>> Chun
>>
>>
>> On 1 July 2017 at 16:28, Chun Tian (binghe) <binghe.l...@gmail.com>
>> 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 also rethink it as
>>> the set of contants that *remains to be processed*:
>>>
>>> So now I have a definition like this:
>>>
>>> val FN_defn = Hol_defn "FN" `
>>>(FN (nil :('a, 'b) CCS) (J: 'a set) = (EMPTY :'b Label set)) /\
>>>(FN (prefix (label l) p) J = l INSERT (FN p J)) /\
>>>(FN (prefix tau p) J = FN p J) /\
>>>(FN (sum p q) J = (FN p J) UNION (FN q J)) /\
>>>(FN (par p q) J = (FN p J) UNION (FN q J)) /\
>>>(FN (restr L p) J = (FN p J) DIFF (L UNION (IMAGE COMPL_LAB L))) /\
>>>(FN (relab p rf) J = IMAGE (REP_Relabeling rf) (FN p J)) /\
>>>(FN (var x) J = EMPTY) /\
>>>(FN (rec x p) J = if (x IN J) then
>>>  FN (CCS_Subst p (rec x p) x) (J DELETE x)
>>>  else EMPTY) `;
>>>
>>> and by following your way, using: WF_REL_TAC `inv_image ($< LEX $<) (\x.
>>> (size (FST x), CARD (SND x)))`, and then I have the following sub-goal
>>> which looks perfect: (and no need to prove the well-foundness any more)
>>>
>>>  Current goal:
>>>
>>>  size (CCS_Subst p (rec x p) x) < size (rec x p) ∨
>>>  (size (CCS_Subst p (rec x p) x) = size (rec x p)) ∧
>>>  CARD (J DELETE x) < CARD J
>>>  
>>>x ∈ J
>>>
>>> To actually use this definition, I need to set the initial J set as the
>>> set of all constants in the CCS term, but that's irrelevant to the above FN
>>> definition.  So I would say my initial problem has completely resolved.
>>>
>>> Thank you again!!!
>>>
>>> Regards,
>>>
>>> Chun Tian
>>>
>>>
>>> On 1 July 2017 at 12:55, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>>>
>>>> Hi Chun,
>>>>
>>>> Your relation that works looks like a lexicographic relation, which is
>>>> something wf_rel_tac should be able to handle automatically.
>>>> Could you try providing it using the LEX combinator, e.g.,
>>>> wf_rel_tac`inv_image ($< LEX $<) (\x y. (size(FST x), CARD(SND y)))`
>>>>
>>>> Actually, looking more closely, I see that you want the cardinality of
>>>> J to _increase_. This is not obviously well-founded: can you explain what
>>>> the upper limit of the cardinality of J is, and incorporate this into the
>>>> relation?
>>>>
>>>> Cheers,
>>>> Ramana
>>>>
>>>> On 1 July 2017 at 19:51, Konrad Slind <konrad.sl...@gmail.com> wrote:
>>>>
>>>>> Hi Chun Tian,
>>>>>
>>>>>  I'd have to look more closely at your desired function to be able to
>>>>> help.
>>>>> But, it's late and my eyes are giving out.
>>>>>
>>>>> If all you are after is to compute free names, maybe there is a better
>>>>> way.
>>>>> The following is what I would do for defining an operation calculating
>>>>> the free variables
>>>>> in the lambda calculus, and the same idea should I hope also work for
>>>>> CCS. The main benefit is that
>>>>> you don't have a call to another function (substitution) in the
>>>>> recursive call. And termination

Re: [Hol-info] Difficulties in proving the termination of a recursive function

[Ramana Kumar]

Hi Chun,

Your relation that works looks like a lexicographic relation, which is
something wf_rel_tac should be able to handle automatically.
Could you try providing it using the LEX combinator, e.g.,
wf_rel_tac`inv_image ($< LEX $<) (\x y. (size(FST x), CARD(SND y)))`

Actually, looking more closely, I see that you want the cardinality of J to
_increase_. This is not obviously well-founded: can you explain what the
upper limit of the cardinality of J is, and incorporate this into the
relation?

Cheers,
Ramana

On 1 July 2017 at 19:51, Konrad Slind  wrote:

> Hi Chun Tian,
>
>  I'd have to look more closely at your desired function to be able to
> help.
> But, it's late and my eyes are giving out.
>
> If all you are after is to compute free names, maybe there is a better way.
> The following is what I would do for defining an operation calculating the
> free variables
> in the lambda calculus, and the same idea should I hope also work for CCS.
> The main benefit is that
> you don't have a call to another function (substitution) in the recursive
> call. And termination
> is trivial.
> 
> ---
> load "stringLib";
>
> Datatype `term = Var string | App term term | Abs string term`;
>
> val FV_def =
>  Define
>   `(FV (Var s) scope = if s IN scope then {} else {s}) /\
>(FV (App t1 t2) scope = FV t1 scope UNION FV t2 scope) /\
>(FV (Abs v t) scope = FV t (v INSERT scope))`;
>
>
> On Sat, Jul 1, 2017 at 4:14 AM, Chun Tian (binghe) 
> wrote:
>
>> Hi,
>>
>> I have an inductive datatype called CCS and a recursive function FN
>> trying to collect all free names of any CCS term into a set:
>>
>> val FN_def = Define `
>>   (FN (nil :('a, 'b) CCS) (J: 'a set) = (EMPTY :'b Label set)) /\
>> ...
>>   (FN (rec x p) J = if (x IN J) then EMPTY
>>   else FN (CCS_Subst p (rec x p) x)
>>   (x INSERT J))`;
>>
>> val free_names = new_definition ("free_names",
>>  ``free_names p = FN(p, EMPTY)``);
>>
>> The only reason that HOL can’t prove the termination is because of the
>> last branch in above definition involving another recursive function
>> CCS_Subst: in some cases the term ``(CCS_Subst p (rec x p) x)`` may return
>> ``(rec x p)``, and as a result, the size of the first parameter of FN
>> doesn’t decrease!
>>
>> But this is why I have the second parameter J of FN: whenever calculating
>> the value of ``FN (rec x p) J``, it first check if x is in the set J, and
>> the recursive call happens only if it’s not in, and then x is inserted into
>> J to prevent further recursive invocation of FN at deeper levels.  So I
>> believe above definition is well-defined and must always terminate.  In
>> another words, for all other branches, the size of CCS term must decrease
>> in recursive calls, and in the last branch, the cardinality of the set J
>> will increase.
>>
>> I firstly tried to use WF_REL_TAC with a measure, but I could NOT find a
>> good measure with both parameters considered. For example, if I use “the
>> size of CCS term MINUS the cardinality of the set J”, which seems always
>> decrease in each recursive calls, i.e.  WF_REL_TAC `measure (\x. (size o
>> FST) x - (CARD o SND) x)`,   this is actually not a measure, because it may
>> also take negative values, thus not WF at all.
>>
>> Now if I try to use Defn.tgoal to find the tacticals which helps HOL to
>> prove the termination, I got the following initial goal:
>>
>> Initial goal:
>>
>> ∃R.
>>   WF R ∧
>>   (∀p J x.
>>  x ∉ J ⇒ R (CCS_Subst p (rec x p) x,x INSERT J) (rec x p,J)) ∧
>>   (∀q J p. R (p,J) (p || q,J)) ∧ (∀p J q. R (q,J) (p || q,J)) ∧
>>   (∀q J p. R (p,J) (p + q,J)) ∧ (∀p J q. R (q,J) (p + q,J)) ∧
>>   (∀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 recursive call must be strictly “smaller”.  But if I supply
>> such a relation:
>>
>> Q.EXISTS_TAC `\x y. (size (FST x) < size (FST y)) \/
>>((size (FST x) = size (FST y)) /\ (CARD (SND x) > CARD (SND y)))`
>>
>> which seems precisely captured my understanding on the termination
>> condition. But the funny thing is, I can prove all the sub-goals except for
>> the well-foundness (that is, WF R), 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.
>>
>> Regards,
>>
>> Chun Tian
>>
>> --
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>>
>>
>> 
>> --
>> Check out the vibrant tech community on one of the 

Re: [Hol-info] Changed order of qualified variables after SPEC_ALL and GEN_ALL

[Ramana Kumar]

If you're working with a conversion (term -> thm), from which you produce
your thm -> thm function via CONV_RULE, then I suggest looking at
STRIP_QUANT_CONV.

To avoid having to specify the types of variables explicitly, I suggest
looking at Q.GEN and Q.SPEC (and Q.ISPEC). To deal with lists of variables
at once, I suggest Q.GENL and Q.SPECL.

The specific functionality you asked for could be implemented as follows:

fun strip_forall_rule f th =
let val (vs,_) = strip_forall(concl th)
val th' = f (SPECL vs th)
in GENL vs th' end

e.g.,
val f = fst o EQ_IMP_RULE
val th = 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 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, variables appearing first will also come first in the
> results of GEN_ALL, but in above example, the variable C appears before B
> maybe because of specialities of “+”. Any way, this is not what I concerned
> most.
>
> In my developing theory, I often need to convert an equation theorem in
> weaker implication forms. For this purpose I have the following functions:
>
> fun EQ_IMP_LR thm = (GEN_ALL o fst o EQ_IMP_RULE o SPEC_ALL) thm;
> fun EQ_IMP_RL thm = (GEN_ALL o snd o EQ_IMP_RULE o SPEC_ALL) thm;
>
> But they’re not perfect: the resulting theorems usually have different
> orders for the qualified variables. And this may result into failures when
> actually using these theorems in other proofs in which some tacticals apply
> to only the first several qualified variables.  As a result, I have to
> create the following partial versions and then do the GEN_ALL by a series
> of GEN calls manually.
>
> fun EQ_IMP_LR' thm = (fst (EQ_IMP_RULE (SPEC_ALL thm)));
> fun EQ_IMP_RL' thm = (snd (EQ_IMP_RULE (SPEC_ALL thm)));
>
> So instead of having
>
> val TRANS_REC = save_thm ("TRANS_REC",
>   (EQ_IMP_LR TRANS_REC_EQ);
>
> Now I have to write this instead: (and I must know and supply the name and
> type of each qualified variable)
>
> val TRANS_REC = save_thm ("TRANS_REC",
>   ((GEN ``X :string``) o
>(GEN ``E :CCS``) o
>(GEN ``u :Action``) o
>(GEN ``E' :CCS``))
>   (EQ_IMP_LR' TRANS_REC_EQ));
>
> What I want to know is,  does anyone know (or have ever implemented) a
> general tools function, which can apply an arbitrary function of type (thm
> -> thm) between SPEC_ALL and things like a GEN_ALL, but the resulting
> theorems doesn’t change the orders of all qualified variables? (just first
> level would be enough for me)
>
> Regards,
>
> Chun Tian
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

[Ramana Kumar]

Hi Chun,

Try with the latest update 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) <binghe.l...@gmail.com> wrote:

> Hi,
>
> I see you have already consulted in OpenTheory mailing list and Joe Hurd
> has suggested to use the development version of OpenTheory. Now I see this
> error:
>
> Test.ot.art
> FAILED!
>  ('@temp
> @ind_typeTest0list'
> a1))
>   ('@temp @ind_typeTest0list'
>  a1'
>('@temp @ind_typeTest0list' a1' <=>
>   HOL4.Test.@temp @ind_typeTest7 (abs r) = r)) in
>   P (HOL4.min. P)
>  different constants at path 10110 subterms: HOL4.min.@ vs HOL4.min.
>  different constants: HOL4.min.@ vs HOL4.min.
>  different constant names
>
> I'm sorry for not understanding things at this level, only wondering: is
> this indicating a bug in HOL's OpenTheory module?
>
> Regards,
>
> Chun
>
>
>
>
> On 26 April 2017 at 03:57, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> 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 end of this email), but they look like
>> valid inputs to the "trans" function to me. It could be something to do
>> with the fact that some of the constants have been deleted, but I don't
>> know why this would make a difference to OpenTheory, which never deletes
>> anything.
>>
>> So maybe we should ask on the OpenTheory mailing list and supply the
>> Test.art file?
>>
>> first argument to trans:
>> #|- (∃abs.
>> #  (∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
>> #  ∀r.
>> #(λa1'.
>> #   ∀'Dertree' '@temp @ind_typeTest0list' .
>> # (∀a0'.
>> #(∃a0 a1.
>> #   (a0' =
>> #(λa0 a1.
>> #   ind_type$CONSTR 0 a0
>> # (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
>> #  a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
>> #'Dertree' a0') ∧
>> # (∀a1'.
>> #(a1' =
>> # ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
>> #(∃a0 a1.
>> #   (a1' =
>> #(λa0 a1.
>> #   ind_type$CONSTR (SUC (SUC 0)) ARB
>> # (ind_type$FCONS a0
>> #(ind_type$FCONS a1 (λn. ind_type$BOTTOM
>> #  a0 a1) ∧ 'Dertree' a0 ∧
>> #   '@temp @ind_typeTest0list' a1) ⇒
>> #'@temp @ind_typeTest0list' a1') ⇒
>> # '@temp @ind_typeTest0list' a1') r ⇔
>> #(Test$old1->@temp @ind_typeTest7<-old (abs r) = r)) ⇔
>> #   (λP. P ($@ P))
>> # (λabs.
>> #(∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
>> #∀r.
>> #  (λa1'.
>> # ∀'Dertree' '@temp @ind_typeTest0list' .
>> #   (∀a0'.
>> #  (∃a0 a1.
>> # (a0' =
>> #  (λa0 a1.
>> # ind_type$CONSTR 0 a0
>> #   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
>> #a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
>> #  'Dertree' a0') ∧
>> #   (∀a1'.
>> #  (a1' =
>> #   ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
>> #  (∃a0 a1.
>> # (a1' =
>> #  (λa0 a1.
>> # ind_type$CONSTR (SUC (SUC 0)) ARB
>> #   (ind_type$FCONS a0
>> #  (ind_type$FCONS a1
>> # (λn. ind_type$BOTTOM a0 a1) ∧
>> # 'Dertree' a0 ∧ '@temp @ind_typeTest0list' a1) ⇒
>> #  '@temp @ind_typeTest0list' a1') ⇒
>> #   '@temp @ind_typeTest0list' a1') r ⇔
>> #  (Test$old1->@temp @ind_typeTest7<-old (abs r) = r))
>>
>> second argument to trans:
>> #|- (λP. P ($@ P))
>> # (λabs.
>> #(∀a. abs (Test$old1

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

[Ramana Kumar]

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 error
messages you sent.

On 29 April 2017 at 23:25, Chun Tian (binghe) <binghe.l...@gmail.com> 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 got the next issue round line 3:
>
> FATAL ERROR: opentheory failed:
> in Article.fromTextFile:
> error in file "Test.art" around line 3:
> thm
> 13076
> ref
> …
> Rule.alpha: not alpha-equivalent
>
> Full logs in zip is in attach. (the mail is re-sent with compressed
> attachments)
>
> Regards,
>
> Chun Tian
>
>
>
>
> > Il giorno 29 apr 2017, alle ore 15:21, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> >> Il giorno 29 apr 2017, alle ore 01:02, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
> >>
> >> Hi Chun,
> >>
> >> Try with the latest update 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) <binghe.l...@gmail.com>
> wrote:
> >> Hi,
> >>
> >> I see you have already consulted in OpenTheory mailing list and Joe
> Hurd has suggested to use the development version of OpenTheory. Now I see
> this error:
> >>
> >> Test.ot.art
>  FAILED!
> >> ('@temp
> @ind_typeTest0list'
> >>a1))
> >>  ('@temp @ind_typeTest0list'
> >> a1'
> >>   ('@temp @ind_typeTest0list' a1' <=>
> >>  HOL4.Test.@temp @ind_typeTest7 (abs r) = r)) in
> >>  P (HOL4.min. P)
> >> different constants at path 10110 subterms: HOL4.min.@ vs HOL4.min.
> >> different constants: HOL4.min.@ vs HOL4.min.
> >> different constant names
> >>
> >> I'm sorry for not understanding things at this level, only wondering:
> is this indicating a bug in HOL's OpenTheory module?
> >>
> >> Regards,
> >>
> >> Chun
> >>
> >>
> >>
> >>
> >> On 26 April 2017 at 03:57, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> 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 end of this email), but they look like
> valid inputs to the "trans" function to me. It could be something to do
> with the fact that some of the constants have been deleted, but I don't
> know why this would make a difference to OpenTheory, which never deletes
> anything.
> >>
> >> So maybe we should ask on the OpenTheory mailing list and supply the
> Test.art file?
> >
>
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

[Ramana Kumar]

 ∧
#   '@temp @ind_typeTest0list' a1) ⇒
#'@temp @ind_typeTest0list' a1') ⇒
# '@temp @ind_typeTest0list' a1') r ⇔
#(Test$old1->@temp @ind_typeTest7<-old (abs r) = r))
# (@abs.
#(∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
#∀r.
#  (λa1'.
# ∀'Dertree' '@temp @ind_typeTest0list' .
#   (∀a0'.
#  (∃a0 a1.
# (a0' =
#  (λa0 a1.
# ind_type$CONSTR 0 a0
#   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
#a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
#  'Dertree' a0') ∧
#   (∀a1'.
#  (a1' =
#   ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
#  (∃a0 a1.
# (a1' =
#  (λa0 a1.
# ind_type$CONSTR (SUC (SUC 0)) ARB
#   (ind_type$FCONS a0
#  (ind_type$FCONS a1
# (λn. ind_type$BOTTOM a0 a1) ∧
# 'Dertree' a0 ∧ '@temp @ind_typeTest0list' a1) ⇒
#  '@temp @ind_typeTest0list' a1') ⇒
#   '@temp @ind_typeTest0list' a1') r ⇔
#  (Test$old1->@temp @ind_typeTest7<-old (abs r) = r))



On 26 April 2017 at 03:55, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:

> Hi again,
>
> The issue happens because of the following mini theory with just one
> datatype definition:
>
> open HolKernel Parse boolLib bossLib;
> val _ = new_theory "Test”;
>
> val _ = Datatype `Dertree = Der 'a (Dertree list)`;
>
> val _ = export_theory ();
>
> Error outputs:
>
>  FATAL ERROR: opentheory 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) <
> binghe.l...@gmail.com> ha scritto:
> >
> > Hi Ramana,
> >
> > Thanks for your detailed explanation.  For your question about what am I
> planning to do with the ot files, to be honest I have no plan. If I
> understand OpenTheory correctly, the theory I developed may be able to run
> in HOL light and Isabelle without full porting work, but currently I have
> no such need or interest at all.
> >
> > So I’m going to find out which exact theorem caused the issue first, and
> move this theorem (I hope it’s just one) into a whole new script file, then
> try to find out which proof step caused the issue. In case I can isolate
> the issue, I’ll ask help here 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 <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
> >>
> >> Hi Chun Tian,
> >>
> >> It's hard to know exactly what's wrong, but I expect there's a bug in
> the OpenTheory proof recording facility of HOL4, which is implemented in
> src/opentheory/postbool/Logging.sml.
> >>
> >> When you ask Holmake to generate an .ot.art file it first generates a
> raw .art file by recording all the proofs (and definitions etc.) in the
> theory directly, then it post-processes this .art file into the .ot.art
> file using the external opentheory tool. The external tool might have a
> bug, or, more likely, the original generated .art file is invalid. You can
> see the semantics of .art files on the OpenTheory website here:
> http://www.gilith.com/research/opentheory/article.html.
> >>
> >> One way to debug this would be to edit Logging.sml so that whenever it
> generates a "trans" line in the article, it first checks that the theorems
> it just logged really have the correct shape, and print them out if not.
> Another approach would be to try reading the generated .art file until it
> fails with your own custom reader that can print more debugging information
> (or maybe ask on the OpenTheory mailing list if the opentheory tool has
> some options for printing more info). There is code for reading articles in
> HOL4, under src/opentheory/postbool/Opentheory.sml.
> >>
> >> I hope that helps. What are you planning to do with the recorded
> OpenTheory packages when you get this to work?
> >>
> >> If you send me as small an example as you can make of the failure, I
> may be able to debug it. It might take me a while to find time for it
> though.
> >>
> >> Cheers,
> >> Ramana
> >>

Re: [Hol-info] "terms not alpha-equivalent" when outputing OpenTheory files

[Ramana Kumar]

Hi Chun Tian,

It's hard to know exactly what's wrong, but I expect there's a bug in the
OpenTheory proof recording facility of HOL4, which is implemented in
src/opentheory/postbool/Logging.sml.

When you ask Holmake to generate an .ot.art file it first generates a raw
.art file by recording all the proofs (and definitions etc.) in the theory
directly, then it post-processes this .art file into the .ot.art file using
the external opentheory tool. The external tool might have a bug, or, more
likely, the original generated .art file is invalid. You can see the
semantics of .art files on the OpenTheory website here:
http://www.gilith.com/research/opentheory/article.html.

One way to debug this would be to edit Logging.sml so that whenever it
generates a "trans" line in the article, it first checks that the theorems
it just logged really have the correct shape, and print them out if not.
Another approach would be to try reading the generated .art file until it
fails with your own custom reader that can print more debugging information
(or maybe ask on the OpenTheory mailing list if the opentheory tool has
some options for printing more info). There is code for reading articles in
HOL4, under src/opentheory/postbool/Opentheory.sml.

I hope that helps. What are you planning to do with the recorded OpenTheory
packages when you get this to work?

If you send me as small an example as you can make of the failure, I may 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 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 building process failed strangely saying “terms not alpha-equivalent”
> ?! like this:
>
> CutFree.ot.art
> FAILED!
>
>  FATAL ERROR: opentheory failed:
>  error in file "CutFree.art" around line 77960:
>  trans
>  10633
>  def
>  while executing trans command:
>  terms not alpha-equivalent
> Lambek.ot.art
> M-KILLED
> make: *** [all] Error 1
>
> The issue happens when generating *.ot.art files from *.art files. Maybe
> it’s an issue in “opentheory” but HOL?
>
> But any way, does anyone have any idea on what’s going on? the *.art files
> are so long and each line is so short, it’s unreadable to me, thus I have
> no idea which of my theorems (at line 77960) caused the issue:
>
> def
> 10614
> ref
> appTerm
> 10631
> def
> betaConv
> 10632
> def
> trans
> 10633   <—  line 77960
> def
> 10593
> ref
> 10599
> ref
> appTerm
> 10634
> def
> betaConv
>
> Regards,
>
> Chun Tian
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to eliminate existential quantifier in a goal about list?

[Ramana Kumar]

Better, in my opinion, is to use

e( qexists_tac`0` );

which parses the quotation in the context of the goal, so you don't need to
give an explicit type annotation.

On 13 April 2017 at 14:11, Thomas Tuerk  wrote:

> 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:num``);
>
> Cheers
>
> Thomas
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Problems building HOL from source

[Ramana Kumar]

On 3 April 2017 at 13:50, Lars Hupel  wrote:

> Dear list,
>
> I've been trying to build a recent commit of HOL (4b08982).
>
> My environment is Arch Linux x64, Poly/ML 5.6.
>
> This is the output of "bin/build":
>
>
> Building directory src/holyhammer/hh [03 Apr, 14:01:12]
> hh_parse.ml   / toolbox.. | Holmake: Fail exception: Unknown
> result status
>
> Build failed in directory /home/lars/work/reify/HOL/src/holyhammer/hh
> (exited with code 1)
>
>
Whatever the problem was here, it might have left some stale or incomplete
files in that directory, which might then be causing the subsequent
problems. You could clean the hh directory (either Holmake cleanAll or, for
really everything, git clean -xdf) before trying to build again.

As for avoiding the error above, you might like to try the fixes-5.6 branch
of Poly/ML rather than the released version, since I think there were some
bug fixes made that are relevant to parallel Holmake (I'm not sure).
Alternatively, try passing the -j1 option to bin/build (or Holmake), which
turns off the parallelism.


> If I re-run "bin/build" I get an error that seems to be related to OCaml:
>
> Building directory src/holyhammer/hh [03 Apr, 14:03:21]
> hh_parse.{cmi,cmx}
> FAILED!
>  File "hh_parse.ml", line 1:
>  Error: Could not find the .cmi file for interface hh_parse.mli.
> Build failed in directory /home/lars/work/reify/HOL/src/holyhammer/hh
> (exited with code 1)
>
>
> NB, the released Kananaskis 11 also fails to build, but with enough
> repeated invocations of "bin/build" it eventually succeeds.
>
> Cheers
> Lars
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to define PAT_X_ASSUM to PAT_ASSUM in K11 final release (and before) and do nothing in K12 (and later version)?

[Ramana Kumar]

OK... You could check directly whether "PAT_X_ASSUM" is bound in the PolyML
global namespace, and enter it if necessary:

val ns = PolyML.globalNameSpace;
val () = #enterVal ns ("PAT_X_ASSUM", Option.getOpt (#lookupVal ns
"PAT_X_ASSUM", Option.valOf(#lookupVal ns "PAT_ASSUM")));

There might be an easier way to conditionally make a declaration that 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) <binghe.l...@gmail.com> wrote:

> Hi… thanks, but it doesn’t work in HOL K11 final (where PAT_X_ASSUM is not
> defined):
>
> -
>HOL-4 [Kananaskis 11 (expknl, built Tue Mar 07 09:23:36 2017)]
>
>For introductory HOL help, type: help "hol";
>To exit type -D
> -
> > val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else
> PAT_X_ASSUM;
> poly: : error: Value or constructor (PAT_X_ASSUM) has not been declared
> Found near if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM
> Static Errors
>
> > Il giorno 25 mar 2017, alle ore 04:02, Ramana Kumar <
> ram...@member.fsf.org> 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 Tian (binghe) <binghe.l...@gmail.com>
> wrote:
> > 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
> assumption I want,  just like a more flexible version of  POP_ASSUM.
> >
> > My goal is to have my proof scripts being able to run in both K11 final
> release and current ongoing K12 versions, so when I need to “pop” an
> assumption, I always write it as PAT_X_ASSUM and having this line in all my
> *Script.sml 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 Tian
> >
> >
> > 
> --
> > Check out the vibrant tech community on one of the world's most
> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> > ___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to define PAT_X_ASSUM to PAT_ASSUM in K11 final release (and before) and do nothing in K12 (and later version)?

[Ramana Kumar]

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 Tian (binghe)  wrote:

> 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
> assumption I want,  just like a more flexible version of  POP_ASSUM.
>
> My goal is to have my proof scripts being able to run in both K11 final
> release and current ongoing K12 versions, so when I need to “pop” an
> assumption, I always write it as PAT_X_ASSUM and having this line in all my
> *Script.sml 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 Tian
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proving a trivial goal

[Ramana Kumar]

I didn't know about ELIM_UNCURRY - cool!

I would have done rw[GSYM pairTheory.LAMBDA_PROD] (after trying a bunch of
things that didn't work..)
Also, rw[FORALL_DEF,Once FUN_EQ_THM,pairTheory.UNCURRY] seems to work.

As for where this goal came from, I've seen it coming from EVAL_TAC before.

On 17 November 2016 at 03:38, Johannes Åman Pohjola 
wrote:

> (forgot to reply to list the first time)
>
> On 2016-11-16 17:35, Scott Owens wrote:
> > Thanks, that works.
> >
> > For the curious, the ELIM_UNCURRY theorem is ``∀f. UNCURRY f = (λx. f
> (FST x) (SND x))``. Not obviously relevant...
> >
> > Scott
> >
> >> On 2016/11/16, at 16:23, Johannes Åman Pohjola 
> wrote:
> >>
> >> Try this:
> >>
> >> REWRITE_TAC [pairTheory.ELIM_UNCURRY]
> >>
> >> Cheers / Johannes
> >>
> >>
> >> On 2016-11-16 17:04, Scott Owens wrote:
> >>> Does anyone know how to prove this goal:
> >>>
> >>> ∀(p1,p1',p2). T
> >>>
> >>> I’m not sure how I got it, and I can’t work out how to prove it, but
> it’s probably true :)
> >>>
> >>> Scott
> >>> 
> --
> >>> ___
> >>> hol-info mailing list
> >>> hol-info@lists.sourceforge.net
> >>> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> 
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Using HolyHammer

[Ramana Kumar]

I thought I would share the approach I have to using HolyHammer currently.
I put this in my .hol-config.sml file:

load"holyHammer";
fun hh_tac ls g =
  (Thread.Thread.fork
 ((fn () => holyHammer.hh ls (list_mk_imp g)),
  [Thread.Thread.EnableBroadcastInterrupt true]);
   ALL_TAC g)

Now, if I run hh_tac[] as a tactic in the middle of a proof, it will fork a
new thread (works in PolyML only) to search for a proof of the current
goal. Meanwhile I can keep working on trying to prove it manually. But if
eventually HolyHammer comes back with a proof, it will print out the call
to metis that I could have used at the point I called hh_tac.

You can pass more theorems in the list to hh_tac as context for HolyHammer
to use (which may not be visible to its database, e.g., if they are not yet
saved theorems).

If you try this and run into issues, I encourage you to reply to this email
and/or open some issues on the issue tracker.

Cheers,
Ramana
--
The Command Line: Reinvented for Modern Developers
Did the resurgence of CLI tooling catch you by surprise?
Reconnect with the command line and become more productive. 
Learn the new .NET and ASP.NET CLI. Get your free copy!
http://sdm.link/telerik___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] conservativity of HOL constant and type definitions

[Ramana Kumar]

Just to answer the question-mark in (2.1), I mechanised a proof that
new_type_definition is model-theoretically conservative for standard models
and arbitrary base theories. To be clear, the proof assumes the base theory
contains "fun", "bool", and "=", and that it has a model that interprets
these types/constants in the standard way. I presume this counts as
"arbitrary", but maybe it doesn't :) (The proof is at
https://github.com/CakeML/cakeml/blob/master/candle/standard/semantics/
holExtensionScript.sml#L366.)

On 25 October 2016 at 09:06, Andrei Popescu  wrote:

> The counterexample I had in mind is due to Makarius Wenzel (
> https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf, page 8): The
> theory T containing the single HOL formula "no type has cardinal 3" has a
> Henkin model M; yet, M has no expansion to the theory T extended with the
> definition of the type {1,2,3}. But actually this extension is not
> proof-theoretically conservative either (as it even breaks consistency) ...
>
>
> In fact, now I see that I have not clearly spelled out all the assumptions
> of the statements in my summary. So let me try again, also factoring in
> the base (i.e., to-be-extended)  theory:
>
>
> (1) The constant definition mechanisms (including the more general ones)
> are known to be:
> (1.1) model-theoretic conservative w.r.t. standard (Pitts) models and
> arbitrary base theories
> (1.2) model-theoretic conservative w.r.t. Henkin models and arbitrary
> base theories
> (1.3) proof-theoretic conservative and arbitrary base theories
>
> (2) The type definition mechanism is known to be:
> (2.1) model-theoretic conservative w.r.t. standard models and
> arbitrary(?) base theories
>
> and known *not* to be:
> (2.2) model-theoretic conservative w.r.t. Henkin models and arbitrary
> base theories
> (2.3) proof-theoretic conservative w.r.t. Henkin models and arbitrary
> base theories
>
> On the other hand, it is of course legitimate to lower the expectation for
> typedefs, so we could ask what happens with (2.2) and (2.3) if we restrict
> to base theories that are themselves definitional. Here, the above
> counterexample does not work. And yes, Rob, without being able to follow
> your Heyting arithmetic analogy, I do see the similarity between a possible
> semantic proof of definitional-base-(2.2) and a possible syntactic proof
> of definitional-base-(2.3) (both revolving around the notion of
> relativization to sets).
>
> But I am surprised that a lot of attention has been given to
> the conservativity of constant definitions/specifications, but not to that
> of the old and venerable typedef.
>
> Best,
>  Andrei
>
>
>
>
>
>
> --
> *From:* Rob Arthan 
> *Sent:* 24 October 2016 21:37
> *To:* Ondřej Kunčar
> *Cc:* Andrei Popescu; Prof. Andrew M. Pitts; Prof. Thomas F. Melham;
> cl-isabelle-us...@lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B.
> Andrews; HOL-info list
> *Subject:* Re: conservativity of HOL constant and type definitions
>
> Ondrej,
>
> > On 24 Oct 2016, at 20:32, Ondřej Kunčar  wrote:
> >
> > On 10/24/2016 09:16 PM, Rob Arthan wrote:
> >> I am pretty sure nothing has been published and, if you are right about
> (2.2),
> >> then I don't think type definitions can be proof-theoretically
> conservative.
> I made that sound too strong: I was just making a conjecture: for "think"
> read "feel".
>
> > They could. You can try to argue by "unfolding" the type definitions.
>
> "Unfolding" of types is exactly what I had in mind when I mentioned
> the methods used in connect with Heyting arithmetic.
>
> > Again, the model-theoretic conservativity is stronger than the
> proof-theoretic in general. And here you don't have an existential
> quantifier for type constructors so you [can't] use the approach as you did
> for constants.
>
> Yes, but if the unfolding approach works, you would have reduced the
> essential properties of the type definition to a statement about the
> existence
> of a certain subset of the representation type bearing a relationship with
> some
> siubsets of the parameter types and you would then be able to deduce
> model-theoretic conservativeness. That's why I felt, that if Andrei is
> right that
> the type definition principle is not model-theoretically conservative
> w.r.t.
> Henkin models (his point (2.2)), then it won't be proof-theoretically
> conservative
> either, because the unfolding argument must break down somewhere.
> It would be very useful to see an example of a type definition that is not
> conservative w.r.t. Henkin models.
>
> Regards,
>
> Rob.
>
>
>
>
> 
> --
> The Command Line: Reinvented for Modern Developers
> Did the resurgence of CLI tooling catch you by surprise?
> Reconnect with the command line and become more productive.
> Learn the new .NET and ASP.NET CLI. Get your free copy!
> 

Re: [Hol-info] change of email address

[Ramana Kumar]

I believe you can subscribe with your new address at
https://lists.sourceforge.net/lists/listinfo/hol-info.
(Of course, the list moderator may be willing to do that on your behalf
instead :))

On 1 October 2016 at 12:41, Brian Graham  wrote:

> My current email address (which this message originates from) will be gone
> next week.
>
>
>
> Can you please change it to: brian.t.grah...@gmail.com
>
>
>
> Thanks very much.
>
>
>
> Brian T. Graham
>
> Res (403) 287-2086
>
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, SlashDot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most 
engaging tech sites, SlashDot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A question about the definition of the function in HOL4

[Ramana Kumar]

Hi Ada,

It still looks like you might be mixing up ML and HOL. Are you trying to
define an ML function, or a HOL function?

In ML, the conjunction of two Boolean expressions can be formed using the
"andalso" operator.
Now, maybe you already defined /\ like this, and gave it infix status:

infix /\;
fun op /\ (a, b) = a andalso b;

Then I would expect your definition to work.

But please note that this is a definition in ML. If you want to make a
definition in HOL, use Define.
For example:

val ccdd_def = Define`ccdd a b c d = if ((a = b) /\ (c = d)) then T else F`;

Cheers,
Ramana


On 30 June 2016 at 22:51, Ada <956066...@qq.com> wrote:

> Hi,guys
> I am working with HOL4.
> I defined a function in HOL4,like following
> - fun ccdd a b c d  = if ((a = b) /\ (c = d)) then true else false;
> It responded that:
> ! Toplevel input:
> ! fun ccdd a b c d  = if ((a = b) /\ (c = d)) then true else false;
> ! ^^^
> ! Type clash: expression of type
> !   bool
> ! cannot have type
> !   'a -> 'b
> I can't understand it.
> Who know the reason?
> Thanks!
>
>
> --
> Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Certificate issue

[Ramana Kumar]

Hi Peter,

Thank you for the note. You were right, the certificate was expired. It has
now been renewed. Sorry for the trouble.
I am supposed to receive automated email notices when expiration is coming
up. I will now investigate why that did not seem to happen.

Cheers,
Ramana

On 28 June 2016 at 23:51, Peter Vincent Homeier <
palan...@trustworthytools.com> wrote:

> Dear Michael and Ramana,
>
> You may want to renew the certificate for the hol-theorem-prover.org
> website. The certificate that it is presenting, from Let's Encrypt
> Authority X3, is currently expired.
>
> Cheers,
> Peter
>
> --
>
>
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] TAKE_def and DROP_def should not be automatic rewrites

[Ramana Kumar]

Hi hol-info,

I want to ask whether anyone thinks these are good automatic rewrites in
listTheory?

|- (∀n. TAKE n [] = []) ∧
   ∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs
|- (∀n. DROP n [] = []) ∧
   ∀n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n − 1) xs

I find them annoying because they introduce a conditional, which then
causes subgoal splits when rewriting (with rw or srw_tac). While they are
sometimes good rewrites, I don't think they should be _automatic_, as they
currently are.

Shall we remove them from srw_ss?

On another note, is there a way to remove things from srw_ss after they
have been added? I see only how to do that for named fragments (which I
don't think the above rewrites are in one of).

Ramana
--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A question about the theorem in HOL4?

[Ramana Kumar]

FST is a function in logic, not in ML.

In this case, there does happen to be a similar function, called fst, in ML.

Are you trying to specify/prove something in logic? Or are you trying to
write an ML program?

On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote:

> Hi,guys
> I am working with HOL4.
> FST is in pairTheory, its definition is
>
>   [*FST*]  Theorem
>
>   |- ∀x y. FST (x,y) = x
>
>   But, When I use it  like following:
>
>   val n = FST (1,2);
>
>  It responses:
>
> ! Toplevel input:
> ! val n = FST (1,2);
> ! ^^^
> ! Type clash: expression of type
> !   thm
> ! cannot have type
> !   'a -> 'b
>
>  What is the reason? Does anyone know how to use it?
>
> Thanks!
>
>
> --
> Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL-Light Beginner Questions

[Ramana Kumar]

I expect it could be because the Boolean constants are spelled "T" and "F"
rather than "true" and "false" in the logic, so the latter are being
treated as free variables.

On 16 June 2016 at 01:09, Heiko Becker  wrote:

> Hello everyone,
>
> I am currently learning HOL-Light and therefore working through the
> tutorial from the official page.[1]
> To get a feeling for the inductive definitions, I started a
> formalization similar to the semantics on page 109.
> My problem is that when I try to define some small step semantics I get
> a failure saying that I have some unbound free variables, but I cannot
> resolve this failure.
>
> My formalization:
>
> let exp_INDUCT, exp_REC= define_type
>"exp = Var num
>| Const real
>| Plus exp exp
>| Sub exp exp
>| Mult exp exp
>| Div exp exp";;
>
> let exp_eval_SIMPS = define
>`(exp_eval (Var x) E = E x) /\
>(exp_eval (Const r) E = r) /\
>(exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
>(exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
>(exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
>(exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
>
> let bexp_INDUCT, bexp_REC = define_type
>"bexp = leq exp exp
>  | less exp exp";;
>
> let bval_SIMPS = define
>`(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E))
> /\
>(bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;
>
> let cmd_INDUCT, cmd_REC = define_type
>"cmd = Ass num exp cmd
> | Ite bexp cmd cmd
> | Nop";;
>
> let upd_env_simps1 = define
>`upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E
> y)`;;
>
> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
>`(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v
> E)) /\
>(! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
>(! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;
>
>
> When loading the sstep definitions I get the following failure:
>  Exception: Failure "new_definition: term not closed".
>
>
> Can someone maybe help me figuring out where this failure comes from?
>
> Thanks in advance.
>
> Best regards,
>
> Heiko
>
> ---
> [1]: https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf
>
>
> --
> What NetFlow Analyzer can do for you? Monitors network bandwidth and
> traffic
> patterns at an interface-level. Reveals which users, apps, and protocols
> are
> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
> J-Flow, sFlow and other flows. Make informed decisions using capacity
> planning
> reports.
> http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL Workshop 2016: Final call

[Ramana Kumar]

Thinking of submitting an abstract for the HOL workshop this year?
They are due tomorrow! It's easy to write one. Don't miss out :)
See the call below.

---


CALL FOR ABSTRACTS

   2016 International Workshop on
   the HOL Theorem Proving System
 (HOL'16)
 hosted by ITP-2016
  August 25-27, 2016, Nancy, France

https://hol-theorem-prover.org/workshops/hol16

IMPORTANT DATES

Abstract Submission 15th June 2016
Author Notification  1st July 2016

THEME

The theme of the workshop is ProTips. We invite both expert and
novice users to share tips and tactics for building efficient,
maintainable, and scalable formal developments. We are especially
interested to hear from the authors of new or neglected features that
could aid the engineering of large proofs. We also solicit opinions
from experienced users on good proof style.

A portion of the workshop will be dedicated to large examples,
including CakeML, exhibiting uses or opportunities to use the protips
above. We will also encourage discussion of, planning of, and hacking
on improvements to HOL and its applications during the workshop.

ABSTRACT SUBMISSION

To register your interest in discussing tips and tactics,
please submit a short abstract describing what you want to do and how
long you would like to have the floor (from 5 through 30 minutes).
There will be flexibility for impromptu talks and discussion, but we
highly encourage early submissions to give priority to
better-prepared work. See the website for submission details.

ABOUT

HOL4 is the latest version of the original theorem prover for
Higher-Order Logic, and is still a popular choice for programming
tactics and proof automation, and developing formal theories.
Continuing the workshop series started in 2014, we invite everyone
interested in the use and development of HOL to participate in this
year's workshop dedicated to improving both the tool itself and the
breadth of knowledge spread across its community of users.
--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Difficulty with higher order matching

[Ramana Kumar]

Hi Peter,

I'm not sure I can explain why HO_MATCH_MP_TAC is not powerful enough for
this kind of match, but I can say what would use instead in this situation.
Namely, numLib.LEAST_ELIM_TAC. More generally, I would use DEEP_INTRO_TAC
with theorems such as LEAST_ELIM, which is how LEAST_ELIM_TAC is
implemented.

Cheers,
Ramana

On 9 June 2016 at 07:35, Peter Vincent Homeier <
palan...@trustworthytools.com> wrote:

> I am trying to apply HO_MATCH_MP_TAC, but it is not successfully matching
> the consequent of the theorem to the current goal the way I thought it
> would. The example below is not meant to be a provable theorem, just a
> simple instance to show this issue.
>
> By the way, HO_PART_MATCH fails for this case as well.
>
> I can certainly force the matching to work by providing explicit
> substitutions, such as shown below, but this is both ugly and not robust
> for proof maintenance. The explicit substitutions show the original theorem
> can match the goal, but the matching substitution is not found by higher
> order matching in this case.
>
> What am I not understanding here? Why does higher order matching fail?
>
> Transcript:
>
> -
>HOL-4 [Kananaskis 11 (stdknl, built Tue May 24 15:32:51 2016)]
>
>For introductory HOL help, type: help "hol";
>To exit type -D
> -
> [extending loadPath with Holmakefile INCLUDES variable]
> [In non-standard heap:
> /usr/local/hol/cakeml/cakeml-master/candle/set-theory/heap]
> > > > > load "bitTheory";
> val it = (): unit
> > g `BIT (LEAST n. BIT n x) x`;
> val it =
>Proof manager status: 1 proof.
> 1. Incomplete goalstack:
>  Initial goal:
>
>  BIT (LEAST n. BIT n x) x
>
>
> :
>proofs
> > whileTheory.LEAST_ELIM;
> val it =
>|- ∀Q P. (∃n. P n) ∧ (∀n. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ Q n) ⇒ Q ($LEAST
> P):
>thm
> > e(HO_MATCH_MP_TAC whileTheory.LEAST_ELIM);
> OK..
>
> Exception raised at Tactic.HO_MATCH_MP_TAC:
> at HolKernel.ho_match_term:
> at Term.dest_comb:
> not a comb
> Exception-
>HOL_ERR
>  {message =
>   "at HolKernel.ho_match_term:\nat Term.dest_comb:\nnot a comb",
>   origin_function = "HO_MATCH_MP_TAC", origin_structure = "Tactic"}
>raised
>
>
> > (BETA_RULE o SPECL[``\a. BIT a x``,``\n. BIT n x``])
> whileTheory.LEAST_ELIM;
> val it =
>|- (∃n. BIT n x) ∧ (∀n. (∀m. m < n ⇒ ¬BIT m x) ∧ BIT n x ⇒ BIT n x) ⇒
>BIT (LEAST n. BIT n x) x:
>thm
> > e(HO_MATCH_MP_TAC ((BETA_RULE o SPECL[``\a. BIT a x``,``\n. BIT n x``])
> whileTheory.LEAST_ELIM));
> OK..
> 1 subgoal:
> val it =
>
> (∃n. BIT n x) ∧ ∀n. (∀m. m < n ⇒ ¬BIT m x) ∧ BIT n x ⇒ BIT n x
>
> :
>proof
> >
>
> Thanks for your help.
>
> Peter
>
>
>
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
>
> --
> What NetFlow Analyzer can do for you? Monitors network bandwidth and
> traffic
> patterns at an interface-level. Reveals which users, apps, and protocols
> are
> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
> J-Flow, sFlow and other flows. Make informed decisions using capacity
> planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Problem installing HOL 4

[Ramana Kumar]

PolyML 5.6 is supported by the development version of HOL4 (i.e., the head
of the master branch), and has been for a while.

On 24 May 2016 at 18:39, Chun Tian (binghe)  wrote:

> 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 libraries were installed there, but
>> the old ones were still in there causing trouble. Anyhow, purging the
>> old ones solved the issue.
>>
>> Many thanks
>>
>> Thomas
>>
>> On 24/05/16 07:23, Michael Norrish wrote:
>> > 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 
>> wrote:
>> >>
>> >> Hi all,
>> >>
>> >> I have a problem installing HOL 4, which is puzzling me. It would be
>> >> great if someone had a idea how to help me.
>> >>
>> >> I wanted to update my HOL 4 installation. I had an old PolyML installed
>> >> and got the error message that at least version 5.5.1 is needed. So, I
>> >> installed the latest version 5.6 and then ran
>> >>
>> >> poly < tools/smart-configure.sml
>> >>
>> >> I got a strange error message. I also tried with versions 5.5.2, 5.5.1
>> >> with same effect:
>> >>
>> >> -
>> >> Poly/ML 5.5.1 Release
>> >>
>> >> HOL smart configuration.
>> >>
>> >> Determining configuration parameters: holdir OS poly polymllibdir
>> >> OS: linux
>> >> poly:   /usr/local/bin/poly
>> >> polyc:  /usr/local/bin/polyc
>> >> polymllibdir:   /usr/local/lib
>> >> holdir: /home/thtuerk/HOL
>> >> DOT_PATH:   /usr/bin/dot
>> >>
>> >> Configuration will begin with above values.  If they are wrong
>> >> press Control-C.
>> >>
>> >> Will continue in 1 seconds.
>> >>
>> >> Loading system specific functions
>> >> Compiling system specific functions (sml)
>> >> Beginning configuration.
>> >> Making mllex
>> >> Making mlyacc
>> >>
>> >> The exported object file has version 5.51 but this library supports
>> >> 5.10-5.50
>> >> Failed to make mlyacc
>> >> -
>> >>
>> >> 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
>> >>
>> >>
>> --
>> >> Mobile security can be enabling, not merely restricting. Employees who
>> >> bring their own devices (BYOD) to work are irked by the imposition of
>> MDM
>> >> restrictions. Mobile Device Manager Plus allows you to control only the
>> >> apps on BYO-devices by containerizing them, leaving personal data
>> untouched!
>> >> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
>> >> ___
>> >> hol-info mailing list
>> >> hol-info@lists.sourceforge.net
>> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>> >
>> >
>> > 
>> >
>> > The information in this e-mail may be confidential and subject to legal
>> professional privilege and/or copyright. National ICT Australia Limited
>> accepts no liability for any damage caused by this email or its attachments.
>> >
>>
>>
>> --
>> Mobile security can be enabling, not merely restricting. Employees who
>> bring their own devices (BYOD) to work are irked by the imposition of MDM
>> restrictions. Mobile Device Manager Plus allows you to control only the
>> apps on BYO-devices by containerizing them, leaving personal data
>> untouched!
>> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
>
> --
> Chun Tian (binghe)
>
>
> --
> Mobile security can be enabling, not merely restricting. Employees who
> bring their own devices (BYOD) to work are irked by the imposition of MDM
> restrictions. Mobile Device Manager Plus allows you to control only the
> apps on BYO-devices by containerizing them, leaving personal data
> untouched!
> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> 

[Hol-info] HOL Workshop 2016: 2nd call for abstracts

[Ramana Kumar]

Don't forgot to submit an abstract for the HOL workshop this year :)
The submission deadline is under one month away.
See the call below.
---

CALL FOR ABSTRACTS

   2016 International Workshop on
   the HOL Theorem Proving System
 (HOL'16)
 hosted by ITP-2016
  August 25-27, 2016, Nancy, France

https://hol-theorem-prover.org/workshops/hol16

IMPORTANT DATES

Abstract Submission 15th June 2016
Author Notification  1st July 2016

THEME

The theme of the workshop is ProTips. We invite both expert and
novice users to share tips and tactics for building efficient,
maintainable, and scalable formal developments. We are especially
interested to hear from the authors of new or neglected features that
could aid the engineering of large proofs. We also solicit opinions
from experienced users on good proof style.

A portion of the workshop will be dedicated to large examples,
including CakeML, exhibiting uses or opportunities to use the protips
above. We will also encourage discussion of, planning of, and hacking
on improvements to HOL and its applications during the workshop.

ABSTRACT SUBMISSION

To register your interest in discussing the development agenda,
please submit a short abstract describing what you want to do and how
long you would like to have the floor (from 5 through 30 minutes).
There will be flexibility for impromptu talks and discussion, but we
highly encourage early submissions to give priority to
better-prepared work. See the website for submission details.

ABOUT

HOL4 is the latest version of the original theorem prover for
Higher-Order Logic, and is still a popular choice for programming
tactics and proof automation, and developing formal theories.
Continuing the workshop series started in 2014, we invite everyone
interested in the use and development of HOL to participate in this
year's workshop dedicated to improving both the tool itself and the
breadth of knowledge spread across its community of users.
--
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] What is the advantage of HOL4?

[Ramana Kumar]

Some strengths of HOL4 (off the top of my head, so maybe not comprehensive):

   - It is based on simple type theory. See "The seven virtues of simple
   type theory"
   .
   - It is implemented in Standard ML. This is a formally specified
   programming language with multiple implementations.
   - It exposes APIs that make it relatively easy to write theorem-proving
   automation. It is highly programmable.
   - It can export proofs in a standard format (OpenTheory). It also has an
   implementation-independent representation of saved theories.
   - It is a suite of tools following the Unix philosophy.
   - It has reasonably large libraries and various big and interesting
   examples, including CakeML.
   - It is being actively improved and developed, and is free software.
   - It has reasonably thorough documentation (not perfect, but pretty
   good).


On 3 May 2016 at 17:34, Ada <956066...@qq.com> wrote:

> Hi,guys
> I am working with HOL4. Recently, I read some papers, knowing that
> there are some other theorem provers, like PVS,COQ. They are similar in
> many aspects. For
> example, the logic used by them is Higher order logic. I am wondering What
> is the advantage of HOL4?
> Thanks!
>
>
> --
> Find and fix application performance issues faster with Applications
> Manager
> Applications Manager provides deep performance insights into multiple
> tiers of
> your business applications. It resolves application problems quickly and
> reduces your MTTR. Get your free trial!
> https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Instantiating existentials under existentials

[Ramana Kumar]

Depending on the body of the existential, you might be better off not
mentioning any of the variable names and instead using
part_match_exists_tac and a "pattern" that both picks out the `y` and
provides the `5`.

On 22 March 2016 at 07:12, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:

> Yes there is:
> CONV_TAC(RESORT_EXISTS_CONV(sort_vars["y"])) \\ qexists_tac`5`
>
> On 22 March 2016 at 07:08, Magnus Myreen <mo...@cam.ac.uk> wrote:
>
>> Hi hol-info,
>>
>> Quick question: is there a tactic for instantiating a nested
>> existential based on a name? Example: for a goal such as
>>
>>   ?x y z. ... y ...
>>
>> I want to use a tactic foo_tac `y` `5` and get:
>>
>>   ?x z. ... 5 ...
>>
>> Is there such a foo_tac tactic? I suspect this functionality is there
>> somewhere already. If not, then I'll implement it.
>>
>> Note: I don't need the advanced feature of being able to instantiate
>> it with `x+z+1` where the variables refer to the other existentially
>> quantified variables.
>>
>> Many thanks,
>> Magnus
>>
>>
>> --
>> Transform Data into Opportunity.
>> Accelerate data analysis in your applications with
>> Intel Data Analytics Acceleration Library.
>> Click to learn more.
>> http://pubads.g.doubleclick.net/gampad/clk?id=278785351=/4140
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
--
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785351=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A question about a proof with TAKE and DROP?

[Ramana Kumar]

Also, since the proof appears not to mention CX_def anywhere, it should be
possible to generalise the theorem to be about any two lists with the same
length (and not mention CX); that might be an easier statement to deal with.

On 15 March 2016 at 09:25, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:

> I was able to prove it as follows, but I needed to prove another lemma
> about TAKE which really should be in listTheory.
>
> open HolKernel boolLib bossLib Parse
>  listTheory rich_listTheory arithmeticTheory
>
> val _ = new_theory"ada"
>
> val CX_def = Define`
>   (CX [] p q = p) ∧
>   (CX (x::xs) p q =
>   TAKE x (CX xs p q) ++
>   DROP x (CX xs q p))`;
>
> val CX_length = Q.store_thm("CX_length",
>   `!l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q) = LENGTH p)`,
>   Induct \\ rw[CX_def,LENGTH_TAKE_EQ]);
>
> (* TODO: this should be moved to listTheory *)
> val TAKE_TAKE_EQ = Q.store_thm("TAKE_TAKE_EQ",
>   `TAKE n (TAKE m l) = TAKE (MIN n m) l`,
>   Cases_on`m < LENGTH l`
>   \\ rw[TAKE_LENGTH_TOO_LONG,MIN_DEF,TAKE_TAKE]);
> (* -- *)
>
> val ada_thm = Q.store_thm("ada_thm",
> `!p q. (LENGTH p = LENGTH q)
>  ==> !l m n .
>TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
>DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
>TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
>DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q)) `,
>   rw[TAKE_APPEND,DROP_APPEND,LENGTH_TAKE_EQ,CX_length,TAKE_TAKE_EQ]
>   \\ simp[MIN_COMM,DROP_DROP_T]
>   \\ Cases_on`n ≤ m` \\ fs[]
>   \\ rw[]
>   \\
> rw[LIST_EQ_REWRITE,LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
>   \\ TRY (`m - n  = 0` by DECIDE_TAC \\ pop_assum SUBST_ALL_TAC)
>   \\ TRY (`n - m  = 0` by DECIDE_TAC \\ pop_assum SUBST_ALL_TAC)
>   \\ fs[]
>   \\ Cases_on`x < n - m`
>   \\
> rw[LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
>   \\ Cases_on`x < m - n`
>   \\
> rw[LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
>   \\ qmatch_abbrev_tac`EL n1 ls = EL n2 ls`
>   \\ `n1 = n2` by (unabbrev_all_tac \\ decide_tac) \\ rw[]);
>
> val _ = export_theory();
>
> On 14 March 2016 at 19:06, Ada <ada.k...@qq.com> wrote:
>
>> Hi,guys
>> I am working with HOL4.
>> I am going to prove
>> g`!p q. (LENGTH p = LENGTH q)
>>  ==> !l m n .
>>TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
>>DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
>>TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
>>DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q)) `;
>> Where the definition of CX is
>>
>>   val CX_def = Define`
>>   (CX [] p q = p) ∧
>>   (CX (x::xs) p q =
>>   TAKE x (CX xs p q) ++
>>   DROP x (CX xs q p))`;
>>
>> I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q)
>> = LENGTH p)", named "CX_length".
>>
>> I had tried several times. But the proof failed. How to prove it?
>> Does anyone have any good idea?
>>
>> Thanks!
>>
>>
>> --
>> Transform Data into Opportunity.
>> Accelerate data analysis in your applications with
>> Intel Data Analytics Acceleration Library.
>> Click to learn more.
>> http://pubads.g.doubleclick.net/gampad/clk?id=278785231=/4140
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
--
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785231=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A question about a proof with TAKE and DROP?

[Ramana Kumar]

I was able to prove it as follows, but I needed to prove another lemma
about TAKE which really should be in listTheory.

open HolKernel boolLib bossLib Parse
 listTheory rich_listTheory arithmeticTheory

val _ = new_theory"ada"

val CX_def = Define`
  (CX [] p q = p) ∧
  (CX (x::xs) p q =
  TAKE x (CX xs p q) ++
  DROP x (CX xs q p))`;

val CX_length = Q.store_thm("CX_length",
  `!l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q) = LENGTH p)`,
  Induct \\ rw[CX_def,LENGTH_TAKE_EQ]);

(* TODO: this should be moved to listTheory *)
val TAKE_TAKE_EQ = Q.store_thm("TAKE_TAKE_EQ",
  `TAKE n (TAKE m l) = TAKE (MIN n m) l`,
  Cases_on`m < LENGTH l`
  \\ rw[TAKE_LENGTH_TOO_LONG,MIN_DEF,TAKE_TAKE]);
(* -- *)

val ada_thm = Q.store_thm("ada_thm",
`!p q. (LENGTH p = LENGTH q)
 ==> !l m n .
   TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
   DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
   TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
   DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q)) `,
  rw[TAKE_APPEND,DROP_APPEND,LENGTH_TAKE_EQ,CX_length,TAKE_TAKE_EQ]
  \\ simp[MIN_COMM,DROP_DROP_T]
  \\ Cases_on`n ≤ m` \\ fs[]
  \\ rw[]
  \\
rw[LIST_EQ_REWRITE,LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
  \\ TRY (`m - n  = 0` by DECIDE_TAC \\ pop_assum SUBST_ALL_TAC)
  \\ TRY (`n - m  = 0` by DECIDE_TAC \\ pop_assum SUBST_ALL_TAC)
  \\ fs[]
  \\ Cases_on`x < n - m`
  \\
rw[LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
  \\ Cases_on`x < m - n`
  \\
rw[LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
  \\ qmatch_abbrev_tac`EL n1 ls = EL n2 ls`
  \\ `n1 = n2` by (unabbrev_all_tac \\ decide_tac) \\ rw[]);

val _ = export_theory();

On 14 March 2016 at 19:06, Ada  wrote:

> Hi,guys
> I am working with HOL4.
> I am going to prove
> g`!p q. (LENGTH p = LENGTH q)
>  ==> !l m n .
>TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
>DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
>TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
>DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q)) `;
> Where the definition of CX is
>
>   val CX_def = Define`
>   (CX [] p q = p) ∧
>   (CX (x::xs) p q =
>   TAKE x (CX xs p q) ++
>   DROP x (CX xs q p))`;
>
> I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q) =
> LENGTH p)", named "CX_length".
>
> I had tried several times. But the proof failed. How to prove it? Does
> anyone have any good idea?
>
> Thanks!
>
>
> --
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785231=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785231=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Singletons belong to Borel sets

[Ramana Kumar]

Have you already proved the two lemmas you suggested already?
Namely: all singletons are closed, and all closed sets are Borel?
I would suggest proving those two separately first.

On 11 March 2016 at 06:41, Muhammad Qasim  wrote:

> Hello Everyone,
>
> I want to prove the following,
>
> `{PosInf} IN subsets Borel` or
> `{x:extreal} IN subsets Borel`
>
> Since all closed sets belong to Borel sets and all singletons are
> closed sets, it should be provable. I have tried different approaches
> but failed. Can someone suggest a way to prove it in HOL4?
>
> Thank you.
>
> Regards
>
> Qasim
>
>
>
> --
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785111=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785111=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

[Ramana Kumar]

If you want to build HOL with Poly/ML, you should run
  poly < tools/smart-configure.sml
before running bin/build.

On 2 March 2016 at 13:18, 康漫 <956066...@qq.com> wrote:

> Thank you for your reply!
> My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10
> 14:27:30 2014)], where Moscow ML version 2.01 (January 2004). Then from
> https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and
> pointed ""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon
> Feb 29 21:47:05 2016)],where Moscow ML version 2.01 (January 2004).
> I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ,
> it responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had
> downloaded the files in https://github.com/HOL-Theorem-Prover/HOL. How to
> add it to HOL4's directory? After that ,I could print  "open listTheory;"
> in HOL4, and use LENGTH_TAKE_EQ.
>
> Thanks.
>
>
>
> -- Original --
> *From: * "hol-info-request";;
> *Date: * Wed, Mar 2, 2016 06:31 AM
> *To: * "hol-info";
> *Subject: * hol-info Digest, Vol 118, Issue 1
>
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
>
> You can reach the person managing the list at
> 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: How to transform list format from "(cx l q p)" to "l"
>   (Anthony Fox)
>2. Re: Existential quantifier length (Michael Norrish)
>3. ? Summer School on Real-World Crypto and Privacy, June 5-10,
>   Croatia (Veelasha)
>
>
> --
>
> Message: 1
> Date: Mon, 29 Feb 2016 10:25:51 +
> From: Anthony Fox 
> Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
> to "l"
> To: ?? <956066...@qq.com>
> Cc: hol-info 
> Message-ID: <6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk>
> Content-Type: text/plain; charset=utf-8
>
> Which version of HOL4 are you using? The definitions of TAKE and DROP were
> altered in Jan 2008 (around about the time of kananaskis-5).
>
> With the latest version of HOL4 Jeremy Dawson?s suggestion works fine for
> me. The proof seems to be trivial. (I?ve not tried it with older versions
> of HOL4.) How exactly did you define ?cx??
>
> With
>
> val cx_def = Define`
>   (cx [] p q = p) /\
>   (cx (h :: t) p q = TAKE h (cx t p q) ++ DROP h (cx t q p))`
>
> we have
>
> val th = Q.prove(
>   `!p q l. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
>   Induct_on `l` THEN RW_TAC list_ss [cx_def, listTheory.LENGTH_TAKE_EQ])
>
> To get something closer to your definition of ?cx? I did
>
> val cx_def = tDefine "cx" `
>   (cx [] p q = p) /\
>   (cx (h :: t) p q =
>TAKE (HD (h :: t)) (cx (TL (h :: t)) p q) ++
>DROP (HD (h :: t)) (cx (TL (h :: t)) q p))`
>   (WF_REL_TAC `measure (\(x,y,z). LENGTH x)` THEN simp [])
>
> but the proof worked without modification.
>
> Regards,
> Anthony
>
> > On 29 Feb 2016, at 07:38, ?? <956066...@qq.com> wrote:
> >
> > Hi,Jeremy
> > Thank you for your reply!
> > I tried. But it can't work.
> > It responsed:
> > - e (RW_TAC list_ss [LENGRH_DROP]);
> > OK..
> > Exception raised at Tactical.VALID:
> > Invalid tactic
> > ! Uncaught exception:
> > ! HOL_ERR
> > I think the reason is that the format of "(cx l q p)"  is not equal to
> "l", though they are the same type "bool list".
> > Thank you!
> >
> > -- Original --
> > From:  "hol-info-request";;
> > Date:  Mon, Feb 29, 2016 01:08 PM
> > To:  "hol-info";
> > Subject:  hol-info Digest, Vol 117, Issue 9
> >
> > Send hol-info mailing list submissions to
> > hol-info@lists.sourceforge.net
> >
> > To subscribe or unsubscribe via the World Wide Web, visit
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> > or, via email, send a message with subject or body 'help' to
> > hol-info-requ...@lists.sourceforge.net
> >
> > You can reach the person managing the list at
> > 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. How to transform list format from "(cx l q p)" to "l" ( Ada )
> >2. Re: How to transform list format from "(cx l q p)" to "l"
> >   (Jeremy Dawson)
> >3. Two postdoc positions - Reasoning about concurrency and
> >   distribution - Imperial College London (Petar Maksimovic)
> >
> >
> > 

Re: [Hol-info] a question about rewrite in HOL4

[Ramana Kumar]

Section 6.2 (The Trace System) of the Description manual describes the
trace system.

Interactively, the functions traces and set_trace may be of interest. I
think the simplifier trace is called "simplifier".

On 6 March 2016 at 01:16, Piotr Trojanek  wrote:

> On Sat, Mar 5, 2016 at 3:04 AM, Michael Norrish
>  wrote:
> > I turned the simplifier trace on to see the following steps taken:
>
> The simplifier trace looks really nice! How do I turn it on? I do not
> see this in the documentation...
>
>
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] a question about rewrite in HOL4

[Ramana Kumar]

I think RW_TAC doesn't handle conditional rewrites very well. Try using rw
or simp instead.

This worked for me:

open listTheory

val cx_def = Define`
  (cx [] p q = p) ∧
  (cx (x::xs) p q =
  TAKE x (cx xs p q) ++
  DROP x (cx xs q p))`

val cx_length = Q.prove(
  `!l p q . (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
  Induct \\ simp[cx_def,LENGTH_TAKE_EQ]);

val th = Q.prove(
  `!p q n l.
(LENGTH p = LENGTH q) /\ (LENGTH p <= n) ==>
  LENGTH (cx l p q) <= n `,
  simp[cx_length]);


On 5 March 2016 at 01:06, Ada  wrote:

> Hi,guys
> I am working with HOL4.
> I am going to prove
> g`!p q n l. ( (LENGTH p = LENGTH q) /\ (LENGTH p <= n)) ==> (LENGTH
> (cx l p q) <=n ) `;
> Where the definition of cx is
>
>   val cx_def = Define`
>   (cx [] p q = p) ∧
>   (cx (x::xs) p q =
>   TAKE x (cx xs p q) ++
>   DROP x (cx xs q p))`
>
> I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) =
> LENGTH p)", named "cx_length"
> so I used,
> e (RW_TAC list_ss [cx_length]);
> But it can't work, does anyone know the reason?
>
> Thanks!
>
>
> --
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL breakthrough in American politics

[Ramana Kumar]

Wonderful! :-)

Though one should perhaps reconsider their media engagement strategy when
the majority of one's coverage is in The Onion.
On 4 Mar 2016 04:51, "Konrad Slind"  wrote:

>“By expanding on pioneering work in the fields of applied statistics,
> higher-order logic, and number theory, we’ve arrived at a new branch of
> mathematics that provides for a multitude of feasible outcomes in which
> Donald Trump is not the 2016 GOP nominee,”
>
>
> http://www.theonion.com/article/gop-statisticians-develop-new-branch-math-formulat-52463
>
> Konrad.
>
>
>
> --
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] RESTRICT left over in definition

[Ramana Kumar]

Yes, I thought that was one of the more likely possible causes. Let me
know if you can devise a better congruence rule that still gets the
termination argument to go through.

On 23 February 2016 at 15:40, Konrad Slind <konrad.sl...@gmail.com> wrote:
> Preliminary comment: the congruence rule looks a bit suspect. I doubt the
> termination condition extractor is setup to deal with pairs in the
> concluding equality of a congruence rule.
>
> Konrad.
>
>
> On Mon, Feb 22, 2016 at 9:36 PM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> wrote:
>>
>> Hi Konrad,
>>
>> Thanks for looking into this. I have made a cut-down version of the
>> problem in the attached script file. It should build in a recent
>> version of HOL without any prerequisites. The problem is that the
>> theorem returned by the final call to Define (for my_quote_exp_aux)
>> still contains RESTRICT. (In my real example, I also needed to provide
>> a termination tactic for this call, but in the cut down version
>> termination is proved automatically, but luckily for me the problem
>> still showed up.)
>>
>> Let me know if you figure it out.
>>
>> Cheers,
>> Ramana
>>
>> On 23 February 2016 at 04:39, Konrad Slind <konrad.sl...@gmail.com> wrote:
>> > Looks horrible. There shouldn't be remaining occurrences of RESTRICT.
>> > Termination-condition extraction should remove them all.
>> >
>> > Can you send me a cut-down version of the problematic function?
>> >
>> > Konrad.
>> >
>> >
>> > On Sun, Feb 21, 2016 at 5:34 AM, Ramana Kumar
>> > <ramana.ku...@cl.cam.ac.uk>
>> > wrote:
>> >>
>> >> I have managed to make a definition where the theorem returned to me
>> >> by tDefine still contains occurrences of ``RESTRICT new_func (@R. WF R
>> >> /\ ...)``.
>> >>
>> >> Is this to be expected from tricky input equations, or is it a sign of
>> >> a problem in the recursive function package?
>> >>
>> >> Would it be easy to post-process the resulting definition theorem to
>> >> remove the RESTRICT?
>> >>
>> >> As is usual in such situations, there is a fair amount of context
>> >> required to explore what's going on interactively, but if anyone is
>> >> interested the relevant definition is made here:
>> >>
>> >>
>> >> https://github.com/machine-intelligence/Botworld.HOL/blob/37747faa1eda333086612101023803967a8645e5/botworld_quoteScript.sml#L135
>> >>
>> >>
>> >>
>> >> --
>> >> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>> >> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>> >> Monitor end-to-end web transactions and take corrective actions now
>> >> Troubleshoot faster and improve end-user experience. Signup Now!
>> >> http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
>> >> ___
>> >> hol-info mailing list
>> >> hol-info@lists.sourceforge.net
>> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>> >
>> >
>
>

--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [Hol-developers] dep_rewrite

[Ramana Kumar]

What needs to be documented? I think I just meant put an "open
dep_rewrite" into bossLib.

On 22 February 2016 at 11:19, Michael Norrish
<michael.norr...@nicta.com.au> wrote:
> Please document somewhere, but yes.
>
> Michael
>
>> On 22 Feb 2016, at 09:24, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>>
>> So, yes?
>>
>> On 2 February 2016 at 15:51, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>>> On 2 February 2016 at 15:04, Michael Norrish <michael.norr...@nicta.com.au>
>>> wrote:
>>>>
>>>> Don't know.
>>>>
>>>> Is it clearly adding functionality we don't have any other way?
>>>
>>>
>>> Yes, I think so. The other way to get the functionality is cumbersome:
>>> abbreviate lots of your goal and try to instantiate the dependent rewrite
>>> theorem manually.
>>>
>>>>
>>>>
>>>> Is it big (makes a difference to Moscow ML); does it contaminate the
>>>> environment at all (declares new constants; adjusts grammars; adjusts other
>>>> global elements of the system)?
>>>
>>>
>>> It doesn't touch the logical environment, and I don't think it's very big.
>>>
>>> Implicational rewriting (issue #160) would be better, but we don't have
>>> that.
>>>
>>>>
>>>>
>>>> Michael
>>>>
>>>> On 2 Feb 2016, at 12:17, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>>>>
>>>> Tap tap tap... is this thing on?
>>>>
>>>> On 22 January 2016 at 17:56, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
>>>> wrote:
>>>>>
>>>>> Would there be any harm in adding dep_rewrite to the standard set of
>>>>> libraries that are loaded by default? (Similarly to how quantHeuristicsLib
>>>>> was added some time recently.)
>>>>
>>>>
>>>>
>>>> --
>>>> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>>> Monitor end-to-end web transactions and take corrective actions now
>>>> Troubleshoot faster and improve end-user experience. Signup Now!
>>>>
>>>> http://pubads.g.doubleclick.net/gampad/clk?id=267308311=/4140___
>>>> Hol-developers mailing list
>>>> hol-develop...@lists.sourceforge.net
>>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>>>
>>>>
>>>>
>>>> 
>>>>
>>>> The information in this e-mail may be confidential and subject to legal
>>>> professional privilege and/or copyright. National ICT Australia Limited
>>>> accepts no liability for any damage caused by this email or its 
>>>> attachments.
>>>
>>>
>
>
> 
>
> The information in this e-mail may be confidential and subject to legal 
> professional privilege and/or copyright. National ICT Australia Limited 
> accepts no liability for any damage caused by this email or its attachments.
>
> --
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] RESTRICT left over in definition

[Ramana Kumar]

I have managed to make a definition where the theorem returned to me
by tDefine still contains occurrences of ``RESTRICT new_func (@R. WF R
/\ ...)``.

Is this to be expected from tricky input equations, or is it a sign of
a problem in the recursive function package?

Would it be easy to post-process the resulting definition theorem to
remove the RESTRICT?

As is usual in such situations, there is a fair amount of context
required to explore what's going on interactively, but if anyone is
interested the relevant definition is made here:
https://github.com/machine-intelligence/Botworld.HOL/blob/37747faa1eda333086612101023803967a8645e5/botworld_quoteScript.sml#L135

--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL Workshop 2016: call for abstracts

[Ramana Kumar]

CALL FOR ABSTRACTS

   2016 International Workshop on
   the HOL Theorem Proving System
 (HOL'16)
 hosted by ITP-2016
  August 25-27, 2016, Nancy, France

https://hol-theorem-prover.org/workshops/hol16

IMPORTANT DATES

Abstract Submission 15th June 2016
Author Notification  1st July 2016

THEME

The theme of the workshop is ProTips. We invite both expert and
novice users to share tips and tactics for building efficient,
maintainable, and scalable formal developments. We are especially
interested to hear from the authors of new or neglected features that
could aid the engineering of large proofs. We also solicit opinions
from experienced users on good proof style.

A portion of the workshop will be dedicated to large examples,
including CakeML, exhibiting uses or opportunities to use the protips
above. We will also encourage discussion of, planning of, and hacking
on improvements to HOL and its applications during the workshop.

ABSTRACT SUBMISSION

To register your interest in discussing the development agenda,
please submit a short abstract describing what you want to do and how
long you would like to have the floor (from 5 through 30 minutes).
There will be flexibility for impromptu talks and discussion, but we
highly encourage early submissions to give priority to
better-prepared work. See the website for submission details.

ABOUT

HOL4 is the latest version of the original theorem prover for
Higher-Order Logic, and is still a popular choice for programming
tactics and proof automation, and developing formal theories.
Continuing the workshop series started in 2014, we invite everyone
interested in the use and development of HOL to participate in this
year's workshop dedicated to improving both the tool itself and the
breadth of knowledge spread across its community of users.

--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] word problem

[Ramana Kumar]

Scott informed me that it is likely false (e.g., take m = 1 and a = 2). I
can add additional assumptions that may help, though.

Alternatively, I have a variant of the problem that looks like this:

0. m < dimword (:'a)
1. a <= m
2. 0 < m
3. 0 < a

n2w m - n2w a < n2w m

That one seems more likely to be true. But how to prove it?

On 9 February 2016 at 10:02, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:

> Hi,
>
> Does anyone know whether the following goal is true or false?
>
> How would you prove it?
>
> If it's false, under what reasonable additional assumptions would it be
> true?
>
>   0.  m < dimword (:α)
>   1.  m < a
>   2.  0 < m
> 
> n2w m − n2w a < n2w m
>
> Cheers,
> Ramana
>
--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] word problem

[Ramana Kumar]

Hi,

Does anyone know whether the following goal is true or false?

How would you prove it?

If it's false, under what reasonable additional assumptions would it be
true?

  0.  m < dimword (:α)
  1.  m < a
  2.  0 < m

n2w m − n2w a < n2w m

Cheers,
Ramana
--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] About Binary Relations

[Ramana Kumar]

What's the problem/what is going wrong?

On 5 February 2016 at 17:48, Nadeem Iqbal <nadeem.iqbal...@gmail.com> wrote:

> Yes, I want the set of first components of the pairs. I replaced S with A,
> and used IMAGE FST (A CROSS A), but the problem is not solved.
>
>
>
> On Fri, Feb 5, 2016 at 8:52 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> wrote:
>
>> ``S CROSS S`` is a set of pairs. Although ``S`` is usually parsed as a
>> constant, so you might want to use a different letter, or use Parse.hide"S".
>>
>> Do you want the set of first components of the pairs? That would be
>> ``IMAGE FST (S CROSS S)``, and should be equal to ``S``.
>>
>> On 5 February 2016 at 14:42, Nadeem Iqbal <nadeem.iqbal...@gmail.com>
>> wrote:
>>
>>> Hi,
>>>
>>> Dear All,
>>>
>>> I am working in HOL4. I want to extract the domain of the set of binary
>>> relations.
>>> For example, when I tried this goal,
>>>
>>> g `! S. (FST (S CROSS S)) SUBSET (FST (S CROSS S))`;
>>>
>>> It could not run. Can any one guide me?
>>>
>>> Regards,
>>>
>>> Nadeem Iqbal
>>> HoD School of Computing and Information Sciences,
>>> Imperial College of Business Studies,
>>> Lahore, Pakistan.
>>>
>>>
>>>
>>> --
>>> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>> Monitor end-to-end web transactions and take corrective actions now
>>> Troubleshoot faster and improve end-user experience. Signup Now!
>>> http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
>>> ___
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>
>
--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] some questions about the proving process in HOL4

[Ramana Kumar]

listinfo/hol-info
> >
>
>
>
> --
>
> Message: 2
> Date: Tue, 15 Dec 2015 20:48:18 +0800
> From: " ?? " <956066...@qq.com>
> Subject: [Hol-info] [SPAM] Re: some questions about the proving
> process in HOL4
> To: " hol-info " <hol-info@lists.sourceforge.net>
> Message-ID: <tencent_7de4e1d26609f7a50013c...@qq.com>
> Content-Type: text/plain; charset="gb18030"
>
>
> Hi,Ramana,Thanks for your reply!
>after I used listTheory.LENGTH_NIL, I get that:
>  - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL);
> OK..
> 1 subgoal:
> > val it =
>  first 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>  : proof
>  Then Which tactic could be used to prove the goal? I tried many times
> , but it failed.
>  Thanks! -Wish
>
>
>
>
> --
>
> Message: 3
> Date: Tue, 15 Dec 2015 11:27:35 +0800
> From: " Ada " <ada.k...@qq.com>
> Subject: [Hol-info] [SPAM] some questions about the proving process in
> HOL4
> To: " hol-info " <hol-info@lists.sourceforge.net>
> Message-ID: <tencent_7f77ca956510ebe87ffaf...@qq.com>
> Content-Type: text/plain; charset="iso-8859-1"
>
> Hey guys,
>
> I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
>  When I was proving one property of TAKE, I find an interesting thing. As
> follows:
>  - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
> > val it =
>  TAKE 0 p = p
> 
>   LENGTH p = 0
>  : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
> > val it =
>  TAKE 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>   2.  !l n.
> (LENGTH l = NUMERAL (BIT1 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
>   3.  !l n.
> (LENGTH l = NUMERAL (BIT2 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
>   4.  !l n1 n2.
> (LENGTH l = n1 + n2) <=>
> ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
>  : proof
>  The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove that.
> Could anyone prove it?
>
>  Thanks! --Wish.
> -- next part --
> An HTML attachment was scrubbed...
>
> --
>
> Message: 4
> Date: Tue, 15 Dec 2015 14:34:44 +1100
> From: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> Subject: Re: [Hol-info] [SPAM] some questions about the proving
> process in HOL4
> To: Ada <ada.k...@qq.com>
> Cc: hol-info <hol-info@lists.sourceforge.net>
> Message-ID:
> 

Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

[Ramana Kumar]

fs[LENGTH_NIL,TAKE_def]

On 15 December 2015 at 14:27, Ada  wrote:

> Hey guys,
>
> I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
> When I was proving one property of TAKE, I find an interesting thing. As
> follows:
> - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
> > val it =
> TAKE 0 p = p
> 
>   LENGTH p = 0
>  : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
> > val it =
> TAKE 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>   2.  !l n.
> (LENGTH l = NUMERAL (BIT1 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
>   3.  !l n.
> (LENGTH l = NUMERAL (BIT2 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
>   4.  !l n1 n2.
> (LENGTH l = n1 + n2) <=>
> ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
>  : proof
> The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove that.
> Could anyone prove it?
>
> Thanks! --Wish.
>
>
> --
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Holmake Problem

[Ramana Kumar]

An opinion I'd like to share: if a package is broken, fixing the package so
everyone benefits is a better response than compiling the program from
source for yourself.

On 5 December 2015 at 03:21, Ian Zimmerman  wrote:

> On 2015-12-04 13:00 +0330, Ali Abbassi wrote:
>
> > I am using ubuntu, and I had problem using Poly/ML, so I used Moscow ML.
> > The problem is when I execute "poly < tools/smart-configure.sml" the
> error
> > below occurs :
> >
> > undefined reference to `__gxx_personality_v0'
>
> Do you have a packaged Poly/ML or have you compiled it yourself from
> source?  I recommend the latter.
>
> --
> Please *no* private copies of mailing list or newsgroup messages.
> Rule 420: All persons more than eight miles high to leave the court.
>
>
> --
> Go from Idea to Many App Stores Faster with Intel(R) XDK
> Give your users amazing mobile app experiences with Intel(R) XDK.
> Use one codebase in this all-in-one HTML5 development environment.
> Design, debug & build mobile apps & 2D/3D high-impact games for multiple
> OSs.
> http://pubads.g.doubleclick.net/gampad/clk?id=254741911=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] some questions about the use of HD and TL in listTheory

[Ramana Kumar]

HOL syntax for lists uses semicolons (;) to separate list elements, not
commas (,).

On 30 November 2015 at 18:42, Ada  wrote:

> Hey guys,
>
> I am learning to use HOL4. I defined a function named "first" in HOL4.
> This function can get the first n elements in a list. As follows:
>
> - val first_def = Define`(first [] n = [] )
>/\ (first (p::pl) 0 = [] )
>/\ (first (p::pl) n = HD (p::pl) :: first (TL
> (p::pl)) (n-1)) `;
> <>
> Equations stored under "first_def".
> Induction stored under "first_ind".
> > val first_def =
> |- (!n. first [] n = []) /\ (!pl p. first (p::pl) 0 = []) /\
>!v4 pl p.
>  first (p::pl) (SUC v4) =
>  HD (p::pl)::first (TL (p::pl)) (SUC v4 - 1) : thm
> In which, I saw HD and TL had been defined in listTheory. HD gets the
> first element in a list, TL gets the last.
>
> But , when I tried to use "first", failed. As followes:
>
> - first ([0,1,0,1,0],3);
> ! Toplevel input:
> ! first ([0,1,0,1,0],3);
> ! ^
> ! Type clash: expression of type
> !   ('a -> bool) -> 'a list -> 'a
> ! cannot have type
> !   'b * 'c -> 'a list -> 'a
>
> - first  [0,1,0,1,0] 3;
> ! Toplevel input:
> ! first  [0,1,0,1,0] 3;
> ! ^^
> ! Type clash: expression of type
> !   'a list
> ! cannot have type
> !   'b -> bool
>
> I was wondering why it failed. Could anyone find the reasion?
>
> Thanks! --Wish.
>
>
> --
> Go from Idea to Many App Stores Faster with Intel(R) XDK
> Give your users amazing mobile app experiences with Intel(R) XDK.
> Use one codebase in this all-in-one HTML5 development environment.
> Design, debug & build mobile apps & 2D/3D high-impact games for multiple
> OSs.
> http://pubads.g.doubleclick.net/gampad/clk?id=254741551=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741551=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] irule vs MP_CANON

[Ramana Kumar]

I'd say a big difference is that irule can only be used as a tactic,
whereas MP_CANON is a rule that can be used in more general situations.

Could the technology inside irule be split out into a rule or conversion,
or is it essentially a tactic?

On 17 November 2015 at 00:39, Jeremy Dawson <jeremy.daw...@anu.edu.au>
wrote:

> Hi Ramana,
>
> Well, they are both ways of matching the final consequent of a1 ==> a2
> ==> a3 ==> ... ==> c with the goal.
>
> Until I saw your question I hadn't been aware of the existence of
> MP_CANON.
>
> Possibly the biggest difference is that irule will produce multiple new
> subgoals (eg, in the above case, one for each ai - except as noted below).
>
> There's a bit of reimplementation of irule recently and continuing,
> involving the behaviour when there are variables some of the ai but not
> in c, (like MATCH_MP_TAC, it introduces existentials, which also may
> require collecting together some of the ai) which may affect ordering
> and exact form of the new subgoals.
>
> Cheers,
>
> Jeremy
>
>
>
> On 16/11/15 22:28, Ramana Kumar wrote:
> > What is the difference between irule and (match_mp_tac o MP_CANON)?
> >
> > I'm more interested in differences in the intended design than in minor
> > details in the implementation. Which is preferred style? Which should
> > get more developer time?
> >
> > Maybe they're actually rather different, but as far as I saw, from a
> > brief look, they are intended to do the same thing.
> >
> >
> >
> --
> > Presto, an open source distributed SQL query engine for big data,
> initially
> > developed by Facebook, enables you to easily query your data on Hadoop
> in a
> > more interactive manner. Teradata is also now providing full enterprise
> > support for Presto. Download a free open source copy now.
> > http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140
> >
> >
> >
> > ___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>
> --
> Presto, an open source distributed SQL query engine for big data, initially
> developed by Facebook, enables you to easily query your data on Hadoop in a
> more interactive manner. Teradata is also now providing full enterprise
> support for Presto. Download a free open source copy now.
> http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741551=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Definition of Binary Relation in HOL

[Ramana Kumar]

maybe this?
val relns_def = Define`relns A = { R | R x y ==> x IN A /\ y IN A }`

On 20 November 2015 at 14:29, Muhammad Nadeem Iqbal
<muhammadnadeemiq...@uoslahore.edu.pk> wrote:
> Let me rephrase my problem:
>
> I have a set A and I want the definition of set of binary relations between
> A and A in HOL.
>
> Regards,
> Nadeem
>
> On Thu, Nov 19, 2015 at 4:21 PM, Yong Kiam <tanyongk...@gmail.com> wrote:
>>
>> Or you can type annotate them:
>>
>> Define`numeq (x:num) y <=> x = y`
>>
>> which gives numeq with type num -> num -> bool
>>
>> On Thu, Nov 19, 2015 at 7:14 PM, Ramana Kumar <ram...@member.fsf.org>
>> wrote:
>>>
>>> How about this?
>>> Define`issucsuc x y <=> x < y /\ (y - 2 = x)`;
>>>
>>> On 19 November 2015 at 10:31, Muhammad Nadeem Iqbal
>>> <muhammadnadeemiq...@uoslahore.edu.pk> wrote:
>>> > in your first example, you have specified two constants to x and y.
>>> > Mine is
>>> > a bit different case. I want the one in which there should not be such
>>> > specification.
>>> >
>>> > On Wed, Nov 18, 2015 at 10:28 PM, Ramana Kumar <ram...@member.fsf.org>
>>> > wrote:
>>> >>
>>> >> Which binary relation? What do you mean?
>>> >>
>>> >> Here's a binary relation that relates natural numbers 1 and 2:
>>> >> val a_binary_relation_def = Define`a_binary_relation x y <=> (x = 1)
>>> >> /\ (y
>>> >> = 2)`;
>>> >>
>>> >> Here's a binary relation that relates two Booleans iff exactly one of
>>> >> them
>>> >> is true:
>>> >> val another_binary_relation_def = Define`
>>> >> (another_binary_relation T T = F) /\
>>> >> (another_binary_relation T F = T) /\
>>> >> (another_binary_relation F T = T) /\
>>> >> (another_binary_relation F F = F)`;
>>> >>
>>> >> On 18 November 2015 at 17:01, Muhammad Nadeem Iqbal
>>> >> <muhammadnadeemiq...@uoslahore.edu.pk> wrote:
>>> >>>
>>> >>> I have a query that how can we define a binary relation in HOL with a
>>> >>> specified type?
>>> >>>
>>> >>>
>>> >>>
>>> >>>
>>> >>>
>>> >>> --
>>> >>>
>>> >>> ___
>>> >>> hol-info mailing list
>>> >>> hol-info@lists.sourceforge.net
>>> >>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>> >>>
>>> >>
>>> >
>>> >
>>> >
>>> > --
>>> >
>>> > ___
>>> > hol-info mailing list
>>> > hol-info@lists.sourceforge.net
>>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>>> >
>>>
>>>
>>> --
>>> ___
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] proof structure in Coq

[Ramana Kumar]

I usually use ">>" instead of literally "THEN". Arguably that's still too
much "shift".

Yes I think you're right about tactician - it's for going back and forth
between those styles.

On 18 November 2015 at 08:41, Freek Wiedijk  wrote:

> Hi Ramana,
>
> >Apparently Coq somewhat recently gained the ability to be explicit about
> >proof structure:
> >http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html
> >(Of course that comes naturally when using tacticals like THEN, THEN1,
> etc.)
>
> Not _very_ recently.  It was introduced in 8.4, which is
> from late 2011.  And maybe Ssreflect had it long before
> that already?  (In my opinion Ssreflect is a much underrated
> proof language, even if it looks like perl.)
>
> Of course in Flyspeck many (most?) proofs are the other
> way around, where there is just a list of tactics that is
> processed like you would successively "e" them interactively.
> I think Mark Adams tactician is exactly about converting
> a THEN-THEN proof to that format?
>
> But I agree that a more structured "bulleted" proof is nicer.
> Even though ergonomically of course having to type THEN
> is monstrous.
>
> Freek
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] how to prove by contradiction

[Ramana Kumar]

It's also worth mentioning

`~A` by PROVE_TAC[]

since it can sometimes be faster than metis_tac.

On 17 November 2015 at 07:16, Ramana Kumar <ram...@member.fsf.org> wrote:

> there are many options:
>
> `~A` by metis_tac[]
>
> `~A` by (strip_tac >> fs[])
>
> first_assum(assume_tac o CONTRAPOS) >> res_tac
>
> first_x_assum(imp_res_tac o CONTRAPOS)
>
> Cases_on`A` >> fs[]
>
> `~A` by (spose_not_then strip_assume_tac >> res_tac)
>
> `~A` by (CCONTR_TAC >> fs[])
>
> ...
>
> On 17 November 2015 at 02:25, shengyu shen <shengyus...@icloud.com> wrote:
>
>> Dear all:
>>
>> suppose that I have two assuptions:
>>
>> 1 A->B
>> 2 ~B
>>
>> So which tactic should I use to get the conclusion  ~A?
>>
>> Shen
>>
>>
>> --
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] how to search my theorems with DB.match

[Ramana Kumar]

The call should look like:

DB.match theories pattern-term

where theories is a list of names of theories in which to search for the
pattern-term. If you leave the list empty, it searches in all theories in
the current hierarchy. I think if you give "-" as a the name, it might
search in the current theory.

You can also use print_apropos as an alternative to DB.match [].

On 16 November 2015 at 11:59, shengyu shen  wrote:

> Dear all:
>
> I know that I can search some particular theorem xx with DB.match like
> this :
>
>
> DB.match ["xx"] pattern
>
> but how can I search the set of theorem proved by me in current session ?
>
>
> Shen
>
>
> --
> Presto, an open source distributed SQL query engine for big data, initially
> developed by Facebook, enables you to easily query your data on Hadoop in a
> more interactive manner. Teradata is also now providing full enterprise
> support for Presto. Download a free open source copy now.
> http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Presto, an open source distributed SQL query engine for big data, initially
developed by Facebook, enables you to easily query your data on Hadoop in a 
more interactive manner. Teradata is also now providing full enterprise
support for Presto. Download a free open source copy now.
http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] irule vs MP_CANON

[Ramana Kumar]

What is the difference between irule and (match_mp_tac o MP_CANON)?

I'm more interested in differences in the intended design than in minor
details in the implementation. Which is preferred style? Which should get
more developer time?

Maybe they're actually rather different, but as far as I saw, from a brief
look, they are intended to do the same thing.
--
Presto, an open source distributed SQL query engine for big data, initially
developed by Facebook, enables you to easily query your data on Hadoop in a 
more interactive manner. Teradata is also now providing full enterprise
support for Presto. Download a free open source copy now.
http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] implicitely referring to large set of proven theorems in METIS_TAC

[Ramana Kumar]

val mythms = [thm1, th2, th3, ..., th20];
fun metis_extra_tac ths = metis_tac (ths@mythms);

... e(metis_extra_tac [...])...


On 15 November 2015 at 11:54, shengyu shen  wrote:

> Dear all:
>
> assume that I have proven a large number of theorems, for example , 20,
> can I make METIS_TAC to use them without explictly list all of them?
>
>
> Shen
>
>
> --
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [HOL-INFO] programming mode in HOL4?

[Ramana Kumar]

Use computeLib.EVAL.

On 14 November 2015 at 13:23, shengyu shen  wrote:

> Dear all:
>
> I have some experience in ACL2 and COQ, which have a programming mode, in
> which I can try running some function. For example, I define a fact
> function that compute the factorial of a particular integer n. And in both
> ACL2 and Coq, I can run this function to test if it is defined corectly.
>
> But in HOL4, how can I do this?
>
> Shen
>
>
> --
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

[Ramana Kumar]

I have this problem again. Can anyone help?

% camlp5 -v
Camlp5 version 6.14 (ocaml 4.02.3)

hol-light % make
\
if test `ocamlc -version | cut -c1-3` = "3.0"  ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
cut -c1-6` = "6.02.1" ; \
 then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
 else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.'
| cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.06" ; \
  then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
  else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.08" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.11" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.12" ; \
   then cp pa_j_3.1x_6.11.ml pa_j.ml; \
   else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' |
cut -c1`.xx.ml pa_j.ml; \
   fi \
  fi \
 fi \
fi
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
   then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo"
-I `camlp4 -where` pa_j.ml; \
   else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
q_MLast.cmo" -I `camlp5 -where` pa_j.ml; \
   fi
File "pa_j.ml", line 1918, characters 35-43:
While expanding quotation "str_item":
Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type'
(in
  [str_item])
File "pa_j.ml", line 1:
Error: Error while running external preprocessor
Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' >
/tmp/ocamlpp428d9c

Makefile:40: recipe for target 'pa_j.cmo' failed
make: *** [pa_j.cmo] Error 2


On 19 September 2014 at 09:38, Nela Cicmil 
wrote:

> Thanks again for everyone's replies.
>
> @Marco: After typing hol_light and waiting a few minutes for the warnings
> stop, HOL Light seems to be running fine by this Nix installation. Thank
> you!
>
> @Mark: I'm not sure why this combination isn't working for my Mac when
> Ocaml, camlp5 and HOL Light are installed individually. I removed and
> re-downloaded HOL Light via svn, checked the ocaml & camlp5 versions again
> in the hol_light directory, used make clean followed by make, and the same
> error appeared (copied in below).
>
> @Ramana: Thank you for pointing out the HOL Light Workbench link -
> actually I had come across it earlier via
> http://www.eng.utah.edu/~cs6110/install-hol-light.html - sorry I didn't
> to mention this in my original email. Unfortunately, this automated
> approach did not work for my Mac. I didn't make a record of the errors but
> as far as I remember the automated script installation of ocaml failed, so
> camlp5 installation failed and HOL Light did not run.
>
> In any case, I shall now press on with HOL Light as installed with Nix -
> thanks again.
>
> All the best,
> Nela
>
> hol_light nc$ ocaml -version
> The OCaml toplevel, version 4.01.0
> hol_light nc$ camlp5 -v
> Camlp5 version 6.11 (ocaml 4.01.0)
> hol_light nc$ make clean
> rm -f pa_j.ml pa_j.cmi pa_j.cmo hol hol.multivariate hol.sosa hol.card
> hol.complex;
> hol_light nc$ make
> \
> if test `ocamlc -version | cut -c1-3` = "3.0"  ; \
> then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
> else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
> cut -c1-6` = "6.02.1" ; \
>  then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
>  else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
> -f1-3 -d'.' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.06" ; \
>   then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
>   else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut 

Re: [Hol-info] Emacs Macros for HOL Light Proof

[Ramana Kumar]

You forgot to mention the comprehensive Vim mode for HOL4.
(See tools/vim in the HOL4 repository.)

On 4 November 2015 at 16:22, Joe Leslie-Hurd  wrote:
> For those of you who use HOL Light in an Emacs shell, I wrote some
> simple Emacs Lisp macros to support interactive proof:
>
> https://github.com/gilith/hol-light-emacs
>
> It's just basic stuff, but I have found that they speed up proof
> development (and the jump-to-proof-point is a boon to proof
> maintenance).
>
> These macros fill a gap between more comprehensive efforts: Michael
> Norrish's hol-mode for interacting with HOL4 in Emacs, and Freek
> Wiedijk's vi mode for HOL Light.
>
> Cheers,
>
> Joe
>
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] What would you like from a HOL workshop?

[Ramana Kumar]

Dear HOL users and developers,

I will endeavour to organise a workshop for HOL, to be co-located with ITP
2016 (France, end of August).

Before planning the details, I want to ask you: what kind of workshop would
serve you best?

Please send me any requests or comments, and together we can use this
opportunity to create an event of high value. (Early replies appreciated;
at some point decisions must be made.)

Cheers,
Ramana
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] EVAL WHILE

[Ramana Kumar]

To my surprise, EVAL went into a loop on the following term:
``WHILE (\x. x = 0) (\x. x) 1``

I thought in the default setup, EVAL would only evaluate the first argument
of a conditional, reducing it to true or false, skipping the other
arguments (the then and else branches) until it was known which one to
follow.

Now, even if that is not the default behaviour of EVAL, I can't even figure
out how to set up a compset to get that behaviour. Does anyone know how?

The default setup uses lazyfy_thm on COND_CLAUSES, with a set_skip of NONE,
which I would have thought would be right, but it goes into a loop on the
above term.
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] map_option

[Ramana Kumar]

Hi Jeremy,

Thanks for the links and information. It's rather more than I was
expecting. Do you (or anyone on list) think that function deserves a place
(perhaps under a different name) in optionTheory?

Cheers,
Ramana

On 25 September 2015 at 21:21, Jeremy Dawson <jeremy.daw...@anu.edu.au>
wrote:

> Hi Ramana,
>
> It's rather a similar situation to what I wrote about in
>
> http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/fgs/fgs.pdf
>
> and also
>
> http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/cats/fgc.ps
>
> except that I seem to have used sets instead of lists (which I don't think
> should make a difference), and I seem to not have noticed that I was
> reinventing the standard option type.
>
> I used these types to represent a non-deterministic computation with the
> possibility of non-termination.
>
> For the 'a set option result type, a computation is regarded as (let's
> say) "unreliable" and so non-terminating, when there is only the
> possibility of non-termination.
> For the 'a option set result type, you are interested in the possible
> (terminating) results even when non-termination is also possible.
>
> Both types, ie, 'a option set, and 'a set option, are compound monads, and
> your function is a monad morphism, which is also used in a certain
> construction which can be used to prove that the latter is indeed a
> compound monad.
>
> Cheers,
>
> Jeremy
>
>
> On 20/09/15 18:08, Ramana Kumar wrote:
>
>> Hi all,
>>
>> I think this must be some neat combination of category theory things.
>> Does anyone know which? Or if it's already defined somewhere?
>>
>> val map_option_def = Define`
>>(map_option [] = SOME []) ∧
>>(map_option (NONE::_) = NONE) ∧
>>(map_option (SOME x::ls) =
>> case map_option ls of
>> | SOME ls => SOME(x::ls)
>> | NONE => NONE)`;
>>
>> Cheers,
>> Ramana
>>
>>
>> --
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] map_option

[Ramana Kumar]

Hi all,

I think this must be some neat combination of category theory things.
Does anyone know which? Or if it's already defined somewhere?

val map_option_def = Define`
  (map_option [] = SOME []) ∧
  (map_option (NONE::_) = NONE) ∧
  (map_option (SOME x::ls) =
   case map_option ls of
   | SOME ls => SOME(x::ls)
   | NONE => NONE)`;

Cheers,
Ramana

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Unicode versions

[Ramana Kumar]

What is the difference between these functions?

Parse.overload_on
Parse.Unicode.uoverload_on
Parse.Unicode.unicode_version

Which ones should be used when? Does more than one need to be used at once?
From some of my recent playing around, it seems like unicode_version
sometimes but not always requires an additional call to one of the overload
functions before the parser recognises the unicode version. That is pretty
confusing behaviour.
--
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Final call for abstracts (HOL4 Workshop)

[Ramana Kumar]

Hi all,

A reminder: the deadline for abstracts for the upcoming HOL4 Workshop is
less than one week away. All details can be found at the website:

https://www.cl.cam.ac.uk/~rk436/hol15/

We look forward to receiving your abstracts, and to seeing you in Berlin
for the workshop!
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Question about rewriting in proofs

[Ramana Kumar]

In both cases it sounds like the problem is that rewriting is rewriting too
much - you only want to rewrite a particular occurrence of a term.
You might try using ONCE_REWRITE_RULE or Once.
If that doesn't work, you can be much more specific about where you apply
rewriting by using the rewriting conversion directly and other
conversion-builders above it to specify a particular position in the term.
For example, in your situation (1), if D looks like !a b c. D0 == (D1 /\
D2), I would do:
CONV_TAC(STRIP_QUANT_CONV(RAND_CONV(LAND_CONV(REWRITE_CONV[UNDISCH_ALL
rewrite_th]. The various _CONV functions help me locate the specific
part of the term where I want to apply REWRITE_CONV. I used UNDISCH_ALL on
the theorem that actually does the rewrite, because you said the
assumptions are necessary, so I'm assuming rewrite_th looks like |- A == B
== C == D1 = D1'.

On 21 May 2015 at 12:39, Robert White ai.robert.wangsh...@gmail.com wrote:

 Dear all,

 Happy proving :)

 1) I wonder how I suppose to tackle situation like this
 A, B, C |- D.
 and D is a complicated term with D1 and D2 somewhere in it.

 D1 can be rewrite to D1' under assumption of A,B,C while if I simply use
 the ASM_REWRITE_RULE  then I will do some other changes in D which I don't
 want to.

 2) Another related question: is there any way I can deal with situation
 like
 A, B, C |- D but I want to replace C by C' where C = C'
 one way in my mind is to get
 A, B |- C == D then use rewrite to get C' == D as concl but, that may
 lead to the change in D as well.

 It would be very nice if you can give me some advice.

 Thanks very much!

 --

 Regards,
 Robert


 --
 One dashboard for servers and applications across Physical-Virtual-Cloud
 Widest out-of-the-box monitoring support with 50+ applications
 Performance metrics, stats and reports that give you Actionable Insights
 Deep dive visibility with transaction tracing using APM Insight.
 http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info


--
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Question about rewriting in proofs

[Ramana Kumar]

Another option is to abbreviate the parts of the term that you don't want
to be rewritten. See Q.PAT_ABBREV_TAC for example.

On 21 May 2015 at 13:12, Ramana Kumar ram...@member.fsf.org wrote:

 In both cases it sounds like the problem is that rewriting is rewriting
 too much - you only want to rewrite a particular occurrence of a term.
 You might try using ONCE_REWRITE_RULE or Once.
 If that doesn't work, you can be much more specific about where you apply
 rewriting by using the rewriting conversion directly and other
 conversion-builders above it to specify a particular position in the term.
 For example, in your situation (1), if D looks like !a b c. D0 == (D1 /\
 D2), I would do:
 CONV_TAC(STRIP_QUANT_CONV(RAND_CONV(LAND_CONV(REWRITE_CONV[UNDISCH_ALL
 rewrite_th]. The various _CONV functions help me locate the specific
 part of the term where I want to apply REWRITE_CONV. I used UNDISCH_ALL on
 the theorem that actually does the rewrite, because you said the
 assumptions are necessary, so I'm assuming rewrite_th looks like |- A == B
 == C == D1 = D1'.

 On 21 May 2015 at 12:39, Robert White ai.robert.wangsh...@gmail.com
 wrote:

 Dear all,

 Happy proving :)

 1) I wonder how I suppose to tackle situation like this
 A, B, C |- D.
 and D is a complicated term with D1 and D2 somewhere in it.

 D1 can be rewrite to D1' under assumption of A,B,C while if I simply use
 the ASM_REWRITE_RULE  then I will do some other changes in D which I don't
 want to.

 2) Another related question: is there any way I can deal with situation
 like
 A, B, C |- D but I want to replace C by C' where C = C'
 one way in my mind is to get
 A, B |- C == D then use rewrite to get C' == D as concl but, that may
 lead to the change in D as well.

 It would be very nice if you can give me some advice.

 Thanks very much!

 --

 Regards,
 Robert


 --
 One dashboard for servers and applications across Physical-Virtual-Cloud
 Widest out-of-the-box monitoring support with 50+ applications
 Performance metrics, stats and reports that give you Actionable Insights
 Deep dive visibility with transaction tracing using APM Insight.
 http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info



--
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL Workshop 2015

[Ramana Kumar]

  SECOND CALL FOR ABSTRACTS

 2015 International Workshop on HOL4
   The HOL Theorem Proving System
 (HOL'15)
 hosted by CADE-25
   August 2-3, 2015, Berlin, Germany

https://www.cl.cam.ac.uk/~rk436/hol15/

The deadline for expressions of interest to present an idea at the workshop
is
next month! I encourage and welcome anyone who has any interest in HOL4 to
submit something. The original call for abstract follows.

IMPORTANT DATES

Abstract Submission 15th June 2015
Author Notification  1st July 2015

INVITED SPEAKER

HOL4's lead developer, Michael Norrish, will speak at the workshop.

THEME

The theme of the workshop is the development agenda. We hope to gather
both users and developers of HOL4 to brainstorm and decide:
  - What tasks or projects (from small to large scale) should we prioritise
for HOL4's continued development?
  - How can we apply the latest developments in the fields of automated and
interactive theorem proving back to HOL4, and is it worth it?
  - Should HOL4 merge with or evolve into another system?
  - How might we increase the amount of developer time put into the system
(e.g., attracting new users, holding more workshops)?

Being co-located with CADE, we also intend the workshop to be
beginner-friendly with the possibility of some tutorial introductions, and
we hope to focus some of the time on integrating ATP with ITP.

Specific development ideas can be found on the workshop website:
  https://www.cl.cam.ac.uk/~rk436/hol15/

ABSTRACT SUBMISSION

To register your interest in discussing the development agenda, please
submit a short abstract describing what you want to do and how long you
would like to have the floor (from 5 through 30 minutes). There will be
flexibility for impromptu talks and discussion, but we highly encourage
early submissions to give priority to better-prepared work.

Submission is via EasyChair:
  https://easychair.org/conferences/?conf=hol15

ABOUT

HOL4 is the latest incarnation of the original theorem prover for
Higher-Order Logic, and is still a popular choice for programming
tactics and proof automation, and developing formal theories.
Continuing the workshop series started last year, we invite everyone
interested in the use and development of HOL4 to participate in this
year's workshop dedicated to improving both the tool itself and the
breadth of knowledge spread across its community of users.
--
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Bindings for embedded languages in HOL

[Ramana Kumar]

There is an example of a nominal datatype in
HOL4/examples/unification/triangular/nominal.

On Wed, Mar 18, 2015 at 4:10 PM, Petros Papapanagiotou p...@ed.ac.uk
wrote:

 Hello everyone,

 Having reached the ceiling of what I can achieve by hacking variable
 bindings and substitutions for embedded languages in HOL Light, I am now
 looking for a better way to deal with these.

 I have gone through some of the results of the (now almost 10yo!)
 POPLmark challenge and subsequent papers, and I am aware of the existing
 HOAS and Nominal libraries in Coq and/or Isabelle. Has anything related
 been done in HOL Light or HOL4?

 I came across the HOL4/examples/lambda theories. These may be just
 enough for what I need, but any pointers to other work that I have
 missed would be valuable.

 Thank you.

 Regards,
 Petros




 --
 Petros Papapanagiotou, Ph.D.
 CISA, School of Informatics
 The University of Edinburgh

 Email: p...@ed.ac.uk

 ---
 The University of Edinburgh is a charitable body, registered in
 Scotland, with registration number SC005336.


 --
 Dive into the World of Parallel Programming The Go Parallel Website,
 sponsored
 by Intel and developed in partnership with Slashdot Media, is your hub for
 all
 things parallel software development, from weekly thought leadership blogs
 to
 news, videos, case studies, tutorials and more. Take a look and join the
 conversation now. http://goparallel.sourceforge.net/
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info

--
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Viewing HOL proofs

[Ramana Kumar]

One method is editor integration, which makes the process of viewing the
proof less painful than manual copy-paste.

In HOL4 there is integration for both Vim (
https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim) and Emacs,
which might be a suitable starting point. (These essentially just automate
the copy-paste process.)

For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is
perhaps even better for interactive proof-viewing, since it also keeps
track of where you are up to in the editor buffer, and shows all subgoals
of the proof in the viewing terminal.

What you really want is something like Proviola (
http://mws.cs.ru.nl/proviola/). Something like that could be implemented
for HOL Light, with a bit of work.

I made something 4 years ago for annotating proofs. I'll copy an email I
sent to Michael Norrish about it (probably should have gone to this list!),
in case it's helpful. The code linked from the email is still there.

I've decided that HTML is too difficult at the moment.
 I also looked at MathML - seems like it would be worthwhile writing a
 function to turn a HOL term into a Content MathML ... thing (i.e. a
 math element), and then use some stylesheet magic to turn the
 Content MathML into Presentation MathML that can be viewed in
 (basically not) any browser. I tried doing this for a few hours but
 got too confused about what MathML actually is and how to write it
 properly... do you know if there are any XML tools for SML?

 But the real purpose of this email is to tell you what I did succeed with!
 1. Some tactics for annotating a proof, and
 2. Some technology for turning an annotated proof into LaTeX.

 Code is here https://github.com/xrchz/CERN-LHC-BLMTC-SRS/tree/explanation
 In particular, see annotate.{sig,sml}, the proof of
 output_input_at_update_times in simplifiedScript.sml, and proof.tex.

 For 1, the basic idea is a tactic that acts like ALL_TAC but takes a
 string description of what's going on and side-effects some reference
 with the description and the current proof state.
 So while you're stepping through your proof you can insert  ... THEN
 anno_tac Now we apply some theorem and it simplifies as follows.
 THEN ... at significant points in the proof to save the state for
 later viewing.
 Actually it's a bit more ugly than that, and I would appreciate any
 pointers on how to make it nicer.
 The overall design might (i.e. side effects) might also be considered
 ugly, in which case don't bother :) - but any better ideas?

 For 2, I use EmitTeX to do most of the work.
 Perhaps the most interesting things here are my pretty-printings rules
 for dealing with SIGMA (\m. f m) (count n) and n ** m, which get them
 to print nicely in LaTeX.
 I had to use a custom printer for the sums.
 There's a lot of hackery here too, in particular with getting the
 pretty-printer to think that the superscripts and subscripts for SIGMA
 are of 0 width, so it doesn't think the lines are much longer than
 they actually are.
 Is there a better way to do that?
 LaTeX dies when there are linebreaks in the source inside a \sp or \sb
 inside an alltt, so it's really annoying if the pretty-printer puts
 them in.



On Fri, Mar 13, 2015 at 12:56 AM, Petros Papapanagiotou p...@ed.ac.uk
wrote:

 Hello,

 You might find Mark Adams's Tactician helpful:
 http://www.proof-technologies.com/tactician/index.html

 It can break down packaged proofs to g() and e() statements (among
 other things).

 I am not aware of any other alternatives.

 Also, unless I misunderstood, you can use b() to undo a proof step in an
 interactive proof.

 Hope this helps.

 Regards,
 Petros


 On 13/03/2015 00:07, Mario Carneiro wrote:
  Hello all,
 
  What is the usual method for viewing a proof stored in HOL Light, if
  you wanted to read it like a regular math textbook (assuming you can get
  over syntax difficulties)? (Of course it is not really feasible to look
  at the code in isolation, because you can't see the formulas.) The
  method I have been using so far is to copy the tactics one at a time
  into a HOL session using g() and e(), but it's very tedious and
  time-consuming, and it is also difficult to undo if you make a copying
  mistake during the process. (I should note that I am still a relative
  newbie to using HOL Light and this is essentially the only thing I have
  tried to do with it - I have yet to write an actual proof of my own in
  HOL Light.)
 
  I feel like this is a common enough goal that there should be some
  program to do what I am doing and log the output. Better yet, if there
  was a website or downloadable collection of these proofs processed into
  a form that did not require interactivity in the OCaml session, this
  would make it much easier for mathematicians who do not necessarily want
  to write proofs but want to examine the many existing HOL Light proofs
  in order to understand them (like me). Does such a thing exist?
 
  Mario Carneiro
 
 
 
 

Re: [Hol-info] Inductive_set definition in HOL4

[Ramana Kumar]

The Description Manual for HOL4 explains how to use Hol_reln. I think it
would prefer you to define sigma_sets as a predicate (i.e. without using
IN). Of course, you end up with the same set (since sets and predicates are
the logically the same in HOL).

Try this:
Hol_reln `
  (!sp st. sigma_sets sp st {}) /\
  (!sp st a. a IN st == sigma_sets sp st a) /\
  (!sp st a. sigma_sets sp st a == sigma_sets sp st (sp DIFF a)) /\
  (!sp st A. (!i. sigma_sets sp st ((A:num-'a-bool) i)) ==
 sigma_sets sp st (BIGUNION {A i | i IN UNIV}))`;

(I don't know if the last rule is what you intended, I made a guess.)


On Wed, Mar 11, 2015 at 8:23 PM, Muhammad Qasim m_q...@encs.concordia.ca
wrote:

 Hello Sir,

 I am trying to write the sigma_sets definition in isabelle. I tried
 Hol_reln as following.

 Hol_reln `(!sp st. {} IN sigma_sets sp st) /\
   (!sp st a. a IN st == a IN sigma_sets sp st) /\
   (!sp st a. a IN sigma_sets sp st == sp DIFF a IN sigma_sets sp st)
 /\
   (!sp st A i. (A:num-'a-bool) i IN sigma_sets sp st ==
BIGUNION {A i | i IN UNIV} IN sigma_sets sp st)`;

 and it gives me unification failure. I guess it is different.

 Regards

 Qasim

 Quoting Ramana Kumar ram...@member.fsf.org:

  Is this something different from what Hol_reln will give you?
 
  On Tue, Mar 10, 2015 at 6:33 PM, Muhammad Qasim 
 m_q...@encs.concordia.ca
  wrote:
 
  Hello Everyone,
 
  I saw an inductive_set definition in Isabelle. Is there a way to do
  such definitions in HOL4?
 
  Thank you.
 
  Regards
 
  Qasim
 
 
 
 
 --
  Dive into the World of Parallel Programming The Go Parallel Website,
  sponsored
  by Intel and developed in partnership with Slashdot Media, is your hub
 for
  all
  things parallel software development, from weekly thought leadership
 blogs
  to
  news, videos, case studies, tutorials and more. Take a look and join the
  conversation now. http://goparallel.sourceforge.net/
  ___
  hol-info mailing list
  hol-info@lists.sourceforge.net
  https://lists.sourceforge.net/lists/listinfo/hol-info
 
 




 --
 Dive into the World of Parallel Programming The Go Parallel Website,
 sponsored
 by Intel and developed in partnership with Slashdot Media, is your hub for
 all
 things parallel software development, from weekly thought leadership blogs
 to
 news, videos, case studies, tutorials and more. Take a look and join the
 conversation now. http://goparallel.sourceforge.net/
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info

--
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] type grammar for munger

[Ramana Kumar]

I'm having a lot of trouble trying to remove a type abbreviation when using
the HOL-TeX munger. I make the munger with a main theory that calls
Parse.disable_tyabbrev_printing reln. And if I load this theory in an
interactive HOL session and type ``:'a - 'a - bool`` it prints back as I
expect. But if I use \HOLty{:'a - 'a - bool} in my LaTeX document and run
it through the munger, it prints as 'a reln in the resulting tex file.

I've also tried making the munger with a ppLib.sml that explicitly sets the
type grammar to something that does not include reln (using
type_grammar.remove_abbreviation), but it still appears in the output! How
does the grammar for the munger get determined?
--
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Holmake broken?

[Ramana Kumar]

I'm having a lot of trouble getting Holmake to work when I have
dependencies included (via INCLUDES in my Holmakefile). Has something
substantial changed in how I'm supposed to write a Holmakefile? It seems
like Holmake is using the INCLUDES from my current directory even when it
makes recursive calls, which leads to bogus paths.
--
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration  more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=190641631iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Holmake broken?

[Ramana Kumar]

Related to this: are relative paths allowed in the INCLUDES? and in that
case, shouldn't they be relative to the directory containing the
Holmakefile?

On Wed, Feb 18, 2015 at 11:21 AM, Ramana Kumar ramana.ku...@cl.cam.ac.uk
wrote:

 I'm having a lot of trouble getting Holmake to work when I have
 dependencies included (via INCLUDES in my Holmakefile). Has something
 substantial changed in how I'm supposed to write a Holmakefile? It seems
 like Holmake is using the INCLUDES from my current directory even when it
 makes recursive calls, which leads to bogus paths.

--
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration  more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=190641631iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Holmake broken?

[Ramana Kumar]

Here is how to create a small test case that breaks:

dir:
my1Script.sml

dir/bar
Holmakefile - INCLUDES = foo
my3Script.sml depends on my2Theory

dir/bar/foo:
Holmakefile - INCLUDES = ../..
my2Script.sml depends on my1Theory

Holmake in dir/bar

N.B. if you manually call Holmake in dir, then dir/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 
michael.norr...@nicta.com.au wrote:

 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 working with the repository version), it is clearly broken in some
 cases.

 Michael


  On 19 Feb 2015, at 4:03 am, Ramana Kumar ramana.ku...@cl.cam.ac.uk
 wrote:
 
  Related to this: are relative paths allowed in the INCLUDES? and in that
 case, shouldn't they be relative to the directory containing the
 Holmakefile?
 
  On Wed, Feb 18, 2015 at 11:21 AM, Ramana Kumar 
 ramana.ku...@cl.cam.ac.uk wrote:
  I'm having a lot of trouble getting Holmake to work when I have
 dependencies included (via INCLUDES in my Holmakefile). Has something
 substantial changed in how I'm supposed to write a Holmakefile? It seems
 like Holmake is using the INCLUDES from my current directory even when it
 makes recursive calls, which leads to bogus paths.
 
 
 --
  Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
  from Actuate! Instantly Supercharge Your Business Reports and Dashboards
  with Interactivity, Sharing, Native Excel Exports, App Integration  more
  Get technology previously reserved for billion-dollar corporations, FREE
 
 http://pubads.g.doubleclick.net/gampad/clk?id=190641631iu=/4140/ostg.clktrk___
  hol-info mailing list
  hol-info@lists.sourceforge.net
  https://lists.sourceforge.net/lists/listinfo/hol-info


 

 The information in this e-mail may be confidential and subject to legal
 professional privilege and/or copyright. National ICT Australia Limited
 accepts no liability for any damage caused by this email or its attachments.

--
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration  more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=190641631iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info