Questions tagged [isabelle]

Use this tag with the proof assistant Isabelle, if your question is specific to a certain object logic please use the corresponding tag (eg. questions specific to Isabelle/HOL should also be tagged with (isabelle-hol)).

7 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
15 votes
0 answers

Code generation from Locales and Sublocales in Isabelle

Problem Description I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in ...
Wno-all's user avatar
  • 1,098
4 votes
0 answers

Implementing object-logics in Isabelle Best Practices?

I'm patching up Isabelle/Mizar to work with Isabelle2023, and I am wondering what are the best practices for implementing an object logic in Isabelle? (Usually there is great documentation for ...
Alex Nelson's user avatar
  • 1,529
3 votes
0 answers

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

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

Referring to a session properly in another ROOT file in Isabelle

This is a follow-up to ROOT file for building a heap image in Isabelle . I have a main directory where my main theory resides. I have a ROOT file there: ...
Gergely's user avatar
  • 299
1 vote
0 answers

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

Simple and proper methods in Isar talks about We note a slight difference. In the variant with intro, a trivial goal remains that we need to solve by ‹assumption›....
Gergely's user avatar
  • 299