Skip to main content

Questions tagged [isabelle-hol]

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

6 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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
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
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
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