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)).
49
questions
1
vote
0
answers
32
views
Can this Free Logic prove everything ZFC can?
I would like to reason about undefinedness in a theorem prover so I was wondering if this Free Logic formalization will allow me to prove everything ZFC can? As I understand it Free Logic is a ...
- 33
1
vote
0
answers
51
views
Bad session in Isabelle
I am trying to run Incompleteness from afp-2019-08-19 on Isabelle2023. When I open the ROOT file
...
- 111
1
vote
1
answer
145
views
Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?
Remark 1. The following counting formula can be derived using arithmetic properties of inequalities, properties of floor / ceiling, inclusion-exclusion, sieve-of-Eratosthenes, and the inclusion-...
- 303
0
votes
1
answer
51
views
Automatic proofs after simp
My previous question about automatic proofs in Isabelle was answered by @BenjaminBisping pointing out how to use simp.
However, here's a simple example which is the ...
2
votes
1
answer
67
views
Properties of determinants in Isabelle
I would like to use the facts that $\det AB=\det A \det B$ and $\det A = \det A^t$ to prove that $\det AA^t = (\det A)^2$ in Isabelle. Is there a fast way to do this without doing this from scratch?
- 141
1
vote
1
answer
105
views
Using Isabelle's Archive of Formal Proofs
I am new to Isabelle proof assistant and want to use it to verify a standard proof of the Bruck Ryser Chowla theorem. Since this theorem is about symmetric block designs, I figured that the folder ...
- 141
5
votes
1
answer
124
views
Automatic proofs concerning inequalities
I've heard that Isabelle can be used to get automatic answers to questions like this:
lemma "∃ x :: real . 2 /3 < x ∧ x < 3 /4"
Of course, this one ...
0
votes
0
answers
18
views
How do I fold a function over the bindings in a map in Isabelle?
Coq has the FMap modules, is there a similar Isabelle theory module?
https://coq.inria.fr/doc/v8.19/stdlib/Coq.FSets.FMapInterface.html
What I want to be able to do is fold a function over the ...
- 75
2
votes
2
answers
72
views
Auto in Isabelle
Extremely trivial:
The last line doesn't work, any idea how to fix? Is there a way to say: let h be the proof of the antecedent; obtain a,b from h; now use a,b to prove the consequent, the way one can ...
1
vote
0
answers
116
views
Proving Quine's notion that identity belongs to logic within type-constrained proof assistants
I'm having difficulty generalizing the following proof to permit predicates of any finite arity.
Consider the following axioms of identity consistent with W. V. O. Quine's argument that relative ...
- 111
2
votes
1
answer
76
views
Extract explicit value from Isabelle proof
How can I extract an explicit value for a schematic variable in Isabelle after using it in a proof? For
example, in the following goal, I’m looking to extract a numerical value for ...
- 21
2
votes
2
answers
109
views
What is an assumption in Isar?
I have the following code:
lemma assumes "A" shows "A ∧ A"
proof -
show "A ∧ A"
apply (rule conjI)
apply assumption
Now, ...
- 323
2
votes
2
answers
117
views
How to choose an axiom system in Isabelle/HOL?
First of all, sorry if my question is too nonsensical and naive, I'm just getting started with Isabelle/HOL. I am reading Hou's "Fundamentals of Logic and Computation: With Practical Automated ...
- 121
4
votes
3
answers
228
views
For formal proofs of graph structures and algorithms, which proof assistant should I learn?
My goal is to be able to make formal proofs for graph structures and algorithms, proving i.e. for every vertex in a directed-acyclic-graph there exists a path from a source vertex to that vertex, or i....
- 63
2
votes
1
answer
82
views
Concrete examples in an Isabelle theory
I'd like to include example instances of various structures in an Isabelle document, just as is often done in mathematics textbooks.
If we look at the formalisation of an algebra text by Clemens ...
- 367
1
vote
1
answer
60
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:
...
- 323
2
votes
1
answer
57
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:
...
- 323
4
votes
0
answers
42
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 ...
- 1,574
0
votes
1
answer
157
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 ...
3
votes
1
answer
74
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, ...
- 33
1
vote
2
answers
131
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?
- 111
6
votes
1
answer
336
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 ...
- 313
4
votes
1
answer
183
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, ...
- 4,087
2
votes
1
answer
197
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
...
- 495
3
votes
1
answer
208
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.
...
- 133
2
votes
0
answers
90
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 ...
- 121
0
votes
0
answers
36
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›....
- 323
3
votes
1
answer
34
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
...
- 323
10
votes
1
answer
257
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 ...
- 314
3
votes
0
answers
56
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 ...
- 131
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, ...
- 111
9
votes
2
answers
1k
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 ...
- 93
5
votes
1
answer
82
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
249
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 ...
- 323
9
votes
1
answer
148
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,846
8
votes
2
answers
218
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.
...
- 2,320
6
votes
1
answer
154
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 ...
- 3,105
5
votes
2
answers
207
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,846
19
votes
2
answers
420
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,846
7
votes
1
answer
233
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 ...
- 2,320
8
votes
1
answer
157
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,348
8
votes
2
answers
103
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
...
- 2,320
5
votes
1
answer
87
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 ...
- 2,320
9
votes
3
answers
216
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
104
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,128
9
votes
1
answer
63
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 ...
- 2,320
15
votes
0
answers
222
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,128
18
votes
1
answer
315
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?
- 1,934
12
votes
1
answer
351
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 ...
- 6,346