Skip to main content

Questions tagged [isabelle-hol]

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

Filter by
Sorted by
Tagged with
1 vote
0 answers
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 ...
James Bowery's user avatar
1 vote
0 answers
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 ...
Red Banana's user avatar
2 votes
1 answer
64 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 ...
John's user avatar
  • 367
1 vote
1 answer
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: ...
John's user avatar
  • 367
1 vote
1 answer
116 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 ...
wizzwizz4's user avatar
  • 495
1 vote
1 answer
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 ...
Gergely's user avatar
  • 311
3 votes
1 answer
190 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. ...
Mesabloo's user avatar
  • 133
2 votes
0 answers
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 ...
Charles Staats's user avatar
1 vote
1 answer
66 views

How to write a low-level proof in Isar?

I would like to formalize ...
Gergely's user avatar
  • 311
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 ...
Marco's user avatar
  • 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, ...
oberstet's user avatar
  • 111
0 votes
0 answers
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 ...
RobertK's user avatar
5 votes
1 answer
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 ...
Gokul's user avatar
  • 53
7 votes
1 answer
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 ...
Gergely's user avatar
  • 311
9 votes
1 answer
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"...
Guy Coder's user avatar
  • 2,846
8 votes
1 answer
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:: ...
Mark Utting's user avatar
8 votes
1 answer
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).
taylor.2317's user avatar
  • 1,338