Skip to main content
17 votes
Accepted

Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

Isabelle the program is designed as a "generic" LCF-style proof assistant/logical framework; it gives you a very minimal base logic (based on Church's simple type theory (pdf) and called ...
Josh's user avatar
  • 297
17 votes
Accepted

How can all functions be total in Isabelle?

If you have a Isabelle/HOL function f :: a ⇒ b between two types a and b (NB: the function ...
Joachim Breitner's user avatar
12 votes
Accepted

What are "locales" in Isabelle?

Basically, a locale is a name for a set of fixed parameters, that come with assumptions. Inside the locale, these assumptions are added implicitly to everything you define/prove. When you have ...
Peter Lammich's user avatar
10 votes
Accepted

Learning Math Proof via Proof Assistants

I have a degree in software engineering and share the same goal as yours. Start with Informal Proofs Truth be told, you can learn more about proof by reading introductory maths book at university ...
zacque's user avatar
  • 350
10 votes

How to prove Gauss summation of integers with proof assistants using forward reasoning?

Like @Bubbler, I think a nice forward proof can be done using a chain of equalities, to spell out each step: ...
Joachim Breitner's user avatar
9 votes
Accepted

What are some useful resources for a mathematician interested in learning Isabelle/HOL?

Once you installed Isabelle (following these instructions), you will have all the materials listed on the tag isabelle as a local copy. Definitely go through this one for a good (field agnostic) ...
Wno-all's user avatar
  • 1,118
8 votes
Accepted

Tracing the classical reasoner in Isabelle

I recall there is no end-user method to trace the classical reasoner, but there is a diagnosis configuration. You should add a line ...
Pedro Sánchez Terraf's user avatar
7 votes

Standard ML is used for many proof systems. Is there a recommended implementation to use for Isabelle?

Historically, we always tried to ensure that Isabelle would run on both Poly/ML and SML/NJ. It's a curious fact that Poly/ML always greatly outperformed SML/NJ even though the latter seemed much ...
Lawrence Paulson's user avatar
6 votes

Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

There are many more, notably: Isabelle/Pure (the core logic), Isabelle/jEdit (the bundled IDE), Isabelle/ML (its version of the ML language and its libraries), Isabelle/Scala (same for Scala), I ...
Pedro Sánchez Terraf's user avatar
6 votes
Accepted

How "generic" are "generic proof assistants"?

Isabelle/Sequents contains a formalisation of intuitionistic linear logic, so conceivably you have a chance of implementing your logic in Isabelle, following the techniques used there. Whether what ...
Lawrence Paulson's user avatar
6 votes
Accepted

Is there a way to convert free variables to (meta) universally quantified variables in Isabelle?

My question is: Is there an idiomatic way to convert the first goal to the second goal during a proof, and vice versa from lemma 2 to lemma 1? Yes, there is. ...
user9716869 - supports Ukraine's user avatar
5 votes

Is there a way to convert free variables to (meta) universally quantified variables in Isabelle?

You should first note that the tutorial you're reading is in the “Old” documentation section and thus the style of the proofs is a bit dated. For instance, they would seem to recommend ...
Pedro Sánchez Terraf's user avatar
5 votes

How to prove Gauss summation of integers with proof assistants using forward reasoning?

Not exactly sure if Lean counts as "similar proof assistant" to Isabelle, but Lean mathlib has the proof of essentially the same statement, using calc mode which allows to gradually ...
Bubbler's user avatar
  • 684
4 votes
Accepted

Standard ML is used for many proof systems. Is there a recommended implementation to use for Isabelle?

I wondered about the same question before. Based on this blog, it seems that the only supported SML implementation now is Poly/ML. 17-Feb-2016 marks the historic day when support for SML/NJ was ...
tinlyx's user avatar
  • 2,116
4 votes
Accepted

Is there a way to use sledgehammer in Isar proofs?

It will work in an Isar proof, however you will want to pull a subgoal into focus. Unless your most recent tactic is something like induction, you will find ...
Wno-all's user avatar
  • 1,118
4 votes
Accepted

Architecture of Isabelle: What parts are written in SML? What parts are written in Scala? What does the boundary look like?

Scala appears to use the JVM, and this has been marketed as a feature, not a bug. According to Isabelle/Scala: Isabelle/ML is for ‹mathematics›, to develop tools within the context of symbolic logic, ...
Alex Nelson's user avatar
  • 1,564
4 votes

How to rename a type class operator in a subclass in Isabelle/HOL?

Perhaps you checked the general tutorial, but the one you need to look at is on locales and locale interpretation, or the more specialized Haskell-style type classes with Isabelle/Isar. I'm more ...
Pedro Sánchez Terraf's user avatar
4 votes

Generic proof assistants/modularity of the proof assistants?

It sounds like you're after a logical framework, i.e., a system which allows you to reason within a given foundations. Isabelle is a bit more than this, it's a so-called "meta-logical framework&...
Alex Nelson's user avatar
  • 1,564
3 votes

Is the Archive of Formal Proofs indexed in journal databases?

I find that Journal of Formalized Reasoning (Univ. Bologna) is covered by MathSciNet. I guess that journal ran from 2008 to 2020. LINK Also, Journal of Automated Reasoning (Springer) is covered by ...
Gerald Edgar's user avatar
3 votes

(Dis)Advantages of basing a proof assistant on CH correspondence?

Let us separate two things here: having dependent types, and using them to express logic a la propositions-as-types. As far as formalization of mathematics is concerned, there are no disadvantages to ...
Andrej Bauer's user avatar
  • 9,553
3 votes

How can I derive other type classes in Isabelle/HOL?

To register a new type class with the Deriving_Manager, I found Derive_Aux.define_overloaded useful. Here is an example usage : ...
Wno-all's user avatar
  • 1,118
3 votes
Accepted

Are `subclass` and `instance` commands equivalent in defining subclass relation between typeclasses in Isabelle?

Citing The Isabelle/Isar Reference which is part of the official documentation: A weakened form of [subclass] is available through a further variant of instance: instance c1 ⊆ c2 opens a proof that ...
Wno-all's user avatar
  • 1,118
3 votes

For formal proofs of graph structures and algorithms, which proof assistant should I learn?

I believe both Lean and Isabelle are good candidates for formalizing your proofs of algorithms on graphs. Here are some entry points for both assistants. A simple natural language query using Moogle ...
Pedro Sánchez Terraf's user avatar
2 votes
Accepted

How does a logical framework become a meta-logical framework?

Let me try taking a stab at a few provisional definitions. I can make these arbitrarily rigorous, but being fully general makes it hard to see the forest for the trees (at least, for me). Provisional ...
Alex Nelson's user avatar
  • 1,564
2 votes

Generic proof assistants/modularity of the proof assistants?

Both Metamath (and Metamath Zero) are naturally foundation generic. Metamath Like Isabelle, most of the active work done in Metamath is in just one theory (specifically set.mm uses ZFC). Nonetheless, ...
Jason Rute's user avatar
  • 8,835
2 votes

Generic proof assistants/modularity of the proof assistants?

I believe one "emerging proof assistant" along these lines is Andromeda. The theory of Andromeda is essentially an extensional dependent type theory with equality reflection, which can be ...
Mike Shulman's user avatar
  • 3,180
2 votes
Accepted

Semantics verification of an LTL fragment logic

Simp rules for recursive definitions are supposed to be transparent, so you shouldn't need to invoke them for some simple applications. Tools like auto and ...
Pedro Sánchez Terraf's user avatar
2 votes
Accepted

New types in higher order logic

First, there is no reason to remove function types, so you should put those in. Then you can remove special treatment of propositions because they are just functions with codomain $\Omega$. So far we ...
Andrej Bauer's user avatar
  • 9,553
2 votes
Accepted

How do I do for-all introduction in Isabelle?

You have just successfully did $\forall$-introduction after the first apply. But sometimes using rule is too low-level. After ...
Pedro Sánchez Terraf's user avatar
2 votes
Accepted

How to reason with notations directly?

This is a general problem, not just with notations: you always have to deal with the elaborated code, not the "one you wrote". This applies to notations, but also to type-classes resolution (...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible