In Isar-style Isabelle proofs, this works nicely: from `a ∨ b` have foo proof assume a show foo sorry next assume b show foo sorry qed The implicit rule called by proof here is rule conjE. B...

Most proof assistants are functional programming languages with dependent types. They can proof programs/algorithms. I'm interested, instead, in proof assistant suitable best for mathematics and on...

I asked a series of question to get to the point I can define the following simple model in Isabelle, But I still stuck in getting what I wanted. I try to very briefly describe the problem with an ...

Suppose that I have the following expression in Isabelle/HOL: typedecl Person typedecl Car consts age :: "Person ⇒ int" consts drives ::"(Person × Car) set" consts owns ::"(Person × Car) set" ...

So far I wrote proofs by contradiction in the following style in Isabelle (using a pattern by Jeremy Siek): lemma "<expression>" proof - { assume "¬ <expression>" then have False so...

I have an Isabelle proof structured as follows: proof (cases "n = 0") case True (* lots of stuff here *) show ?thesis sorry next case False (* lots of stuff here too *) show ?thesis sorry qe...

Isar has, besides assume, also the command presume to introduce facts in an Isar proof block. From what I can see and read in the docs, it does not require the assumption (presumption?) to be expli...

I'd like to know about Isabelle/HOL subtypes. I explain a little about why it's important to me in my partial answer to my last SO question: Trying to Treat Type Classes and Sub-types Like Sets an...