Questions tagged [isabelle]
Isabelle is an interactive theorem prover, mostly used as Isabelle/HOL which is based on higer-order logic
11 questions
0
votes
0
answers
44
views
How to specify in Isabelle that there exists j in an interval
I am looking to specify something in Isabelle of the form that there exists a $j$ such that $lb < j < ub$, where $lb$ and $ub$ are lower and upper bounds.
For a single condition, we can say, for ...
- 1
0
votes
1
answer
95
views
2
votes
1
answer
204
views
Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?
I haven't been able to find a good explanation of how these are different and relate to each other. I know that $\to$ is part of HOL and $\Rightarrow$ and $\Longrightarrow$ part of Isabelle, but it ...
- 4,122
2
votes
1
answer
124
views
What are the differences between LCF's Theorem and Automath's Prop?
How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do ...
- 31
3
votes
1
answer
350
views
How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
- 1,401
2
votes
0
answers
78
views
Difference between the logic and the type system of a proof assistant?
In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says:
A ...
- 2,204
3
votes
1
answer
66
views
Naming facts exported from blocks in Isabelle/HOL
I'm using Isabelle/HOL. Isabelle exports the last fact in a block, allowing the context that contains the block to use it. Ordinarily when I generate facts, I can give them convenient names. How do ...
- 318
3
votes
1
answer
341
views
When can the coinduction hypothesis be used?
We can use the induction hypothesis when we are proving a property for a structure that is well-ordered. I am aware that there is a proof for this.
When it comes to coinduction, I'm confused.
One of ...
- 153
2
votes
0
answers
80
views
Understanding Isabelle's implementation of coinduction
I'm studying how coinduction was encoded in Isabelle. At page 7 of the attached document, the author describes how some datatypes can be encoded as initial algebras. Here is one example:
Finite lists
...
- 2,204
11
votes
1
answer
367
views
How did 'Isabelle' (the theorem prover) get its name?
The title says it all, but I'm curious because it isn't obvious how a theorem prover came to be named 'Isabelle'. Was it named for a person? I couldn't find out by some Google searches.
- 221
4
votes
1
answer
340
views
Proof on tree size using Isabelle
I'm trying to learn a little bit about Isabelle and proofs in general, and it's uses in Programming Language Theory. I'm following a book, "Concrete Semantics with Isabelle/HOL". I'm still in the ...
- 41