Questions tagged [isabelle]

Use this tag with the proof assistant Isabelle, if your question is specific to a certain object logic please use the corresponding tag (eg. questions specific to Isabelle/HOL should also be tagged with (isabelle-hol)).

Filter by
Sorted by
Tagged with
19 votes
2 answers
381 views

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

For most proof assistants the name alone is common, E.g. Coq, Lean but with Isabelle it is often seen as Isabelle/<xyz>? Why the two parts? What is Isabelle/HOL Isabelle/FOL Isabelle/ZF ...
Guy Coder's user avatar
  • 2,836
18 votes
1 answer
278 views

How can all functions be total in Isabelle?

Isabelle/HOL’s logic is called a logic of “total functions”, yet there are functions that are obviously not total, such as division div. How does this make sense?
Joachim Breitner's user avatar
15 votes
0 answers
193 views

Code generation from Locales and Sublocales in Isabelle

Problem Description I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in ...
Wno-all's user avatar
  • 1,098
12 votes
1 answer
266 views

What are "locales" in Isabelle?

How does it compare to dependent records in Agda/Lean/etc.? I heard that locales in Isabelle are used to model algebraic structures in a talk, bu. Isn't this a kind of dependent type in some sense? Is ...
ice1000's user avatar
  • 5,974
10 votes
1 answer
222 views

How "generic" are "generic proof assistants"?

I've read that Isabelle and Metamath (and maybe Andromeda) are "generic" proof assistants in some sense that allows them to be used to implement different theories such as HOL, ZF and ...
Max New's user avatar
  • 304
9 votes
2 answers
779 views

Learning Math Proof via Proof Assistants

I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my ...
quidproquo's user avatar
9 votes
3 answers
201 views

Generic proof assistants/modularity of the proof assistants?

One notable feature of Isabelle is that it allows for the definition and in-built integrated support of alternative object logics via the interface of Isabelle/Pure in combination with Isabelle/Isar. ...
user9716869 - supports Ukraine's user avatar
9 votes
1 answer
53 views

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

Given two typeclasses (e.g. group and monoid), I have seen both the subclass and the ...
tinlyx's user avatar
  • 1,906
8 votes
2 answers
192 views

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

As shown in an exercise here, we can prove the Gauss summation (that $\Sigma_{i=0..n}{i} = n \cdot (n + 1)/2$ ) in Isabelle/Isar using mathematical induction, as follows. ...
tinlyx's user avatar
  • 1,906
8 votes
2 answers
92 views

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

Universally quantified variables are the same as free variables in the following two lemmas from the Isabelle (2021) tutorial section 8.1.2 (with slight changes on the second one): Given ...
tinlyx's user avatar
  • 1,906
8 votes
1 answer
141 views

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

What are some useful and reliable resources for a mathematician interested in learning Isabelle/HOL? Could be online (websites) or physical (books).
taylor.2317's user avatar
  • 1,308
8 votes
1 answer
139 views

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

In a recent answer, Isabelle was noted as a Logical Framework. A comment noted it was a Meta-Logical Framework. In researching for an understanding found "Logical and Meta-Logical Frameworks"...
Guy Coder's user avatar
  • 2,836
7 votes
1 answer
245 views

Tracing the classical reasoner in Isabelle

Some time ago I asked this question on Stack Overflow but got no answer: https://stackoverflow.com/questions/60521384/tracing-tactics-in-isabelle Section 9.4 The Classical Reasoner of the Isar ...
Gergely's user avatar
  • 299
7 votes
1 answer
192 views

Is there a way to use sledgehammer in Isar proofs?

I tried to use the sledgehammer command in Isabelle/HOL (2021) after the proof command, and got an error: Illegal application ...
tinlyx's user avatar
  • 1,906
6 votes
1 answer
310 views

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

Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
Weier's user avatar
  • 293
5 votes
2 answers
181 views

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

Is there a recommended implementation of Standard ML to use for Isabelle? Note: An answer should strive to include why that implementation (noted in build instructions is acceptable). While not needed ...
Guy Coder's user avatar
  • 2,836
5 votes
1 answer
132 views

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

My question is based on this question, which asks about swapping out different SML implementations when building Isabelle. I've read on Wikipedia that Isaballe is written in Scala and SML. Based on ...
Greg Nisbet's user avatar
  • 2,711
5 votes
1 answer
72 views

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

