[Hol-info] request for literature pointers

[Konrad Slind]

I made the following claim in a document:

  "user errors in formally modelling artifacts and expressing properties are
   far more common than errors in the design and implementation
   of formal methods tools"

To me this seems uncontroversial, but it would be nice to be able to point
to a paper that backs this up. Off the top of my head, I can't think of any.
Can anybody help?

Thanks,
Konrad.
--
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] Bindings for embedded languages in HOL

[Konrad Slind]

 See (in the HOL4 distribution)

   examples/lambda/*  for quite a lot of lambda calculus based on a
nominal-sets approach  and
   examples/fsub  for the POPLmark challenge

Both by Michael Norrish.

Konrad.


On Sun, Mar 22, 2015 at 3:04 PM, John Harrison  wrote:

>
> Petros writes:
>
> | 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?
>
> Sean McLaughlin made some sort of start on a nominal package for HOL
> Light, but I don't think it was ever completed. I have some of the
> existing code, which I hope Sean would not mind my sharing. I've
> copied him on this message in case he has anything to add.
>
> John.
>
>
> --
> 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] HOL4 build, deps etc.

[Konrad Slind]

Quick and superficial answer:

  A tool called Holdep computes
the dependencies by a quick syntacctic analysis of the ML files in
the current directory. It then the dependencies in a sub-directory called
.HOLMK.

 Section 6.3 in the Description part of the Manual gives a detailed
description of what Holmake does.

regards,
Konrad.


On Wed, Jul 15, 2015 at 8:25 AM, Makarius  wrote:

> Dear HOL4 experts,
>
> I am trying to understand HOL4 build management.  After some initial
> struggles, I have managed to make a regular build of everything via
> bin/build.  Now I want to see which sources are used in which canonical
> order.
>
> The file tools/build-sequence appears to specify that abstractly, but I
> want to get the resulting sequences of ML files.  I've looked around
> tools/build.sml and tools/buildutils.sml a bit, and it ultimately seems to
> converge towards Holmake invocations.
>
> The latter is unclear to me.  Which are typical targets, e.g. for the
> kernel or core theories?  Maybe there is even some Holmake command line
> option to ask for used file dependencies of such targets?
>
>
> Makarius
>
>
> --
> 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
>
--
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

Re: [Hol-info] where is the higher order logic in HOL?

[Konrad Slind]

As Michael said, higher order is all over the place, even
if first order reasoning is commonplace. One of my favourite
higher order statements is the following encapsulation of
Skolemization:

 SKOLEM_THM;
val it =
   |- ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x):
   thm

Konrad.


On Wed, Nov 18, 2015 at 8:23 PM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:

> Some of the definitions are higher-order.  For example, the universal
> quantifier has to be higher order because it's a function that takes a
> predicate as an argument.
>
> Even functions like MAP are higher-order because they take functions as
> arguments.  Often metis is capable of proving useful facts about MAP
> because 1) there's a well-known translation that turns higher-order
> problems into first-order ones (which metis uses if it has to), or 2) the
> goal mentioning MAP is fundamentally first-order anyway. For example, the
> theorem
>
>|- MAP f (l1 ++ l2) = MAP f l1 ++ MAP f l2
>
> is first order, and this may be the only property needed to prove the goal.
>
> Michael
>
> > On 19 Nov 2015, at 12:14, shengyu shen  wrote:
> >
> > Dear all:
> >
> > HOL is a higher order logic theorem prover, while most of the time, we
> use first order lib such as season and metis,
> >
> > So where is the higher order?
> >
> > Shen
> >
> --
> > ___
> > 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.
>
>
> --
> ___
> 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] NFM 2016 - Call for Papers

[Konrad Slind]

The 8th NASA Formal Methods Symposium
-

http://crisys.cs.umn.edu/nfm2016

June 07 - June 09 2016

McNamara Alumni Center
University of Minnesota
200 Oak Street S.E., Minneapolis, MN 55455

Theme of the Symposium
--


The widespread use and increasing complexity of mission-critical and
safety-critical systems at NASA and the aerospace industry requires
advanced techniques that address their specification, design,
verification, validation, and certification requirements. The NASA
Formal Methods Symposium is a forum to foster collaboration between
theoreticians and practitioners from NASA, academia, and the industry,
with the goal of identifying challenges and providing solutions
towards achieving assurance for such critical systems.

New developments and emerging applications like autonomous on-board
software for Unmanned Aerial Systems (UAS), UAS Traffic Management
(UTM), advanced separation assurance algorithms for aircraft, and the
need for system-wide fault detection, diagnosis, and prognostics
provide new challenges for system specification, development, and
verification approaches. Similar challenges need to be addressed
during development and deployment of on-board software for spacecraft
ranging from small and inexpensive CubeSat systems to manned
spacecraft like Orion, as well as for ground systems.

The focus of the symposium will be on formal techniques and other
approaches for software assurance, their theory, current capabilities
and limitations, as well as their potential application to aerospace,
robotics, and other NASA-relevant safety-critical systems during all
stages of the software life-cycle.

Topics of interest include but are not limited to
-

* Model checking
* Theorem proving
* SAT and SMT solving
* Symbolic execution
* Static analysis
* Model-based development
* Runtime verification
* Software and system testing
* Safety assurance
* Fault tolerance
* Compositional verification
* Security and intrusion detection
* Design for verification and correct-by-design techniques
* Techniques for scaling formal methods
* Applications of formal methods in the development of:
* autonomous systems
* safety-critical artificial intelligence systems
* cyber-physical, embedded, and hybrid systems
* fault-detection, diagnostics, and prognostics systems
* Use of formal methods in:
* assurance cases
* human-machine interaction analysis
* requirements generation, specification, and validation
* automated testing and verification

Important Dates
---

- Paper Submission:2/19/2016
- Paper Notifications: 4/8/2016
- Camera-ready Papers: 4/27/2016
- Symposium:   6/7 - 6/9/2016

Location


The symposium will take place at McNamara Alumni Center, University of
Minnesota.

Registration is required but is free of charge.

Submission Details
--

There are two categories of submissions:

1. Regular papers describing fully developed work and complete
   results (maximum 15 pages)

2. Short papers on tools, experience reports, or work in progress
   with preliminary results (maximum 6 pages)

All papers must be in English and describe original work that has not
been published or submitted elsewhere. All submissions will be fully
reviewed by at least three members of the Program Committee.

Papers will appear in a volume of Springer's Lecture Notes in Computer
Science (LNCS), and must use LNCS style formatting. Papers must be
submitted in PDF format at the EasyChair submission site:

https://easychair.org/conferences/?conf=nfm2016

Authors of selected best papers may be invited to submit an extended
version to a special issue of the Journal of Automated Reasoning
(Springer).

Organizing Committee


- Michael Lowry, NASA Ames Research Center, USA (NASA Liaison)
- Johann Schumann, SGT, Inc./NASA Ames Research Center, USA (General Chair)
- Oksana Tkachuk, SGT, Inc./NASA Ames Research Center, USA (PC Chair)
- Sanjai Rayadurgam, University of Minnesota, USA (PC Chair)
- Mike Whalen, University of Minnesota, USA (Financial Chair)
- Mats Heimdahl, University of Minnesota, USA (Local Arrangements Chair)

Program Committee
-

- Julia Badger, NASA Johnson Space Center, USA
- Clark Barrett, New York University, USA
- Saddek Bensalem, Verimag and  University Joseph Fourier, France
- Dirk Beyer, University of Passau, Germany
- Borzoo Bonakdarpour, McMaster University, Canada
- Alessandro Cimatti, FBK, Italy
- Darren Cofer, Rockwell Collins, Inc., USA
- Myra Cohen, University of Nebraska-Lincoln, USA
- Misty Davies, NASA Ames Research Center, USA
- Leonardo de Moura, Microsoft, USA
- Ben Di Vito, NASA Langley Research Center, USA
- Alexandre Duret-Lutz, LRDE / EPITA, France
- Andrew Gacek, Rockwell Collins, Inc., USA
- Pierre-Loic Garoche, ONERA, France
- Shalini Ghosh, SRI International, USA
- Susanne Graf, Univer

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

[Konrad Slind]

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 
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&iu=/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&iu=/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

[Konrad Slind]

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 
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  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  >
> > 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&iu=/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&iu=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL breakthrough in American politics

[Konrad Slind]

   “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&iu=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to show the function body in ML?

[Konrad Slind]

I think that function is DB.find (PolyML and therefore HOL4 has separate
namespaces due to the module system).

 You can ask the help system about it:

   help "find";

which will bring up a menu listing all structures known to the help system
that have a "find" function in their signature. As follows:

h> elp "find";

--
|   1 | val  PIntMap.find|
|   2 | val  LVTermNet.find  |
|   3 | val  Redblackmap.find|
|   4 | val  KernelSig.find  |
|   5 | val  Redblackset.find|
|   6 | val  Intset.find |
|   7 | val  TypeNet.find|
|   8 | val  DB.find |
|   9 | val  mlibPatricia.find   |
|  10 | HOL DB.find (help/Docfiles/DB.find.adoc) |
|  11 | val  mlibSolver.find |
--

Choose number to browse, or quit: 10

+ --
+ find  (DB)
+ --
+ find : string -> data list
+
+ SYNOPSIS
+ Search for theory element by name fragment.
+



On Tue, Jun 21, 2016 at 4:29 AM, Thomas Tuerk 
wrote:

> Hi Ada,
>
> you can't print the definition from the ML REPL. I expect you use
> PolyML. In this case look into the file "POLYML_DIR/basis/List.sml".
> There you will find the following definition.
>
> fun find _ [] = NONE
> | find f (a::b) = if f a then SOME a else find f b
>
> Best
>
> Thomas
>
> On 21.06.2016 11:18, Ada wrote:
> > Hi,guys
> > I am working with HOL4.
> > I finded a function "find" in ML Structure list,and I wanted to see
> > the function body of "find". I printed :
> >- find;
> >> > val it = fn : string -> ((string * string) * (thm * class)) list
> >The result only shows the types of the function.
> >Its description in ML library is:
> >[*find* p xs] applies f to each element x of xs, from left to  right
> > until p(x) evaluates to true; returns SOME x if such an x  exists
> > otherwise NONE.
> > But,the function body or the definition of function doesn't exist.
> > Does anyone know how to show the function body ?
> > Thanks!
> >
> >
> >
> --
> > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T 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&T Tech Expo July 15-16. Meet us at AT&T 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&T Tech Expo July 15-16. Meet us at AT&T 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] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Konrad Slind]

I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has
caused me a lot of pain. I can see the argument for the renaming, but
it has broken a lot of proofs.

Konrad.


On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk 
wrote:

> Hi Chun,
>
> PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit
> fa81d70b67a61d6eddc6a517f968594c21be384d
>
> https://github.com/HOL-Theorem-Prover/HOL/commit/
> fa81d70b67a61d6eddc6a517f968594c21be384d
>
> for details and explanation. The reason was to unify naming. The X
> actually indicates that the assumption is removed, while the version
> without X keeps it. So in order to get your old proof working, you just
> need to replace "PAT_ASSUM" with "PAT_X_ASSUM".
>
> Best
>
> Thomas Tuerk
> On 16.01.2017 19:47, Chun Tian (binghe) wrote:
> > Hi,
> >
> > HOL Reference said that, PAT_ASSUM "Finds the first assumption that
> matches the term argument, applies the theorem tactic to it, and removes
> this assumption.” But I found it actually doesn’t remove the assumption in
> latest Kananaskis 11.
> >
> > To see this, try the following goal (open listTheory first):
> >
> >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> > val it =
> >Proof manager status: 1 proof.
> > 1. Incomplete goalstack:
> >  Initial goal:
> >  ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> > :
> >proofs
> >
> > First I rewrite it:
> >
> >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> > OK..
> > 1 subgoal:
> > val it =
> > FILTER ($= x) l = [x]
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> >   1.  MEM x l
> > :
> >proof
> >
> > Then I want to pick the assumption 0 and specialize the quantifier with
> `x`:
> >
> >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> > <>
> > OK..
> > 1 subgoal:
> > val it =
> > ((x = h) ∨ MEM x l ⇒
> >  ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> > (FILTER ($= x) l = [x])
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> >   1.  MEM x l
> > :
> >proof
> > Now you can see, the assumption 0 is still here. It’s not removed as the
> manual said.
> >
> > In Kananaskis 10, the behavior is exactly the same as described in the
> manual:
> >
> > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> > <>
> >> val it =
> > Proof manager status: 1 proof.
> > 1. Incomplete goalstack:
> >  Initial goal:
> >  ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> >  : proofs
> >
> > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> > OK..
> > 1 subgoal:
> >> val it =
> > FILTER ($= x) l = [x]
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) =
> [x])
> >   1.  MEM x l
> >  : proof
> >
> > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> > <>
> > OK..
> > 1 subgoal:
> >> val it =
> > ((x = h) ∨ MEM x l ⇒
> >  ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> > (FILTER ($= x) l = [x])
> > 
> >   MEM x l
> >  : proof
> >
> > See, the used assumption has been removed.
> >
> >
> > Now let’s insist that, the behavior in latest Kananaskis 11 is more
> reasonable (thus we should update the manual), because later we may be able
> to use the assumption again for another different purpose. Now to finish
> the proof, in Kananaskis 10 a single rewrite almost finish the job using
> theorem FILTER_NEQ_NIL:
> >
> > - FILTER_NEQ_NIL;
> >> val it =
> > |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x
> >  : thm
> > - e (RW_TAC std_ss [FILTER_NEQ_NIL]);
> > OK..
> > 1 subgoal:
> >> val it =
> > MEM h l
> > 
> >   MEM h l
> >  : proof
> >
> > Now the goal is the same as the only assumption left:
> >
> > - e (FIRST_ASSUM ACCEPT_TAC);
> > OK..
> >
> > Goal proved.
> >  [.] |- MEM h l
> >
> > Goal proved.
> >  [.]
> > |- ((x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> >(FILTER ($= x) l = [x])
> >
> > Goal proved.
> >  [..] |- FILTER ($= x) l = [x]
> >
> > But in Kananaskis 11 the same tactical cannot prove the theorem any more:
> >
> >> FILTER_NEQ_NIL;
> > val it =
> >|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x:
> >thm
> >
> >> e (RW_TAC std_ss [FILTER_NEQ_NIL]);
> > OK..
> > 1 subgoal:
> > val it =
> >
> > FILTER ($= x) l = [x]
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> >   1.  MEM x l
> > :
> >proof
> >
> > In fact we’re going back to previous status before PAT_ASSUM was used!
> In short words, the following theorem definition doesn’t work any more: (it
> wo

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Konrad Slind]

Oh, and the other thing that now bites (I think) is the

  FIRST_ASSUM --> FIRST_X_ASSUM

replacement, which, if not done, can derail proofs.

Konrad.


On Mon, Jan 16, 2017 at 5:47 PM,  wrote:

> There were really two changes. If it was just a rename, then a
> find-and-replace (pat_assum -> pat_x_assum) would solve all the problems.
> However, there was another change to do with the handling of free variables
> in the pattern.  As per the release notes, that change might require the
> use of underscores where previously needlessly specific variable names were
> being used.
>
>
>
> Michael
>
>
>
> *From: *Konrad Slind 
> *Date: *Tuesday, 17 January 2017 at 07:41
> *To: *Thomas Tuerk 
> *Cc: *HOL-info mailing list 
> *Subject: *Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now?
> (and a theorem cannot be proved in K11 any more)
>
>
>
> I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has
>
> caused me a lot of pain. I can see the argument for the renaming, but
>
> it has broken a lot of proofs.
>
>
>
> Konrad.
>
>
>
>
>
> On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk 
> wrote:
>
> Hi Chun,
>
> PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit
> fa81d70b67a61d6eddc6a517f968594c21be384d
>
> https://github.com/HOL-Theorem-Prover/HOL/commit/
> fa81d70b67a61d6eddc6a517f968594c21be384d
>
> for details and explanation. The reason was to unify naming. The X
> actually indicates that the assumption is removed, while the version
> without X keeps it. So in order to get your old proof working, you just
> need to replace "PAT_ASSUM" with "PAT_X_ASSUM".
>
> Best
>
> Thomas Tuerk
>
> On 16.01.2017 19:47, Chun Tian (binghe) wrote:
> > Hi,
> >
> > HOL Reference said that, PAT_ASSUM "Finds the first assumption that
> matches the term argument, applies the theorem tactic to it, and removes
> this assumption.” But I found it actually doesn’t remove the assumption in
> latest Kananaskis 11.
> >
> > To see this, try the following goal (open listTheory first):
> >
> >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> > val it =
> >Proof manager status: 1 proof.
> > 1. Incomplete goalstack:
> >  Initial goal:
> >  ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> > :
> >proofs
> >
> > First I rewrite it:
> >
> >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> > OK..
> > 1 subgoal:
> > val it =
> > FILTER ($= x) l = [x]
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> >   1.  MEM x l
> > :
> >proof
> >
> > Then I want to pick the assumption 0 and specialize the quantifier with
> `x`:
> >
> >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> > <>
> > OK..
> > 1 subgoal:
> > val it =
> > ((x = h) ∨ MEM x l ⇒
> >  ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> > (FILTER ($= x) l = [x])
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
> >   1.  MEM x l
> > :
> >proof
> > Now you can see, the assumption 0 is still here. It’s not removed as the
> manual said.
> >
> > In Kananaskis 10, the behavior is exactly the same as described in the
> manual:
> >
> > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> > <>
> >> val it =
> > Proof manager status: 1 proof.
> > 1. Incomplete goalstack:
> >  Initial goal:
> >  ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> >  : proofs
> >
> > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> > OK..
> > 1 subgoal:
> >> val it =
> > FILTER ($= x) l = [x]
> > 
> >   0.  ∀x.
> > (x = h) ∨ MEM x l ⇒
> > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) =
> [x])
> >   1.  MEM x l
> >  : proof
> >
> > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> > <>
> > OK..
> > 1 subgoal:
> >> val it =
> > ((x = h) ∨ MEM x l ⇒
> >  ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> > (FILTER ($= x) l = [x])
> > 
> >   MEM x l
> >  : proof
> >
> > See, t

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

[Konrad Slind]

To print theory "foo" as html :

   DB.html_theory "foo";

Konrad.


On Fri, Apr 7, 2017 at 6:50 AM, Chun Tian (binghe) 
wrote:

> yes, I know these signature files, I use them too (when the proofs do not
> interest me), but I found that, in signatures, all theorems and definitions
> are sorted in lexicographic order, which is sometimes very different from
> the source scripts. But the source scripts well preserved the relationships
> (and dependences) between theorems, i.e. later theorems were proved by
> previous theorems, they're kind of very useful information to me.
>
> By the way, is it possible to generate HTML files from any theory
> signature?   I know how to use EmitTeX.print_theories_as_tex_doc() to
> print my theory into PDF finally. But I find HOL's HTML outputs beautiful
> and compat, I would like have the same for my own theories ... (sorry for
> bring this last question to you, today ^_^)
>
> Regards,
>
> Chun
>
> On 7 April 2017 at 13:17, Thomas Tuerk  wrote:
>
>> Hi Chun,
>>
>> learning Holyhammer is also on my TODO list.
>>
>> One minor trick. I often look at the theory signature instead of the
>> Script-file. So I read "relationTheory.sig". For the theories comming with
>> HOL, the signature is available in the HTML help. For my own theories, I
>> just open the "*Theory.sig" file.
>>
>> https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/
>> src-sml/htmlsigs/relationTheory.html#LinearOrder-val
>>
>> Best
>>
>> Thomas
>>
>> On 07.04.2017 13:07, Chun Tian (binghe) wrote:
>>
>> Thanks again, this is really convenient.
>>
>> Actually a large piece of my time was spent on reading HOL's
>> relationScript.sml and other scripts that I needed, I try to find useful
>> theorems by their name (otherwise I couldn't know RTC_CASES*, RTC_INDUCT,
>> RTC_SINGLE, etc.), but maybe the scripts are too long, I don't know how to
>> I missed RTC_INDUCT_RIGHT1, etc.)
>>
>> I hope one day I could learn to use the Holyhammer ...
>>
>> Regards,
>>
>> Chun
>>
>>
>> On 7 April 2017 at 12:57, Thomas Tuerk  wrote:
>>
>>> Hi Chun,
>>>
>>> by the way. I always find DB.match and DB.find very helpful. You can for
>>> example try
>>>
>>> DB.print_match [] ``RTC``
>>> DB.print_match [] ``RTC _ x x``
>>> DB.print_find "RTC"
>>> to find interesting theorems about RTC.
>>>
>>> Cheers
>>>
>>> Thomas
>>>
>>>
>>> On 07.04.2017 12:51, Chun Tian (binghe) wrote:
>>>
>>> Hi Thomas,
>>>
>>> Thank you very much!! Obviously I didn't know those RTC_ALT* and
>>> RTC_RIGHT* series of theorems before. Now I can prove something new:)
>>>
>>> Best regards,
>>>
>>> Chun
>>>
>>>
>>> On 7 April 2017 at 12:08, Thomas Tuerk  wrote:
>>>
 Hi,

 1) They are the same. You can easily proof with induction (see below).

 2) Yes you can prove it. You would also do it via some kind of
 induction proof. However there is no need, since it is already present in
 the relationTheory as  RTC_INDUCT_RIGHT1.

 Cheers

 Thomas



 open relationTheory

 val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
 (!x. RTC1 R x x) /\
 (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;

 val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
 (!x. RTC2 R x x) /\
 (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;

 val RTC1_ALT_DEF = prove (``RTC1 = RTC``,

   `!R. (!x y. RTC1 R x y ==> RTC R x y) /\
(!x y. RTC R x y ==> RTC1 R x y)` suffices_by (
  SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
   THEN

   GEN_TAC THEN CONJ_TAC THENL [
 Induct_on `RTC1` THEN
 METIS_TAC [RTC_RULES],

 MATCH_MP_TAC RTC_INDUCT THEN
 METIS_TAC[RTC1_rules]
   ]);


 val RTC2_ALT_DEF = prove (``RTC2 = RTC``,

   `!R. (!x y. RTC2 R x y ==> RTC R x y) /\
(!x y. RTC R x y ==> RTC2 R x y)` suffices_by (
  SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
   THEN

   GEN_TAC THEN CONJ_TAC THENL [
 Induct_on `RTC2` THEN
 METIS_TAC [RTC_RULES_RIGHT1],

 MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
 METIS_TAC[RTC2_rules]
   ]);



 On 07.04.2017 11:49, Chun Tian (binghe) wrote:

 Hi,

 If I try to define RTC manually (like those in HOL tutorial, chapter 6,
 page 74):

 val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
 (!x. RTC1 R x x) /\
 (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;

 It seems that (maybe) I can also define the "same" relation with a
 different transitive rule:

 val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
 (!x. RTC2 R x x) /\
 (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;

 Here are some observations:

 1. If I directly use the RTC definition from HOL's relationTheory,
 above two transitive rules are both true, easily provable by theorems
 RTC_CASES1 and RTC_CASES2 (re

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

[Konrad Slind]

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 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] Counting Subgoals in a Proof

[Konrad Slind]

To follow up on Thomas' post, you can easily write a tactical that will do
such counting. In
the following I print out the number, but you could also store it in a
reference cell, as Thomas
does.

  fun COUNT_TAC tac g =
   let val res as (sg,_) = tac g
   val _ = print ("subgoals"^Int.toString (List.length sg)^"\n")
   in res
   end

The nice thing about this is that you can wrap any tactic with it and get a
count out, which
should help for your application.

Example (here the compound tactic generates 4 subgoals, three of which get
solved by
the trailing "simp_tac list_ss []" tactic):

 g `!l1 l2. REVERSE(l1 ++ l2) = REVERSE l2 ++ REVERSE l1`;

> e (COUNT_TAC (Induct >> (Induct ORELSE (gen_tac >> Induct))) >> simp_tac
list_ss []);
OK..
subgoals: 4
1 subgoal:
val it =


∀h'. REVERSE (l1 ++ h'::l2) = REVERSE l2 ++ [h'] ++ REVERSE l1

  0.  ∀l2. REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1
  1.  REVERSE (h::l1 ++ l2) = REVERSE l2 ++ REVERSE (h::l1)
:
   proof

Konrad.


On Tue, Jul 11, 2017 at 6:36 AM, Thomas Tuerk 
wrote:

> Hi Matthias,
>
> I'm not aware of an easy way. Moreover, for me it is unclear how to
> count subgoals. I could well imagine that one wants to count only
> "interesting ones", i.e. ignore trivial ones like "Cases_on `x:num` >>
> ASM_REWRITE_TAC[...]", where the case for "0" is automatically discarded.
>
> One idea would be to define a tactic for counting, i.e. something like
>
>
> val subgoal_counter = ref 0;
> fun COUNT_TAC (asm, g) = (subgoal_counter := !subgoal_counter + 1;
> ALL_TAC (asm, g))
>
>
> You can then add it at the places, where you want counting to happen,
> e.g. after a "REPEAT CASE_TAC". Add some stuff for resetting the counter
> and printing it, e.g. by a tactical like
>
>
> fun PRINT_COUNT tac (asm, g) = let
>   val _ = subgoal_counter := 0;
>   val res = tac (asm, g);
>   val _ = print ("\n\nCOUNTER: "^(int_to_string
> (!subgoal_counter))^"\n\n");
> in res end;
>
> And you have some basic infrastructure. Very hackish, but probably
> working, flexible and not too much work.
>
> Cheers
>
> Thomas
>
>
>
> On 11.07.2017 12:34, Matthias Stockmayer wrote:
> > Hi,
> >
> > I'm working on a proof that produces many subgoals due to a rather
> > complex case-splitting structure. To see, if some changes to the proof
> > increase or decrease the complexity, I'd like to know how many
> > subgoals are produced and solved in the whole proof.
> >
> > So, is there any way to find out the number of subgoals, without
> > manually stepping through the proof and counting?
> >
> > I know I can use the running time of the proof to compare different
> > approaches, but I'm not sure how accurate this will be.
> >
> >
> > With regards,
> >
> > Matthias
> >
> >
> >
> > 
> --
> >
> > 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] How to write a general EQ_CONV ?

[Konrad Slind]

EVAL_CONV should do it. It is a general-purpose evaluator that works by
deduction. It may even be that string_EQ_CONV is implemented in terms
of it. The documentation about computeLib in
the Description should tell you more.

Konrad.


On Sat, Jul 22, 2017 at 4:23 PM, Chun Tian (binghe) 
wrote:

> Hi,
>
> If I have two terms s1 and s2 of type ``:string``, then
>
> string_EQ_CONV ``^s1 = ^s2``
>
> returns a theorem like:  |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F``
> about the equality the two terms.  But if I don’t know the types of s1 and
> s2, how can I achieve the same goal by finding a function like
> string_EQ_CONV and call it?
>
> 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

[Hol-info] Fwd: [mike-gordon-update] sad news

[Konrad Slind]

Sad news for hol-info readers, and many others. Mike was a profound
influence, a professional and personal inspiration. He is gone too soon.

Konrad.

-- Forwarded message --
From: Katriel Cohn-Gordon 
Date: Tue, Aug 22, 2017 at 12:58 PM
Subject: [mike-gordon-update] sad news
To: mike-gordon-upda...@googlegroups.com


Dear all,

I'm sorry to report that Mike Gordon died peacefully this evening after a
short illness. He is survived by his wife of 38 years Avra Cohn and by his
sons Katriel and Reuben. He'll be greatly missed by his family and friends,
but equally by the academic community of which he was such a long-standing
pillar. There will be a memorial service in Cambridge in due course to
celebrate his life.

Please do forward this message to any mailing lists or people that you
think would like to know.

Best,
Avra, Reuben and Katriel

-- 
You received this message because you are subscribed to the Google Groups
"Updates about Mike Gordon" group.
To unsubscribe from this group and stop receiving emails from it, send an
email to mike-gordon-updates+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--
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?

[Konrad Slind]

Hi Chun Tian,

  The constant ALL_DISTINCT in listTheory is what you are looking for, I
think.

Konrad.


On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) 
wrote:

> 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] The use of optionTheory for representing invisible actions in transition systems

[Konrad Slind]

Hi Chun Tian,

 For your Label type the most appropriate primitive type would be
sums (co-products). These are formalized in sumTheory, so you
could look at that if  you are interested. However, I think you might
lose some clarity in your formalization by using them.

Cheers,
Konrad.


On Mon, Oct 9, 2017 at 8:07 AM, Chun Tian (binghe) 
wrote:

> Hi again,
>
> For example, if I use pairTheory to represent my Label type, something
> like:
>
> val _ = type_abbrev ("Label", ``'b # bool``);
> val _ = overload_on ("name", ``\s. (s, T)``);
> val _ = overload_on ("coname", ``\s. (s, F)``);
>
> then retrieving the underlying names is simply the FST of the pair, and
> relabeling operation is inverting the SND of pairs.  Is this idea
> recommended? (although I see no benefits other than shorter generated
> theory files)
>
> Regards,
>
> Chun Tian
>
>
>
> On 9 October 2017 at 13:58, Chun Tian (binghe) 
> wrote:
>
>> Hi,
>>
>> I was having the following two Datatype definitions for representing
>> "labels" and "actions" in transition systems like CCS/LTS:
>>
>> val _ = Datatype `Label = name 'b | coname 'b`;
>> val _ = Datatype `Action = tau | label ('b Label)`;
>>
>> But yesterday, after my thesis work has been committed into HOL's example
>> directory, I suddenly realized: isn't the "Action" type a perfect case to
>> use HOL's optionTheory? that is, using NONE as tau (invisible action), and
>> SOME for all others:
>>
>> val _ = type_abbrev ("Action", ``:'b Label option``);
>> val _ = overload_on ("tau", ``NONE :'b Action``); (* NONE is invisible
>> (tau) *)
>> val _ = overload_on ("label", ``\(l :'b Label). SOME l``);
>>
>> optionTheory provided already the induction, nchotomy, one_one, ...
>> theorems, so all I need to do is to use INST_TYPE to convert them into
>> theorems for my fake "Action" type, e. g.
>>
>> (* Define structural induction on actions
>>|- ∀P. P tau ∧ (∀L. P (label L)) ⇒ ∀A. P A
>>  *)
>> val Action_induction = save_thm (
>>"Action_induction", INST_TYPE [``:'a`` |-> ``:'b Label``]
>> option_induction);
>>
>> So I've made the changes, and it works amazingly well.  Isn't this too
>> perfect?
>>
>> P. S. Is there any existing "simple" type in HOL such that I can prevent
>> using Datatype for defining the "Label" type?
>>
>> Regards,
>>
>> Chun Tian
>> University of Bologna (Italy)
>>
>>
>
>
> --
> 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] Spurious parent theories

[Konrad Slind]

When /bin/hol starts up, it is sitting on top of a somewhat
ad hoc collection of theories:

  > ancestry"-";
  val it =
   ["ConseqConv", "quantHeuristics", "patternMatches", "ind_type", "while",
"one", "sum", "option", "pair", "combin", "sat", "normalForms",
"relation", "min", "bool", "marker", "num", "prim_rec", "arithmetic",
"numeral", "basicSize", "numpair", "pred_set", "list", "rich_list",
"indexedLists"]: string list

Some of these are support for other proof infrastructure, but the main
theories give you booleans, products, sums, options, numbers, lists,
and sets. This is a useful basis on which to begin most formalizations.

But if you want to have a minimal ancestry for your theory, you could try
building on /bin/hol.bare which  has very little:

> ancestry"-";
val it = ["min", "bool"]: string list

Then you will have to explicitly load in all the needed tools and theories.
For use of Holmake, I am pretty sure there is an option to support
hol.bare,
but I am not sure what it is.

Konrad.



On Sun, Oct 22, 2017 at 10:01 AM, Mario Castelán Castro <
marioxcc...@yandex.com> wrote:

> Hello.
>
> When I process the following file with Holmake from a recent Git build I
> get indexedLists and patternMatches as parents; with Kananaskis-11 I get
> quantHeuristics and rich_list as parents. Why? There is no apparent
> dependency on anything but the bool theory.
>
> “open HolKernel Parse boolLib boolTheory;
> val _ = new_theory "test";
> save_thm("T", TRUTH);
> val _ = export_theory ();”
>
> --
> 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] On the order of "variable" substitutions in lists or recursive structures

[Konrad Slind]

Hi Chun Tian,

  There are all kinds of issues with substitutions and applying them to
term-like
structures. I would probably start by choosing finite maps
(finite_mapTheory) as
the representation for variable substitutions since they get rid of most if
not all
the issues with ordering of replacements. The alistTheory provides a more
computationally friendly version, and provides a formal connection back to
fmaps.

 Also see

/examples/unification/triangular/first-order

for a unification case study.

Konrad.


On Mon, Oct 23, 2017 at 10:48 AM, Chun Tian  wrote:

> Hi,
>
> Suppose I have a list (or recursive structure defined by Datatype) in
> which there’re some special elements marked as “variables”, e.g. ``var X``,
> ``var Y``, …  and I have a substitution function which correctly replaces a
> variable into another closed term (i.e. term without variables), and an
> extended version of this function can do repeated variable substitutions on
> a list of variables and their corresponding substitutions.  E.g. ``SUBST E
> Ps Xs`` will do substitutions in list of strings E, finding each appearance
> of variable in Xs and replace with the corresponding one in Ps. The type of
> SUBST should be something like ``:string list -> string list -> string list
> -> string list``.
>
> I can imagine that, for whatever permutations of Xs (or the order of
> variables), with Ps also changed in the same order,  the resulting term
> ``SUBST Es Ps Xs`` must be unique. (if Ps also contains variables, the
> resulting term may not be unique any more.)
>
> How can expression this property (e.g. in listTheory)? What’s the name of
> this phenomena? and what’s the idea in its proof?
>
> Regards,
>
> Chun Tian
>
>
> 
> --
> 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] The origin of the HOL4 logo

[Konrad Slind]

Maybe you are thinking of the snow-watching latern?

https://www.cl.cam.ac.uk/archive/mjcg/lantern.html

Konrad.


On Thu, Dec 14, 2017 at 11:23 AM, Mario Castelán Castro <
marioxcc...@yandex.com> wrote:

> Hello.
>
> I recall having read that the HOL4 logo (as found in TUTORIAL, MANUAL,
> DESCRIPTION, LOGIC) is based on a photo of a lamp found in Canada.
> Despite searching my browser history and using a search engine I failed
> to find the message again.
>
> To somebody who knows what photo I am referring to or otherwise knows
> the origin of the HOL4 logo, could you please link me to further
> information about the origin of the logo, including the photo that it is
> based from?
>
> This is just for curiosity.
>
> 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] INST

[Konrad Slind]

Hi Michael,

  What I think is happening is that each quoted element is being
parsed separately.
This means that the type of the x in `x` is a type variable while the type
of `2` is :num. Since INST (I think) just fails if the two types
aren't identical,
you get the displayed behaviour. There may well be a version of INST in
Hol Light that normalizes the arguments but I don't know it.

Konrad.


On Thu, Jan 4, 2018 at 8:04 PM, Michael Beeson  wrote:
> an example from the tutorial
>
> let th1 = REFL `x+1`;;
>
> val th1 : thm = |- x + 1 = x + 1
>
> # let th3 = INST [`2`,`x:num`] th1;;
>
> val th3 : thm = |- 2 + 1 = 2 + 1
>
> Fine.  But if we leave off the type information about x it doesn't work.
>
> # let th3 = INST [`2`,`x`] th1;;
>
> Warning: inventing type variables
>
> Exception: Failure "vsubst: Bad substitution list".
>
> I don't understand why this fails.   In general you might not
> know what type x has in th1  (eg.,  has prioritize_real() or
> prioritize_vector()  been done just before this?) .Is there
> a command I can issue to ask for "the type of `x` in th1 " ?
>
> Michael Beeson
>
> --
> 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] Share list of terms with later theories

[Konrad Slind]

Theorems that need to persist between sessions are most easily stored by name
in theories. Maybe some kind of PolyML database magic could also be
used, I don't
know. As far as DB searches, it wouldn't be hard to implement a
refined DB search
mechanism that first discarded all theorems that met some kind of
naming convention
(e.g., those starting with an underscore or something like that) and
then did the usual
search (which can be on name fragment or pattern).

Konrad.


On Wed, Jan 10, 2018 at 7:09 PM, Magnus Myreen  wrote:
> Ah, I didn't realise this existed. Thanks for the pointers!
>
> How does storing of theorems work in this setting? One can't construct
> a theorem from a string in a decode function.
>
> I guess the string could refer to a theorem name that's stored in the
> theory, but this is a bit inconvenient because some of the theorems in
> the translator's state are currently not stored in the theory (other
> than in the automatically produced theorem that is an encoding of the
> entire state). I guess an encode function could invent an unused name
> and store the theorem while it's producing the encoding. This can lead
> to some strange things turning up in DB searches (as is the case with
> the current approach).
>
> Cheers,
> Magnus
>
>
> On 11 January 2018 at 11:24,   wrote:
>> That level of generality is already possible, and has always been a 
>> desideratum for the design.  (The grammar update information stored is about 
>> that complicated for example; consider the types that occur in a call to 
>> add_rule.)
>>
>> The painful part is that you have to write functions to encode and decode 
>> the types into and out of strings (because these strings are written into 
>> the theory files).  There are functions for doing basic SML types in 
>> src/parse/Coding, and the handling of terms is handled by writing functions 
>> that take functions for doing this as parameters.  See the bottom of 
>> src/parse/term_grammar for the encoding and decoding, and 
>> src/parse/GrammarDeltas for the way this is put together for the grammar 
>> example.
>>
>> You can see the fundamental building blocks at the LoadableThyData structure 
>> in src/postkernel/Theory.
>>
>> Certainly, providing a method for going through a generic s-expression type 
>> might be easiest for users to understand, so perhaps I can build that as 
>> well as term lists.
>>
>> Michael
>>
>> On 11/1/18, 11:08, "Magnus Myreen"  wrote:
>>
>> Hi Michael,
>>
>> I see that you are considering to add a TermSetData feature. Could you
>> please add something more general? I'd appreciate a feature that can
>> store the CakeML translator's state in theories. Currently, the CakeML
>> translator stores its state in a single theorem so that the other
>> theories can load the state and continue from previous states.
>>
>> As far as I can tell, the ThmSetData machinery (and probably the
>> TermSetData equivalent) won't help with the translator. The reason is
>> that the translator's state is a collection of lists of list of tuples
>> of combinations of strings, type, terms and theorems.
>>
>> The current approach encodes all of these structures into a single
>> unreadable theorem. This works but it seems a bit ad hoc and causes
>> huge unreadable theorems to pop up in various DB searches.
>>
>> Suggestion: could we have a way to store a s-expression-like data into
>> theories? If the s-expressions would allow strings, types, terms,
>> theorems and, of course, pairs/lists of s-expressions, then I think
>> the translator's state could very naturally be stored in theories.
>>
>> Cheers,
>> Magnus
>>
>> > There is generic machinery for adding values of various forms to 
>> theories so
>> > that future theories and ML code can see them.  The smoothest 
>> instantiation
>> > is in ThmSetData (in src/1) which allows storage of sets of theorems 
>> in a
>> > “2D matrix” indexed by theory-name and set-name.  For example, the 
>> automatic
>> > rewrites behind the “simp” attribute are implemented this way.
>> >
>> > The storage of grammar updates is handled with the same technology.
>> >
>> > A hacky way to store terms would be to use theorems with conclusions 
>> of the
>> > form
>> >
>> >K T (myterm)
>> >
>> > and to then use ThmSetData.
>> >
>> > A better way, which, now that I’ve been prodded, I may implement soon, 
>> would
>> > be to write a TermSetData.
>> >
>> > I hope this helps. I’m happy to discuss the details of this relatively
>> > undocumented feature further if you want more help.
>> >
>> > Best wishes,
>> > Michael
>> >
>> > On 11/1/18, 01:51, "Heiko Becker"  wrote:
>> >
>> > Hello everyone,
>> >
>> > suppose I have a custom tactic that depends on a list of terms and 
>> I
>> > want to keep adding elements to the list throughout my 

Re: [Hol-info] Gender-neutral pronouns

[Konrad Slind]

Maybe we can stick to higher order logic? This discussion does not
belong on hol-info.

Thanks,
Konrad.


On Tue, Jan 30, 2018 at 8:58 AM, Mario Xerxes Castelán Castro
 wrote:
> Hello Bram. Welcome to the mailing list.
>
> On 30/01/18 05:22, Bram Geron wrote:
>> I have only just subscribed to this list before you sent this message, but I 
>> believe that the use of "he" as a neutral pronoun makes women subconsciously 
>> feel like they are not really welcome in the community.
>
> The claim that “women subconsciously feel like they are not really
> welcome in the community” is not _even_ wrong as some physicists would
> put it. The problem is that it is not falsifiable, because the
> “subconscious” is a vague concept on which anything can be claimed and
> nothing can be proved because the very concept of subconscious implies
> that it has no observable effect.
>
> Anyway, if we delete “subconscious” from your message we are left with a
> less vague claim. My reply would be this: If anybody feels excluded by
> the use of generic (w.r.t. grammatical gender) grammar is because he
> wants to feel excluded. By definition, generic nouns are inclusive of
> both sexes.
>
>> Participation of women in computer science is problematically low across the 
>> globe, and I do think that small things like using "he" to refer to a group 
>> including women hurts this cause. I think you'll find you get used to 
>> they/them/their surprisingly quickly, and in a great number of 
>> (scientific/industry) communities it is now accepted as the gender-neutral 
>> pronoun.
>
> No, it is not “problematically” low. What “problems” does it bring for
> “computer science”? none; it may be against the ultraliberals' politcal
> agenda, but that is not computer science problem. Anyway, it is not just
> computer science but intellectual activities in general.
>
> Anybody can send a patch, publish computer software or a book about
> mathematics. Sex makes no difference. If one sex does so less often than
> the other, it is because of lack of capability and interest.
>
> This way of thinking seems to be a result of the push for “diversity”
> and “social justice”. Through history, men as group have shown higher
> intellectual success than women. The feminists cried that this was
> because of systematic oppression (this itself is an intellectual
> achievements, since men succeeded while women failed to achieve such
> oppression for their benefit). Well, society gave women a chance. Now
> (in nearly all of the world) women have either the same or more (there
> are social programs exclusively for women, but hardly any exclusively
> for men) opportunities w.r.t. knowledge than men, yet they still show
> the same poor performance as a group (I can cite examples if requested).
> They were given an opportunity and failed. Thus the claim that both
> sexes are “equal” with respect to intellectual capability has lost its
> credibility.
>
> This is to much disgust of the ultraliberals, because it undermines
> their agenda that includes making everybody believe that we are all
> “equal” (reality notwithstanding!). It is them who must accept reality,
> not the rest of us who must become oblivious to it.
>
> I refuse to become oblivious to reality and jump into the “we are all
> equal“ bandwagon. I urge you to refuse too.
>
>
> --
> 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] verifying the Gordon computer

[Konrad Slind]

The proofs might still run. I'd be keen to help get them going, if
they can be dug up. After Tamarack, Brian Graham verified a
hardware-level SECD machine while a student of Graham Birtwistle.
Perhaps they have running versions of those proofs.

Konrad

On Sun, Apr 1, 2018 at 4:39 AM, Lawrence Paulson  wrote:
> In 1983, using LCF_LSM, Mike verified his computer with the comment “The 
> entire specification and verification described here took several months, but 
> this includes some extending and debugging of LCF_LSM … it would take me two 
> to four weeks to do another similar exercise now. The complete proof requires 
> several hours CPU time on a 2 megabyte Vax/750.”
>
> Jeff Joyce verified several versions of this computer (which he called 
> Tamarack) using HOL. Do any of these proofs still run? I wonder how long it 
> takes now?
>
> 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] About the experimental kernel

[Konrad Slind]

End users should see no difference, but occasionally a proof script
generated on top of one kernel won't run on the other. That is due to
differences in how renaming is implemented in each kernel.

For some specific cases, one kernel performs better than the other.
The "standard" kernel runs the EVAL conversions faster, while the
experimental kernel deals better with manipulations of terms with
deeply nested binders.

Konrad.


On Wed, Apr 11, 2018 at 10:59 AM, Mario Xerxes Castelán Castro
 wrote:
> Hello.
>
> What are the reasons for choosing either the standard or the
> experimental kernel over the other one?
>
> I understand that at the level of implementation, the standard kernel
> uses de Bruijn indices and has support for explicit lazy beta
> conversions (with an internal explicit substitution calculus) while the
> experimental kernel has no lazy beta conversions and uses the same
> representation for free and bound variables. But what are the
> differences at the end user level?
>
> --
> 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] modelling sequential devices in higher-order logic

[Konrad Slind]

In the way Mike and colleagues modelled hardware, a device is modelled
as a predicate over the external wires (ports) of the device.
Information hiding is achieved by existential quantification
(relational composition). The basics of this are laid out in

  https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf

There is a sequential circuit example in that tech. report, which may help.

Konrad.


On Mon, Apr 23, 2018 at 9:09 AM, Lawrence Paulson  wrote:
> Somebody asked me, how do we represent the state of a sequential device in 
> HOL? And I am not quite sure. Mike himself wrote that it is simply about 
> incorporating time into the model, so that if we have a counter then we can 
> describe it by C(t+1) = C(t)+1, where C is its (visible) output and t 
> represents time.
>
> But what if we have a primitive that doesn't expose its full state to the 
> outside? Imagine a device that contains a counter that increments with every 
> clock tick, but the counter value is hidden and the output is only a single 
> bit to tell us whether the value of the counter is a prime number or not. 
> Surely in such a case the counter itself would have to be visible in the 
> formalisation even if no device was allowed to connect to it?
>
> Larry Paulson
>
>
>
>
> --
> 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] Tactic

[Konrad Slind]

Here's an old-school solution:

fun locate P left [] = NONE
  | locate P left (h::t) =
  if P h then
SOME (rev left, h, t)
  else
  locate P (h::left) t;

fun ASM_CONJ_TAC (asl,c) =
case locate is_conj [] asl
 of NONE => raise ERR "ASM_CONJ_TAC" "no conj in assums"
  | SOME(left,conj,right) =>
let val (t1,t2) = dest_conj conj
val th = SPECL [t1,t2,c] AND_IMP_INTRO
in ([(left @ [t2,t1] @ right, c)],
fn [thm] => UNDISCH(EQ_MP th (DISCH t1 (DISCH t2 thm
end

Test.

g `a ==> b /\ c ==> d /\ e ==> k`;
e (rpt disch_tac);
e (rpt ASM_CONJ_TAC);


On Fri, Jun 29, 2018 at 2:27 AM Heiko Becker  wrote:

> Hello,
>
> On 06/28/2018 11:44 PM, Dylan Melville wrote:
> > Also, the version Im using is HOL - Light
> >
> >> On Jun 28, 2018, at 5:38 PM, Dylan Melville 
> wrote:
> >>
> >> Is there a tactic for splitting conjoined assumptions into separate
> assumptions?
>
> In HOL-Light you can try using CONJ_PAIR[1] for an assumption of the
> form A /\ B and CONJUNCTS[2] for finitely many conjuncts. These can then
> be added back using ASSUME_TAC.
>
> Alternatively you can use CONJUNCTS_THEN[3] in combination with ASSUME_TAC.
>
>
> Hope this helps.
>
> Best regards,
>
>
> Heiko
>
>
> [1]: http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJ_PAIR.html
>
> [2]:
> http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJUNCTS_UPPERCASE.html
>
> [3]:http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJUNCTS_THEN.html
>
>
>
> --
> 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] INST on a theorem

[Konrad Slind]

Hi Dylan,

1. Your "EX" is basically the same as listTheory.EXISTS_DEF (in HOL4). If
you are in HOL Light, I am sure there is an analogous definition already
available. You should use it, since there are lots of theorems proved about
it already and you will save on work.

2. The problem is likely that you need to first type instantiate the
definition before calling INST.

(Following is HOL4).

First get the definition into your form:

val EXISTS_DEF_0 = LIST_CONJ (map SPEC_ALL (CONJUNCTS
listTheory.EXISTS_DEF));
val EXISTS_DEF_0 =
   ⊢ (EXISTS P [] ⇔ F) ∧ (EXISTS P (h::t) ⇔ P h ∨ EXISTS P t): thm

Second, type instantiate:

val EXISTS_DEF' = INST_TYPE [alpha |-> ``:string``] EXISTS_DEF_0;
val EXISTS_DEF' = ⊢ (EXISTS P [] ⇔ F) ∧ (EXISTS P (h::t) ⇔ P h ∨ EXISTS P
t): thm

Third, instantiate variable P (now of type ``:string->bool``):

INST [``P:string->bool`` |-> ``(=) "T"``] EXISTS_DEF';
val it =
   ⊢ (EXISTS ($= "T") [] ⇔ F) ∧
 (EXISTS ($= "T") (h::t) ⇔ ("T" = h) ∨ EXISTS ($= "T") t): thm




On Mon, Jul 23, 2018 at 12:41 PM Chun Tian (binghe) 
wrote:

> > show_types := true;
> val it = (): unit
> > INFINITY_AX;
> val it = ⊢ ∃(f :ind -> ind). ONE_ONE f ∧ ¬ONTO f: thm
>
> > Il giorno 23 lug 2018, alle ore 18:22, Dylan Melville <
> dylanmelvi...@gmail.com> ha scritto:
> >
> > Is there a way to print theorems with types displayed?
> >
> >> On Jul 23, 2018, at 12:20 PM, Thomas Tuerk 
> wrote:
> >>
> >> Hi,
> >>
> >> hard to say, why it does not work without further details. However, one
> guess is that types do not match. I would recommend showing the types when
> printing the theorem. I expect that P might be of type `'a -> bool`. In
> this case you need to instantiate 'a to string first.
> >>
> >> Best
> >>
> >> Thomas
> >>
> >> On 23.07.2018 18:10, Dylan Melville wrote:
> >>> I have a theorem called EX which returns true when a value is an
> element of a list. It is defined as:
> >>>
> >>> thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t)
> >>>
> >>> I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t`
> being a long list of strings which contains “T”.  Unfortunately my attempts
> to use INST on this theorem haven’t worked. Why doesn’t the following work?
> >>>
> >>> INST [`(\x:string. x = “T")`,`P:(string->bool)`] EX;;
> >>>
> >>> Thank you.
> >>>
> >>> -Dylan Melville (McMaster University)
> >>>
> >>>
> >>>
> --
> >>> 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
>
>
> --
> 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 (automatically) change the names of quantified variables in a theorem?

[Konrad Slind]

See also Conv.RENAME_VARS_CONV

On Fri, Aug 3, 2018 at 9:00 AM Chun Tian (binghe) 
wrote:

> Hi Thomas,
>
> thanks very much, now I see the possibility of changing whatever variable
> names I want!  (I never knew nor needed ALPHA before, although
> alpha-conversion is familiar to me)
>
> —Chun
>
> Il giorno 03 ago 2018, alle ore 15:03, Thomas Tuerk <
> tho...@tuerk-brechen.de> ha scritto:
>
> Hi Chun,
>
> the easiest way is using alpha-equivalence. If you really just want to
> rename vars, you can state the new form explicitly and use apha-equivalence
> via e.g. ALPHA directly. Tools like METIS_TAC should in theory be able to
> do it, but in practice try to do too much and therefore time out, I fear.
>
> There are also tools for renaming bound vars. "rename_bvar" for example is
> a conversion for renaming an outermost bound var.
>
> Variables at subpositions can also be renamed using the quantifier
> heuristics lib (see, e.g. INST_QUANT_CONV)
>
> Vaguely related are tools for renaming free vars during a tactical proof.
> There are various related tactics for this, e.g. RENAME_TAC. However, since
> these deal with free vars during a proof, this does not fit really here.
>
> So, there are plenty of options. Looking at your description, I expect
> using ALPHA is the easiest and fasted possibility for your problem. I would
> use something like
>
> fun ALPHA_RULE t thm = let
>   val t0 = concl thm
>   val thm1 = ALPHA t0 t
>   val thm2 = EQ_MP thm1 thm
> in
>   thm2
> end
>
>
> val t0 = ``?A.  A  \/ !B  C. ?D.  D  B  C``
> val t  = ``?A'. A' \/ !B' C. ?DD. DD B' C``
>
> val thm0 = METIS_PROVE [] t0
> val thm = ALPHA_RULE t thm0
>
> Best
>
> Thomas
>
>
>
> On 03.08.2018 14:34, Chun Tian (binghe) wrote:
>
> Hi,
>
> suppose I have proved (or generated) a theorem like this:
>
>  ⊢ ∀a0 a1.
>  a0 ∼ a1 ⇔
>  ∀u.
>  (∀E1. a0 --u-> E1 ⇒ ∃E2. a1 --u-> E2 ∧ E1 ∼ E2) ∧
>  ∀E2. a1 --u-> E2 ⇒ ∃E1. a0 --u-> E1 ∧ E1 ∼ E2
>
> but I don’t like the variables names (a0, a1, E1, E2), I want a new theorem, 
> essentially the same one, but with variables names same as in text book:
>
> ⊢ ∀P Q.
>  P ∼ Q ⇔
>  ∀u.
>  (∀P'. P --u-> P' ⇒ ∃Q'. Q --u-> Q' ∧ P' ∼ Q') ∧
>  ∀Q'. Q --u-> Q' ⇒ ∃P'. P --u-> P' ∧ P' ∼ Q’
>
> if I understood HOL correctly, it is impossible to directly modify any 
> theorem (as first-class object), replacing its bound variables with different 
> names (if not conflicting others).
>
> Actually, changing the outside universal quantifiers is easy, as I just need 
> to do a SPEC with new variables, then GEN them. On the other side, I don’t 
> see any automatic way to replace inner variables.   I also tried to prove the 
> new theorem by PROVE_TAC or METIS_TAC with the old theorem, sometimes the 
> theorem can be directly proved, but most of time it fails, I think because of 
>  those existential quantifiers.
>
> Does anyone have such experiences? (it’s a painful process to go over all 
> proofs again, fixing almost every step with different variable names)
>
> 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 
> listhol-info@lists.sourceforge.nethttps://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
>
--
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] assumption matching in SPLIT_LT

[Konrad Slind]

Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
first one is the pop_assum match_mp_tac succeeding. So the proof is failing
before it gets to the THEN_LT.

Konrad.


On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
hol-info@lists.sourceforge.net> wrote:

> Hi,
>
> I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
> facing error with assumption matching. For instance, I've a proof goal of
> this form:
>
> `(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
>
> rw []
> \\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
> ALLGOALS (rw[]))
>
> I'm getting following matching error...
>
> Exception raised at Tactic.MATCH_MP_TAC:
> No match
> Exception-
>HOL_ERR
>  {message = "No match", origin_function = "MATCH_MP_TAC",
>   origin_structure = "Tactic"} raised
>
> It works otherwise for handling them individually...
> --
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>
> ___
> 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] Element assignment in structures

[Konrad Slind]

There seems to be some problems with the syntax. For one, the !ch ... on
the right hand side of the definition means that the rhs is boolean, which
conflicts with the record values being returned by the if-then-else.

Konrad.


On Wed, Dec 19, 2018 at 8:04 PM 幻＠未来 <849678...@qq.com> wrote:

> The following data types are defined in HOL4.
>
>val _ = Datatype `
>
>  coordinate = <|
>
> x_axis: real;
>
> y_axis: real;
>
> z_axis: real
>
>  |> `;
>
>val _ = Datatype `
>
>chromosome = <|
>
>r: num;
>
>b: num;
>
>distance: real;
>
>rx: coordinate;
>
>path: coordinate list;
>
>bx: coordinate
>
>|> `;
> val ch = ``ch: chromosome``;
> val pop = ``pop: chromosome list``;
>  val get_def = Define `
>  get pop = !ch  if (Certain condition) then (ch with <| distance 
> := ch.distance + max_distance pop |>)
>else (ch with <| distance := ch.distance |>)`;
>
>
> Given a pop(:chromosome list), I want to achieve a goal : If if-condition 
> is met, the distance value of the ch in the pop is assigned to other values, 
> otherwise the distance value of ch is unchanged. How to solve this problem?
>
> ___
> 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] Element assignment in structures

[Konrad Slind]

I recommend learning about the syntax of HOL a bit more. Also, as Michael
suggested (to you or someone else) maybe write the code up first as an SML
program and then translate to HOL. In any case, here are some nonsense
definitions that HOL allows. They should help you get further.

load "realLib";

val _ =
 Datatype `
  coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `;

val _ =
 Datatype `
chromosome = <| r: num; b: num; distance: real;
rx: coordinate; path: coordinate list;
bx: coordinate |> `;

val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;

val get_def =
  Define `
   get E pop =
case E pop
 of SOME ch => (ch with <| distance := ch.distance + 145 |>)
  | NONE => (HD pop with <| distance := (HD pop).distance |>)`;

val getA_def =
  Define `
   getA pop =
case pop
 of [] => ARB
  | ch::t =>
 if ch.r < ch.b
   then (ch with <| distance := ch.distance + 145 |>)
   else ch`;


On Wed, Dec 19, 2018 at 9:09 PM 幻＠未来 <849678...@qq.com> wrote:

> The following data types are defined in HOL4.
>
>val _ = Datatype `
>
>  coordinate = <|
>
> x_axis: real;
>
> y_axis: real;
>
> z_axis: real
>
>  |> `;
>
>val _ = Datatype `
>
>chromosome = <|
>
>r: num;
>
>b: num;
>
>distance: real;
>
>rx: coordinate;
>
>path: coordinate list;
>
>bx: coordinate
>
>|> `;
> val ch = ``ch: chromosome``;
> val pop = ``pop: chromosome list``;
>
>
> Given a pop(:chromosome list), I want to achieve a goal : If if-condition 
> is met, the distance value of the ch in the pop is assigned to other values, 
> otherwise the distance value of ch is unchanged. How to solve this problem? 
> How to define such an operation?
>
> ___
> 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 do this kind of induction?

[Konrad Slind]

There is discussion of something like this in the Euclid's Theorem
tutorial. You can do Induct_on `j - i` or do the trick where you prove ?k.
j = i + SUC k, eliminate j, and then induct on k.

Konrad.


On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe) 
wrote:

> sorry, "i ≤ j” should be “i < j” actually:
>
>∀i j. i < j ⇒ f (SUC i) ⊆ f j
>
>  0.  ∀n. f n ⊆ f (SUC n)
>  1.  ∀n. 0 < n ⇒ f 0 ⊆ f n
>
> > Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > I have the following goal to prove: (f : num -> ‘a set)
> >
> >   ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
> >   
> > 0.  ∀n. f n ⊆ f (SUC n)
> >
> > but how can I do the induction on … e.g. `j - i`?
> >
> > —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] How to do this kind of induction?

[Konrad Slind]

... also meant to mention that "Induct_on" and "completeInduct_on" have
online documentation.


On Sat, Jan 5, 2019 at 3:20 PM Konrad Slind  wrote:

> There is discussion of something like this in the Euclid's Theorem
> tutorial. You can do Induct_on `j - i` or do the trick where you prove ?k.
> j = i + SUC k, eliminate j, and then induct on k.
>
> Konrad.
>
>
> On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe) 
> wrote:
>
>> sorry, "i ≤ j” should be “i < j” actually:
>>
>>∀i j. i < j ⇒ f (SUC i) ⊆ f j
>>
>>  0.  ∀n. f n ⊆ f (SUC n)
>>  1.  ∀n. 0 < n ⇒ f 0 ⊆ f n
>>
>> > Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) <
>> binghe.l...@gmail.com> ha scritto:
>> >
>> > Hi,
>> >
>> > I have the following goal to prove: (f : num -> ‘a set)
>> >
>> >   ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
>> >   
>> > 0.  ∀n. f n ⊆ f (SUC n)
>> >
>> > but how can I do the induction on … e.g. `j - i`?
>> >
>> > —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] New grammar of defining theorems?

[Konrad Slind]

Isn't it clear just from the form?

  Theorem name quote (ML)--> val name = Q.store_thm(name,quote,ML)
  Theorem name (ML)  --> val name = save_thm(name,ML)



On Mon, Jan 7, 2019 at 8:34 PM  wrote:

> Forward and backward give us nice terminology, thanks!  It may also be
> possible to have the quotation filter figure things out by looking for the
> left-parenthesis that is required to follow the name in the forward case.
> I may play with that.
>
> Michael
>
> On 8/1/19, 12:38, "Chun Tian (binghe)"  wrote:
>
> Hmmm, well… all theorems are essentially *derived* from earlier
> theorems or axioms, thus it seems (to me) that the word “derived” still
> doesn’t capture the characterization of “save_thm” from “store_thm”.   But
> the word “dervied” makes more senses than previous “calculated” as
> “save_thm”’s body is mainly using “derived rules” instead of “tactics”.
> However, I see the essential difference is the direction in the proof: from
> proof goal to existing theorems, or from existing theorems to proof goal.
>
> This whole mail thread is not really a technical discussion, thus
> whatever I said here must be highly subjective, however I suggest the
> following:
>
> 1. using keyword “forward” and “backward” to distinguish theorems
> built by “save_thm” and “store_thm”, respectively:
>
> - Theorem(forward) name (MLcode);
> - Theorem(backward) name tmquote (MLcode);
>
> 2. the keyword (backward) is optional (simply because this is the most
> case), thus backward theorems can also be expressed (if detected the
> tmquote part, somehow) in your current way:
>
> - Theorem name tmquote (MLcode);
>
> 3. if ML’s parser is smart enough, even the keyword (forward) can be
> eliminated, because the number of arguments is different: in forward proof
> it is 2, in backward proof it is 3:
>
> - Theorem name (MLcode);
> - Theorem name tmquote (MLcode);
>
> How much you can go with above idea, depends on how powerful the ML
> quotation code can be.
>
> Hope this helps,
>
> —Chun
>
> > Il giorno 08 gen 2019, alle ore 02:10,
> michael.norr...@data61.csiro.au ha scritto:
> >
> > Indeed, they are both calculated.  In one, you state the desired
> end-state and head towards it with a tactic.  In the other, you transform
> existing theorems with rules of inference and derive a final statement
> (hence the good practice, which you mentioned, of putting the statement
> into a comment).
> >
> > Given that, what about
> >
> >   Theorem(derived) name (MLcode);
> >
> > ?
> >
> > Michael
> >
> > On 7/1/19, 20:31, "Chun Tian (binghe)" 
> wrote:
> >
> >Hi Michael,
> >
> >Thanks, now I see your points: if it’s really a “lemma”, then
> there’s no need to export it, thus `Q.prove` (or `prove`) should just do
> the job.
> >
> >Among the two syntactic sugars, I personally like your first
> version (Theorem(calculated) …), because it emphasized that, a `Theorem`
> generated by `save_thm` has no differences (in use) with a `Theorem`
> generated by `store_thm`, just the word “calculated” could have a better
> name, as both kinds of theorems are essentially calculated.
> >
> >—Chun
> >
> >> Il giorno 07 gen 2019, alle ore 01:16,
> michael.norr...@data61.csiro.au ha scritto:
> >>
> >> The Theorem keyword is a prettier way of writing `store_thm`,
> which, as the name suggests, is indeed for theorems.  In other words, the
> choice of Theorem merely reflects our existing naming convention.
> >>
> >> If you have a lemma that shouldn’t be “stored”, then you should
> probably be using `Q.prove` (or `prove`).  The use of theory files that
> make theorem values persistent is the way in which users can distinguish
> important results that should persist (that is, “theorems”), and those that
> should be more ephemeral.
> >>
> >> The existing `save_thm` entrypoint has the same problem with
> requiring redundant typing of names. I’m thus tempted to invent a Theorem
> analogue to map to it.  My current feeling is to go for something like
> >>
> >>   Theorem(calculated) thmname (ML code);
> >>
> >> Or
> >>
> >>  Computed_Theorem thmname (ML code)
> >>
> >> Or …?
> >>
> >> Suggestions welcome.
> >>
> >> Michael
> >>
> >> From: "Chun Tian (binghe)" 
> >> Date: Thursday, 3 January 2019 at 23:20
> >> To: Makarius 
> >> Cc: Michael Norrish , hol-info <
> hol-info@lists.sourceforge.net>
> >> Subject: Re: [Hol-info] New grammar of defining theorems?
> >>
> >> So the key is to make sure that they’re not distinguished
> internally by some tools, and if some tools do, it’s their problems but
> HOL’s.
> >>
> >> I personally don’t like the keyword “Theorem” because I think many
> small theorems with 3 lines of tactics do not deserve the name “Theorem”.
> The correct way of using these co

Re: [Hol-info] Confused about Induct_on

[Konrad Slind]

I suspect that the order of quantification in the goal is important, since
that controls how the induction predicate is instantiated. So try

  !Gamma A. Gm Gamma A ==> !Gamma'. 

since that makes it explicit for the machinery.

Konrad.


On Tue, Jan 15, 2019 at 1:30 AM Chun Tian (binghe) 
wrote:

> Hi,
>
> I think you should use HO_MATCH_MP_TAC (together with your induction
> theorem of “Gm”, of the form ``!Gm. X ==> P Gm``) in this case.  I only use
> Induct and Induct_on on simple variables like your Γ Γ’ A.
>
> —Chun
>
> > Il giorno 15 gen 2019, alle ore 14:49, Alexander Cox <
> u6060...@anu.edu.au> ha scritto:
> >
> > I am having an issue using Induct_on on a Hol_reln called Gm.
> >
> > If I try to use it on a trivial goal it works, e.g.
> >
> > > g `!Γ A. Gm Γ A ==> Gm Γ A`;
> > …
> > > e (Induct_on `Gm`);
> > OK..
> > 1 subgoal:
> > val it =
> >
> >
> >(∀A. Gm {|A|} A) ∧ …
> >
> > but if I use on a useful goal such as:
> >
> > g `!Γ Γ' A. Gm Γ A ==> Gm (Γ' + Γ) A`;
> > …
> > e (Induct_on `Gm`);
> > OK..
> >
> > Exception raised at BasicProvers.Induct_on:
> > at BasicProvers.induct_on_type:
> > Type: :(α formula -> num) -> α formula -> bool is not registered in the
> types database
> >
> > Any ideas where I’m going wrong? Is the latter the goal in the wrong
> form? Where should I look to figure this out?
> >
> > Thank you,
> > Alex
> >
> > ___
> > 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 ???

[Konrad Slind]

It's a deliberate choice. See the discussion in Section 1.2 of

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692&rep=rep1&type=pdf



On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) 
wrote:

> Hi,
>
> in HOL's realTheory, division is defined by multiplication:
>
> [real_div]  Definition
>
>   ⊢ ∀x y. x / y = x * y⁻¹
>
> and zero multiplies any other real number equals to zero, which is
> definitely true:
>
>[REAL_MUL_LZERO]  Theorem
>
>   ⊢ ∀x. 0 * x = 0
>
> However, above two theorems together gives ``0 / 0 = 0``, as shown below:
>
> > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
> val it = ⊢ 0 / 0 = 0: thm
>
> How do I understand this result? Is there anything "wrong"?
>
> (The same problems happens also in extrealTheory, since the definition
> of `*` finally reduces to `*` of real numbers)
>
> Regards,
>
> Chun Tian
>
> ___
> 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] Dealing with INFINITE num set ...

[Konrad Slind]

Rephrasing things might bring clarity:

load "pred_setLib";
open pred_setTheory;

val set_ss = (arith_ss ++ pred_setLib.PRED_SET_ss);

val lem = Q.prove
(`~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`,
 rw_tac set_ss [EQ_IMP_THM,SUBSET_DEF,IN_DEF]
  >- (`FINITE P \/ ?n. P n /\ ~P n` by metis_tac []
   >> imp_res_tac SUBSET_FINITE
   >> full_simp_tac std_ss [SUBSET_DEF, IN_DEF])
  >- metis_tac[]);

>From this and the original assumption, you should be able to get that P is
finite, so has a maximum element.

Konrad.



On Fri, Feb 15, 2019 at 1:12 PM Chun Tian (binghe) 
wrote:

> Hi,
>
> I'm blocked at the following (strange) situation:
>
> I have an infinite set of integers (num) in which each integer n
> satisfies a property P(n):
>
> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
>
> Suppose above proposition is NOT true, how can I derive that, there must
> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
>
> ?m. !n. m <= n ==> ~(P n)
>
> Thanks in advance,
>
> Chun Tian
>
> ___
> 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] Dealing with INFINITE num set ...

[Konrad Slind]

This can be proved by contradiction, using the fact that the set of numbers
less than any given number is finite.

val lemB = Q.prove
(`!N m. INFINITE N ==> ?n. m <= n /\ n IN N`,
 spose_not_then strip_assume_tac
  >> `FINITE (count m)` by metis_tac [FINITE_COUNT]
  >> `N SUBSET (count m)`
  by (rw_tac set_ss [SUBSET_DEF]
   >> `~(m <= x)` by metis_tac []
   >> decide_tac)
  >> metis_tac [SUBSET_FINITE])

On Fri, Feb 15, 2019 at 1:47 PM Chun Tian (binghe) 
wrote:

> And also this one:
>
> Given `INFINITE N` and a fixed number `m`, how can I assert the
> existence of another number `n` such that,
>
> m <= n /\ n IN N
>
> i.e. prove that
>
> ``!N m. INFINITE N ==> ?n. m <= n /\ n IN N``
>
> --Chun
>
> Il 15/02/19 20:11, Chun Tian (binghe) ha scritto:
> > Hi,
> >
> > I'm blocked at the following (strange) situation:
> >
> > I have an infinite set of integers (num) in which each integer n
> > satisfies a property P(n):
> >
> > ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
> >
> > Suppose above proposition is NOT true, how can I derive that, there must
> > exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
> >
> > ?m. !n. m <= n ==> ~(P n)
> >
> > Thanks in advance,
> >
> > Chun Tian
> >
>
> ___
> 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 ???

[Konrad Slind]

Just a minor note: ARB is declared as an uninterpreted constant of type 'a.
It used to be defined to be @x.T.

Konrad.


On Tue, Feb 19, 2019 at 11:49 PM  wrote:

> Your right hand side is no better than ARB really.  You say that your aim
> is to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a
> literal extreal, then I will define
>
>   val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>
> and then I can certainly prove that x/0 = pni.  If ARB is a literal
> extreal, surely pni is too.
>
> (Recall that ARB's definition is `ARB = @x. T`.)
>
> Michael
>
>
> On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
>
> Some further updates:
>
> With my last definition of `extreal_div`, I still have:
>
>  |- !x. x / 0 = ARB
>
> and
>
>  |- 0 / 0 = ARB
>
> trivially holds (by definition). This is still not satisfied to me.
>
> Now I tried the following new definition which looks more reasonable:
>
> val extreal_div_def = Define
>`extreal_div x y = if y = Normal 0 then
>   (@x. (x = PosInf) \/ (x = NegInf))
>   else extreal_mul x (extreal_inv y)`;
>
> literally, it says anything (well, let's ignore zero) divides zero is
> equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
> irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
> 0 = y`` being proved, in which y is a literal extreal. For example, if
> I
> try to prove ``!x. x / 0 = ARB``:
>
> (* with the new definition, ``x / 0 = ARB`` (or any other extreal)
> can't
> be proved, e.g.
> val test_div = prove (
>`!x. extreal_div x (Normal 0) = ARB`,
> RW_TAC std_ss [extreal_div_def]
>  >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>  >- RW_TAC std_ss []
>  >> MATCH_MP_TAC SELECT_ELIM_THM
>  >> RW_TAC std_ss [] (* 3 gubgoals *)
>NegInf = ARB
>
>PosInf = ARB
>
>∃x. (x = PosInf) ∨ (x = NegInf));
>  *)
>
> at the end I got 3 subgoals like above. I *believe*, no matter what
> value I put instead of ARB, at least one of the subgoals must be false.
> Thus the theorem should be unprovable. (am I right?)
>
> Can I adopt this new definition of `extreal_div` in the future? Any
> objection or suggestion?
>
> --Chun
>
> Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> > I'm going to use the following definition for `extreal_div`:
> >
> > (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> > val extreal_div_def = Define
> >`extreal_div x y = extreal_mul x (extreal_inv y)`;
> >
> >new definition of `extreal_div`, excluding the case `0 / 0`: *)
> > val extreal_div_def = Define
> >`extreal_div x y = if (y = Normal 0) then ARB
> >   else extreal_mul x (extreal_inv y)`;
> >
> > previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <>
> 0` as
> >  antecedent, which makes perfectly senses.
> >
> > P.S. the division of extended reals in HOL4 are not used until the
> > statement and proof of Radon-Nikodým theorem, then the conditional
> > probability.
> >
> > --Chun
> >
> > Il 15/02/19 17:39, Mark Adams ha scritto:
> >> I think there is definitely an advantage in keeping ``x/y``
> undefined
> >> (even granted that it will always be possible to prove ``?y. x/0 =
> y``),
> >> namely that it means that your proofs are much more likely to
> directly
> >> translate to other formalisms of real numbers where '/' is not
> total.
> >>
> >> Of course there is also a disadvantage, in that it makes proof
> harder.
> >> But then, arguably, being forced to justify that we are staying
> within
> >> the "normal" domain of the function is probably a good thing (in a
> >> similar way as being forced to conform to a type system is a good
> >> thing).  I understand that, historically, it is this disadvantage of
> >> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
> >> much easier for automated routines if they don't have to consider
> side
> >> conditions.
> >>
> >> Mark.
> >>
> >> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
> >>> Thanks to all kindly answers.

Re: [Hol-info] How to express a finite_map or alist using a key list and a value list?

[Konrad Slind]

See also examples/balanced_bst/balanced_mapTheory, which has a "fromList"
construct.
That does have the requirement of having the domain type capable of being
ordered.

Konrad.


On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe) 
wrote:

> Hi,
>
> I wonder what's the most natural/native way to express a finite_map or
> alist, using a key list and a value list (assuming their lengths are the
> same, and the key list is all distinct)?
>
> My current idea is to use MAP2 to build an alist of type ``:('a # 'b)
> list``:
>
> MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list)
>
> then (if needed), `alist_to_fmap` will lead me to a finite_map. But
> shouldn't it be already provided by a definition in alistTheory (or
> finite_mapTheory) that I just didn't find out?
>
> --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] Simplify/normalize propositional logic terms?

[Konrad Slind]

A couple of places to look in HOLindex: refuteLib and normalForms structure.


On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) 
wrote:

> Hi,
>
> it can be proven (by DECIDE_TAC) that,
>
> |- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x
>
> but is there any conversion function available in HOL4 such that from LHS
> of above equation I can directly get the RHS - something like a canonical
> form?
>
> --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] Using @ for multiple selections in HOL Light

[Konrad Slind]

If you have |- !p. ?m c. ... as a theorem, then you are set up to use
constant specification. Just have to apply SKOLEM_THM to move the
existentials out to the top level .

Konrad.


On Tue, Feb 18, 2020 at 4:33 PM Norrish, Michael (Data61, Acton) <
michael.norr...@data61.csiro.au> wrote:

> Maybe use the choice function to select a pair. I.e., write
>
> @(m,c). .
>
> ?
>
> Michael
>
> On 19 Feb 2020, at 09:30, "jpe...@student.bham.ac.uk" <
> jpe...@student.bham.ac.uk> wrote:
>
> 
> Hi
>
> This is a question about using the select operator @ to return multiple
> values which depend on each other in HOL Light.
>
> For example when working with polynomial_function defined as
> polynomial_function p <=> ?m c. !x. p x = sum(0..m) (\i. c i * x pow i)​  it
> might be useful to be able to use the @ operator to return the upper bound
> m and the coefficient function c, however as the choice of m depends on c
> and visa versa you cannot use 2 separate select statements. (e.g. if m >
> degree(p) then c(n) must be 0 for degree(p)
> What is the best way to approach this? Is there a way to return both of
> the values or would they have to be "combined together" inside the select
> statement?
>
>  Thanks
>
> James
> ___
> 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] EVAL when equations have an antecedent

[Konrad Slind]

I think so, for example, if "x" is a concrete term, then EVAL "f x" should
return a theorem |- f x = c. However, if function f is only defined for x
meeting P, then things may be more fiddly.

Konrad.


On Thu, Jul 30, 2020 at 2:40 PM Mario Xerxes Castelán Castro <
marioxcc...@yandex.com> wrote:

> Suppose I have a theorem like “P x ⇒ f x = t” where t is a metavariable
> for an expression to which “f x” should evaluate. Is it possible to have
> computeLib attempt to evaluate “P x” to “T” and then use “f x = t” to
> compute?
>
>
> ___
> 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 replay?

[Konrad Slind]

HOL4 has a notion of persistent theory, so you could spawn many
parallel sessions, each delivering a theory with one result, then
create a single descendant theory, import all the parent
theories, and chain your implications or inequalities there.

It also provides integer decision procedures, so the calls to
INT_ARITH might possibly be directly substitute-able.

Konrad.


On Thu, Jan 28, 2021 at 5:07 PM D. J. Bernstein  wrote:

> Thanks for the references and suggestions. As a scaled-down example of
> part of the time consumption, this takes 400 million CPU cycles:
>
>INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1)
>   <= &47942158315484610560 * (&2 * (x:int) + &1)
>  + &135203236847161865141
>   /\
>   &0 <= &2655641718416121605914624 * (&2 * x + &1)
> + &2208414543647439060992 * (&2 * y + &1)
> + &6004289407548407186399935
>   ==>
>   &0 <= &13137886070707932161376256 * (&2 * x + &1)
> + &17509226798704706453504 * (x + y + &1)
> + &36152178747194683600721967`;;
>
> Hand proof: take 653244900095080313091/700376017867732114912 and
> 26794012414555294513937/5603008142941856919296 times the first and
> second inequalities, add, and observe that you now have a stronger
> version of the conclusion, offset by 1581608968911709059178093879/256.
>
> Changing INT_ARITH to g still takes around 100 million CPU cycles, which
> makes me wonder whether there's some bottleneck in parsing or printing.
>
> The code that I wrote to do a bunch of searching to find and print the
> whole sequence of relevant presumed theorems is, with no optimization
> effort, thousands of times faster than this. Of course that code doesn't
> have to bother with the symbolic aspects of proof manipulation.
>
> ---Dan
> ___
> 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 replay?

[Konrad Slind]

Also, there seems to be some inefficiency: the posted formula gets proved
quite quickly in HOL4:

Count.apply ARITH_CONV tm;
runtime: 1.2s,gctime: 0.77200s, systime: 0.0s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 493764; Total: 493764
val it =
   ⊢ 193650890589077504 * (2 * y + 1) ≤
 47942158315484610560 * (2 * x + 1) + 135203236847161865141 ∧
 0 ≤
 2655641718416121605914624 * (2 * x + 1) +
 2208414543647439060992 * (2 * y + 1) + 6004289407548407186399935 ⇒
 0 ≤
 13137886070707932161376256 * (2 * x + 1) +
 17509226798704706453504 * (x + y + 1) + 36152178747194683600721967 ⇔ T:
   thm

On Thu, Jan 28, 2021 at 6:57 PM Konrad Slind  wrote:

> HOL4 has a notion of persistent theory, so you could spawn many
> parallel sessions, each delivering a theory with one result, then
> create a single descendant theory, import all the parent
> theories, and chain your implications or inequalities there.
>
> It also provides integer decision procedures, so the calls to
> INT_ARITH might possibly be directly substitute-able.
>
> Konrad.
>
>
> On Thu, Jan 28, 2021 at 5:07 PM D. J. Bernstein  wrote:
>
>> Thanks for the references and suggestions. As a scaled-down example of
>> part of the time consumption, this takes 400 million CPU cycles:
>>
>>INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1)
>>   <= &47942158315484610560 * (&2 * (x:int) + &1)
>>  + &135203236847161865141
>>   /\
>>   &0 <= &2655641718416121605914624 * (&2 * x + &1)
>> + &2208414543647439060992 * (&2 * y + &1)
>> + &6004289407548407186399935
>>   ==>
>>   &0 <= &13137886070707932161376256 * (&2 * x + &1)
>> + &17509226798704706453504 * (x + y + &1)
>> + &36152178747194683600721967`;;
>>
>> Hand proof: take 653244900095080313091/700376017867732114912 and
>> 26794012414555294513937/5603008142941856919296 times the first and
>> second inequalities, add, and observe that you now have a stronger
>> version of the conclusion, offset by 1581608968911709059178093879/256.
>>
>> Changing INT_ARITH to g still takes around 100 million CPU cycles, which
>> makes me wonder whether there's some bottleneck in parsing or printing.
>>
>> The code that I wrote to do a bunch of searching to find and print the
>> whole sequence of relevant presumed theorems is, with no optimization
>> effort, thousands of times faster than this. Of course that code doesn't
>> have to bother with the symbolic aspects of proof manipulation.
>>
>> ---Dan
>> ___
>> 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 replay?

[Konrad Slind]

Just for clarification:  the HOL4 term parser handled the supplied term
without alteration, and
intLib.ARITH_CONV is the HOL4 analog of INT_ARITH.




On Thu, Jan 28, 2021 at 6:59 PM Konrad Slind  wrote:

> Also, there seems to be some inefficiency: the posted formula gets proved
> quite quickly in HOL4:
>
> Count.apply ARITH_CONV tm;
> runtime: 1.2s,gctime: 0.77200s, systime: 0.0s.
> Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 493764; Total: 493764
> val it =
>⊢ 193650890589077504 * (2 * y + 1) ≤
>  47942158315484610560 * (2 * x + 1) + 135203236847161865141 ∧
>  0 ≤
>  2655641718416121605914624 * (2 * x + 1) +
>  2208414543647439060992 * (2 * y + 1) + 6004289407548407186399935 ⇒
>  0 ≤
>  13137886070707932161376256 * (2 * x + 1) +
>  17509226798704706453504 * (x + y + 1) + 36152178747194683600721967 ⇔
> T:
>thm
>
> On Thu, Jan 28, 2021 at 6:57 PM Konrad Slind 
> wrote:
>
>> HOL4 has a notion of persistent theory, so you could spawn many
>> parallel sessions, each delivering a theory with one result, then
>> create a single descendant theory, import all the parent
>> theories, and chain your implications or inequalities there.
>>
>> It also provides integer decision procedures, so the calls to
>> INT_ARITH might possibly be directly substitute-able.
>>
>> Konrad.
>>
>>
>> On Thu, Jan 28, 2021 at 5:07 PM D. J. Bernstein  wrote:
>>
>>> Thanks for the references and suggestions. As a scaled-down example of
>>> part of the time consumption, this takes 400 million CPU cycles:
>>>
>>>INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1)
>>>   <= &47942158315484610560 * (&2 * (x:int) + &1)
>>>  + &135203236847161865141
>>>   /\
>>>   &0 <= &2655641718416121605914624 * (&2 * x + &1)
>>> + &2208414543647439060992 * (&2 * y + &1)
>>> + &6004289407548407186399935
>>>   ==>
>>>   &0 <= &13137886070707932161376256 * (&2 * x + &1)
>>> + &17509226798704706453504 * (x + y + &1)
>>> + &36152178747194683600721967`;;
>>>
>>> Hand proof: take 653244900095080313091/700376017867732114912 and
>>> 26794012414555294513937/5603008142941856919296 times the first and
>>> second inequalities, add, and observe that you now have a stronger
>>> version of the conclusion, offset by 1581608968911709059178093879/256.
>>>
>>> Changing INT_ARITH to g still takes around 100 million CPU cycles, which
>>> makes me wonder whether there's some bottleneck in parsing or printing.
>>>
>>> The code that I wrote to do a bunch of searching to find and print the
>>> whole sequence of relevant presumed theorems is, with no optimization
>>> effort, thousands of times faster than this. Of course that code doesn't
>>> have to bother with the symbolic aspects of proof manipulation.
>>>
>>> ---Dan
>>> ___
>>> 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] Abstract algebra in HOL4 and Isabelle/HOL – Re: Abstract algebra in HOL4 – Re: Release notes for HOL4, Kananaskis-14

[Konrad Slind]

> I just want to point out that the goalposts have shifted
> slightly. The material pointed to by Michael shows that a fair
> bit of basic abstract algebra can be cleanly done in HOL's type
> theory, which I gather was the original point in question.
>
> re: Ken's questions.
>
> 1. The carrier is expressed as a predicate on a polymorphic type,
>so it is indeed a term. Moreover, the UNIV operator can be
>used to get the set of elements of a type. So I am not really
>seeing this as an impediment, at least for the simple examples
>being discussed.
>
> 2. Yes, there is no quantification of type variables in the HOL
>logic. This has been discussed at length in earlier postings
>on this list. Extensions of HOL with type quantification have
>been proposed by Melham and, later, by Homeier. These have
>been implemented and applied to interesting examples, but
>HOL4 hasn't moved to type quantification yet.
>
> Konrad.
>

(Deleted previous messages in thread because MailMan complains)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Problem with GEN_REWRITE_TAC

[Konrad Slind]

>> I would also like to know if there is any way of defining the
>> reflexive-transitive closure of a relation in a better way (i.e., so
>> that HOL knows what it is and there is no need to prove, for example,
>> that WiresRTC(WiresRTC(a)) = WiresRTC(a)).
>>

RTC is defined in relationTheory, and you can find out a little about
it in the Description, in the section on Basic Theories. You can
also find useful definitions and theorems in an interactive session
by invoking

 find "rtc";

Konrad.


-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Adding assumptions to solve a goal

[Konrad Slind]

Hi Juan,

Although it is useful, RW_TAC is not the only reasoning tool to
use in HOL, as you are finding. In your example, if you want to
get to a state

>  seq IN
>  setSeqLast
>(setSeqConcat
> (setSetConcat
>(seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
>   (sm c'))
>(seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm  
> c0)))
>   (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
>  ?hwa. seq = Link hwa Empty
> --
> 1 ~((sm c') = {})
> 2 ~((sm c0) = {})
> 3 ...
> .
> .
> .
> n ~((setSetConcat
>  (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
>  (seqSetConcat
>   (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm c0)))
> = {})

where the last hypothesis will solve the goal, I'd explicitly state the
last hypothesis as a new sub-goal, prove it in isolation, and
then return to the main line of the proof. To do this, I'd start
by doing

e (`~((setSetConcat
  (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
 (sm c'))
  (seqSetConcat
   (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm c0)))
 = {})`
by ALL_TAC);

and then apply some lemmas (maybe using METIS_TAC) that propagate
non-emptiness under the operations in your formula. Once you are
doing with proving the hypothesis, it will appear on your assumption
list and you should be able to finish your proof then.

Konrad.






On Sep 25, 2007, at 10:51 AM, Juan Perna wrote:

> Hello,
>
> This is probably a simple question, but I couldn't find a way of doing  
> it...
>
> I am proving this subgoal:
>
>seq IN
>setSeqLast
>  (setSeqConcat
> (setSetConcat
>(seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
>   (sm c'))
>(seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm  
> c0)))
> (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
>?hwa. seq = Link hwa Empty
>
> this looks quite ugly, but it can be "abstracted" to:
>
>  seq IN
>  setSeqLast
>(setSeqConcat
>   setOfTraces
>   (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
>  ?hwa. seq = Link hwa Empty
>
> I have a couple of results that should be enough to solve the proof,  
> the
> main one being:
>
> setSeqLastSetSeqConcat |-
>~(seq = Empty) /\ ~(seqSet = {}) ==>
>   (setSeqLast (setSeqConcat seqSet seq) = {seqLast seq})
>
> under valid assumptions, this should reduce the goal to something like:
>  seq IN
>  {seqLast (Link {CA (SignalLink s (P_f c0))} Empty))} ==>
>  ?hwa. seq = Link hwa Empty
>
> and from there it is possible to finish it.
>
> The problem is how to "add" the assumptions that setSeqLastSetSeqConcat
> needs (i.e., that the setOfTraces is not the empty set). In this
> direction, I have some results that would provide what is needed (for
> example: I have a thm telling me: !c. ~((sm c) = {})). My problem here
> is that I don't know how to tell HOL how to use this theorems.
>
> I tried with RW_TAC std_ss [all pertinent thms here], but nothing
> happened (I think it was not possible for HOL to infer what I wanted to
> do). I also tried with ACCEPT_TAC, but doesn't seem to be what I need
> (as none of these theorems will solve the goal just by themselves).
>
> What I need is a way of adding assumptions to the proof. For example, I
> think it would be necessary to add that ~((sm c) = {}) to the
> assumptions (knowing this is valid assumption given the result I
> mentioned before). With this, I think I should be getting something  
> like:
>
>  seq IN
>  setSeqLast
>(setSeqConcat
> (setSetConcat
>(seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
>   (sm c'))
>(seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm  
> c0)))
>   (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
>  ?hwa. seq = Link hwa Empty
> --
> 1 ~((sm c') = {})
> 2 ~((sm c0) = {})
> 3 ...
> .
> .
> .
> n ~((setSetConcat
>  (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
>  (seqSetConcat
>   (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm c0)))
> = {})
>
> with this additional hypothesis, I think a RW_TAC std_ss
> [setSeqLastSetSeqConcat] should get me where I want to go...
>
> Thank you,
>
> Juan
>
> --- 
> --
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2005.
> http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
> __

Re: [Hol-info] Commuting quantifiers

[Konrad Slind]

Juan Perna wrote:
> Hello,
>
> I am needing to transform a goal of the form: "?x.!y. (P x y)" into 
> "!y.?x. (P x y)" but I haven't been able to find anything like that in 
> the "bool" theory (or anywhere else). I looked for it using:
>
> DB.match ["-"] ``!P. (!x.?y. P) ==> (?y.!x. P)``;
>   
DB.match [] ... gives the same result. I would have probably
searched with a slightly more general expression, something
like

   DB.match [] ``?y. !x. P x y``

but it's a matter of taste. This will find SKOLEM_THM
which is related to what you want ...
> but this didn't bring any results.
>
> On the other hand, I know it is true that:
>
> ?x.!y. (P x y) ==> !y.?x. (P x y)
>
> (which is what I need).
>   
You can prove this with METIS_PROVE:

  - METIS_PROVE [] ``(?x.!y. (P x y)) ==> !y.?x. (P x y)``;
  <>
   metis: r[+0+3]#
  > val it = |- (?x. !y. P x y) ==> !y. ?x. P x y : thm

but you won't be able to apply it to advance your goal. The
implication is going the wrong way. And the other direction
isn't valid (consider < on the integers).
> How do I look for this kind of 
> rules/conversions in the existing theories?
>   
Most of the basics having to do with boolean structure and
quantifiers is already proved in boolTheory. So you can
find it there using DB.match. Or you can attempt to prove
such things on the fly, using DECIDE or METIS_PROVE
(using decision procedures as a kind of database lookup).

Konrad.

-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proving with inductive definitions

[Konrad Slind]

Hi Juan,

   Seems to be something about the way the goal is stated.
You've got

>> `!a. smPred a ==>
>>   !sec c. (a = (c,seq)) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`

If this is restated as

!a. smPred a ==> ?hwa. seqLast (SND a) = Link hwa Empty

then the IHs end up looking like what you want.

Konrad.


On Oct 5, 2007, at 4:49 AM, Juan Ignacio Perna wrote:

> Hello everybody,
>
> I am using an inductively defined predicate "smPred" defined as:
>
> val (smPred_rules, smPred_ind, smPred_cases) =
> Hol_reln
>(* DELAY *)
>   `(!s f. smPred((Delay s f),(Link {} Empty))) /\
>
>(* SEQUENTIAL COMPOSITION *)
>(!s f c1 c2 c1Seq c2Seq. smPred(c1,c1Seq) /\ smPred(c2,c2Seq)
>==> smPred((SeqComp s f c1 c2),
>   (concat
>  (concat c1Seq c2Seq)
>  (Link {(CA (SignalLink f (P_f c2)))} Empty`;
>
> that relates a circuit with the sequences of actions that describe its
> semantics.
>
> I also have a function that returns the last element of a given  
> sequence
> ("seqLast") (I am attaching a simple version of the source file so you
> can have a look if you want).
>
> I am trying to prove that the last element of a sequence (for all  
> sequences generated by the predicate) is always of the form "?hwa.  
> (Link hwa Empty)" (which we can say is true by inspecting the way in  
> which the predicate "builds" the sequences).
>
> I am intending to use smPred_ind to make the proof, so I stated the  
> goal as:
>
> `!a. smPred a ==>
>   !sec c. (a = (c,seq)) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`
>
> After doing "e (HO_MATCH_MP_TAC smPred_ind)", stripping the goal and
> proving the base case, I end up with:
>
> ?hwa. seqLast seq = Link hwa Empty
> 
>  0.  !sec c.
> ((c1,c1Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>  1.  !sec c.
> ((c2,c2Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>  2.  (SeqComp s f c1 c2,
> concat (concat c1Seq c2Seq)
>   (Link {CA (SignalLink f (P_f c2))} Empty)) =
> (c,seq)
>
> I have tried to reduce/simplify/transform:
>
>  0.  !sec c.
> ((c1,c1Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>
> into: "?hwa. seqLast c1Seq = Link hwa Empty" which is the inductive
> hypothesis I was expecting to get (one of them), but I haven't been  
> able
> to make much progress. The problem seems to be in the way the  
> variables are quantified (i.e., it doesn't allow me to instantiate  
> "seq" to "c1Seq" that is what I need).
>
> Is there any way to get the inductive hypothesis in a more "useful"  
> way?  (Is there any transformation I haven't check?). Should I try to  
> re-state the goal in a different way? (I tried to do this, but I  
> wasn't able to use HO_MATCH_TAC with the induction principle on them).
>
> I also explored the possibility of using Tom Melham's "IndDefRules"  
> and defined the induction tactic for smPred as:
>
> val smPred_INDUCT_TAC =
>   IndDefRules.RULE_INDUCT_THEN smPred_ind STRIP_ASSUME_TAC
>   STRIP_ASSUME_TAC;
>
> but it seems to accept goals only in the form required by  
> "HO_MATCH_TAC smPred_ind" (and it produces the same results). I tried  
> to use it with some other versions of the goal (such as: `!seq c.  
> smPred(c, seq) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`) but got  
> the exception: "Inappropriate goal" (I read Tom Melham's paper about  
> IndDefRules that comes with the HOL source files, but I wasn't able to  
> find a precise description of the "format" of the goal that the tactic  
> expects). Is there any further information about this somewhere?
>
> I also found a curious thing when trying to prove the goal from Tom  
> Melham's package. The sub-goal of the proof related to the inductive  
> step of the definition is:
>
>  !sec c.
>((SeqComp s f c1 c2,
> concat (concat c1Seq c2Seq) (Link {SignalLink f (P_f c2)} Empty)) =
>(c,seq)) ==>
> ?hwa. seqLast seq = Link hwa Empty
> 
>0.  !sec c.
>  ((c1,c1Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>1.  !sec c.
>  ((c2,c2Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>
> if we do (FULL_SIMP_TAC std_ss []), we get the two "seq" in the  
> assumptions abstracted (together with some simplification in the goal  
> as well):
>
>   (concat (concat c1Seq c2Seq) (Link {SignalLink f (P_f c2)} Empty) =
>  seq) ==>
>?hwa. seqLast seq = Link hwa Empty
>   
>0.  (c1Seq = seq) ==> ?hwa. seqLast seq = Link hwa Empty
>1.  (c2Seq = seq) ==> ?hwa. seqLast seq = Link hwa Empty
>
> if we do "RW_TAC std_ss []" here, we get the two "seq" occurrences in  
> the assumptions expanded with the information in the goal:
>
> ?hwa.
>seqLast
> (concat (concat c1Seq c2Seq) (Link {SignalLink f (P_f c2)} Empty))  
> =
> Link hwa Empty
> --

Re: [Hol-info] rookie question

[Konrad Slind]

This is a situation where type abbreviations probably won't
help you, since you have to mention all the type variables
when writing the abbreviation (just like in ML).

Antiquotations might help. At the ML level you could write

  val my_type = ``:('a,'b,'c,'d,'e,'f,'g,'h)my_type``

and then later in a type quotation you could write

   ``:  ^my_type ... ``

and in a term quotation you could write

   `` ... (r : ^(ty_antiq my_type)) ... ``

for example.

Konrad.


Bingham, Jesse D wrote:
> I've defined a nested record type structure my_type that contains 8 
> type variables 'typevar1,...,'typevar8.  Whenever I  mention this 
> type, I have to do something like
>  
> ('typevar1,'typevar2,'typevar3,'typevar4,'typevar5,'typevar6,'typevar7,'typevar8)my_type
>  
> which is obviously a little messy.  My question (and I'm not sure if 
> this even makes sense): is there a way to make type variables have 
> scope as being a whole theory?  I suppose what I'm after is the 
> ability to simply write
>  
> my_type
>  
> or something slimilar and have HOL interpret this as the messy type 
> expression above.  Thanks
>  
> -Jesse
> 
>
> -
> This SF.net email is sponsored by: Splunk Inc.
> Still grepping through log files to find problems?  Stop.
> Now Search log events and configuration files using AJAX and a browser.
> Download your FREE copy of Splunk now >> http://get.splunk.com/
> 
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>   

-
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems?  Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Tools and Techniques for Verification of System Infrastructure (Announce)

[Konrad Slind]

 
=

   Tools and Techniques for Verification of System Infrastructure
 A Festschrift in honour of Prof. Michael J. C. Gordon FRS

   March 25-26, 2008, Royal Society, London

 http://www.ttvsi.org/
 
=

In today's increasingly computer-based society, crucial
infrastructure---such as programming languages, compilers, networks,
and microprocessors---needs to meet a very high standard of
correctness in order to deliver the necessary quality and reliability
for applications. One way to achieve the necessary level of assurance
is to use formal specification and proof. Tool support for this
approach has steadily grown in sophistication and power, to the point
where the specification and verification of important system
infrastructure is an emerging fact.

To survey the state of the art and discuss future possibilities and
challenges, we are pleased to announce a two day research meeting, to
be held in honour of Professor Mike Gordon on the occasion of his 60th
birthday.  The meeting will be held on Tuesday 25 and Wednesday 26
March 2008 at the Royal Society, London.

The following speakers will present their research:

Mike Gordon, Cambridge University
John Harrison, Intel
Sava Krstic, Intel
Xavier Leroy, INRIA
Tom Melham, Oxford University
Robin Milner, Cambridge University
J Moore, University of Texas at Austin
Tobias Nipkow, Technical University of Munich
Michael Norrish, NICTA
Larry Paulson, Cambridge University
Peter Sewell, Cambridge University
Laurent Thery, INRIA

An important part of the meeting will be poster presentation sessions,
in which attendees may present their research.  Detailed information
about how to submit an abstract for a poster presentation, and to
register for the meeting, will be announced in due course.

Organizing Committee:

   Richard Boulton, Icera
   Joe Hurd, Galois
   Konrad Slind, University of Utah

For all enquiries about the Festschrift, please use the email address  
[EMAIL PROTECTED]


-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] BIGINTER definition question.

[Konrad Slind]

On Dec 27, 2007, at 9:59 AM, [EMAIL PROTECTED] wrote:

> Hi,
>  
> pred_setTheory.BIGINTER seems to be a generalized UNION defintion if 
> I'm understanding it correctly.  for example, suppose..

No, it's a generalized intersection. Here's a version of your example.
We want to show

> BIGINTER {{1; 2; 3}; {3; 4; 5; 6}} = {3}
>

So apply extensionality to the goal:

> (* load "pred_setLib"; open pred_setTheory; *)
> - e (RW_TAC std_ss [EXTENSION]);
> OK..
> 1 subgoal:
> > val it =
> x IN BIGINTER {{1; 2; 3}; {3; 4; 5; 6}} = x IN {3}
>

And then you can just call EVAL_TAC (depends on some mods
I just added to the repository).

> - e EVAL_TAC;
> OK..
>
> Goal proved.
> |- x IN BIGINTER {{1; 2; 3}; {3; 4; 5; 6}} = x IN {3}
> > val it =
> Initial goal proved.
> |- BIGINTER {{1; 2; 3}; {3; 4; 5; 6}} = {3} : goalstack


Konrad.


-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] defining a recursive func for real

[Konrad Slind]

On Dec 22, 2007, at 12:21 PM, [EMAIL PROTECTED] wrote:

> val F_defn = Hol_defn "F"
>  `F (x:real) = if x <= 0 then 0 else x + F(x - 0.5)`;
>
>

The "x.y" syntax is used for record field selection in HOL-4.
I got the example to be accepted by using 1/2 instead
of 0.5:

Hol_defn
   "Fn"
   `Fn (x:real) = if x <= 0 then 0 else x + Fn(x - 1/2)`;


Konrad.


-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Tools and Techniques for Verification of System Infrastructure (Call for posters)

[Konrad Slind]

CALL FOR POSTERS

Tools and Techniques for Verification of System Infrastructure (TTVSI)

   http://www.ttvsi.org/

TTVSI is a meeting organized to honour Professor Michael Gordon, a
longtime leader in the field of formal verification. On the occasion
of Professor Gordon's 60th birthday, a two day workshop has been
organized for March 25-26, 2008, at the Royal Society in London,
England.

Attendees of TTVSI are invited to submit abstracts for posters,
describing research related to the theme of the conference. The
abstracts will be reviewed and accepted abstracts will appear in the
proceedings of TTVSI. Posters will be presented in special sessions
at the meeting.

FORMAT. Poster submissions should be 1 page in length, using LNCS
format. The submission should be an extended abstract summarizing the
poster contents.

Important dates:

   February 1:  submissions open
   February 15: submission deadline
   February 22: acceptance notification
   February 29: revised submissions due

Further details will appear in due course at the conference homepage.


-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Defining two mutually recursive funtions

[Konrad Slind]

On Feb 6, 2008, at 12:54 PM, [EMAIL PROTECTED] wrote:

> I am trying to defining two mutually recursive funtions. I have to
> prove termination.
> HOL has introduced INL and INR defined in the sumTheory. Their
> introduction has caused a problem for me.

Right. Mutually recursive functions are modelled by a single
function over a sum type. Chapter 4 of

   http://www.cs.utah.edu/~slind/papers/phd.ps.gz

spells out the details.

> I tried to apply SUM_ss to
> check if it can help in simplifying, it fails.

Your problem is not with SUM_ss, which is already
incorporated into std_ss, arith_ss, and list_ss. What
you need to do is come up with a termination relation
that operates over the sum type ``:real + real``. For
simplicity, I translated your problem to one over nums
instead, but the idea should transfer.

First, set up the definition and extract termination conditions:

val defn = Hol_defn "fn1fn2"
`(fn1 x = if x = 0 then 1 else fn1 (x-1) + (fn2 (x-1) - fn2  
(x-2))) /\
 (fn2 x = if x = 0 then 1 else fn2 (x-1) + (fn1 (x-1) - fn1  
(x-2)))`;

Then use the sometimes useful function TotalDefn.guessR,
which guesses a standard collection of termination measures.
Some will work, some won't.

TotalDefn.guessR defn;
> val it =
[``inv_image $< (\v. 0)``, ``inv_image $< (sum_size (\x. x)  
(\x. x))``]
: term list

In this case, the second one works: it just measures the size
of the injected argument.

- val [_,R] = it;
 > val R = ``inv_image $< (sum_size (\x. x) (\x. x))`` : term

- Defn.tgoal defn;
 > val it =
 Proof manager status: 1 proof.
 1. Incomplete:
  Initial goal:
  ?R.
WF R /\ (!x. ~(x = 0) ==> R (INL (x - 1)) (INL x)) /\
(!x. ~(x = 0) ==> R (INL (x - 1)) (INR x)) /\
(!x. ~(x = 0) ==> R (INL (x - 2)) (INR x)) /\
(!x. ~(x = 0) ==> R (INR (x - 1)) (INL x)) /\
(!x. ~(x = 0) ==> R (INR (x - 1)) (INR x)) /\
!x. ~(x = 0) ==> R (INR (x - 2)) (INL x)

- e (WF_REL_TAC `^R`);
OK..
 > val it =
 Initial goal proved.
 |- ((fn1 x =
  (if x = 0 then
 1
   else
 fn1 (x - 1) + (fn2 (x - 1) - fn2 (x - 2 /\
 (fn2 x =
  (if x = 0 then
 1
   else
 fn2 (x - 1) + (fn1 (x - 1) - fn1 (x - 2) /\
!P0 P1.
  (!x.
 (~(x = 0) ==> P0 (x - 1)) /\ (~(x = 0) ==> P1 (x - 1)) /\
 (~(x = 0) ==> P1 (x - 2)) ==>
 P0 x) /\
  (!x.
 (~(x = 0) ==> P0 (x - 1)) /\ (~(x = 0) ==> P0 (x - 2)) /\
 (~(x = 0) ==> P1 (x - 1)) ==>
 P1 x) ==>
  (!v0. P0 v0) /\ !v0. P1 v0 : goalstack


Konrad.




> Following is the complete trace with the two erros that I got. I konw
> why I am getting the first error, how can we go around. Why I am
> getting the second error.
>
> val TwoMutalRecursive_defn = Hol_defn "TwoMutalRecursive"
> `(E x:real =
>   if x <= 0 then 1 else
> E (x - 1) + (F(x - 1) - F(x-2)))
> /\
> (F x:real =
>   if x <=  0 then 1 else
> F (x - 1) + (E(x - 1) - E(x-2)))
> `;
> <>
>> val TwoMutalRecursive_defn =
>  HOL function definition (mutual recursion)
>
>  Equation(s) :
>   [...]
>  |- E x = (if x <= 0 then 1 else E (x - 1) + (F (x - 1) - F (x  
> - 2)))
>   [...]
>  |- F x = (if x <= 0 then 1 else F (x - 1) + (E (x - 1) - E (x  
> - 2)))
>
>  Induction :
>   [...]
>  |- !P0 P1.
>   (!x.
>  (~(x <= 0) ==> P0 (x - 1)) /\ (~(x <= 0) ==> P1 (x -  
> 1)) /\
>  (~(x <= 0) ==> P1 (x - 2)) ==>
>  P0 x) /\
>   (!x.
>  (~(x <= 0) ==> P0 (x - 1)) /\ (~(x <= 0) ==> P0 (x -  
> 2)) /\
>  (~(x <= 0) ==> P1 (x - 1)) ==>
>  P1 x) ==>
>   (!v0. P0 v0) /\ !v0. P1 v0
>
>  Termination conditions :
>0. !x. ~(x <= 0) ==> R (INL (x - 1)) (INL x)
>1. !x. ~(x <= 0) ==> R (INL (x - 1)) (INR x)
>2. !x. ~(x <= 0) ==> R (INL (x - 2)) (INR x)
>3. !x. ~(x <= 0) ==> R (INR (x - 1)) (INL x)
>4. !x. ~(x <= 0) ==> R (INR (x - 1)) (INR x)
>5. !x. ~(x <= 0) ==> R (INR (x - 2)) (INL x)
>6. WF R : defn
> - - Defn.tgoal TwoMutalRecursive_defn;
>> val it =
>  Proof manager status: 1 proof.
>  1. Incomplete:
>   Initial goal:
>   ?R.
> WF R /\ (!x. ~(x <= 0) ==> R (INL (x - 1)) (INL x)) /\
> (!x. ~(x <= 0) ==> R (INL (x - 1)) (INR x)) /\
> (!x. ~(x <= 0) ==> R (INL (x - 2)) (INR x)) /\
> (!x. ~(x <= 0) ==> R (INR (x - 1)) (INL x)) /\
> (!x. ~(x <= 0) ==> R (INR (x - 1)) (INR x)) /\
> !x. ~(x <= 0) ==> R (INR (x - 2)) (INL x)
>
>
>   : proofs
> ERROR 1:
> e (WF_REL_TAC  `measure(\x. clg x)`);
> OK..
> Type inference failure: the term
> measure (\(x :real). clg x)
> on line 50, characters 18-35
> which has type
> :real -> real -> bool
> can not b

[Hol-info] TTVSI call for participation, registration, and posters

[Konrad Slind]

CALL FOR PARTICIPATION, REGISTRATION, and POSTERS

Tools and Techniques for Verification of System Infrastructure (TTVSI)

  http://www.ttvsi.org/

  Today's increasingly computer-based society is dependent on the
correctness and reliability of crucial infrastructure, such as
programming languages, compilers, networks, and microprocessors. One
way to achieve the required level of assurance is to use formal
specification and proof, and tool support for this approach has
steadily grown to the point where the specification and verification
of important system infrastructure is now feasible.

  To survey the state of the art and discuss future possibilities and
challenges, we are pleased to announce a two day research meeting, to
be held in honour of Prof. Michael J. C. Gordon FRS on the occasion of
his 60th birthday.

Invited Speakers.
=

The following speakers will present their research at the meeting:

* Michael Gordon, Cambridge University
  Synthesizing Implementations Using a Theorem Prover

* John Harrison, Intel
  Formalizing an Analytic Proof of the Prime Number Theorem

* Sava Krstic, Intel
  Decision Procedures for Parametric Theories

* Xavier Leroy, INRIA
  Micro-architecture Verification, Compiler Verification: What Next?

* Tom Melham, Oxford University
  TBA

* Robin Milner, Cambridge University
  Memories and Reflections: Whose Proofs Need a Machine?

* J Moore, University of Texas at Austin
  Proof Search Debugging Tools in ACL2

* Tobias Nipkow, Technical University of Munich
  Linear Quantifier Elimination

* Michael Norrish, NICTA
  Defining a C++ Semantics

* Larry Paulson, Cambridge University
  Automatic Proof for Theorems On Transcendental Functions

* Larry Paulson, Cambridge University
  Automatic Proof for Theorems On Transcendental Functions

* Peter Sewell, Cambridge University
  Network Protocols: The Terror and the Glory

* Laurent Thery, INRIA
  Proving and Computing: Certifying Large Prime Numbers


Poster Presentations.
=

  Attendees of TTVSI are invited to submit abstracts for posters,
describing research related to the theme of the conference. The
abstracts will be reviewed and accepted abstracts will appear in the
proceedings of TTVSI. Posters will be presented in sessions during the
meeting.

FORMAT. Poster submissions should be 1 page in length, using LNCS
article format. The submission should be an extended abstract
summarizing the poster contents. Please email the submission to
[EMAIL PROTECTED] by the poster abstract deadline. All received
poster abstracts will be acknowledged by email. Instructions on
poster preparation will be sent to authors of accepted abstracts.


Important Dates.


15 February 2008Poster abstract deadline
22 February 2008Notification of poster abstract acceptance/rejection
27 February 2008Early registration deadline
29 February 2008Final version of abstracts due
14 March 2008   Registration deadline
25-26 March 2008TTVSI research meeting

Sponsors.
=

TTVSI is sponsored by the University of Cambridge Computer Laboratory,
Galois, Inc., and Lemma 1, Ltd.


Other Information.
=

To contact the organizers please use the email address [EMAIL PROTECTED]
-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] TTVSI early registration deadline

[Konrad Slind]

[ Early registration deadline is today. ]

Tools and Techniques for Verification of System Infrastructure (TTVSI)

   http://www.ttvsi.org/

   Today's increasingly computer-based society is dependent on the
correctness and reliability of crucial infrastructure, such as
programming languages, compilers, networks, and microprocessors. One
way to achieve the required level of assurance is to use formal
specification and proof, and tool support for this approach has
steadily grown to the point where the specification and verification
of important system infrastructure is now feasible.

   To survey the state of the art and discuss future possibilities and
challenges, we are pleased to announce a two day research meeting, to
be held in honour of Prof. Michael J. C. Gordon FRS on the occasion of
his 60th birthday.

Important Dates.


27 February 2008Early registration deadline
14 March 2008   Registration deadline
25-26 March 2008TTVSI research meeting

Sponsors.
=

TTVSI is sponsored by the University of Cambridge Computer Laboratory,
Galois, Inc., and Lemma 1, Ltd.


Other Information.
=

To contact the organizers please use the email address [EMAIL PROTECTED]




-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] TTVSI registration deadline

[Konrad Slind]

[  Final Registration Deadline is Friday ]

Tools and Techniques for Verification of System Infrastructure (TTVSI)

  http://www.ttvsi.org/

  Today's increasingly computer-based society is dependent on the
correctness and reliability of crucial infrastructure, such as
programming languages, compilers, networks, and microprocessors. One
way to achieve the required level of assurance is to use formal
specification and proof, and tool support for this approach has
steadily grown to the point where the specification and verification
of important system infrastructure is now feasible.

  To survey the state of the art and discuss future possibilities and
challenges, we are pleased to announce a two day research meeting, to
be held in honour of Prof. Michael J. C. Gordon FRS on the occasion of
his 60th birthday.

Important Dates.


14 March 2008   Registration deadline
25-26 March 2008TTVSI research meeting

Sponsors.
=

TTVSI is sponsored by the University of Cambridge Computer Laboratory,
Galois Inc., and Lemma 1, Ltd.


Other Information.
=

To contact the organizers please use the email address [EMAIL PROTECTED]
-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Well-founded relation help

[Konrad Slind]

On Apr 4, 2008, at 9:51 AM, Augusto Ribeiro wrote:

> Dear All,
>
> Sorry for the extensive background if you prefer please go straight
> to the PROBLEM that is a bit below in the mail.
>
> > BACKGROUND <
>
> I'm trying to use HOL to prove termination of recursive functions
> with preconditions in VDM. What I plan to do is generate the
> termination conditions myself by inspecting the VDM source file and
> then trying to prove them in HOL. I know HOL doesn't support sub-
> typing so what I'm doing at the moment is for example:
>
> f(x) = if (x=3) then 3 else f(x-1)
> precondition: x >= 3

One trick for sneaking in subtyping is to define
the function as

   f(x) =
  if x >= 3 then
if x = 3 then 3
else f(x-1)
  else ARB

With that, termination should be proved automatically
by Define. You can subsequently prove

   |-  x >= 3 ==> (f x = if x=3 then 3 else f(x-1))

>
>
> What is inserted into HOL is a goal like this:
>
> - g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`;
>
> The thing if I try to prove this using the command:
>
> e (WF_REL_TAC `measure (\x.x)`)
>
> I am successful because '<' is well founded and the rest of the
> equation is true. But the proof is unsound because inserting the
> '(x>=3)' assumption makes this statement  "~(x=3) /\ (x>=3) ==> R
> (x-1) x" true. This could be solved if I use (\x.x-3) instead of
> '(\x.x)'. But what I'm trying to do is for use of general use so I
> don't want people to incur in the risk of making unsound proofs.

There is no danger of unsoundness using WF_REL_TAC, just
of providing a witness relation that doesn't actually lead to
provable termination conditions.


Konrad.


>
> > PROBLEM <
>
> So what I tried to follow other approach and define the 'measure'
> relation myself, like this:
>
> - g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`;
> - val measure2 = Define `measure2 f x y = if (x>= 3 /\ y >= 3) then f
> x < f y else F`;
> - e (WF_REL_TAC `measure2 (\x.x)`)
> - e (RW_TAC arith_ss [measure2])
>
> And using this tactic all goes alright until I get stuck with:
>> val it =
>  WF (measure2 (\x. x))
>
>   : goalstack
> Although the relation is well founded because it's just a restriction
> of the Naturals. I couldn't prove it until now. Is there a tactic to
> prove this or at least to do some simplification. I couldn't do
> nothing to continue this proof yet. Or maybe there is other ways to
> do this. Thank you for your time and help.
>
> Cheers,
> Augusto Silva
>
>
>
> -- 
> ---
> This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
> Register now and save $200. Hurry, offer ends at 11:59 p.m.,
> Monday, April 7! Use priority code J8TLD2.
> http://ad.doubleclick.net/clk;198757673;13503038;p?http:// 
> java.sun.com/javaone
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


-
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference 
Register now and save $200. Hurry, offer ends at 11:59 p.m., 
Monday, April 7! Use priority code J8TLD2. 
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Infinite rewrite - "if then else" recursive function

[Konrad Slind]

Hi Augusto:

 1. One way to control rewriting is to attach a tag to the
  rewrite rule that will set a limit on how many times it is
  expanded.

  RW_TAC arith_ss [Once half]

 2. You will need to use induction to prove your goal. You can
  use math. induction via

Induct

 but you will then need to do some case-splitting. For this
 proof it is simpler to use the induction coming from the
 definition of "half"

  val half_ind = fetch "-" "half_ind";
  g `!x. x >= half x`;
  e (recInduct half_ind);
  e (REPEAT STRIP_TAC);
  e (RW_TAC arith_ss [Once half]);

Cheers,
Konrad.

On Apr 7, 2008, at 3:57 AM, Augusto Ribeiro wrote:


Dear All,

I'm trying to prove a simple property over a function. This is the  
function:


- val half = Define `half(x) = if x = 0 then 0 else if x = 1 then 0  
else 1 + half(x - 2)`

- g `x >= half x`
- e (RW_TAC arith_ss [half_def]);

And I'm trying to prove this goal with the rewrite tactic. The  
problem is this tactic leads to infinite rewrites. Is there any  
other way to do it or is it impossible to do rewrites in recursive  
functions with "if then else" expression.

Thank you for the attention and help.

Cheers,
Augusto



-- 
---

This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Register now and save $200. Hurry, offer ends at 11:59 p.m.,
Monday, April 7! Use priority code J8TLD2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http:// 
java.sun.com/javaone___

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


-
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference 
Register now and save $200. Hurry, offer ends at 11:59 p.m., 
Monday, April 7! Use priority code J8TLD2. 
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Infinite rewrite - "if then else" recursive function

[Konrad Slind]

If you now want to see how annoying proof with HOL can be, try to
prove

  half (x + 4) = half x + 2

This doesn't need an induction.


Not so annoying: the following works.

   RW_TAC arith_ss [Ntimes half 2]

Konrad.

On Apr 7, 2008, at 8:01 PM, Michael Norrish wrote:

val half = Define `half(x) = if x = 0 then 0 else if x = 1 then 0  
else

1 + half(x - 2)`


-
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference 
Register now and save $200. Hurry, offer ends at 11:59 p.m., 
Monday, April 7! Use priority code J8TLD2. 
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] modules in HOL-Light?

[Konrad Slind]

Hi,

  I have a student wanting to translate Michael Norrish's
DPLL example to HOL-Light. Part of that involves
replacing HOL-4's use of the Binarymap structure
with the appropriate thing in HOL-Light. It seemed
like instantiating OCaml's Map functor was the right
approach, but we weren't able to even define the
appropriate instance of OrderedType needed as
input to Map. Thus

  module OrderedTerm =
  struct
  type t = term
  let compare x y = (Pervasives.compare: term -> term -> int) x y
  end;;

was rejected as being badly formed. However, the only slightly
different

module OrderedInt =
 struct
   type t = int
   let compare x y = (Pervasives.compare:int->int->int) x y
 end;;

was accepted in pure Ocaml. Is there something about
HOL-Light that disallows the above definition of OrderedTerm,
or have I bungled the syntax?

Thanks,
Konrad.

-
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference 
Don't miss this year's exciting event. There's still time to save $100. 
Use priority code J8TL2D2. 
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Nested functions

[Konrad Slind]

> I'm interested in proving termination of nested functions and I  
> have some questions:
>
> 1- First I noticed that HOL is able to prove the termination of  
> this definition
>automatically:
>
>Define `(ack 0 y = 1 + y)
>/\ (ack (SUC u) 0 = ack u (SUC 0))
>/\ (ack (SUC u) (SUC v) = ack u (ack (SUC u) v))`;
>
> I want to know how, because I'm tried to prove it manually using  
> Hol_defn and
> I couldn't.
>

Lexicographic combination of <. If you apply TotalDefn.guessR to the
result of Hol_defn on the above recursion equations, you get the
"guesses" that the automated termination prover makes when trying
to find a suitable termination relation. In the above case, there are
two:

- TotalDefn.guessR defn;
 > val it =
 [``inv_image $< (\(x,y). x + y)``,
  ``inv_image ($< LEX $<) (\(v1,v2). (v1,v2))``] : term list

and the second one works.

> 2 - Although the function above can be proved automatically the  
> following can't:
>
> Define `ack x y = if (x = 0) then (1 + y) else
>   if (y = 0) then (ack (x - 1) 1) else
>   ack (x - 1) (ack x (y - 1))`;
>
> I wanted to know why, and again if it is possible to prove it  
> manually.
>

In recent versions of HOL-4 this is proved automatically.

> 3 - I want to know if it is possible to prove termination of a  
> function like this:
>
> val defn = Hol_defn "nest" `nest x = if x = 0 then 0 else nest  
> (nest x-1)`
>

No. Your recursive call is ((nest x) - 1). You probably meant to
write (nest (x-1)), and when the function is defined that way, it is
possible to show termination.  It's not obvious how to do this, though,
since there is a bit of an involved story. First, the termination  
conditions
that need to be proved are phrased in terms of an auxiliary function
"nest_aux":

   ?R. WF R /\ (!x. ~(x = 0) ==> R (x - 1) x) /\
!x. ~(x = 0) ==> R (nest_aux R (x - 1)) x

The equations and induction theorem for nest_aux can be extracted from
the defn datastructure. They also have to be instantiated to the
desired termination relation (less-than, in this case). Once
instantiated with (<), some of the constraints on the induction
theorem and recursion equations can be eliminated, via Defn.prove_tcs.

   val nest_aux_defn = Defn.set_reln (valOf (Defn.aux_defn defn)) `` 
(<)``;
   val nest_aux_defn' = Defn.prove_tcs nest_aux_defn
  (SIMP_TAC arith_ss [prim_recTheory.WF_LESS]);
   val nest_aux_ind = valOf (Defn.ind_of nest_aux_defn');
   val [E] = Defn.eqns_of nest_aux_defn';

Now the termination proof can most easily be accomplished by proving  
that
nest_aux (<) is the constant 0 function, and this is done by  
induction with
nest_aux_ind':

val nest_aux_thm = Q.prove
(`!n. nest_aux (<) n = 0`,
 recInduct nest_aux_ind' THEN
 REPEAT STRIP_TAC THEN RW_TAC arith_ss [DISCH_ALL E]);

With this theorem in hand, termination is quite simple to prove:

val (nest_def,nest_ind) =
  Defn.tprove
  (defn, WF_REL_TAC `$<` THEN RW_TAC arith_ss [nest_aux_thm]);

which yields the desired recursion equations and induction theorem  
for nest:

val nest_def = |- nest x = (if x = 0 then 0 else nest (nest (x -  
1)))
val nest_ind =
 |- !P. (!x. (~(x = 0) ==> P (nest (x - 1))) /\
 (~(x = 0) ==> P (x - 1)) ==>  P x) ==> !v. P v

There is some detail on this approach in Chapter 4 of

   http://www.cs.utah.edu/~slind/papers/phd.html

Konrad.


-
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference 
Don't miss this year's exciting event. There's still time to save $100. 
Use priority code J8TL2D2. 
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proving equality between 2 recursions

[Konrad Slind]

Hi Ewa,

  When reasoning about recursively defined functions,
you are probably going to have to do an induction,
and also expand out the definition(s) of the functions.

But in the example you have given, it may not even be
necessary to do that. I would separately prove
that function "i" is the identity function for numbers >= 1.
Then the proof just amounts to using the commutativity
of multiplication.

Konrad.

On Aug 31, 2008, at 6:14 PM, Ewa Rom wrote:


Hi all,

I'm trying to prove equality between 2 recursions (2 different way  
of defining a factorial)


So far I have:

let i = define `i n = if n <= 1 then 1 else i ( n - 1 ) + 1`;;
let fac = define `fac n = if n <= 1 then 1 else fac ( n - 1 ) * i n`;;
let fact = define `fact n = if n <= 0 then 1 else n * fact(n - 1)`;;

Then I defined a goldstack:

g `!k. (( i k <= k) /\ 1 <= k) ==> (fac k = fact k)`;;

I used GEN_TAC and STRIP_TAC to get to subgoal:  fac k = fact k

What should be the next step?  Whatever I use gives me 'Exception:  
Failure "linear_ineqs: no contradiction".'
I know the tutorial shows iformation on how to deal with Nonlinear  
reasoning in Chapter 9.2.  I tried the REAL_RING and it failed.   
The other option is to use SOS_RULE, but it requires additional  
module to be loaded.  I want to check if there are any other  
options for me to accomplish this that going with a module, or  
maybe I'm just doing something wrong.


Thank you
Ewa Romanowicz

__
Please visit http://www.EwaRomanowicz.com



-- 
---
This SF.Net email is sponsored by the Moblin Your Move Developer's  
challenge
Build the coolest Linux based applications with Moblin SDK & win  
great prizes
Grand prize is a trip for two to an Open Source event anywhere in  
the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/ 
___

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


-
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How were type variables added to higher order logic?

[Konrad Slind]

  This prompted me to go back and check Andrews'
book "An Introduction to Mathematical Logic and
Type Theory:To Truth Through Proof". In there,
he presents Q_0, which does not have object
language type variables. Variables in the meta
language are used instead. I wonder why he
decided not to use the Q from his thesis ...

Konrad.


On Oct 9, 2008, at 10:03 AM, Tom Melham wrote:

> Rob, Peter:
>
> Peter Andrews' PhD thesis, supervised by Church and published by
> North-Holland in 1965, describes a simple type theory called "Q" that
> definitely includes object-language type variables. In fact Q also  
> includes
> object-language universal quantification over these variables.
>
> Tom
>

-
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Uncaught exception: Chr

[Konrad Slind]

This exception is probably not directly caused by running out of
space. Chr is raised by

Char.chr : int -> char

when applied to an int that doesn't map to a char.

Konrad.

On Oct 14, 2008, at 3:33 AM, Mike Gordon wrote:

>
> Does anyone recognise:
>
> ! Uncaught exception:
> ! Chr
>
> as a symptom of some kind of running out of space?
>
> It arises when rebuilding examples/acl2/ml in newer versions of hol
> (warning: this takes a long time before crashing).
>
> Mike
>
> -- 
> ---
> This SF.Net email is sponsored by the Moblin Your Move Developer's  
> challenge
> Build the coolest Linux based applications with Moblin SDK & win  
> great prizes
> Grand prize is a trip for two to an Open Source event anywhere in  
> the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


-
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proving of "equal" theorems

[Konrad Slind]

Hi Vladimir,

* It could be that types are different in lemma5_8 and
   in your goal. If you try

 MATCH_MP_TAC lemma5_8

and it fails, this is probably the case. Then you
should set

 show_types := true

   and have a look at the types in the goal and the theorem.

  * Try METIS_TAC instead of PROVE_TAC, as it
 can be more effective in some cases.

Konrad.

On Nov 5, 2008, at 3:46 PM, Vladimir Timashov wrote:

> Hello,
>
> I again need your help in some beginner questions.
>
> I have a theorem proved:
>
> - lemma5_8;
> > val it =
>   |- (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) /\
>  ((!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>  
> (access t2 (k + 1) = access t1 (k + 1))) /\
>  ((!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>  
> (access t2 k = access t1 k)) /\
>  access t1 k <= access t1 (k + 1) ==>
>   access t2 k <= access t2 (k + 1) : thm
>
> I need to prove a theorem. After some intermediate transformations  
> I get the following subgoal:
>
>   Current goal:
>   access t2 k <= access t2 (k + 1)
>   
>   0. !k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)
>   1. (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>  
> (access t2 (k + 1) = access t1 (k + 1))
>   2. (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>  
> (access t2 k = access t1 k)
>   3. access t1 k <= access t1 (k + 1)
>
> You can see that even names of variables and order of assumptions  
> are the same for lemma and subgoal. But I was not able to prove  
> this. For example:
> e(PROVE_TAC[lemma5_8]);
>
> fails with "Too deep" exception with 287320 inferences on the 30-th  
> step.
>
> Am I correct that "assumptions" and "goal" is in fact an  
> implication of  conjunctions and goal and my theorems are equal?
>
> So could you please advice how I should prove the theorem using lemma?
>
>
> Thank you.
>
> -- 
>
> Sincerely yours,
>Vladimir Yu. Timashov
> ICQ: 334366950
> -- 
> ---
> This SF.Net email is sponsored by the Moblin Your Move Developer's  
> challenge
> Build the coolest Linux based applications with Moblin SDK & win  
> great prizes
> Grand prize is a trip for two to an Open Source event anywhere in  
> the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/ 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


-
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Question on higher order matching

[Konrad Slind]

Hi Peter,

  Your example is actually a first order matching problem and
the first order matcher fails:

> match_term ``\x:'a. y:'b`` ``\x:num. x + x`` handle e => Raise e;
>
> Exception raised at Term.raw_match_term error:
> variable bound by scope

The higher order matcher should fail but returns an incorrect
substitution.

On the other hand, if you make the problem into a higher order
matching problem by using the pattern ``\x. y x``, then higher
order matching succeeds with a substitution that works, binding
y to ``\x. x+x``

> ho_match_term [] empty_tmset ``\x:'a. y x`` ``\x:num. x + x``  
> handle e => Raise e;
> <>
> > val it =
> ([{redex = ``y``, residue = ``\x. x + x``}],
>  [{redex = ``:'b``, residue = ``:num``},
>   {redex = ``:'a``, residue = ``:num``}])



Konrad.


On Dec 6, 2008, at 11:58 AM, Peter Vincent Homeier wrote:

> Is the following behavior of Kananaskis-5 correct?
>
> -
>HOL-4 [Kananaskis 5 (built Fri Nov 28 13:45:15 2008)]
>
>For introductory HOL help, type: help "hol";
> -
>
> [loading theories and proof tools ** ]
> [closing file "/usr/local/hol/kananaskis-5/tools/end-init-boss.sml"]
> - show_types := true;
> > val it = () : unit
> - val (tmins,tyins) = ho_match_term [] empty_tmset ``\x:'a. y:'b``  
> ``\x:num. x + x``;
> > val tmins = [{redex = ``(y :num)``, residue = ``(x :num) + x``}] :
>   {redex : term, residue : term} list
>   val tyins =
> [{redex = ``:'b``, residue = ``:num``},
>  {redex = ``:'a``, residue = ``:num``}] :
>   {redex : hol_type, residue : hol_type} list
> - subst tmins (inst tyins ``\x:'a. y:'b``);
> > val it = ``\(x' :num). (x :num) + x`` : term
> - aconv it ``\x:num. x + x``;
> > val it = false : bool
> -
>
> It seems unreasonable that these two terms should match, since then  
> the instantiation of the pattern term (as shown above using the  
> results of the higher order match) does not in fact produce the  
> target term.  Isn't that the point of matching, to arrive at a  
> substitution that makes the pattern into the target?
>
> Peter
>
>
> -- 
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
> -- 
> 
> SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas,  
> Nevada.
> The future of the web can't happen without you.  Join us at MIX09  
> to help
> pave the way to the Next Web now. Learn more and register at
> http://ad.doubleclick.net/clk;208669438;13503038;i?http:// 
> 2009.visitmix.com/___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas, Nevada.
The future of the web can't happen without you.  Join us at MIX09 to help
pave the way to the Next Web now. Learn more and register at
http://ad.doubleclick.net/clk;208669438;13503038;i?http://2009.visitmix.com/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] FOLD and SETSUM

[Konrad Slind]

Hi Naeem,

1. "op" is not the keyword to use. Instead, use either
 the "dollar" notation (thus, "$+" or "arithmetic$+"), or the
 "paren" notation "(+)", which is also supported.

2. FOLD on sets is already defined: it is called ITSET.
   See the Description (page 102) for a short description.

3. Your SETSUM is a simple instance of SUM_IMAGE,
   which is also defined in pred_set.

Cheers,
Konrad.


On Dec 7, 2008, at 1:54 PM, [EMAIL PROTECTED] wrote:

> Hello,
>
> I am trying to define a function named SETSUM which uses another
> function FOLD:
> (FOLD)
> - val FOLD_defn = Defn.Hol_defn
>   "FOLD"
>  `FOLD (f:'a->'a->'a) (g:'b->'a) (z:'a)  
> (A:'a->bool) =
> if FINITE A then if A={} then z else FOLD f g (CHOICE A) (REST A)  
> else ARB`;
>> val FOLD_defn =
>  HOL function definition (recursive)
>
>  Equation(s) :
>   [..]
>  |- FOLD f g z A =
> (if FINITE A then
>(if A = {} then z else FOLD f g (CHOICE A) (REST A))
>  else
>ARB)
>
>  Induction :
>   [..]
>  |- !P.
>   (!f g z A.
>  (FINITE A /\ ~(A = {}) ==> P f g (CHOICE A) (REST A)) ==>
>  P f g z A) ==>
>   !v v1 v2 v3. P v v1 v2 v3
>
>  Termination conditions :
>0. !z g f A.
> FINITE A /\ ~(A = {}) ==> R (f,g,CHOICE A,REST A)  
> (f,g,z,A)
>1. WF R : defn
>
> The definition of setsum is as follows:
>
> val SETSUM_defn = Defn.Hol_defn
> "SETSUM"
>  `SETSUM (f:'b->real) (A:real->bool) = if FINITE A
> then FOLD (op +) f 0 A else 0`;
>
> on line 16, characters 82-85:
> No rule for [+]
>
> Exception raised at Parse.Absyn:
> at line 16, character 88:
> Parse failed
> ! Uncaught exception:
> ! HOL_ERR
> -
>
>
>
> I am not sure why I am getting this error message, Am I using "op"
> correctly, can some please help?
>
> Naeem
>
>
> -- 
> 
> SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas,  
> Nevada.
> The future of the web can't happen without you.  Join us at MIX09  
> to help
> pave the way to the Next Web now. Learn more and register at
> http://ad.doubleclick.net/clk;208669438;13503038;i?http:// 
> 2009.visitmix.com/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas, Nevada.
The future of the web can't happen without you.  Join us at MIX09 to help
pave the way to the Next Web now. Learn more and register at
http://ad.doubleclick.net/clk;208669438;13503038;i?http://2009.visitmix.com/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] convert HOL formula to latex

[Konrad Slind]

Hi Lu,

   See the interface at /src/emit/EmitTeX.sig.
This allows tex to be generated from HOL terms, definitions,
theorems and theories. Snippet:

 val print_term_as_tex : term -> unit
 val print_type_as_tex : hol_type -> unit
 val print_theorem_as_tex  : thm -> unit
 val print_theory_as_tex   : string -> unit
 val print_theories_as_tex_doc : string list -> string -> unit
 val tex_theory: string -> unit

You will need the .sty files from thatdirectory (holtex.sty and
holtexbasic.sty). I am not sure if there is more extensive
documentation available yet, but the above is pretty simple
to use.

Konrad.



On Jan 4, 2009, at 4:30 AM, Lu Zhao wrote:

> Hi,
>
> I'd like to put some HOL theorems in a paper that is written in latex.
> Is there an easy way to format HOL formulas nicely in latex?
>
> Thanks.
> Lu
>
> -- 
> 
> ___
> 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] Compress HOL message for match_term

[Konrad Slind]

Hi Lu,

   That message comes from the parser, when
unconstrained type variables remain after
type inference. So it seems that you are making
an invocation

match_term `` ...``   `` ... ``;

where one or both of the terms involved are
being parsed. If you don't want to see any
messages you can do

Globals.notify_on_tyvar_guess := false;

If you want finer control, you'll have to make
the invocation of the parser as part of a
function call, e.g.

Lib.with_flag
(Globals.notify_on_tyvar_guess,false)
(fn () => match_term ``foo x`` ``FACT 3``)
();

(This isn't the most transparent example, alas.)

Konrad.



On May 27, 2009, at 6:05 PM, Lu Zhao wrote:

> Hi,
>
> When I use match_term with some types unspecified, HOL always  
> generates
> a message similar to the following:
>
> <>
>
> Is there a way to depress the message so that I don't have to see a  
> long
> list of messages. Specifying the types is not a good option since the
> matched terms have multiple types at the same sub-term position.
>
> Thanks a lot.
> Lu
>
> -- 
> 
> Register Now for Creativity and Technology (CaT), June 3rd, NYC. CaT
> is a gathering of tech-side developers & brand creativity  
> professionals. Meet
> the minds behind Google Creative Lab, Visual Complexity, Processing, &
> iPhoneDevCamp as they present alongside digital heavyweights like  
> Barbarian
> Group, R/GA, & Big Spaceship. http://p.sf.net/sfu/creativitycat-com
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Register Now for Creativity and Technology (CaT), June 3rd, NYC. CaT 
is a gathering of tech-side developers & brand creativity professionals. Meet
the minds behind Google Creative Lab, Visual Complexity, Processing, & 
iPhoneDevCamp as they present alongside digital heavyweights like Barbarian 
Group, R/GA, & Big Spaceship. http://p.sf.net/sfu/creativitycat-com 
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] efficient way to prove concrete sets disjoint?

[Konrad Slind]

Hi Lu,

   If I do the following  (MoscowML based HOL),

 - app load ["wordsLib","pred_setLib"];
 - g `DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
 {a | a >= 0x0w /\ a < 0x1000w}`;
 - time e
 (RW_TAC (srw_ss()) [pred_setTheory.DISJOINT_DEF,  
pred_setTheory.EXTENSION]
  THEN wordsLib.WORD_DECIDE_TAC);

the result comes back in about 3.5 seconds on my ancient laptop:

 OK..
 runtime: 3.548s,gctime: 0.378s, systime: 0.457s.
 > val it =
 Initial goal proved.
 |- DISJOINT {a | a >= 4096w /\ a < 8192w} {a | a >= 0w /\ a  
< 4096w} :

The only difference with what you are trying is the (superfluous)  
Cases_on,
and also the use of srw_ss, which knows basic simplifications for the
"current context: which in this case includes sets and set  
comprehensions.

Konrad.



On Aug 7, 2009, at 10:11 PM, Lu Zhao wrote:

> Hi,
>
> I'd like to prove two sets disjoint. Currently, I use
> DISJOINT_DEF,INTER_DEF,EXTENSION to rewrite the goal first, then
> Cases_on each bound, and finally use WORD_DECIDE_TAC. This approach
> works, but it takes a long time.
>
> For example, it takes over 40s to prove the following theorem:
>
> DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
>{a | a >= 0x0w /\ a < 0x1000w}
>
> I can't image how long it takes if each set has multiple segments. Is
> there any efficient way to prove two sets are disjoint?
>
> Thanks a lot.
> Lu
>
> -- 
> 
> Let Crystal Reports handle the reporting - Free Crystal Reports  
> 2008 30-Day
> trial. Simplify your report design, integration and deployment -  
> and focus on
> what you do best, core application coding. Discover what's new with
> Crystal Reports now.  http://p.sf.net/sfu/bobj-july
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] specify an out-of-order universally quantified variables?

[Konrad Slind]

Hi Lu,

   This is easy to code up in HOL. You can strip
the leading foralls, use INST to replace your variable
by a term and then put all the foralls back, except
for the replaced one:

fun MY_SPEC v tm th =
  let val (vs,body) = strip_forall(concl th)
  val (_,vs') = Lib.pluck (equal v) vs
  in
 GENL vs' (INST [v |-> tm] (SPEC_ALL th))
  end;

Example:

- val th = mk_thm([],``!(x1:num) (x2:'a) (x3:bool list). P x1 x2 x3  
x3``);
 > val th = |- !x1 x2 x3. P x1 x2 x3 x3 : thm

- MY_SPEC ``x2:'a`` ``foo:'a`` th;
 > val it = |- !x1 x3. P x1 foo x3 x3 : thm

You will have to take care that v and tm have the same
type.

Cheers,
Konrad.

On Sep 11, 2009, at 12:15 PM, Lu Zhao wrote:

> Hi,
>
> I have a theorem of the form:
>
> !x1 x2 ... x(i-1) xi x(i+1) ... xn. t
>
> and I'd like to instantiate xi to another term, say y, without  
> touching
> other universally quantified variables, namely, I want to rewrite  
> it to:
>
> !x1 x2 ... x(i-1) x(i+1) ... xn. t[y/xi]
>
> Is there a handy operation for this, any version of SPECL, or I can
> change the order of xs?
>
> Thanks a lot.
> Lu
>
> -- 
> 
> Let Crystal Reports handle the reporting - Free Crystal Reports  
> 2008 30-Day
> trial. Simplify your report design, integration and deployment -  
> and focus on
> what you do best, core application coding. Discover what's new with
> Crystal Reports now.  http://p.sf.net/sfu/bobj-july
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] loading a huge definition in HOL

[Konrad Slind]

Hi Behzad,

   A 6000 line term is probably making the parser and/or
type inferencer work very hard. It might be better to
build the term using term constructors such as
mk_neg, mk_conj, mk_disj, mk_exists, etc.

Cheers,
Konrad.

On Sep 16, 2009, at 6:56 PM, Behzad Akbarpour wrote:

> Hi everyone;
>
> I have a huge definition of an RTL design function (more that 6000  
> lines of
> HOL code), and I'm trying to load and compile it in HOL, but I  
> couldn't
> succeed. I first tried to copy and paste from emacs but it didn't  
> work.
> Then, I made a script file out of the definition together with the  
> related
> theories but Holmake didn't generate the theory file at the end after
> taking lots of time. I even tried Magnus and Michael's script for
> interaction with HOL via emacs/xemacs using C-space and M-h M-r  
> keys, but
> it didn't work either. Do you have any idea how to solve this problem?
>
> Thanks,
>
> Behzad
>
>
> -- 
> 
> Come build with us! The BlackBerry® Developer Conference in SF, CA
> is the only developer event you need to attend this year. Jumpstart  
> your
> developing skills, take BlackBerry mobile applications to market  
> and stay
> ahead of the curve. Join us from November 9-12, 2009. Register  
> now!
> http://p.sf.net/sfu/devconf
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Come build with us! The BlackBerry® Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay 
ahead of the curve. Join us from November 9-12, 2009. Register now!
http://p.sf.net/sfu/devconf
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] the different between with type and datatype in HOL4

[Konrad Slind]

Hi Amy,

   Matrices are an interesting modelling example, since there are  
several
viable approaches.  For extreme simplicity, I would use functions of  
type

  num -> num -> 'a

to represent them. That makes many of the basic operations quite easy.
You will also need to include the rows and columns. This leads to the
idea of having a record hold the rows, columns, and indexing function:

   Hol_datatype
 `matrix = <| rows:num; cols:num; index:num->num->'a |>`;

To then define an operation like matrix multiplication, you need a  
summation
function:

   val Sigma_def =
 tDefine
  "Sigma"
   `Sigma lo hi f =
   if lo > hi then 0 else f(lo) + Sigma (lo+1) hi f`
 (WF_REL_TAC `measure (\(lo,hi,f). (hi+1) - lo)`);

WIth that you can define the finite product of two vectors:

   val vprod_def =
 Define
`vprod v1 v2 k = Sigma 0 (k-1) (\i. v1(i) * v2(i))`;

And then the matrix product is

   val matrix_prod_def =
 Define
   `matrix_prod (M1:num matrix) (M2:num matrix) =
  <|rows := M1.rows ;
cols := M2.cols ;
index := \r c. vprod (M1.index r) (\r. M2.index r c)  
M1.cols |>`;

It also helps for testing to have something that makes a matrix from a
list of lists:

   Define
  `fromLists lists =
 <| rows := LENGTH lists;
cols := LENGTH (HD lists);
index := \r c. EL c (EL r lists) |>`;

A test:

   val matA_def =
 Define
  `matA = fromLists [[1;2;3;4]; [2;3;5;7]; [9;8;7;2]]`;

val matB_def =
 Define
  `matB = fromLists [[1;2]; [5;7]; [8;7]; [11;3]]`;

EVAL ``(matrix_prod matA matB).index 1 1``;  (* Should be 81 *)

Then you of course have to prove some theorems about the product.
An obvious one would be associativity. Note that you have to constrain
the matrices appropriately.

 (A.cols = B.rows) /\ (B.cols = C.rows)
 ==>
 ( matrix_prod A (matrix_prod B C) = matrix_prod (matrix_prod A B) C

I haven't tried this proof, so there may be lurking problems with the  
above
formulation. But the general idea should be clear. I would be keen to  
hear
of other formalizations of matrices, since, as I mentioned, there are  
multiple
ways to skin this cat.

For example, another approach would be to use a list of equal-length  
lists
to represent the matrix, but my experience with that approach was  
kind of
negative: I got bogged down in relatively horrible inductions to prove
even simple theorems.

Cheers,
Konrad.



On Apr 11, 2010, at 9:42 AM, anythingroom wrote:

> Hi everyone，
>
>
>
> Who know the different between with type and datatype in HOL4? I  
> wanted to define a new type for matrix in HOL4, but I might be  
> confusing type with datatype. I didn’t know how to start to define  
> the type of matrix.
>
>
>
> Who can help me ? Thank you very much. I’m looking for your reply.
>
>
>
> Best wishes,
>
> Amy
>
>
>
> -- 
> 
> Download Intel® Parallel Studio Eval
> Try the new software tools for yourself. Speed compiling, find bugs
> proactively, and fine-tune applications for parallel performance.
> See why Intel Parallel Studio got high marks during beta.
> http://p.sf.net/sfu/intel-sw- 
> dev___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Fwd: Rockwell Collins Automated Analysis

[Konrad Slind]

Begin forwarded message:


From: Rita Gatto 
Date: April 23, 2010 6:33:07 PM CDT
To: sl...@cs.utah.edu
Subject: Rockwell Collins Automated Analysis

Hello Konrad

Once again, RC is expanding and has an opening under Matt Wilding  
in the Automated Analysis group. Rockwell Collins is pursuing a  
long-term research and development program for formal methods and  
automated reasoning. Much of this work is done in the automated  
analysis group in Rockwell Collins� R&D center, the Advanced  
Technology Center. The center�s mix of research and application  
projects encourages creative solutions of real-world problems. The  
work of the automated analysis group supports Rockwell Collins�  
wide range of high-assurance safety and security critical product  
developments.


I have included the description below, and am starting to network  
and get the word out about the opening. If you know of an  
individual that would be interested and qualified, or be interested  
yourself, please apply online at www.rockwellcollins.com. I hope  
all is well and look forward to hearing from you.


All the best,

Rita Gatto

Sourcing Specialist

Rockwell Collins

rmga...@rockwellcollins.com

714-929-3980

VPN 829-3980

Sr Systems Engineer- AUT000Y

The Rockwell Collins Advanced Technology Center (ATC) seeks a self  
motivated Senior Systems Engineer with experience in advanced  
research and development in the area of high assurance computing.   
This position is in the Automated Analysis group, which develops  
and applies techniques that improve the safety, security,  
reliability, correctness, ease of development, verification, and  
certification of computer-based systems.  Recent investigations  
include applying automated theorem provers to critical computer- 
based systems, developing a domain specific language for cross  
domain guard systems, applying model checking to debug flight- 
critical software, modeling computer-based avionics system  
architectures, using automated analysis to improve aircraft network  
design, and developing software architectures for next-generation  
avionics.


The successful candidate will have significant experience with  
formal specification languages or automated reasoning tools and  
will have used mathematics-based analysis to develop or verify  
computer-based systems.  Developing or extending model checkers/ 
automated theorem provers (e.g. NuSMV, SAL, Prover, PVS, ACL2, HOL,  
Coq) or experience applying these tools to meet demanding  
development, verification, or certification requirements is highly  
desirable.The successful candidate will have strong fundamental  
software or hardware development skills, and system engineering and  
full product cycle development experience is highly desirable.  The  
ideal candidate has experience in relevant certification standards  
such as DO-178B or the Common Criteria.  The ideal candidate has  
experience in one or more of Rockwell Collins' diverse product  
domains, such as aircraft avionics, cryptographic systems, multiple  
security domain communication systems, information assurance  
products, and computer networking.


This position offers career growth potential for individuals who  
are innovative and can conceive, develop and execute research  
projects.  Demonstrated ability to formulate, market, and lead a  
successful research program is highly desirable.  A graduate degree  
is desirable, especially if it involved the development and  
execution of a research project.


Bachelor's Degree in applicable engineering or science field, and  
six years of related experience, or, in the absence of a bachelor's  
degree, twelve years of related experience.


Applicant must be capable of obtaining a US Department of Defense  
(DoD) security clearance. US Citizenship is required.


Rockwell Collins is an equal opportunity employer committed to  
building a diverse global culture that values teamwork, integrity,  
innovation, leadership, and an unwavering commitment to our customers.







Rita Gatto
620 Newport Center Dr. #1100-MB
Newport Beach, CA


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

Re: [Hol-info] how to use hol4

[Konrad Slind]

Hi Xiaoyu,

  There's a "quick-start" document at

 http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf

and the HOL4 release has extensive documentation
in the Manual directory.

Konrad.

On Jun 18, 2010, at 12:57 AM, xiaoyu xu wrote:


Dear everyone,
I have installed ML and HOL4 in windows. How can I prove theorems?  
I am a new user of HOL4.
I have also installed ML HOL4 proofgeneral GNU emacs in Linux  
system Fedora. I can't find "proofgeneral"in menu.

"
Each face (Emacs terminology) is controlled by its own  
customization setting. You can display a list of all of them using  
the customize menu:


Proof General -> Advanced -> Customize -> Faces -> Proof Faces.
"
I have modified "proof-site.el" , omit the ";;"before hol4, which  
makes hol4 function enable.
What is wrong with my operation? Please help me! Looking forward to  
your reply.

yours
xiaoyu
-- 


ThinkGeek and WIRED's GeekDad team up for the Ultimate
GeekDad Father's Day Giveaway. ONE MASSIVE PRIZE to the
lucky parental unit.  See the prize list and enter to win:
http://p.sf.net/sfu/thinkgeek- 
promo___

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


--
ThinkGeek and WIRED's GeekDad team up for the Ultimate 
GeekDad Father's Day Giveaway. ONE MASSIVE PRIZE to the 
lucky parental unit.  See the prize list and enter to win: 
http://p.sf.net/sfu/thinkgeek-promo___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Call for participation (Trusted Extensions of ITPs)

[Konrad Slind]

Hello --

We will be hosting a workshop on the topic of trust-preserving
extensions of interactive theorem provers:

   Trusted Extensions of Interactive Theorem Provers
   Cambridge, UK
   August 11-12, 2010

For a fuller description, including speakers, please see the web page:

  http://www.cs.utexas.edu/users/kaufmann/itp-trusted-extensions-aug-2010/

There is no registration fee. If you are interested in attending,
please send an email to

  konrad.sl...@gmail.com

so that we can plan for numbers.


Regards,
Matt Kaufmann and Konrad Slind (co-organizers)
Mike Gordon (local arrangements)
--
This SF.net email is sponsored by Sprint
What will you do first with EVO, the first 4G phone?
Visit sprint.com/first -- http://p.sf.net/sfu/sprint-com-first___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [Hol-developers] Hol example: Simple, functional, sound and complete parsing for all context-free grammars

[Konrad Slind]

Hi Tom,

  That would be fine. If you feel a need to mention untidy proofs,
just add a mention in the README file. For lemmas, they
can sometimes just be put in auxiliary files that the xScript.sml
file depends on. I'm not sure if that's what you are asking ...

Konrad.



On Tue, Apr 26, 2011 at 11:20 AM, Tom Ridge <
tom.j.ridge+hol-develop...@googlemail.com> wrote:

> Dear hol-info/hol-developers,
>
> Some readers may be interested in an application of Hol to verify the
> correctness of a parser generator for all context-free grammars:
>
> http://www.cs.le.ac.uk/people/tr61/parsing/
>
> (hol-developers only) I'd like to put the proof development in the Hol
> SVN as an example, but I don't want to "tidy" the proofs. Would people
> mind if I did this? Also, I have collected many lemmas that I would
> like to include in the relevant Hol script files, but again I don't
> want to "tidy" the proofs. Is there a way to do this cleanly?
>
> Thanks in advance
>
> Tom
>
>
> --
> WhatsUp Gold - Download Free Network Management Software
> The most intuitive, comprehensive, and cost-effective network
> management toolset available today.  Delivers lowest initial
> acquisition cost and overall TCO of any competing solution.
> http://p.sf.net/sfu/whatsupgold-sd
> ___
> Hol-developers mailing list
> hol-develop...@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-developers
>
--
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Back to HOL again!

[Konrad Slind]

On Wed, Sep 28, 2011 at 11:11 PM, Paul Loewenstein  wrote:
>
> I'm back on HOL after more than a decade-long hiatus.  How it's improved!

Lots more automation than back in the day. Also lots more theories and
examples.

Konrad.

--
All of the data generated in your IT infrastructure is seriously valuable.
Why? It contains a definitive record of application performance, security
threats, fraudulent activity, and more. Splunk takes this data and makes
sense of it. IT sense. And common sense.
http://p.sf.net/sfu/splunk-d2dcopy2
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] congruence theorems for partial higher-order functions

[Konrad Slind]

Short answer: totalize MAP2 and you can prove the desired congruence without
mentioning LENGTH.

Long answer : you can prove the congruence without the

   LENGTH l1 = LENGTH l2

clause for a definition of MAP2 that is explicit about what happens when one
of the lists is empty and the other is not. Since the version of MAP2
in listTheory
has strictly less information than that, it can be patched together
from the more
detailed definition. And so any subsequent proofs using MAP2 will
still go through.

  I suggest defining in listTheory the equivalent of

val MAP2_DEF =
  Define
 `(MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2) /\
  (MAP2 f x y = [])`;

and then proving the current equations for MAP2:

  store_thm ("MAP2",
   ``(!f. MAP2 f [] [] = []) /\
  (!f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2)``,
METIS_TAC[MAP2_DEF]);

Then prove the congruence for MAP2, by using the induction theorem for MAP2_DEF,
or just plain list induction.

Cheers,
Konrad.





On Thu, Mar 29, 2012 at 7:02 PM, Ramana Kumar  wrote:
> Is it possible to get good termination condition extraction for functions
> like listTheory$MAP2?
> I can prove something like this:
>     |- ∀l1 l1' l2 l2' f f'.
>  (l1 = l1') ∧ (l2 = l2') ∧ (LENGTH l1 = LENGTH l2) ∧
>  (∀x y. MEM x l1' ∧ MEM y l2' ⇒ (f x y = f' x y)) ⇒
>  (MAP2 f l1 l2 = MAP2 f' l1' l2')
> But it's probably of the wrong form (because of the condition about the
> lengths being equal), and indeed adding it to the database in DefnBase
> doesn't help with termination condition extraction for uses of MAP2.
> Without a condition like that, though, I think the congruence is unprovable.
> Is there a right form?
>
> --
> This SF email is sponsosred by:
> Try Windows Azure free for 90 days Click Here
> http://p.sf.net/sfu/sfd2d-msazure
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here 
http://p.sf.net/sfu/sfd2d-msazure
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Announcement: Prooftoys visual proof assistant for higher-order logic

[Konrad Slind]

You can also check out

   src/bool/boolScript.sml

in the HOL4 distribution where quite a few theorems are proved
about the connectives and quantifiers. Those are forward proofs
since tactics don't yet exist at that stage of system build. So they
should be easy to adapt to your framework. One example:

(* - *)
(* Skolemization:|- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x)*)
(* - *)


val SKOLEM_THM = save_thm("SKOLEM_THM",
 let val P = Term`P:'a -> 'b -> bool`
 val x = Term`x:'a`
 val y = Term`y:'b`
 val f = Term`f:'a->'b`
 val tm1 = Term`!x. ?y. ^P x y`
 val tm2 = Term `?f. !x. ^P x (f x)`
 val tm4 = Term`\x. @y. ^P x y`
 val tm5 = Term`(\x. @y. ^P x y) x`
 val th1 = ASSUME tm1
 val th2 = ASSUME tm2
 val th3 = SPEC x th1
 val th4 = INST_TYPE [alpha |-> beta] SELECT_AX
 val th5 = SPEC y (SPEC (Term`\y. ^P x y`) th4)
 val th6 = BETA_CONV (fst(dest_imp(concl th5)))
 val th7 = BETA_CONV (snd(dest_imp(concl th5)))
 val th8 = MK_COMB (MK_COMB (REFL (Term`$==>`),th6),th7)
 val th9 = EQ_MP th8 th5
 val th10 = MP th9 (ASSUME(fst(dest_imp(concl th9
 val th11 = CHOOSE (y,th3) th10
 val th12 = SYM (BETA_CONV tm5)
 val th13 = SUBST [Term`v:'b` |-> th12] (Term`^P x v`) th11
 val th14 = DISCH tm1 (EXISTS (tm2,tm4) (GEN x th13))
 val th15 = ASSUME (Term`!x. ^P x (f x)`)
 val th16 = SPEC x th15
 val th17 = GEN x (EXISTS(Term`?y. ^P x y`,Term`f (x:'a):'b`) th16)
 val th18 = DISCH tm2 (CHOOSE (f,th2) th17)
 val th19 = MP (MP (SPEC tm1 (SPEC tm2 IMP_ANTISYM_AX)) th18) th14
 in
 GEN P (SYM th19)
 end);

Konrad.


On Tue, Apr 24, 2012 at 1:26 AM, Ramana Kumar  wrote:
> You might want to consider implementing import/export of OpenTheory proofs
> (http://www.gilith.com/research/opentheory/) to get access to some larger
> existing proofs. It would be interesting to see how they would look in the
> web interface.
>
> On Mon, Apr 23, 2012 at 3:32 AM, Cris Perdue  wrote:
>>
>> I would like to announce the Prooftoys visual proof assistant, a work in
>> progress, and invite experimental use of it, available at
>> http://prooftoys.org/.
>>
>> The Prooftoys logic is very close to Peter Andrews' Q0, including
>> essentially the same axioms and the same single fundamental rule of
>> inference, Rule R, which allows replacement of a term by an equal term. The
>> implementation builds up numerous derived rules of inference, which are
>> available in the same way as theorems and the primitive rule of inference
>> through the web-based user interface.
>>
>> Prooftoys and its user interface normally run entirely within the user's
>> web browser for interactivity and immediate access. It includes an
>> interactive proof editor, with ability to save and restore proofs to textual
>> format. It supports inference in the style of natural deduction, using
>> hypotheses.
>>
>> The system aims to make higher-order logic more accessible conceptually
>> and easier to use as a tool, bringing more people to understand and use it.
>>
>> The implementation is very much a work in progress in all dimensions, but
>> has been working well for experimental interactive use. It has a set of
>> axioms for real numbers and some rather primitive derived rules of inference
>> so it is possible to experiment with real numbers.
>>
>> More information is available on the Prooftoys web site.
>>
>> Best regards,
>> Cris Perdue
>>
>>
>>
>> --
>> For Developers, A Lot Can Happen In A Second.
>> Boundary is the first to Know...and Tell You.
>> Monitor Your Applications in Ultra-Fine Resolution. Try it FREE!
>> http://p.sf.net/sfu/Boundary-d2dvs2
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
> --
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com

Re: [Hol-info] [HOL] TypeBasePure.gen_datatype_info undocumented (#65)

[Konrad Slind]

Note that Datatype.build_tyinfos is only guaranteed to work on
types that Hol_datatype produces. Does your datatype have
some other features? In any case, what happens with
gen_datatype_info?

Thanks,
Konrad.


On Wed, Jun 6, 2012 at 12:33 PM, Ramana Kumar  wrote:
> Dear Konrad,
> Thanks a lot for your reply.
> I'm going to take this discussion onto the mailing list rather than the
> issue tracker.
> Further comments and questions below.
>
> On Wed, Jun 6, 2012 at 6:09 PM, Konrad Slind
> 
> wrote:
>>
>> Right, that's exactly the situation that should be documented. You
>> want to use
>>
>>  TypeBase.write
>>     [TypeBasePure.mk_datatype_info {...}];
>>
>> which creates the required tyinfo datastructure and installs it into
>> theTypeBase, which is the collection of useful type information used
>> by a variety of tools. There's a simple version of this invocation
>> at the end of
>>
>>   src/sum/sumScript.sml
>>
>> There is something wrong with it, which I will discuss later. But first,
>> let's
>> go through the supplied fields in the record.
>>
>>     ax=TypeBasePure.ORIG sum_Axiom,
>>
>> This is the prim.rec. axiom characterizing the datatype, in the format
>> determined by the datatype package. The "TypeBasePure.ORIG"
>> constructor is needed because each type  in a mutually recursive type
>> declaration will end up having the same axiom, and I didn't want to
>> barf out the same redundant info when printing out tyinfo information
>> when TypeBase.elts() is invoked. When dealing with a non-mutually
>> recursive type, just use TypeBasePure.ORIG . If the type
>> is mutually recursive, you have to write each type separately; for
>> all but the first type, use TypeBasePure.COPY((thy,ty),axiom).
>>
>>      case_def=sum_case_def,
>>
>> Definition of the case construct for the type.
>>
>>      case_cong=sum_case_cong,
>>
>> Case cong theorem for the type.
>>
>>      induction=TypeBasePure.ORIG sum_INDUCT,
>>
>> Induction theorem for the type. See discussion on ORIG and COPY
>> above.
>>
>>      nchotomy=sum_CASES,
>>
>> Cases theorem for the type.
>>
>>      size=NONE,
>>
>> Definition of a size function for the type. This is used when synthesizing
>> termination measures used by Define's termination prover. In the case
>> of sums, size=NONE because of a bootstrapping issue: numbers haven't
>> been defined at this point in the system build, so I fill in the field
>> with NONE,
>> and replace it later (see src/num/theories/basicSize.sml).
>>
>>      encode=NONE,
>>
>> The encode field is a vestigal remainder from some work I did with Joe
>> Hurd on
>> automatic generation and application of serializers for datatypes. Safe to
>> leave
>> it as NONE.
>>
>>      fields=[], accessors=[], updates=[],
>>
>> These are needed for record types. The way to figure out what they do is
>> to
>> defined some simple record type "foo" then invoke
>>
>>  TypeBase.fields_of ``:foo``;
>>  TypeBase.accessors_of ``:foo``;
>>  TypeBase.updates_of ``:foo``;
>>
>>      recognizers = [ISL,ISR],
>>      destructors = [OUTL,OUTR],
>>
>> We allow destructors and recognizers to be defined over
>> datatypes. I use this feature in Guardol, but if you aren't
>> going to do that for your application, you can leave the
>> lists empty.
>>
>>      lift=SOME(mk_var("sumSyntax.lift_sum",
>>                       Parse.Type`:'type -> ('a -> 'term) ->
>>                                            ('b -> 'term) ->
>> ('a,'b)sum -> 'term`)),
>>
>> lift is another vestigial field left over from the encoding experiment.
>> Actually, it is used to automate the extraction of HOL terms from
>> the results of ML evaluation. Unused at the moment.
>>
>>      one_one=SOME INR_INL_11,
>>      distinct=SOME sum_distinct
>>
>> You know what these are.
>>
>> Now, returning to what's wrogn with this: it occurs at the end of
>> sumScript.sml,
>> so a tyinfo for sum is duly made and installed in the TypeBase. However,
>> then
>> evaluation of sumScript terminates and the sum tyinfo is thrown away.
>> So it seems
>> un-needed. However, the
>>
>> val _ = adjoin_to_theory
>> {sig_ps = NONE,
>>  struct_ps = SOME(fn ppstrm =>
>>   let val S = PP.add_string ppstrm
>>   

Re: [Hol-info] [HOL] TypeBasePure.gen_datatype_info undocumented (#65)

[Konrad Slind]

Sounds like a bug. Can you send me sources?

Thanks,
Konrad.


On Wed, Jun 6, 2012 at 1:30 PM, Ramana Kumar  wrote:
> On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind  wrote:
>>
>> Note that Datatype.build_tyinfos is only guaranteed to work on
>> types that Hol_datatype produces. Does your datatype have
>> some other features?
>
>
> Yes, recursion through the range of a finite map.
>
> It wasn't _too_ difficult to prove what look like the right theorems
> manually, but it will be a pain if the type base still can't do anything
> even with those theorems.
> If it does work, though, I might look later into how to generalise this code
> to allow more datatypes with this kind of recursion to be defined (I've only
> done it for a specific datatype that I need).
>
>>
>> In any case, what happens with
>> gen_datatype_info?
>
>
> Fails the same way:
> Exception- HOL_ERR {message = "", origin_function = "list_mk_binder",
> origin_structure = "Term"} raised
>
>>
>>
>> Thanks,
>> Konrad.
>>
>>
>> On Wed, Jun 6, 2012 at 12:33 PM, Ramana Kumar 
>> wrote:
>> > Dear Konrad,
>> > Thanks a lot for your reply.
>> > I'm going to take this discussion onto the mailing list rather than the
>> > issue tracker.
>> > Further comments and questions below.
>> >
>> > On Wed, Jun 6, 2012 at 6:09 PM, Konrad Slind
>> >
>> > 
>> > wrote:
>> >>
>> >> Right, that's exactly the situation that should be documented. You
>> >> want to use
>> >>
>> >>  TypeBase.write
>> >>     [TypeBasePure.mk_datatype_info {...}];
>> >>
>> >> which creates the required tyinfo datastructure and installs it into
>> >> theTypeBase, which is the collection of useful type information used
>> >> by a variety of tools. There's a simple version of this invocation
>> >> at the end of
>> >>
>> >>   src/sum/sumScript.sml
>> >>
>> >> There is something wrong with it, which I will discuss later. But
>> >> first,
>> >> let's
>> >> go through the supplied fields in the record.
>> >>
>> >>     ax=TypeBasePure.ORIG sum_Axiom,
>> >>
>> >> This is the prim.rec. axiom characterizing the datatype, in the format
>> >> determined by the datatype package. The "TypeBasePure.ORIG"
>> >> constructor is needed because each type  in a mutually recursive type
>> >> declaration will end up having the same axiom, and I didn't want to
>> >> barf out the same redundant info when printing out tyinfo information
>> >> when TypeBase.elts() is invoked. When dealing with a non-mutually
>> >> recursive type, just use TypeBasePure.ORIG . If the type
>> >> is mutually recursive, you have to write each type separately; for
>> >> all but the first type, use TypeBasePure.COPY((thy,ty),axiom).
>> >>
>> >>      case_def=sum_case_def,
>> >>
>> >> Definition of the case construct for the type.
>> >>
>> >>      case_cong=sum_case_cong,
>> >>
>> >> Case cong theorem for the type.
>> >>
>> >>      induction=TypeBasePure.ORIG sum_INDUCT,
>> >>
>> >> Induction theorem for the type. See discussion on ORIG and COPY
>> >> above.
>> >>
>> >>      nchotomy=sum_CASES,
>> >>
>> >> Cases theorem for the type.
>> >>
>> >>      size=NONE,
>> >>
>> >> Definition of a size function for the type. This is used when
>> >> synthesizing
>> >> termination measures used by Define's termination prover. In the case
>> >> of sums, size=NONE because of a bootstrapping issue: numbers haven't
>> >> been defined at this point in the system build, so I fill in the field
>> >> with NONE,
>> >> and replace it later (see src/num/theories/basicSize.sml).
>> >>
>> >>      encode=NONE,
>> >>
>> >> The encode field is a vestigal remainder from some work I did with Joe
>> >> Hurd on
>> >> automatic generation and application of serializers for datatypes. Safe
>> >> to
>> >> leave
>> >> it as NONE.
>> >>
>> >>      fields=[], accessors=[], updates=[],
>> >>
>> >> These are needed for record types. The w

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Konrad Slind]

On Mon, Jun 11, 2012 at 1:12 AM,   wrote:
> I'm using HOL4 in the Windows console. I load a file using the "use"
> command, like this:
>
> use "E:/E_main2/binp/HOL4k7/examples/euclid.sml";
>

On windows I usually run HOL4 under emacs. But of course that's
just personal preference.

> I then edit some ML scripts in an editor and load them into HOL4 using
> the "use" command. My scripts get errors, so when I try to load
> "euclid.sml" again as shown above, I get errors in HOL4 which I didn't
> get before.

Most operations in HOL4 have been designed to be idempotent, i.e.,
if you call them once without error, you should be able to call them
again without error (and get the same result!). However, HOL4 does
have some internal state which can get muddled by re-invocations.
In some cases, this has to do with the HOL4 grammar. SML itself can
fail on re-invocation, typically with "infix" declarations.

Send (or post) a minimal failing version and the maintainers can help
you.

> I close the HOL4 window, and then start HOL4 again, but it doesn't start
> up instantly.

I haven't encountered this problem (on XP).

> Is there a command I can use to reinitialize HOL4 without closing it and
> restarting it?

I don't think so.


Cheers,
Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Konrad Slind]

>> Send (or post) a minimal failing version and the maintainers can help
>> you.
>
> I thought it was me causing problems by loading my own scripts after
> "HOL/examples/euclid.sml", but it wasn't.

The failure comes from making the "divides" constant an infix after its
definition. All is fine the first time around, but the second time the file
is used, divides is encountered in prefix position, but is expected to be
in infix position. Here's the change, which sets the fixity status of
the identifier,
then makes the definition.

set_fixity "divides" (Infix(NONASSOC, 450));

val divides_def =
 Define
  `a divides b = ?x. b = a * x`;


Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Konrad Slind]

> HOL Light just prints them in full, I think.  Ah well,
> as I already wrote, this way of working does not appeal
> too much to me anyway :-)
>
> Freek

It also suffers from the problem that a polymorphic formula
assumed in this way can't be instantiated. Asserting an axiom
is more powerful. In HOL4 axiom usage can be tracked in a similar
way to how assumptions are propagated, so you can get the same
effect as using an assumption.

Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Konrad Slind]

I wrote:
>> It also suffers from the problem that a polymorphic formula
>> assumed in this way can't be instantiated. Asserting an axiom
>> is more powerful. In HOL4 axiom usage can be tracked in a similar
>> way to how assumptions are propagated, so you can get the same
>> effect as using an assumption.

Cris then asked:

> Could you explain for us relative beginners a bit more what you mean here? I
> looked at the HOL Light code for PROVE_HYP, but the meaning and use are not
> clear to me.
>
> And anyway I am wondering if you mean that asserting an axiom is more
> powerful than _any_ ASSUME-like mechanism, or is somehow specific to
> PROVE_HYP.
>
> Additional enlightenment will be much appreciated.
>
> -Cris

One aspect of HOL that occasionally bites is that one needs to remember
that type variables are subject to similar constraints as term variables.
Suppose I want to ASSUME a formula containing a type variable, getting
a theorem

   th = tm |- tm

I won't be able to instantiate said type variable in the conclusion of th
without also instantiating it in the hypotheses. On the other hand

  new_axiom("foo",tm)

returns

 |- tm

and you don't have that limitation to deal with. Of course, you've
then got a new
axiom roaming around and potentially obliterating the usefulness of your
formalization.

Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Konrad Slind]

> Anyway, I've asked myself the same question above, when some HOL person
> will start to implement a version of "sections" or "locales".  My estimate
> is that when starting today, it would take approx. 5 years to make this
> become real. Our very first version of Isabelle locales can be seen here
> (14 years ago):
> http://isabelle.in.tum.de/repos/isabelle/file/5313f781efe0/src/Pure/locale.ML
>
>
> Makarius


My opinion is that Peter Homeier's HOL-Omega is the right setting to
properly implement
something locale-like, since it provides quantification over type
variables in the logic.
In plain old HOL the implementation of locales as essentially assumptions on
goals is too limiting for polymorphism.

Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Konrad Slind]

>> Does HOL4 have anything comparable to sets.ml?

> Yes it will have, and it will probably be spread over many source code
> files, but I'm afraid I don't know where this is in the HOL4 source.  This
> is a question for HOL4 community, Michael et al.  I'm more of a HOL Light
> and HOL Zero person.

The counterpart to sets.ml in HOL4 is in

  /src/pred_set/src/pred_setScript.sml

There is also a description of sets in HOL4 in the manual. Start at p. 102
of the HOL4 Description document:

  
http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-description.pdf/download

Konrad.


On Mon, Aug 13, 2012 at 1:49 AM, "Mark"  wrote:
> Hi Bill,
>
>> Isn't this supposed to be about sets?
>
> No, HOL is about types.  Tom is informally explaining what the HOL logic is,
> rather than explaining it in terms of some other formal notation (e.g. ZFC
> set theory).
>
>> Can you explain how the set abstraction/enumerations of sets.ml are
> lambdas?
>
> It's like I said - a set abstraction is (of course) a set, and so is a set
> enumeration.  Sets in HOL Light and HOL4 are functions to boolean (i.e.
> "predicates").  A lambda is a function.  So therefore one can understand
> how, in HOL Light and HOL4, a set abstraction or enumeration might be a
> lambda.  Maybe I'm misunderstanding what your misunderstanding is...
>
> I think a problem for you here is that, in HOL Light, it's sometimes not
> easy to see through the syntactic sugar.  The parser will automatically
> parse a set enumeration as ` { 1, 2, 3 }`, whereas it is actually internally
> represented as `1 INSERT (2 INSERT (3 INSERT EMPTY))` (and parsing this
> longhand will give precisely the same internal term).  The pretty printer
> will always print out this internal representation as `{ 1, 2, 3 }`.  To get
> around this in HOL Light and see the true internal representation, I think
> you need to use the destructors 'dest_comb' and 'dest_abs'.  Then, if you
> want to know the definitions of the HOL constants used in the internal
> representation, you can examine the ML state variable 'the_definitions',
> which lists all constant definitions that have been made.
>
>> Does HOL4 have anything comparable to sets.ml?
>
> Yes it will have, and it will probably be spread over many source code
> files, but I'm afraid I don't know where this is in the HOL4 source.  This
> is a question for HOL4 community, Michael et al.  I'm more of a HOL Light
> and HOL Zero person.
>
> Mark.
>
>
> on 13/8/12 5:53 AM, Bill Richter  wrote:
>
>> Thanks, Mark!  I looked at Tom Hales's Notices article, as you suggested
>> www.ams.org/notices/200811/tx081101370p.pdf
>> Now Tom is a great mathematician (he's the main reason I'm here), but Tom
> is
>> now an HOL Light expert, and I think mathematicians can't be expected to
>> understand him.  He starts out great:
>>
>> Much day-to-day mathematics is written at a level of abstraction
>> that is indifferent to its exact representation as sets.
>>
>> This layer of abstraction is good news, because it allows us to
>> shift from Zermelo-Fraenkel- Choice (ZFC) set theory to a different
>> foundational system with equanimity and ease.
>>
>> HOL Light is a new axiomatic foundation with types, different from
>> the usual ZFC.
>>
>> That sounds great, but here I want more details:
>>
>> The types are presented in the HOL Light System box.
>>
>> Terms are the basic mathematical objects of the HOL Light system. The
>> syntax is based on Church’s lambda-calculus [to define functions]
>>
>> What is a type?  Compared to a set, I think. What is a term?
>>
>> 1. Types: The collection of types is freely generated from type
>> variables :A,:B,... and type constants :bool (boolean), :ind
>> (infinite type), joined by arrows
>>
>> Isn't this supposed to be about sets?  My code (largely written by John)
>> doesn't obviously obey Tom's rule:
>> new_type("point",0);;
>> new_type_abbrev("point_set",`:point->bool`);;
>> new_constant("Between",`:point->point->point->bool`);;
>> new_constant("Line",`:point_set->bool`);;
>>
>> Maybe I need to read something by Church.
>>
>> 2. `{A,B}` is a set enumeration, not a set abstraction, so I'm not
>> sure why you are pointing to the definition of "INSERT" (which is
>> used in the representation of set enumerations) and then talking
>> about set abstractions.
>>
>> Because it was about all that was explained about sets in the tutorial,
> and
>> because I was intrigued that INSERT was explicitly defined as a lambda in
>> sets.ml.
>>
>> But anyway, any set enumeration or set abstraction is of course a
>> set, and, in HOL Light, any set is a function (as explained by 1.),
>> which is what a lambda is, so there should be no surprise that a
>> set abstraction/enumeration can be expressed as a lambda in HOL
>> Light.
>>
>> Can you explain how the set abstraction/enumerations of sets.ml are
> lambdas?
>> Does HOL4 have anything comparable to sets.ml?
>>
>> Sorry, I had two typos in my last post.  I meant to say
>>
>> let I1 

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Konrad Slind]

> Konrad, this is very interesting, because it's so much like sets.ml:
>
>There is also a description of sets in HOL4 in the manual. Start at
>p. 102 of the HOL4 Description document:
>
> Yours & Michael's Description manual starts pretty much like sets.ml which I 
> cited above.

Not surprising. Those are the usual definitions of the standard
operations on sets. Also,
there is some overlap in naming styles between HOL4 and HOL Light. Many of the
theorems having to do with sets probably have the same name even,
because of the way these systems evolved from a common ancestor.

> What I don't see is anything like what I'm having trouble with, the IN_* 
> theorems.
> Here are two from sets.ml I use constantly:

Those theorems are indeed present and heavily used in HOL4. Think of
it this way:
each basic set operation (union, intersection, complement, powerset,
difference, etc)
is defined via a set abstraction. These definitions tend to be
annoying to reason with,
so for each definition, a theorem with the name IN_ is
proved. These theorems are rewrite rules that push the "IN" operator
deeper into whatever expression they are applied to. IN_INTER is a
typical example.

> Is your HOL4 set abstraction mechanism so simple that you don't need a
> big hammer like IN_ELIM_THM?

It's not simple, as a reading of section 3.5.1.1. in the HOL4
Description reveals.
When abstracting over multiple variables the representation becomes
unfortunately complex and hence expressions like

z IN {x + y | x * y > w}

do not easily reduce to something useful.

Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Konrad Slind]

>
>Generally speaking, I'd say that "the automation is too powerful"
>is a problem we'd love [miz3] to have!
>
> Great!  Right now it's not powerful enough for me.

Bill, I'm struggling to understand your point of view. Of course,
more automation is a good thing, but presumably in your setting
full automation is not achievable, either on the grounds of
undecidability of the theory you are working in, or very high
computational complexity.  So maybe you are saying: "there
should be an algorithm, or heuristic, that efficiently proves all
statements that are obvious (to me)". That was the
approach of the early pioneers in automated proof, but resolution
theorem proving swept that notion aside, and I am not sure on what
scientific basis that could be revived. (Since "obvious" is a nebulous
conceptual blob of an idea.)

Or are you just saying that you wish
MESON proved more things more quickly? (In which case, why not
use the prover9 interface, which I think HOL-Light provides. Maybe you'll
get lucky!)

>The description of HOL in the Logic manual is based on a formal
>semantics inside set theory, developed by Andy Pitts.
>
> I see Andy wrote a paper with your advisor The HOL Logic and System but I 
> can't find a pdf for it.

 http://www.cl.cam.ac.uk/ftp/hvg/papers/HOLPaper.ps.gz

The first part, at least, provides something like what you seem to be
looking for.


Konrad.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Can I define a ZF FOL constant using only FOL symbols?

[Konrad Slind]

Hi Gottfried,

  I didn't read all of your (long) message. However,
I agree with Josef: conservative extension principles for FOL are
well known, even if not discussed in all set theory texts. I just consulted
two (Shoenfield's "Mathematical Logic" and Moschovakis "Notes on
Set Theory"): the former has a detailed discussion, while the latter
discusses Zermelo's idea of a "definite condition" in reasonable depth.

 On the other hand, you might enjoy reading the following article by
Adrian Mathias:

   http://www.dpmms.cam.ac.uk/~ardm/inefff.dvi

Cheers,
Konrad.


On Fri, Sep 7, 2012 at 10:13 AM, Gottfried Barrow
 wrote:
> On 9/7/2012 4:41 AM, Josef Urban wrote:
>> Hi,
>>
>> just a quick comment before this becomes into some HOL vs FOL issue:
>> (conservative) extension by definitions
>> (http://en.wikipedia.org/wiki/Extension_by_definitions) is a standard
>> FOL method that used very often (e.g., when building up math in ZFC).
>> I believe standard logic textbooks (like Mendelson) discuss this
>> early.
>>
>> Best,
>> Josef
>
> Josef,
>
> Thanks for the link. That tends to confirm my basic idea that when the
> many mathematicians say that axiomatic ZFC is the language of
> mathematics, as described in a typical axiomatic set theory book, it's
> not. The language of mathematics based on ZFC sets is possibly something
> as described by the wiki page. All I care about is that the
> mathematicians of the world acknowledge what the real, traditional
> language of mathematics has been for the last 100 years or so.
>
> For me it's not a HOL vs. FOL thing at all. I'm totally out of the
> mentality that I have to choose one or the other. In fact, I'm currently
> assuming that I can acceptably get FOL through HOL. It makes sense. Just
> because HOL provides 2-order and greater logic doesn't mean I have to
> resort to 2-order or greater logic. Actually, it is inescapable that I
> have to resort to a few higher-order functions to get access to the
> constants I need to use in FOL formulas. And, of course, all the FOL
> logical connectives are HOL functions. So maybe it's a matter of I'm
> assuming I can acceptably get the semantics of FOL using HOL, but still,
> other than the constants and predicates that have to be defined with HOL
> functions, I'm primarily limiting myself to the FOL logical connectives
> and quantifiers that HOL gives me.
>
> I'm totally committed to doing math as traditional as possible with
> theorem assistants, but if ZFC sets isn't a complete language, as
> proposed by the many axiomatic set theory books, then it can't ever be
> formalized using proof assistants exactly as it's traditionally
> specified, where I gave the basic specifications in the first email,
> which, of course, have nothing to do with me.
>
> Here's the summary of what I'm doing, and will be doing:
>
> I'm looking for quotes from mathematics, logicians, or computer
> scientists, who have authoritative credentials
> in the field of logic or set theory, to counter the idea that ZFC is a
> complete language, and to counter the idea
> that ZFC has ever really qualified as a complete solution for a formal
> language of mathematics, because of how
> it's been specified and locked in as a language of FOL.
>
> But before I go any further, I'm open to the idea that I have a basic,
> simple misunderstanding of first-order logic, and that's why I pose the
> simple question, "Can someone please tell me how to define a constant
> for the set which exists which has no elements, and do so using only the
> symbols that have been given to ZFC sets, as ZFC sets has been
> specifically defined and initially locked in according to the general
> FOL specification?"
>
> I looked at Mendelson's book. He may discuss logic extensions somewhere
> in the book similar to what the wiki page describes, but starting on
> page 288, he gives a two page summary of ZF sets. I don't see that his
> summary challenges the traditional view that traditional mathematics
> can, in principle, be reduced down to FOL formulas according to the ZFC
> sets definition, which is based on the general FOL specification.
> Mendelson says this:
>
> ZF is now the most popular form of axiomatic set theory: most of the
> modern research in set theory on
> independence and consistency proofs has been carried out with ZF sets.
>
> That sentence implies the typical "in principle" idea, that everything
> based on ZF can be reduced down to FOL formulas using only the logical
> symbols and non-logical symbols initially given to ZF sets, per the FOL
> specification.
>
> I explain some of my motivation below about why I care about this. My
> main practical concern is that mathematicians are perpetuating this idea
> that ZFC, as traditionally specified, is a complete language, with the
> result that people reject other mathematical languages, in particular,
> languages implemented in proof assistants. I only care to have some ammo
> for the challenge "It's different. It's not exactly ZFC s

Re: [Hol-info] MP_TAC

[Konrad Slind]

> Ok, so if I understand this correctly the validity checks are only in
> place to keep you from going down an inference chain that is guarenteed
> to go no where in making progress towards proving your goal.  This being
> only an issue when searching for the proof itself in the interactive
> prompt, not when just verifying it.


The way I think about it is that the validity check makes sure that no
assumptions beyond those stated in the goal enter the proof. For some
applications, adding new assumptions might be just the trick, e.g., when
exploring a proof to see what assumptions are needed. In that case,
expandf is your friend.

Konrad.

--
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_sfd2d_oct
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Hol Light -- Where's the "Easy" button?

[Konrad Slind]

Hi John,

  No it's not that hard. A calculation-like goal such as

  CARD {3;4} = 2

is a one-liner in HOL4 and I'd be surprised if that wasn't also
true in HOL-Light. In HOL4 the one-liner is an invocation of the
simplifier, using the implicit set of rewrites, so

  RW_TAC (srw_ss()) []

solves it. (You could also invoke EVAL_TAC to prove it.)

BUT. Not all goals are so easy, and just firing off automated tools
blindly never gets very far. So you need to develop a deeper understanding
of what theorems, definitions, and tools are available. Browsing proofs
in set.ml (or whatever it is called in HOL-Light) is bound to be
illuminating.
Maybe re-do some of them in Miz3?

By the way, I can't get access to the HOL-Light documentation at the
moment,
but I'm wondering what {3,4} means in HOL Light. In HOL4 it's a singleton
list
holding a pair of numbers.

Konrad.






On Sat, Nov 3, 2012 at 10:48 PM, John Nicol  wrote:

> Hi,
>
> I was pretty excited and optimistic when I found that HOL Light had
> developed a declarative mode, so I started working with the HOL Light
> system a few weeks ago.  (Without going into the whole philosophy, I prefer
> declarative proofs because they're closer to my understanding of proofs,
> they're hopefully portable, and hopefully don't involve all the tactics).
> So in Freek's Miz3 mode, I wrote up several definitions, a bunch of
> unproved theorems, and then:
>
> 1.  Stumbled through a bunch of hidden type errors in my definitions like
> "typechecking error (initial type assignment)".  It was really a bear to
> track down each of those.  BTW, I've used Vincent's typecheck.ml since
> then, and it's a huge help; I recommend something like that be added to the
> system.  Never figured out why real#real is a different type than real*real
> (they're both just tuples, right?), but I digress.
>
> 2.  I tried proving the most basic theorem I had declared.  I got some
> useful skeleton and syntax errors from Miz3 that helped a lot.  But the I
> got stuck on Inference or Timeout errors.  They didn't tell me much, so
> eventually I had to dive into HOL Light tactics and goalstacks directly to
> see what was going on.
>
> 3.  Turned out I couldn't prove *anything*.  So I read through a lot of
> the 2.20 Tutorial, the Reference guide, the Quick Reference, the Very Quick
> Reference, Freek's Miz3 paper, Richter's Miz3 notes, mailing list postings,
> blogs, various ML proofs...
>
> 4. Eventually I was able to prove that the cardinality of {3} was 1, which
> I thought should be trivial from something like SET_TAC, but apparently
> not.  It involved CONJ_TAC, REWRITE_TAC[FINITE_SING], and some other stuff
> I've forgotten, but it worked.
>
> 5.  I still can't prove that the cardinality of {3,4} is 2.  Here's what I
> have:
>  let blah_DEF = new_definition `blah={3,4}`;;
>  g `blah HAS_SIZE 2`;;
>  e(REWRITE_TAC[blah_DEF]);;(* now I have '{3,4} HAS_SIZE 2' *)
>  e(REWRITE_TAC[HAS_SIZE]);;  (* now I have `FINITE {3, 4} /\ CARD {3,
> 4} = 2` *)
>  e(REWRITE_TAC[CONJ_TAC]);;   (* two goals *)
>  e(REWRITE_TAC[FINITE_INSERT;FINITE_RULES];;  (* I've proved that a
> two-element set is finite now, yay.  `CARD {3,4} =2` *)
>  (* Nothing seems to do anything here, except expanding the definition
> more.  e[REWRITE_TAC[CARD_CLAUSES] doesn't do anything here... *)
>  e(REWRITE_TAC[CARD]);; (* `ITSET (\x n. SUC n) {3, 4} 0 = 2` *)
>  e(REWRITE_TAC[ITSET]);; (* Huh?  `(@g. g {} = 0 /\ (!x s.  FINITE s
> ==> g (x INSERT s) = (if x IN s then g s else SUC (g s {3, 4} = 2`  *)
>
>  And then I'm completely stuck.
> REWRITE_TAC[FINITE_INSERT;FINITE_RULES] no longer helps.
> REWRITE_TAC[FINITE_INDUCT_STRONG] doesn't help.  STRIP_TAC, MESON_TAC[]
> barf.
>
> I guess my questions are:
> 1.  It can't really be this hard, can it?  What am I missing?
> 2.  Is there a way to rewind in the goal stack if I do something dumb, or
> do I have to just redeclare my goal?
> 3.  Is there some basic tactic that I could use for trivial problems to
> say, "try everything possible and then tell me what tactics solved this".
> I thought that's what things like MESON_TAC were for, but I'm not sure any
> more.  Would I need to wire in an automated theorem prover or something?
> 4.  Are there any simpler examples than what's in the Examples/ directory?
>
> Thanks,
> John
>
>
> --
> LogMeIn Central: Instant, anywhere, Remote PC access and management.
> Stay in control, update software, and manage PCs from one command center
> Diagnose problems and improve visibility into emerging IT issues
> Automate, monitor and manage. Do more in less time with Central
> http://p.sf.net/sfu/logmein12331_d2d
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
---

Re: [Hol-info] Automatic subgoal to apply a conditional rewrite

[Konrad Slind]

Hi Vincent,

  Peter Homeier has given a thorough treatment of just this problem some
time ago. It can be found in the structure "dep_rewrite". It seems you have
to load it before opening it. There is documentation in
src/1/dep_rewrite.sml
in the distribution.

Cheers,
Konrad.



On Thu, Nov 22, 2012 at 2:31 PM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:

> Hi list,
>
> I often face the following small but annoying problem:
>
> * Situation:
>- I have a theorem (say, "Th") of the form "P ==> t = u"
>  ex: REAL_DIV_REFL
>  (|- !x. ~(x = &0) ==> x / x = &1 in HOL-Light, |- !x. x <> 0 ==> (x
> / x = 1) in HOL4)
>
>- the conclusion of my goal is a (big) term containing a subterm
> (say, " t' ") matching t
>  ex: a big expression with a subterm t / t somewhere deep inside the
> term
>
> * My aim: rewrite t' into u' using Th
>
> * Solution:
>- make a subgoal to prove P' (the instance of P corresponding to t')
>  ex: t / t <> &0
>  (assume t is a big expression to make it annoying to type in)
>
>- use this subgoal to rewrite the original goal
>
> * Problem:
>What annoys me in this frequent use case is that I have to explicitly
> state the subgoal P' whereas it seems it can be automatized.
>So, questions:
>- Am I the only one to find this annoying? :-)
>- If not, I imagine there might already exist a tactic that solves
> this recurrent problem, but if so I did not find it ?
>
> * Possible solution:
>If not, I developed my own tactic which a couple of students here at
> HVG have been using and found useful.
>Please find below the implementation in HOL4 and HOL Light, the
> tactic is called "MP_REWRITE_TAC".
>In order to use it, e.g., for the above situation, just use:
>
>  e(MP_REWRITE_TAC REAL_DIV_REFL)
>
>then the tactic will:
>- search the goal for a subterm matching t (if several matches it
> takes the first one it finds),
>- introduce a subgoal for the corresponding P',
>- rewrite the original goal with Th, taking P' into account.
>- add P' to the set of assumptions of the original goal, so that it
> can be reused later if needed.
>
> Regards,
> V.
>
>
> Code:
>
> HOL-Light:
>
> let MP_REWRITE_TAC th (_,c as g) =
>let sel = lhs o snd o strip_forall o snd o dest_imp in
>let PART_MATCH = PART_MATCH sel (SPEC_ALL th) in
>let th = ref TRUTH in
>ignore (find_term (fun t -> try th := PART_MATCH t; true with _ ->
> false) c);
>(SUBGOAL_THEN (lhand (concl !th)) (fun x ->
>  REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;
>
> HOL4:
>
> fun MP_REWRITE_TAC th g =
>let
>  val sel = lhs o snd o strip_forall o snd o dest_imp
>  val PART_MATCH = PART_MATCH sel (SPEC_ALL th)
>  val th = ref TRUTH
>  val _ =
>find_term (fn t => (th := PART_MATCH t; true) handle _ => false)
> (snd g)
>in
> (SUBGOAL_THEN (lhand (concl (!th))) (fn x =>
>   REWRITE_TAC[MP (!th) x] THEN STRIP_ASSUME_TAC x)) g
> end;
>
> --
> Vincent Aravantinos
> Postdoctoral Fellow, Concordia University, Hardware Verification Group
> http://users.encs.concordia.ca/~vincent
>
>
>
> --
> Monitor your physical, virtual and cloud infrastructure from a single
> web console. Get in-depth insight into apps, servers, databases, vmware,
> SAP, cloud infrastructure, etc. Download 30-day Free Trial.
> Pricing starts from $795 for 25 servers or applications!
> http://p.sf.net/sfu/zoho_dev2dev_nov
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info