Questions tagged [isar]

Use this tag for the ISAR (Intelligible semi-automated reasoning) proof language in the Isabelle proof assistant.

Filter by
Sorted by
Tagged with
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 ...
wizzwizz4's user avatar
  • 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 ...
Gergely's user avatar
  • 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. ...
Gergely's user avatar
  • 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›....
Gergely's user avatar
  • 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 ...
Gergely's user avatar
  • 267
1 vote
1 answer
62 views

How to write a low-level proof in Isar?

I would like to formalize ...
Gergely's user avatar
  • 267
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:: ...
Mark Utting's user avatar
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 ...
Guy Coder's user avatar
  • 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 ...
tinlyx's user avatar
  • 1,772