Posts Tagged ‘IsarMathLib’

IsarMathLib updated to Isabelle2016-1

March 20, 2017

I finally got around to update IsarMathLib to Isabelle2016-1 that was released in  December last year. This was a quite time consuming update. The Isabelle system integrates LaTeX to be able to typeset well looking document proofs. This indeed works well – when it does. When there is a problem though it requires  LaTeX specific knowledge or long time to fix. This is what happened this time. The Isabelle team removed an element of its LaTeX setup that was obsoleted a couple of releases ago. They provided a script that was supposed to make necessary changes to theory files, but in my case running it on IsarMathLib’s 78 theory files just caused the errors to multiply. Fortunately Isabelle distribution sources provide lots of examples how LaTeX should be currently set up. After struggling for some time to understand the errors scattered over a 10MB log file I just created the IsarMathLib LaTeX setup from scratch following the examples and it worked. The IsarMathLib’s proof document and outline look better than ever.

Advertisements

IsarMathLib version 1.9.1 released

January 3, 2014

This is a maintenance release mostly to update IsarMathLib to Isabelle 2013-2. The RIPEMD-160 hash (a2ef972973bb2d072c7702d28dcfabee9026bd3b) of the proof document for this release is timestamped in the Bitcoin blockchain at 1FrXV7eifF2zruVr8YHJdvV8GHucUAqxYy.

IsarMathLib 1.7.2

July 20, 2011

I have released a new version of IsarMathLib. It adds about 50 new lemmas, mostly in group theory and topology, leading to the following characterization of closure in topological groups:

\overline{A} = \bigcap_{H\in \mathcal{N}_0} A+H

Here, \mathcal{N}_0 is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets A,B\subseteq G we define A+B as A+B=\{a+b | a\in A, b\in B\}.

(more…)

Isabelle2011, IsarMathLib 1.7.0 and other news

February 19, 2011

Isabelle team has released Isabelle 2011. The upgrade was not as smooth for me as the previous one. The new ProofGeneral didn’t work with Xemacs shipped with Ubuntu 9.10, giving a “file mode specification error”. I tried then the new jEdit interface that found that ZF logic is missing. Indeed, the Linux bundle does not contain precompiled ZF logic. It was not a big problem, I built it with “build ZF”.

The jEdit interface  (see the screenshot)  represents a new approach based on “continuous proving” concept. While I think it is very interesting technologically, it turned out extremely slow on my Athlon 64 1.8GHz with ony 512MB of RAM. Apparently all this proving in the background with keeping multiple versions of the document was just too much. It would be usable if it was possible to temporarily disable the continuous proving feature, but unfortunately this is not supported yet.

(more…)

Isabelle 2009-1 and IsarMathLib

December 5, 2009

The Isabelle team has just released Isabelle 2009-1. The latest release 1.6.9 of IsarMathLib checks out without any modification, so there is no update needed.

The new installation instructions on the Isabelle web site and the bundle file that can be downloaded from there are specific for Isabelle/HOL. To install Isabelle/ZF for IsarMathLib on x86 Linux one needs to download Isabelle2009-1.tar.gz, polyml-5.3.0.tar.gz,  ProofGeneral-3.7.1.1.tar.gz and ZF_x86-linux.tar.gz and do tar -C /usr/local -xzf on each of them. The installation can be finished by running

./bin/isabelle install -p /usr/local/bin

from /usr/local/Isabelle2009-1.

IsarMathLib 1.6.6 released

December 19, 2008

The release adds about 50 facts leading to a theorem named prod_list_of_sets that can be informally stated as follows:

Suppose G is a commutative semigroup, X is a linearly ordered set, \{a_x\}_{x\in X} an indexed collection of elements of G and M : n \rightarrow X a nonempty list of finite, nonempty and mutually disjoint subsets of the index set X. Then we have

\prod_{i=0}^{n-1} \prod_{x\in M_i} a_x = \prod_{x\in \bigcup_{i \in n} M_i} a_x

In words, we can multiply the elements over each index set M_i for i\in n and multiply the results, or we can multiply all elements a_x for x\in \bigcup_{i \in n} M_i and the results are the same.

(more…)

IsarMathLib version 1.6.5 relased

September 27, 2008

