# Questions tagged [isabelle-hol]

For use with the proof assistant Isabelle with classical higher-order logic.

17 questions
Filter by
Sorted by
Tagged with
140 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
151 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,338
178 views

### Is there an elegant way of proving an equality A=B by going in both directions?

I would like to prove an equality by splitting it into a proof in each direction. Is there a more elegant style to start such a proof than this way:: ...
248 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 ...
• 311
81 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
189 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
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
63 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
83 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 ...
1 vote
114 views

### Result contains obtained parameters? So what?

When proving an existential claim, you can use rule exI and exhibit an example; this is a sufficient proof (as you'd expect!). Conversely, if you have an ...
• 495
1 vote
66 views

### How to write a low-level proof in Isar?

I would like to formalize ...
• 311
1 vote
31 views

### Isabelle warning explanation

I'm dipping my toe back in the water with Isabelle after a 4-year hiatus, and once again finding it a bit frustrating. Here's a sample theory file based on an early chapter of this text: ...
• 367
1 vote
31 views

### Type class constaint is ignored in type synonym definition

My class constraint is ignored in a type synonym definition: for type_synonym 'value myTypeOperator = "'value::group_add" I get ...
• 311
1 vote
104 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
1 vote
61 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 ...
• 111
1 vote