What next after Tiddly Formal Math?

The Tiddly Formal Math site presents 28 out of 60 IsarMathLib theories. It looks like the approach based on TiddlyWiki is close to the limits of its scalability. The page loads slowly, renders even slower and Firefox asks frequently if I really want this script to run as it appears to be hanging. In addition I noticed recently that some proofs don’t want to expand and I don’t feel up to the task of debugging the NestedSlidersPlugin internals. The TiddlyWiki approach was good as a proof of concept but putting 617 pages of IsarMathLib proof document in one HTML file is clearly not a good idea.

So what next? It seems that the next step is to render IsarMathLib theories directly to HTML, CSS and JavaScript. This will open up lots of interesting possibilities for the presentation, like highliting the assumption or labeled references when the  mouse hovers over a label. The only problem is that (I am a bit ashamed) I know next to nothing about HTML, CSS and JavaScript. Well, I guess that has to change. It seems that haXe is an interesting way to write JavaScript.

IsarMathLib 1.6.6 released

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

Suppose is a commutative semigroup, is a linearly ordered set, an indexed collection of elements of and a nonempty list of finite, nonempty and mutually disjoint subsets of the index set . Then we have

In words, we can multiply the elements over each index set for and multiply the results, or we can multiply all elements for and the results are the same.

Interval arithmetic in groups: Pass 1

Gyula Lakos’s paper that I plan to formalize for IsarMathLib uses a natural generalization of interval arithmetic to abelian group setting. In this post I will go over section 2.A “Algebraic sums” in this paper, quoting it as needed and tell how I want to formalize the notions defined there.