Zanasi Fabio | 25 Nov 10:26 2014

CALCO 2015: First Call for Papers


              CALL FOR PAPERS:  CALCO 2015

6th International Conference on Algebra and Coalgebra in Computer Science

                 June 24 - 26, 2015

                Nijmegen, Netherlands



       Abstract submission:    March 22, 2015
       Paper submission:       April 2, 2015
       Author notification:    May 6, 2015
       Final version due:      June 3, 2015


-- SCOPE --

CALCO aims to bring together researchers and practitioners with
interests in foundational aspects, and both traditional and emerging
uses of algebra and coalgebra in computer science.

It is a high-level, bi-annual conference formed by joining the forces 
and reputations of CMCS (the International Workshop on Coalgebraic 
Methods in Computer Science), and WADT (the Workshop on Algebraic 
(Continue reading)

Tjark Weber | 26 Nov 15:17 2014

PhD Position in Formal Verification of Concurrent Systems at Uppsala University

PhD position in Formal Verification of Concurrent Systems
at Uppsala University, Sweden


Multi-core processors are ubiquitous, but writing correct concurrent
code is hard. Multi-threaded applications are prone to subtle bugs,
such as deadlocks and race conditions. These bugs are notoriously
difficult to find. Consequently, there is great interest in formal
verification techniques for concurrent code. The objective of this
project is to build a trustworthy framework that supports the
interactive and semi-automated verification of programs that utilize
low-level concurrency.

The work will be carried out in the Modeling of Concurrent Computation
research group (, which is
part of the Uppsala Programming for Multicore Architectures Research
Centre (

Qualifications: The candidate should have a Master of Science in
Computer Science, Computer Engineering or equivalent, ideally with a
strong background in logic, formal semantics and concurrent/parallel
programming. Experience with interactive theorem proving (e.g.,
Isabelle, Coq) is a plus.

Please see the official announcement at
for further details. Applications close on December 14, 2014.

(Continue reading)

Michael Winter | 24 Nov 16:36 2014

2nd CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

                          2nd CALL FOR PAPERS

                 15th International Conference on
   Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

           28 September to 1 October 2015, Braga, Portugal


We invite submissions in the general area of Relational and Algebraic Methods
in Computer Science. Special focus will lie on formal methods for software
engineering, logics of programs and links with neighbouring disciplines.

Particular topics of interest for the conference cover,
but are not limited to:

* Algebraic approaches to
  - specification, development, verification, and analysis of programs
    and algorithms
  - computational logic, in particular logics of programs, modal and
    dynamic logics, interval and temporal logics
  - semantics of programming languages

* Applications in fields such as
  - relational formal methods such as B or Z, tabular methods
  - information systems
(Continue reading)

Josef Urban | 26 Nov 20:45 2014

QED+20 - JFR Special Issue: Last Call for Papers - EXTENDED DEADLINE

Last Call for Papers - EXTENDED DEADLINE

Special issue of the




Paper submission: EXTENDED, December 14, 2014
Notification of acceptance: March 1, 2015
Final versions: March 22, 2015
Publication in JFR: April-May 2015


This a special issue on the occasion of the QED+20 workshop
( commemorating the 20th
anniversary of the QED Manifesto and the related 1994 and 1995 QED

>From the QED Manifesto (

(Continue reading)

Shruti Chawla | 21 Nov 21:37 2014

Pierce's Law in HOL Light

Hi, I am fairly new to HOL Light and OCaml. I'm unable to find a proof for Pierce's law in HOL Light. Could you provide me with a proof for it?

Also, I was trying to prove a simple goal 
# g `!p q r. p \/ (q /\ r) ==> p /\ q \/ p /\ r`;;
# e (INTRO_TAC "!p q r; p | q r");;

but I keep getting the error 'Unbound value INTRO_TAC"

I would really appreciate it if someone could clarify my doubts. Looking forward to your response eagerly.

Thanks and Regards
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
hol-info mailing list
hol-info <at>
Geoff Sutcliffe | 21 Nov 23:22 2014

CFP for the 9th TESTS AND PROOFS (TAP 2015)

*  9th International Conference
*  on

*  Part of STAF 2015, L'Aquila, Italy, July 20-24, 2015

*  Call for Papers
*  Abstract submission: February 13, 2015
*  Paper submission:    February 20, 2015


The TAP conference is devoted to the synergy of proofs and tests, to
the application of techniques from both sides and their combination
for the advancement of software quality.

Testing and proving seem to be orthogonal techniques: Once a program
has been proven to be correct then additional testing seems pointless;
however, when such a proof in not feasible, then testing the program
seems to be the only option. This view has dominated the research
community for a long time, and has resulted in distinct communities
pursuing the different research areas.

The development of both approaches has led to the discovery of common
issues and to the realization of potential synergy. Perhaps the use of
model checking in testing was one of the first signs that a
counterexample to a proof may be interpreted as a test case. Recent
breakthroughs in deductive techniques such as satisfiability modulo
theories, abstract interpretation, and interactive theorem proving
have paved the way for new and practically effective methods of
powering testing techniques. Moreover, since formal, proof-based
verification is costly, testing invariants and background theories can
be helpful to detect errors early and to improve cost effectiveness.
Summing up, in the past few years an increasing number of research
efforts have encountered the need for combining proofs and tests,
dropping earlier dogmatic views of incompatibility and taking instead
the best of what each of these software engineering domains has to

The TAP conference aims to bring together researchers and
practitioners working in the converging fields of testing and proving
by offering a generous forum for the presentation of ongoing research,
for tutorials on established technologies and for informal

Topics of Interest

Topics of interest cover theory definitions, tool constructions and
experimentations, and include among others:

- Bridging the gap between concrete and symbolic techniques, e.g.
  using proof search in satisfiability modulo theories solvers to
  enhance various testing techniques
- Transfer of concepts from testing to proving (e.g., coverage
  criteria) and from proving to testing
- Program proving with the aid of testing techniques
- Verification and testing techniques combining proofs and tests
- Generation of test data, oracles, or preambles by deductive
  techniques such as: theorem proving, model checking, symbolic
  execution, constraint logic programming
- Model-based testing and verification
- Generation of specifications by deduction
- Automatic bug finding
- Debugging of programs combining static and dynamic analysis
- Case studies combining tests and proofs
- Domain specific applications of testing and proving to new
  application domains such as validating security protocols,
  vulnerability detection of programs, security
- Testing of verification environments and reasoning engines like
  solvers and theorem provers
- New approaches such as crowd-sourcing and serious games to
  infer intended semantics and assess correctness
- Formal frameworks
- Tool descriptions and experience reports

Important Dates:

Abstract submission:     February 13, 2015
Paper submission:         February 20, 2015
Notification:                   April 13, 2015
Camera-ready version: May 3, 2015
STAF conference:          July 20-24, 2015

Program Co-Chairs:

Jasmin C. Blanchette (TU Muenchen, Inria)
Nikolai Kosmatov (CEA LIST)

Program Committee:

Bernhard K. Aichernig
Dirk Beyer
Nikolaj Bjorner
Jasmin C. Blanchette
Achim D. Brucker
Koen Claessen
Robert Clariso
Marco Comini
Catherine Dubois
Juhan Ernits
Gordon Fraser
Angelo Gargantini
Christoph Gladisch
Martin Gogolla
Arnaud Gotlieb
Reiner Haehnle
Bart Jacobs
Thierry Jeron
Jacques Julliand
Gregory Kapfhammer
Nikolai Kosmatov
Victor Kuliamin
Panagiotis Manolios
Karl Meinke
Alexandre Petrenko
Andrew Reynolds
Martina Seidl
Nikolai Tillmann
T.H. Tse
Margus Veanes
Luca Vigano
Burkhart Wolff
Fatiha Zaidi


Please submit your papers via EasyChair:

TAP 2015 will accept three kinds of submissions:

- Regular research papers: full papers with at most 16 pages in LNCS
  format (PDF), which have to be original, unpublished and not
  submitted elsewhere. Research papers should clearly describe the
  addressed problem, the relevant state-of-the-art, the
  scientifically-founded solution, and the benefits of the presented

- Short contributions: work in progress, (industrial) experience
  reports or tool demonstrations, position statements; an extended
  abstract with at most 6 pages in LNCS format (PDF) is expected. The
  same evaluation criteria apply to short papers as to regular
  research papers. Short papers will be reviewed to the same standards
  of quality as regular research papers.

- Tutorial proposals: TAP 2015 further invites one-hour tutorial
  presentations surveying the state-of-the-art of any research field
  related to the topics of TAP. Tutorial proposals shall have a
  maximum length of 3 pages in LNCS format (PDF) and provide
  information about the content, a short outline, information about
  the speakers and previous related tutorials given by the speakers
  (if any).

Accepted full and short papers will be published in the Springer LNCS
series and will be available at the conference. Accepted tutorials
will be assigned a slot of 60 minutes during the conference.

The content of last year's proceedings is available at

Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
Bill Richter | 15 Nov 09:25 2014

formalizing an axiom schema and MacOS OCaml/Camlp binaries

Does anyone know how to formalize an axiom schema in HOL Light?  I'm interested in formalizing the Tarski
axiomatic geometry 
Axiom schema of Continuity
and the part I don't know how to handle involves the universal quantification

Let φ(x) and ψ(y) be first-order formulae containing no free instances of either a or b

The Tarski first order language is quite simple, and is explained below in a code fragment of 
which John essentially wrote for me years ago.  But if someone had formalized an axiom schema for a different
first order language that's surely good enough for me.  Michael Beeson tells me that this is not necessary,
as we can instead just adopt every axiom-instance of the axiom schema that we actually use.  Do folks have an
opinion on that?

I'd like to install HOL Light on a Mac that's not connected to the net, and I'm intimidated by OPAM:
Is there an earlier version of OCaml/Camlp for which inria distribute MacOS binaries that folks trust for
building HOL Light?


NewConstant("ℬ", `:TarskiPlane->TarskiPlane->TarskiPlane->bool`);;

ParseAsInfix("≃",(12, "right"));;

let A1 = NewAxiom `;
  ∀a b. a,b ≃ b,a`;;

let A2 = NewAxiom `;
  ∀a b p q r s. a,b ≃ p,q ∧ a,b ≃ r,s ⇒ p,q ≃ r,s`;;

let A3 = NewAxiom `;
  ∀a b c. a,b ≃ c,c ⇒ a = b`;;

let A4 = NewAxiom `;
  ∀a q b c. ∃x. ℬ q a x ∧ a,x ≃ b,c`;;

let A5 = NewAxiom `;
  ∀a b c x a' b' c' x'.
        ¬(a = b) ∧ a,b,c ≊ a',b',c' ∧
        ℬ a b x ∧ ℬ a' b' x' ∧ b,x ≃ b',x'
        ⇒ c,x ≃ c',x'`;;

let A6 = NewAxiom `;
  ∀a b. ℬ a b a ⇒ a = b`;;

let A7 = NewAxiom `;
  ∀a b p q z.  ℬ a p z ∧ ℬ b q z
    ⇒ ∃x. ℬ p x b ∧ ℬ q x a`;;

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
hol-info mailing list
hol-info <at>
Serge Autexier | 11 Nov 17:08 2014

First CFP CICM 2015

                              Call for Papers              

                Conference on Intelligent Computer Mathematics
                                 CICM 2015

                              13-17 July 2015
                            Washington DC, USA

Digital and computational solutions are becoming the prevalent means for the
generation, communication, processing, storage and curation of mathematical
information. Separate communities have developed to investigate and build
computer based systems for computer algebra, automated deduction, and
mathematical publishing as well as novel user interfaces. While all of these
systems excel in their own right, their integration can lead to synergies
offering significant added value. The Conference on Intelligent Computer
Mathematics (CICM) offers a venue for discussing and developing solutions 
to the great challenges posed by the integration of these diverse areas.

CICM has been held annually as a joint meeting since 2008, co-locating
related conferences and workshops to advance work in these
subjects. Previous meetings have been held in Birmingham (UK 2008),
Grand Bend (Canada 2009), Paris (France 2010), Bertinoro (Italy 2011),
Bremen (Germany 2012), Bath (UK 2013), and Coimbra (Portugal 2014).

This is a (short version of the) call for papers for CICM 2015, which
will be held in Washington, D.C., 13-17 July 2015.

The full version of the CFP is available from the conference web page at

The principal tracks of the conference will be:

* Calculemus (Symbolic Computation and Mechanised Reasoning)
  Chair: Jacques Carette
* DML (Digital Mathematical Libraries)
  Chair: Volker Sorge
* MKM (Mathematical Knowledge Management)
  Chair: Cezary Kaliszyk
* Systems and Data
  Chair: Florian Rabe

Publicity chair is Serge Autexier. The local arrangements will be
coordinated by the Local Arrangements Chairs, Bruce R. Miller
(National Institute of Standards and Technology, USA) and Abdou
Youssef (The George Washington University, Washington, D.C.), and the
overall programme will be organized by the General Programme Chair,
Manfred Kerber (U. Birmingham, UK).

As in previous years, it is anticipated that there will be a number
co-located workshops, including one to mentor doctoral students giving
presentations. We also solicit for project descriptions and
work-in-progress papers.

Important Dates

Conference submissions:
Abstract submission deadline:      16 February 2015
Submission deadline:               23 February 2015
Reviews sent to authors:            6 April    2015
Rebuttals due:                      9 April    2015
Notification of acceptance:        13 April    2015
Camera ready copies due:           27 April    2015
Conference:                     13-17 July     2015

Work-in-progress and Doctoral Programme submissions:
Submission deadline:
(Doctoral: Abstract+CV)             4 May      2015
Notification of acceptance:        25 May      2015
Camera ready copies due:            1 June     2015

More detailed information, e.g. on submission via EasyChair, can be found on

Serge Autexier, serge.autexier <at>,
DFKI Bremen, Cyber-Physical Systems
MZH, Room 3120                             Phone: +49 421 218    59834
Bibliothekstr.1, D-28359 Bremen              Fax: +49 421 218 98 59834
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
principal office, *not* the address for mail etc.!!!:
Trippstadter Str. 122, D-67663 Kaiserslautern
management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
supervisory board: Prof. Hans A. Aukes (chair)
Amtsgericht Kaiserslautern, HRB 2313 

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
Aleksy Schubert | 10 Nov 22:43 2014

RDP 2015 Last Call for Workshops

[apologies for cross posting]

RDP 2015 Last Call for Workshops
(Rewriting, Deduction, and Programming, June-July 2015, Warsaw, Poland)

RDP 2015 is the eighth edition of the International Conference on
Rewriting, Deduction, and Programming, consisting of two main

* RTA (Rewriting Techniques and Applications)
* TLCA (Typed Lambda Calculi and Applications)

Previous RDPs were held in 2003 in Valencia (Spain), 2004 in Aachen
(Germany), 2005 in Nara (Japan), 2007 in Paris (France), 2009 in
Brasilia (Brasil), 2011 in Novi Sad (Serbia), 2013 in Eindhoven (The

We solicit proposals for satellite workshops of RDP 2015 that are
related in topics to one or both of the RDP conferences.

We plan the workshops to proceed for up to 2 days (possibilities of
longer workshops should be discussed with the organisers). It is
tradition at RDP that attendance to workshops is open to participants
of parallel events, similar to the way FLoC workshops are run. There
will be one day (Sunday, June 28, 2015) reserved for workshops only,
however, it will also be possible to run workshops on the other days
in parallel to one of the main conferences.

RDP will provide the possibility to print workshop proceedings,
details of the procedure will be posted later by the local organising
committee. RDP will not be able to reimburse invited workshop speakers
for travel or living expenses, though it may be possible to waive part
of the registration fees for invited speakers. The priority of RDP
will be to keep registration fees for the conferences and workshops

If you want to organise a workshop, please send the following
information to rdp15 <at>

* Workshop title and description of the topic
* Names and affiliations of the organisers
* Pointers to descriptions of previous editions of the workshop, if any
* Proposed workshop duration (from one day to two days)
* Proposed format and agenda (for example, paper presentations,
   tutorials, demo sessions, etc.)
* Plans for invited speakers or special sessions (round-table
   discussion, tutorials, etc.)
* Estimate of the audience size
* Procedures for selecting papers and participants
* Plans for the publication of proceedings (informal proceedings
   distributed to participants, electronic journal, proceedings with
   separate selection process, etc.)
* Other potential organisational issues


Submission of workshop proposals:   November 18, 2014 (Tuesday)
Notification date:                  November 26, 2014 (Wednesday)
Workshop dates:                     June 28-July 3, 2014 (Sunday-Friday)


Questions regarding workshop proposals should be sent to
rdp15 <at>

Aleksy Schubert
Faculty of Mathematics, Informatics and Mechanics
University of Warsaw

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
Michael Norrish | 10 Nov 05:56 2014

HOL4 Kananaskis-10 released

We are pleased to announce the release of the latest version of the HOL4 theorem-proving system.

Download it now from



Release Notes for HOL4, Kananaskis-10


New features:

  • Our TUTORIAL and LOGIC manuals are now available in Italian translations. Work on the DESCRIPTION manual is also far advanced. Many, many thanks to Domenico Masini for doing this work.

  • The abbreviation tactics (Q.ABBREV_TAC and others) now handle abstractions as abbreviations better. In particular, if one sets up an abstraction as an abbreviation (e.g., Q.ABBREV_TAC `f = (λn. 2 * n + 10)`), then the simplifier will find and replace instances not just of the abstraction itself (the old behaviour), but also instances of applications of the abstraction to arguments. For example, given the abbreviation for f above, the simplifier would turn a goal such as 2 * (z + 1) + 10 < 100 into f (z + 1) < 100.

  • The MAX_SET function in pred_setTheory is now defined (to have value 0) on the empty set.

  • There is an alternative syntax for specifying datatypes. Instead of the Hol_datatype entry-point, one can also use Datatype, which takes a slightly different syntax, inspired by Haskell. This does away with the use of the (somewhat confusing) of and => tokens.

    For example, one would define a simple type of binary tree with

    Datatype`tree = Lf num | Node tree tree`

    If the arguments to a constructor are not just simple types (expressible as single tokens), then they need to be enclosed in parentheses. For example:

    Datatype`mytype = Constr mytype ('a -> bool) | BaseCase`

    The Hol_datatype entry-point can continue to be used. However, the LaTeX output of EmitTeX uses the new format, and the various DATATYPE constructors used in the EmitML module take quotations in the new format, rather than the old.

  • The arithmetic decision procedure for natural numbers will now prove slightly more goals by doing case-splits on boolean sub-terms that are not in the Presburger subset. This means that goals such as

    0 < y ⇒ x < x + (if P then y else y + 1)

    are now provable.

  • The Vim mode for HOL now supports multiple simultaneous sessions. See its README for details.

  • Many of the standard libraries now provide an add_X_compset : compset -> unit (e.g., add_pred_set_compset) to ease building of custom call-by-name evaluation conversions that don't, like EVAL, include everything in the_compset().

  • Holmake has a new function, wildcard which allows expansion of “glob” patterns (e.g., *Script.sml) into lists of matching filenames.

  • The standard pretty-printer now annotates constants with their types as well as variables. (Note that these annotations are typically only visible by using mouse-over tooltips in the emacs mode.) The annotation also includes the constant’s real name, in the form thy$name, making overloads easier to tell apart.

    For example, this means that it is possible to have integers, reals and numbers all in scope, to write something like MAP (+), and to then see what constants are involved by using the mouse. (See Github issue #39.)

  • Unicode is handled slightly better on Windows systems. By default, the pretty-printer avoids printing with Unicode characters there, but can still parse Unicode input successfully. This is important because many of the examples distributed with HOL use Unicode characters in their scripts (nothing in src/ does). This behaviour can be adjusted by toggling the PP.avoid_unicode trace. On Windows this trace is initialised to true; elsewhere it is initialised to false.

Bugs fixed:

  • Holmake was unnecessarily quiet when it compiled certain SML files.

  • The “munging” code for turning HOL into LaTeX now does a better job of rendering data type definition theorems. (This change is independent of the new underlying syntax described earlier.)

  • On Windows, the Unicode trace is now off by default.

  • Pretty-printers added to the system with add_user_printer weren’t having terms-to-be-printed tested against the supplied patterns (except by the gross approximation provided by the built-in term-net structure). Thanks to Ramana Kumar for the bug report.

  • Character literals weren’t pretty-printing to LaTeX. We also improved the handling of string literals. Thanks to Ramana Kumar for the bug reports.

  • Piotr Trojanek found and fixed many documentation bugs in our various manuals.

  • The remove_rules_for_term and temp_remove_rules_for_term functions tended to remove rules for binders as well as the desired rules.

New theories:

  • A theory of “list ranges” (listRangeTheory). A range is a term written [ lo ..< hi ], meaning the list consisting of the (natural) numbers from lo up to, but not including, hi. The theory comes with some basic and obvious theorems, such as

    MEM i [lo ..< hi] ⇔ lo ≤ i ∧ i < hi


    LENGTH [lo ..< hi] = hi - lo
  • A new development in src/floating-point, which is a reworking of the theories in src/float. Key differences are listed below.

    1. The data representation:

      • The old ieeeTheory uses a pair ``:num # num`` to represent the exponent and fraction widths and a triple ``:num # num # num`` to represent sign, exponent and fraction values.

      • The new binary_ieeeTheory makes use of HOL records and bit-vectors. The floating-point type ``:(α, β) float`` has values of the form

        <| Sign : word1; Exponent : β word; Significand : α word |>

        The fraction and exponent widths are now constrained by the type, which facilitates type-checking and avoids having to pass size arguments to operations.

    2. The new development now supports standard bit-vector encoding schemes. The theory machine_ieeeTheory defines floating-point operations over 16-bit, 32-bit and 64-bit values. For example, the 16-bit floating point operations are defined by mapping to and from the type :(10, 5) float, which is given the type abbreviation :half. Theories for other sizes can be built using machine_ieeeLib.mk_fp_encoding.

    3. There is now syntax support via the structures binary_ieeeSyntax and machine_ieeeSyntax.

    4. Ground term evaluation is now supported for most operations. This can be enabled by loading binary_ieeeLib.

    5. The full development does not build under Moscow ML 2.01, as it makes use of the IEEEReal and PackRealBig basis structures.

  • A theory of “simple Patricia trees” (sptreeTheory). This theory implements a type α sptree, which is a finite map from natural numbers to values of type α. (This type is not really a Patricia tree at all; for those, see the other theories in src/patricia.) Values of type α sptree feature efficient lookup, insertion, deletion and union (efficient when evaluated with EVAL or simplified). Though there is a efficient (linear-time) fold operation, it does not iterate over the key-value pairs in key-order.

New tools:

  • New libraries enumLib and fmapalLib provide representations in pred_set and finite map types of enumerated constant sets and maps as minimum-depth binary search trees. A suitable total order on the set elements (map arguments) must be supplied, with a conversion for evaluating it; assistance with this is provided. The primary objective has been an IN_CONV, and a similar FAPPLY_CONV, operating with a logarithmic number of comparisons, but additional operations such as UNION_CONV, INTER_CONV, and FUPDATE_CONV are included and have reasonable asymptotic running times. A conversion TC_CONV implements Warshall’s algorithm for transitive closure of a binary relation (treated as a set-valued finite map).


  • The miniml example has been removed. This work has evolved into the CakeML project. That project’s git repository contains all of the material that was once in the HOL distribution, and, given its continuing evolution, much more besides.


  • In relationTheory, the theorems TC_CASES1 and TC_CASES2 have been renamed to TC_CASES1_E and TC_CASES2_E respectively, where the _E suffix indicates that these are elimination rules. In other words, these theorems are of the form TC R x y ⇒ .... This has been done so that new equivalences can be introduced under the old names. For example, TC_CASES1 now states

    TC R x z ⇔ R x z ∨ ∃y. R x y ∧ TC R y z

    This change makes the naming consistent with similar theorems RTC_CASES1 and RTC_CASES2 about the reflexive and transitive closure.

  • A theorem stating

    ⊢ ¬(0 < n) ⇔ (n = 0)

    (for n a natural number) has been added to the automatic rewrites used by SRW_TAC and srw_ss().

  • Some new automatic rewrites from pred_setTheory:

    • ⊢ DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t (and the version of this with DISJOINT s (x INSERT t) as the l.h.s.)
    • ⊢ ∀f s. INJ f ∅ s
    • ⊢ ∀f s. INJ f s ∅ ⇔ (s = ∅)
  • The add_binder and temp_add_binder entry-points in Parse have been removed. They are subsumed by set_fixity <name> Binder and temp_set_fixity <name> Binder respectively. In addition, add_binder was broken, creating an unloadable theory on export.

  • There is a new automatic rewrite from oneTheory:

    ⊢ ∀v:one. v = ()

    stating that every value in the type one (analogue of SML’s unit type) is equal to the designated value ().

  • Constants that print to the TeX backend as symbolic identifiers (e.g., non-alphanumeric tokens like +, **) are now annotated there with the \HOLSymConst command rather than \HOLConst. The default behaviour of \HOLSymConst (defined in holtexbasic.sty) is to do nothing.

  • If
    • Holmake is called in a directory with a Holmakefile, and
    • that Holmakefile has at least one explicit target, and
    • Holmake is called with no command-line targets,

    then: Holmake will attempt to build only the first target in that Holmakefile. We believe that this will cause problems in only a relatively small number of scenarios. The advantage of this change is that it makes Holmake easier to control from a Holmakefile. It also makes Holmake’s behaviour rather more like that of normal make.

    One scenario, among others, where this change may cause problems is where Poly/ML users have set up a rule to create a HOL heap. The fix is to prepend something like the following to your Holmakefile:

    THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml)) TARGETS = $(patsubst %.sml,%.uo,$(THYFILES)) all: $(TARGETS) ... .PHONY: all

    so that all becomes the first target of the Holmakefile. Any previous targets, such as HOL heaps, should be inserted where the ... occurs above.

    Note that Holmakefiles that only include variable declarations such as OPTIONS = ..., INCLUDES = ..., and HOLHEAP = ... don’t have any targets at all, so that Holmake’s behaviour in such files’ directories will not change.

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 <at>
"f~鳓ぁぇ | 4 Nov 03:33 2014

how to prove a goal with "case...of..."

I want to prove a goal like this:
                                          `case "d" of "u" =>1 |"s" =>2|"d" =>3 |"p" =>4`
Is there a tactic which can match "d" with the branch "d" and then execute this branch.
hol-info mailing list
hol-info <at>