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
9 votes
2 answers
319 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 ...
5 votes
1 answer
64 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 ...
  • 53
7 votes
1 answer
226 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 ...
  • 173
8 votes
1 answer
112 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"...
  • 2,786
8 votes
2 answers
142 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. ...
  • 1,370
4 votes
1 answer
86 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 ...
  • 2,611
5 votes
2 answers
118 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 ...
  • 2,786
19 votes
2 answers
286 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 ...
  • 2,786
7 votes
1 answer
76 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 ...
  • 1,370
8 votes
1 answer
114 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).
  • 1,248
8 votes
2 answers
69 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 ...
  • 1,370
5 votes
1 answer
51 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 ...
  • 1,370
9 votes
3 answers
160 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. ...
5 votes
1 answer
52 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 ...
  • 1,088
8 votes
1 answer
39 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 ...
  • 1,370
16 votes
0 answers
117 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 ...
  • 1,088
19 votes
1 answer
208 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?
11 votes
1 answer
144 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 ...
  • 4,992