# Tag Info

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 ...
• 297
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 ...
• 1,904
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 ...
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 ...
• 350

### 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: ...
• 1,904
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) ...
• 1,118
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 ...
• 1,013

### 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 ...

### 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 ...
• 1,013
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 ...
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. ...

### 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 ...
• 1,013

### 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 ...
• 684
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 ...
• 2,116
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 ...
• 1,118
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, ...
• 1,564

### 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 ...
• 1,013

### 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&...
• 1,564

### 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 ...
• 131

### (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 ...
• 9,553

### 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 : ...
• 1,118
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 ...
• 1,118

### 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 ...
• 1,013
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 ...
• 1,564

### 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, ...
• 8,835

### 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 ...
• 3,180
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 ...
• 1,013
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 ...
• 9,553
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 ...
• 1,013