I have released a new version of IsarMathLib. This time there is some new formalized mathematics related to the theorem that two linearly ordered finite sets with the same number of elements are order-isomorphic and the isomorphism is unique. I have written previously on the motivation for this. The theorem was surprisingly tedious to prove and required about 50 lemmas in a couple of theories. Some corner cases were quite bizarre and kōan-like. For example: what is the order automorphism of the empty set? Turns out the empty set is a function, an injection, surjection, bijection and the only order automorphism of itself.

(more…)

IsarMathLib 1.6.4 released

June 30, 2008

Isabelle developers released 2008 version a couple of weeks ago, so I updated IsarMathLib to work with the new version. The update was very easy this time. The only change I had to make was to rename a couple of theory files as standard Isabelle theories were renamed and the new names were identical to some IsarMathLib’s theories.

Isabelle stopped tolerating  repeated names of theorems. A a result the new Isabelle found a couple of places in the theories containing facts translated from Metamath where I did the same work twice.  Translation  was a tedious and a bit mind-dumbing work. The translation tool was doing about 99% of it, but the remaining part was still enough to make me do the same thing a couple of times and not notice. I decided to remove the translation tool from IsarMathLib distribution and replace it with the source for the TiddlyWiki rendering tool. It still requires a lot of work, but it can parse and convert to TiddlyWiki markup 15 out of 47 IsarMathLib theories.

Tiddly Formal Math

March 9, 2008

I have posted a TiddlyWiki rendering of two IsarMathLib theories at tiddlyspot. The theories are Finite_ZF about the finite powerset and Topology_ZF about basic general topology. The rendering looks as I expected with great display of mathematical symbols and structured proofs with subproofs expanded on demand. The only problem is the indentation. I don’t know of a good method of controlling indentation in TiddlyWiki. There is a “{{indent{ ” construct, but this indents only one line instead of a block of text and does not mix well with the sliders. The “===” markup that marks the end of the slider is not noticed by TiddlyWiki when inside an indented line. In addition, indentation achieved this way is too wide – some twelve characters instead of perhaps three that I need for to see something like



   {

      fix k

      fix x

      assume A5: k\in n,   x\in X

      with A1 A3 have a(k) \in  Y

         using apply_funtype

      with A2 A5 I have (T(k))(x) = f\langle x,a(k)\rangle 

         using fix_var_val

   }

There is an old discussion on Gower’s Weblog where Gowers says

“Terry’s discussion of skeleton proofs is closely related to a fantasy I have had for a long time, which could I think become a reality. It’s to present mathematics in such a way that no step in any proof, no definition, nothing at all, is “magic”.”

Indeed, this can easily become a reality with the NestedSliderPlugin for TiddlyWiki. The reader could choose to see a short high level proof with the main points only, or expand the proofs of the facts that are unclear and see a very long and very detailed proof. Floating sliders can provide the statements of referenced theorems. This works very well to reduce verbosity of formally verifiable proofs as on the Tiddly Formal Math site, but would work for informal math too.

IsarMathLib and Isabelle/ZF

December 22, 2007

My impression that the new Isabelle 2007 does not break anything related to ZF was a bit premature. It turns out that the interpretation of locales has changed. There is a locale (context) in IsarMathLib called MMIsar0 that is used for Metamath to Isabelle/ZF translation. This locale has twenty five assumptions corresponding to Metamath’s axioms for complex numbers. The MMIsar_valid theorem in Metamath_interface.thy shows that if we take a model of real numbers (i.e. a completely ordered field) and construct the complex numbers from it in the standard way, then all Metamath axioms about complex numbers are satisfied. The problem is that those assumptions in MMIsar0 are interpreted by Isabelle 2007 not as a flat conjunction, but are grouped with parentheses into a complicated structure nested up to four levels deep in some places. It is not a show stopper, but it will take me some time to reflect this nesting structure in the proof.

This is a symptom of a deeper, architectural problem. When verifying a proof written in Isar Isabelle searches for a low-level proof and once it finds one it considers the Isar proof verified, so it discards the low-level proof. This causes problems every time the proof searching algorithm is changed – that is with every new Isabelle release. Some proofs that were successfully verified before don’t check any more. The only solution to this is to design a system so that the low-level proof is not discarded. Once the low-level proof corresponding to high-level source constructs is found, it can serve as the basis of verification and does not need to be generated again. I think while Isar is great for a high-level proof language, something like Metamath would be great as the underlying low-level language.