Questions tagged [isar]
Use this tag for the ISAR (Intelligible semi-automated reasoning) proof language in the Isabelle proof assistant.
9
questions
1
vote
1
answer
83
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 ...
- 495
1
vote
1
answer
22
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
...
- 267
1
vote
0
answers
23
views
Discharging an assumption in Isar
In Isar, one can make an assumption and then use it as a premise for an implication goal later.
...
- 267
0
votes
0
answers
29
views
Simple and proper methods in Isar
https://isabelle.systems/cookbook/src/proofs/methods/Chained_Facts.thy
talks about
We note a slight difference. In the variant with intro, a trivial goal remains
that we need to solve by ‹assumption›....
- 267
3
votes
1
answer
30
views
Picking this and calculation in Isabelle/JEdit output
This is a follow-up to
How to write a low-level proof in Isar?
Having
...
- 267
1
vote
1
answer
62
views
8
votes
1
answer
175
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::
...
- 81
19
votes
2
answers
361
views
Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?
For most proof assistants the name alone is common, E.g. Coq, Lean but with Isabelle it is often seen as Isabelle/<xyz>?
Why the two parts?
What is
Isabelle/HOL
Isabelle/FOL
Isabelle/ZF
...
- 2,826
7
votes
1
answer
176
views
Is there a way to use sledgehammer in Isar proofs?
I tried to use the sledgehammer command in Isabelle/HOL (2021) after the proof command, and got an error:
Illegal application ...
- 1,772