Skip to main content
17 votes
Accepted

Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

Isabelle the program is designed as a "generic" LCF-style proof assistant/logical framework; it gives you a very minimal base logic (based on Church's simple type theory (pdf) and called ...
Josh's user avatar
  • 297
6 votes

Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

There are many more, notably: Isabelle/Pure (the core logic), Isabelle/jEdit (the bundled IDE), Isabelle/ML (its version of the ML language and its libraries), Isabelle/Scala (same for Scala), I ...
Pedro Sánchez Terraf's user avatar
4 votes
Accepted

Is there a way to use sledgehammer in Isar proofs?

It will work in an Isar proof, however you will want to pull a subgoal into focus. Unless your most recent tactic is something like induction, you will find ...
Wno-all's user avatar
  • 1,128
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: ...
user9716869 - supports Ukraine's user avatar
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 ...
wizzwizz4's user avatar
  • 495
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: ...
Pedro Sánchez Terraf's user avatar
1 vote

What is an assumption in Isar?

I assume the question is about how assumptions can be referenced to in an Isar proof. One way to use assumptions is through the assms keyword like this: ...
Slawomir K.'s user avatar
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 ...
Gergely's user avatar
  • 311
1 vote
Accepted

Picking this and calculation in Isabelle/JEdit output

At each step accumulating facts (i.e., each of moreover and the final ultimately), the proof state will show the fact ...
Pedro Sánchez Terraf's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible