Stack Overflow
Stack Overflow

Questions tagged [isabelle]

Isabelle is a generic proof assistant, with Isabelle/HOL as main instance.

Isabelle is a generic proof assistant, which is best-known for its Isabelle/HOL instance. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. HOL specifications may be turned into program code in SML, OCaml, Haskell, or Scala. Isabelle includes many add-on tools like CVC4, Z3, SPASS, E prover.

User interfaces

Important links

1111 questions
94
votes
3 answers

What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?

Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?
elysefaulkner
  • 973
  • 2
  • 8
  • 8
18
votes
5 answers

Definition of a certified program

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? From what I can tell, all it really means is…
wyer33
  • 6,060
  • 4
  • 23
  • 53
17
votes
0 answers

What is the Parigot Mendler encoding?

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 ➔ cNat cS = Λ A . λ e . λ d . Λ X . λ z . λ s . s · A (λ…
MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
13
votes
3 answers

Isabelle/HOL foundations

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 could take the time to answer: Why doesn't…
Martin Copes
  • 931
  • 1
  • 7
  • 14
12
votes
1 answer

How do I generate LaTeX from Isabelle/HOL?

How can I use Isabelle/HOL to automatically generate LaTeX from my source theory files? Isabelle/HOL's tutorial.pdf is very beautiful. I'm going to write a paper in LaTeX with a lot of Isabelle code in it.
njuguoyi
  • 399
  • 4
  • 10
11
votes
1 answer

In Isabelle, how to print the state (i.e. subgoals to prove) in other formats (like S-expression, Json format...)?

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 syntax tree. The default printing mode doesn't include…
Q.Yang
  • 173
  • 1
  • 5
11
votes
3 answers

How to see step-by-step reasoning of Isabelle 'proofs'

I started to learn Isabelle recently and I cound not find an answer to a very important question: how can one see step-by-step reasoning of 'proofs' found by Isabelle? I am not satisfied with lines like "by auto" or "using Theorem_A by blast", I…
Amateur
  • 119
  • 3
10
votes
2 answers

Idiomatic Proof by Contradiction in Isabelle?

So far I wrote proofs by contradiction in the following style in Isabelle (using a pattern by Jeremy Siek): lemma "" proof - { assume "¬ " then have False sorry } then show ?thesis by blast qed Is there a way…
Christoph Lange
  • 595
  • 2
  • 13
10
votes
3 answers

How to make the assumption of the second case of an Isabelle/Isar proof by cases explicit right in place?

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 qed The first case is actually several pages…
Christoph Lange
  • 595
  • 2
  • 13
10
votes
4 answers

Why won't Isabelle simplify the body of my "if _ then _ else" construct?

I have the following Isabelle goal: lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False" None of the tactics simp, fast, clarsimp, blast, fastforce, etc. make any progress on the goal, despite it being quite simple. Why doesn't Isabelle just simplify…
davidg
  • 5,868
  • 2
  • 33
  • 51
10
votes
3 answers

How can I easily write simple tactics at the ML level of Isabelle?

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 automate proofs, to produce an ML tactic object, these…
davidg
  • 5,868
  • 2
  • 33
  • 51
10
votes
3 answers

Is it possible to not import any theory in Isabelle?

I want to define my own list type in a theory named List, but there is already a theory with that name. Is there a more lightweight theory than Main?
user1494846
  • 244
  • 3
  • 10
9
votes
6 answers

Interactive math proof system

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. Also, the tool must be able to save a session and…
BCS
  • 75,627
  • 68
  • 187
  • 294
9
votes
3 answers

Nested recursion and `Program Fixpoint` or `Function`

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. Inductive Tree := Node : nat -> list Tree ->…
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
9
votes
3 answers

Isabelle: Sledgehammer finds a proof but it fails

Often times I have the problem that sledgehammer finds a proof, but when I insert it, it doesn't terminate. I guess sledgehammer is one of the most important parts of Isabelle, but then it gets annoying if a proof fails. In the Sledgehammer…
mrsteve
  • 4,082
  • 1
  • 26
  • 63
1
2 3
…
74 75