I am trying to define a hierarchy of type classes with binary operations, in which the base class defines a binary operation binop and then each class ...
tinlyx's user avatar
  • 1,906
5 votes
1 answer
90 views

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

The AFP entry Deriving provides a way to derive the following classes: class description comparator generate comparators for given types compare register types in class compare compare_order ...
Wno-all's user avatar
  • 1,098
5 votes
1 answer
79 views

Semantics verification of an LTL fragment logic

I am a beginner to Isabelle and I went over the proof documentation. I am trying to implement a fragment logic of LTL over finite intervals and finite traces called MLTL, the syntax and semantics can ...
Gokul's user avatar
  • 53
4 votes
1 answer
157 views

New types in higher order logic

From my understanding, most descriptions of higher order logic have a clear "phase distinction": We first describe the types, which are usually syntactically simple trees. For concreteness, ...
Trebor's user avatar
  • 3,718
4 votes
0 answers
33 views

Implementing object-logics in Isabelle Best Practices?

I'm patching up Isabelle/Mizar to work with Isabelle2023, and I am wondering what are the best practices for implementing an object logic in Isabelle? (Usually there is great documentation for ...
Alex Nelson's user avatar
  • 1,529
3 votes
1 answer
67 views

Particularization in algebraic statements in Isabelle

I'm new to Isabelle and I'm still becoming familiar with the basics. I have an algebra for which (x || y) ; (z || w) <= (y ; z) ; (x || w) is an axiom, ...
Kipirpo's user avatar
  • 33
3 votes
1 answer
31 views

Picking this and calculation in Isabelle/JEdit output

This is a follow-up to How to write a low-level proof in Isar? Having ...
Gergely's user avatar
  • 299
3 votes
1 answer
159 views

Existential quantification on types in Isabelle

We are currently working on a proof of compactness for classical first order logic using the ultraproduct-based proof. ...
Mesabloo's user avatar
  • 133
3 votes
0 answers
53 views

Why are modules also rings in the HOL-Algebra library?

We would like to use vectors and matrices (2x2 and 3x3) in a project, and have found the Jordan Normal Form AFP entry (Matrix.thy) which provides a concrete ...
Marco's user avatar
  • 131
2 votes
1 answer
28 views

ROOT file for building a heap image in Isabelle

I use Isabelle, and I have a theory that is processed for long interactively so I wanted to build a heap image. Therefore I created a ROOT file: ...
Gergely's user avatar
  • 299
2 votes
1 answer
111 views

How do I do for-all introduction in Isabelle?

It's pretty easy to prove something like this: theory Scratch imports Main begin theorem "foldl (λ x y. x) a b = a" apply (induction b) by auto ...
wizzwizz4's user avatar
  • 495
2 votes
0 answers
74 views

Disjoint unions in Isabelle/HOL

In mathematics there is a notion of a "disjoint union" in which you "consider" all of the sets to be disjoint even if they are not. For instance, you might want to take the ...
Charles Staats's user avatar
1 vote
2 answers
121 views

Is the Archive of Formal Proofs indexed in journal databases?

I was wondering if journals that publish regularly formal proofs are indexed in journal databases like Scopus or Web of Science. Apparently, this is not the case. Why is it so?
user1868607's user avatar
1 vote
1 answer
22 views

Referring to a session properly in another ROOT file in Isabelle

This is a follow-up to ROOT file for building a heap image in Isabelle . I have a main directory where my main theory resides. I have a ROOT file there: ...
Gergely's user avatar
  • 299
1 vote
0 answers
38 views

Characterization of capability-based security in Isabelle/HOL

I am looking for a formal characterization of Capability-based security in Isabelle/HOL using a set of invariants that "is complete". I'm not exactly sure what "complete" means, ...
oberstet's user avatar
  • 111
0 votes
1 answer
132 views

How to reason with notations directly?

Intuitive notations are always a big boost when stating and proving things. Modern interactive theorem provers usually have some way of building syntactic sugars aside from their ordinary abstraction ...
yiyuan-cao's user avatar
0 votes
0 answers
31 views

Simple and proper methods in Isar

https://isabelle.systems/cookbook/src/proofs/methods/Chained_Facts.thy talks about We note a slight difference. In the variant with intro, a trivial goal remains that we need to solve by ‹assumption›....
Gergely's user avatar
  • 299