Intelligible semi-automated reasoning (Isar) is an approach to human readable formal proof documents (as opposed to state-based scripting).
Questions tagged [isar]
95 questions
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
9
votes
3 answers
proof (rule disjE) for nested disjunction
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. But what should I put there to make it work for…
Joachim Breitner
- 25,395
- 6
- 78
- 139
8
votes
1 answer
What is an Isabelle/HOL subtype? What Isar commands produce subtypes?
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 and Subsets
Basically, I only have one type, so it…
user2190811
7
votes
1 answer
Proof assistant for mathematics only
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 only (calculus for instance). Can you recommend one? I…
Yury
- 1,169
- 2
- 16
- 29
7
votes
1 answer
When would you use `presume` in an Isar proof?
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 explicitly listed in the goal, and seems to add a case to…
Joachim Breitner
- 25,395
- 6
- 78
- 139
5
votes
0 answers
Coding-style conventions in Isabelle/Isar
TL;DR: Are there any coding conventions for the Isar language? Is it necessary to respect jEdit's folding strategy?
My team is working on the formalization of mathematics, so one of our main purposes is to obtain readable proofs. Looking into that,…
Pedro Sánchez Terraf
- 231
- 1
- 7
5
votes
2 answers
completely replace the inner syntax in isar?
I am interested in using Isar as a meta language for writing formal proofs about J, an executable math notation and programming language, and I'd like to be able to use J as the inner syntax.
J consists of a large number of primitives, and assigns…
tangentstorm
- 7,183
- 2
- 29
- 38
4
votes
1 answer
What are the semantics of assume for Isabelle/Isar?
I found a surprising behaviour (for me) when using Isar.
I try to use assume and sometimes Isar complains it cannot resolve pending goals, for example my most typical example is having a an assumption and not being able to assume it:
lemma
…
Charlie Parker
- 5,884
- 57
- 198
- 323
4
votes
1 answer
Isabelle/Pure Isabelle/HOL Isabell/Isar conceptual questions
I need to do a presentation on a paper which at some point makes use of Isabelle/Isar and Isabelle/HOL.
I tried researching online about Isabelle/HOL and Isabelle/Isar to be able to eplain the relations in one or two slides.
Here are the relations…
Jonathan
- 552
- 1
- 4
- 10
4
votes
2 answers
Custom case distinctions in proofs
Does Isabelle support custom case distinctions when proving statements? Let's say I want to prove a statement for all natural numbers n, but the proof is entirely different depending on whether n is even or odd. Is it possible to do that case…
Benedikt
- 67
- 4
4
votes
1 answer
Isabelle / isar: Implementing equational reasoning
I'm still trying to get my head around equality relations and how to define one in Isabelle. Luckily there is a chapter about this in the isar reference manual 2.3.1 p38f.
I tried to rebuild the given example. To avoid any overlaps with the…
TKler
- 135
- 7
4
votes
2 answers
Printing out / showing detailed steps of proof methods (like simp) in a proof in isabelle
Suppose I have the following code in Isabelle:
lemma"[| xs@zs = ys@xs ;[]@xs = []@[] |] => ys=zs" (*never mind the lemma body*)
apply simp
done
In the above code, The simp method proves the lemma. I am interested to see and print out the detailed…
qartal
- 2,024
- 19
- 31
4
votes
2 answers
Taming meta implication in Isar proofs
Proving a simple theorem I came across meta-level implications in the proof. Is it OK to have them or could they be avoided? If I should handle them, is this the right way to do so?
theory Sandbox
imports Main
begin
lemma "(x::nat) > 0 ∨ x =…
Gergely
- 6,879
- 6
- 25
- 35
3
votes
1 answer
How to use a definition written on locale parameters in the assumptions of the locale?
If there is some definition on the parameters of a locale which would make the assumptions of the locale easier to write and/or read and/or understand (either because the function is quite complicated so would simplify the statement of the…
Jxek
- 502
- 1
- 4
- 13