10
votes
Accepted
What are some useful resources for a mathematician interested in learning Isabelle/HOL?
Once you installed Isabelle (following these instructions), you will have all the materials listed on the tag isabelle as a local copy. Definitely go through this one for a good (field agnostic) ...
- 1,148
8
votes
Accepted
Tracing the classical reasoner in Isabelle
I recall there is no end-user method to trace the classical reasoner, but there is a diagnosis configuration.
You should add a line ...
- 1,033
3
votes
Properties of determinants in Isabelle
You don't have to do this from scratch. The facts in HOL-Analysis.Determinants and related theories suffice.
Your first fact, $\det AB=\det A \det B$, is ...
- 366
3
votes
How to choose an axiom system in Isabelle/HOL?
If one wants to be really sure that one is not using any of Isabelle/HOL's facts, an alternative to my main answer would be to really start with a blank slate, only building on Isabelle/Pure (i.e. the ...
- 366
3
votes
Is there an elegant way of proving an equality A=B by going in both directions?
I believe there is, provided that L and R are predicates, of course:
...
2
votes
Accepted
How does a logical framework become a meta-logical framework?
Let me try taking a stab at a few provisional definitions. I can make these arbitrarily rigorous, but being fully general makes it hard to see the forest for the trees (at least, for me).
Provisional ...
- 1,749
2
votes
Accepted
How to write a low-level proof in Isar?
One way to accomplish this, somewhat in the lines of what you did, is the following:
...
- 1,033
2
votes
Accepted
Semantics verification of an LTL fragment logic
Simp rules for recursive definitions are supposed to be transparent, so you shouldn't need to invoke them for some simple applications. Tools like auto and ...
- 1,033
2
votes
Accepted
Isabelle warning explanation
As I understand it, auto cannot prove the claim.
However, if you do induction on x, then auto...
- 1,749
2
votes
Result contains obtained parameters? So what?
This one was already answered on Stack Overflow:
Soundness of natural deduction requires that you get hold of the witness before you open the existential quantifier.
This means you need to place the ...
- 515
2
votes
How to choose an axiom system in Isabelle/HOL?
Usually, Isabelle/HOL's proof methods will get most of propositional and predicate logic out of the way immediately. (Otherwise, by blast will solve them reliably.) ...
- 366
1
vote
Using Isabelle's Archive of Formal Proofs
I followed the advice
“If the AFP is in C:\afp, run the following command in a Cygwin terminal:
isabelle components -u /cygdrive/c/afp/thys“
It worked. I was told by one of the experts on Isabelle not ...
- 141
1
vote
Concrete examples in an Isabelle theory
The answer turns out to be relatively simple (as Jason Rute suggests): you can use definition to define not only functions, but other constants. Ballarin in the HOL-...
- 367
1
vote
Type class constaint is ignored in type synonym definition
Yes, datatype is adequate for this:
datatype ('v::group_add) myTypeOperator = MyTyOp 'v
datatype ('v) myTypeOperator2 = MyTyOp2 "'v::group_add"
Type ...
- 323
Only top scored, non community-wiki answers of a minimum length are eligible