Questions tagged [isabelle-hol]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer
91 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
27 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
  • 299
3 votes
1 answer
159 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
74 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
64 views

How to write a low-level proof in Isar?

I would like to formalize ...
Gergely's user avatar
  • 299
3 votes
0 answers
53 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
75 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
79 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
245 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
  • 299
8 votes
1 answer
139 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,836
8 votes
1 answer
176 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
141 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,308