# Questions tagged [isabelle-hol]

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

17 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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: ...
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 ...
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 ...
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. ...
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
66 views

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

I would like to formalize ...
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 ...
1 vote
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, ...
84 views

### Summation over countable but infinite sets

I am trying to prove a simple property of sums over finite but countable sets (namely: all zero elements can be removed) in Isabelle/HOL. The sum function in the ...
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 ...
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 ...
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:: ...
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"...
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).