Questions tagged [isabelle]

Isabelle is an interactive theorem prover, mostly used as Isabelle/HOL which is based on higer-order logic

11 questions
Filter by
Sorted by
Tagged with
33 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 ...
86 views

...
149 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 ...
• 3,632
106 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 ...
342 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,381
70 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,184
55 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 ...
237 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
65 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,184
345 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