In Isabelle, the command print_state can print the current goals needed to be proved. However, I want the goals to to be printed in other easy-to-tackle formats like S-expressions and abstract synt...

I sometimes find it hard to use Isabelle because I cannot have a "print command" like in normal programming. For example, I want to see what ?thesis. The concrete semantics book says: The unkno...

I was trying to go through the Isar chapter for Isabelle (theorem Prover) and the first statement has: lemma "¬ surj(f :: 'a ⇒ 'a set)" I wanted to understand what the constant surj was. I know ...

When goals are displayed by Isabelle in ProofGeneral, assumptions are rendered as having brackets around them as so: In Isabelle/jEdit, however, this seems to have changed to meta-implication ar...

I've been working in an Isabelle 2019 session which has grown a bit large, and at some point I wasn't able to build it anymore using isabelle build in my 8G RAM machine. Nevertheless, when I open t...

I started programming proofs in Isabelle one year and a half ago. Back then I mostly wrote Isabelle/Isar proofs. More recently, I have been doing a little of programming at the Isabelle/ML le...

I want to use Isabelle on weaker laptops and delegate the heavy theorem search/proving to a server on the network. I would guess that this has been done before but I could not find tutorials or rep...

I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages us...

I have some definitions and theorems in Isabelle/HOL and need to use those same definitions and theorems with HOL. Translating the code manually is certainly possible, but cumbersome. Are there any...

I saw the construct THE x. A in the source code of the Isabelle/HOL standard library. What does this construct denote? It seems to be similar to SOME x. A.

The following encoding of Nats is used in some Cedille sources: cNat : ★ cNat = ∀ X : ★ . X ➔ (∀ R : ★ . (R ➔ X) ➔ R ➔ X) ➔ X cZ : cNat cZ = Λ X . λ z . λ s . z cS : ∀ A : ★ . (A ➔ cNat) ➔ A ➔ cN...

How can I verify that a *.thy file is a valid Isabelle proof from the command line? Doing it in the GUI amounts to seeing that there are no issues/errors/warnings etc, I guess. But is there a way t...

I’d like to define the following function using Program Fixpoint or Function in Coq: Require Import Coq.Lists.List. Import ListNotations. Require Import Coq.Program.Wf. Require Import Recdef. Ind...

I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequen...

Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?

There are programming languages and theorem prover based on higher order logic (HOL). Examples include Twelf, lambda prolog, Isabelle. For example Twelf is is both a programming language and a theo...

I see a couple of different research groups, and at least one book, that talk about using Coq for designing certified programs. Is there are consensus on what the definition of certified program is...

Is there a "generic" informal algorithm that users of Isabelle follow, when they are trying to prove something that isn't proved immediately by auto or sledgehammer? A kind of general way of figuri...

Sometimes, when I’m writing apply-style proofs, I have wanted a way to modify a proof method foo to Try foo on the first goal. If it solves the goal, good; if it does not solve it, revert to t...

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...

I've been trying to learn to use Isabelle 2016. While in principle I like the idea of asynchronous proof checking, I don't like Isabelle/jEdit for a number of reasons, the most severe of which is t...

In an Isabelle theory file, I can write simple one-line tactics such as the following: apply (clarsimp simp: split_def split: prod.splits) I find, however, when I start writing ML code to automa...

It has come to my attention that there are several ways to deal with universal quantification when working with Isabelle/HOL Isar. I am trying to write some proofs in a style that is suitable for u...

I have seen a lot of documentation about Isabelle's syntax and proof strategies. However, little have I found about its foundations. I have a few questions that I would be very grateful if someone ...

I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. A...