Editing Isabelle (proof assistant)

{{Short description|Higher-order logic (HOL) automated theorem prover}}
{{Infobox software
| name = Isabelle
| logo = 
| screenshot = Isabelle jedit.png
| caption = Isabelle–jEdit running on [[macOS]] 
| author = [[Lawrence Paulson]]
| developer = [[University of Cambridge]]<br/>[[Technical University of Munich]], et al.
| released = {{Start date and age|1986}}<ref>{{Cite journal |last1=Paulson |first1=L. C. |author1-link=Lawrence Paulson |year=1986 |title=Natural deduction as higher-order resolution |journal=The Journal of Logic Programming |volume=3 |issue=3 |pages=237–258 |doi=10.1016/0743-1066(86)90015-4 |arxiv=cs/9301104 |s2cid=27085090}}</ref>
| latest release version=Isabelle2025
| latest release date = {{Start date and age|2025|03}}
| programming language = [[Standard ML]], [[Scala (programming language)|Scala]]
| operating system = [[Linux]], [[Windows]], [[macOS]]
| genre = [[Mathematics]]
| license = [[BSD licenses|BSD]]
| website = {{URL|isabelle.in.tum.de}}
}}

The '''Isabelle'''{{efn|{{IPAc-en|ˌ|ɪ|z|ə|ˈ|b|ɛ|l}}}} [[automated theorem prover]] is a [[HOL (proof assistant)|higher-order logic (HOL) theorem prover]], written in [[Standard ML]] and [[Scala (programming language)|Scala]]. As a [[Logic for Computable Functions]] (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.

Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories and implementations for code-generating, documenting, and specific support for a variety of [[formal methods]]. It can be seen as an [[integrated development environment]] (IDE) for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle ''Archive of Formal Proofs'' ('''Isabelle AFP''').<ref>{{cite web |last1=Eberl |first1=Manuel |last2=Klein |first2=Gerwin |last3=Nipkow |first3=Tobias |last4=Paulson |first4=Larry |author4-link=Lawrence Paulson |last5=Thiemann |first5=René |title=Archive of Formal Proofs |url=https://www.isa-afp.org/ |access-date=1 May 2021 |ref=AFP}}</ref>

Isabelle was named by [[Lawrence Paulson]] after [[Gérard Huet]]'s daughter.<ref>{{cite web|url=http://www.cl.cam.ac.uk/~mjcg/Research94/node3.html|title=1.2 History|work=Isabelle and HOL|publisher=Cambridge AR Research (The Automated Reasoning Group)|last=Gordon|first=Mike|date=1994-11-16|access-date=2016-04-28|archive-date=2017-03-05|archive-url=https://web.archive.org/web/20170305020417/http://www.cl.cam.ac.uk/~mjcg/Research94/node3.html|url-status=dead}}</ref>

The Isabelle theorem prover is [[free software]], released under the revised [[BSD license]].

==Features<!--'Intelligible semi-automated reasoning', 'Isar (Isabelle)', 'Locale (Isabelle)', 'Metis (theorem prover)', 'Nitpick (Isabelle)', 'Nunchaku (Isabelle)', and 'Sledgehammer (Isabelle)' redirect here-->==
Isabelle is generic: it provides a [[meta-logic]] (a weak [[type theory]]), which is used to encode object logics like [[first-order logic]] (FOL), [[higher-order logic]] (HOL) or [[Zermelo–Fraenkel set theory]] (ZFC). The most widely used object logic is Isabelle/HOL, although significant set theory developments were completed in Isabelle/ZF. Isabelle's main proof method is a higher-order version of [[First-order resolution|resolution]], based on higher-order [[unification (computing)|unification]].

Though interactive, Isabelle features efficient automatic reasoning tools, such as a [[term rewriting]] engine and a [[Method of analytic tableaux|tableaux prover]], various decision procedures, and, through the '''Sledgehammer'''<!--boldface per WP:R#PLA--> proof-automation interface, external [[satisfiability modulo theories]] (SMT) solvers (including [[CVC4]]) and [[Resolution (logic)|resolution]]-based [[automated theorem prover]]s (ATPs), including [[E (theorem prover)|E]], [[SPASS]], and [[Vampire (theorem prover)|Vampire]] (the '''Metis'''<!--boldface per WP:R#PLA-->{{efn|{{IPAc-en|ˈ|m|iː|t|ɪ|s}}}} proof method reconstructs resolution proofs generated by these ATPs).<ref>Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow, [https://people.mpi-inf.mpg.de/~jblanche/frocos2011-dis-proof.pdf "Automatic Proof and Disproof in Isabelle/HOL"], in: Cesare Tinelli, Viorica Sofronie-Stokkermans (eds.), [https://books.google.com/books?id=TT18o_HohVwC&dq= ''International Symposium on Frontiers of Combining Systems – FroCoS 2011''], Springer, 2011.</ref> It also features two [[Model theory|model]] finders ([[counterexample]] generators): '''Nitpick'''<!--boldface per WP:R#PLA--><ref name=:0>Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich & Christoph Weidenbach, [https://www.cs.vu.nl/~jbe248/sat.pdf "A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality"], ''Journal of Automated Reasoning'' '''61''':333–365 (2018).</ref> and '''Nunchaku'''<!--boldface per WP:R#PLA-->.<ref>Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli, [http://homepage.divms.uiowa.edu/~ajreynol/ijcar16a.pdf "Model Finding for Recursive Functions in SMT"], in: Nicola Olivetti, Ashish Tiwari (eds.), [https://books.google.com/books?id=HxFkDAAAQBAJ&dq= ''8th International Joint Conference on Automated Reasoning''], Springer, 2016.</ref>

Isabelle features '''locales'''<!--boldface per WP:R#PLA--> which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope<ref name=:0/> so that they do not have to be repeated for every [[Lemma (mathematics)|lemma]]. 

'''Isar'''<!--boldface per WP:R#PLA--> ("'''intelligible semi-automated reasoning'''<!--boldface per WP:R#PLA-->") is Isabelle's formal proof language. It is inspired by the [[Mizar system]].<ref name=:0/>

==Example proof==
Isabelle allows proofs to be written in two different styles, the [[procedural programming|procedural]] and the [[declarative programming|declarative]]. Procedural proofs specify a series of [[Tactic (computer science)|tactics]] (theorem proving [[Subroutine|functions/procedures]]) to apply. While reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. Declarative proofs (supported by Isabelle's proof language, Isar), on the other hand, specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans.

The procedural style has been deprecated in recent versions of Isabelle.<ref>{{cite web|url=https://isabelle.in.tum.de/doc/isar-ref.pdf|title=The Isabelle/Isar Reference Manual|first=Makarius|last=Wenzel|date=March 13, 2025|access-date=2025-05-10}} Page 148: "Arbitrary goal refinement via tactics is considered harmful". See also section 7.3, "Tactics: improper proof methods", pp. 172–175.</ref>

For example, a declarative [[proof by contradiction]] in Isar that [[Square root of 2#Proof by infinite descent|the square root of two is not rational]] can be written as follows.
<div style="font-family: monospace, monospace;"> 
 {{color|darkblue|theorem}} sqrt2_not_rational:
   {{olive|"sqrt 2 ∉ {{mathbb|Q}}"}}
 {{color|darkblue|proof}}
   {{color|darkblue|let}} ?x = {{olive|"sqrt 2"}}
   {{blue|assume}} {{olive|"?x ∈ {{mathbb|Q}}"}}
   {{color|darkblue|then}} {{blue|obtain}} m n :: nat {{green|where}}
     sqrt_rat: {{olive|"¦?x¦ {{=}} m / n"}} {{green|and}} lowest_terms: {{olive|"coprime m n"}}
     {{color|darkblue|by}} (rule Rats_abs_nat_div_natE)
   {{color|darkblue|hence}} {{olive|"m^2 {{=}} ?x^2 * n^2"}} {{color|darkblue|by}} (auto simp add: power2_eq_square)
   {{color|darkblue|hence}} eq: {{olive|"m^2 {{=}} 2 * n^2"}} {{color|darkblue|using}} of_nat_eq_iff power2_eq_square {{color|darkblue|by}} fastforce
   {{color|darkblue|hence}} {{olive|"2 dvd m^2"}} {{color|darkblue|by}} simp
   {{color|darkblue|hence}} {{olive|"2 dvd m"}} {{color|darkblue|by}} simp
   {{color|darkblue|have}} {{olive|"2 dvd n"}} {{color|darkblue|proof}} -
     {{color|darkblue|from}} {{olive|‹2 dvd m›}} {{blue|obtain}} k {{green|where}} {{color|olive|"m {{=}} 2 * k"}} ..<!--The two dots refer to a complete proof of this claim-->
     {{color|darkblue|with}} eq {{color|darkblue|have}} {{olive|"2 * n^2 {{=}} 2^2 * k^2"}} {{color|darkblue|by}} simp
     {{color|darkblue|hence}} {{olive|"2 dvd n^2"}} {{color|darkblue|by}} simp
     {{blue|thus}} {{olive|"2 dvd n"}} {{color|darkblue|by}} simp
   {{color|darkblue|qed}}
   {{color|darkblue|with}} {{olive|‹2 dvd m›}} {{color|darkblue|have}} {{olive|"2 dvd gcd m n"}} {{color|darkblue|by}} (rule gcd_greatest)
   {{color|darkblue|with}} lowest_terms {{color|darkblue|have}} {{olive|"2 dvd 1"}} {{color|darkblue|by}} simp
   {{blue|thus}} False {{color|darkblue|using}} odd_one {{color|darkblue|by}} blast
 {{color|darkblue|qed}}
</div>

==Applications==
Isabelle has been used to aid [[formal methods]] for the specification, development and [[Formal verification|verification]] of software and hardware systems.

Isabelle has been used to formalize numerous theorems from [[mathematics]] and [[computer science]], like [[Gödel's completeness theorem]], Gödel's theorem about the consistency of the [[axiom of choice]], the [[prime number theorem]], correctness of [[security protocol]]s, and properties of [[Formal semantics of programming languages|programming language semantics]]. Many of the formal proofs are, as mentioned, maintained in the Archive of Formal Proofs, which contains (as of 2019) at least 500 articles with over 2 million lines of proof in total.<ref>{{cite web |last1=Eberl |first1=Manuel |last2=Klein |first2=Gerwin |last3=Nipkow |first3=Tobias |last4=Paulson |first4=Larry |author4-link=Lawrence Paulson |last5=Thiemann |first5=René |title=Archive of Formal Proofs |url=https://www.isa-afp.org/ |access-date=22 October 2019 |ref=AFP}}</ref>

* In 2009, the L4.verified project at [[NICTA]] produced the first formal proof of functional correctness of a general-purpose operating system kernel:<ref Name="Klein_EHACDEEKNSTW_09">
{{ cite conference
 |last1=Klein
 |first1=Gerwin
 |last2=Elphinstone
 |first2=Kevin
 |last3=Heiser
 |first3=Gernot
 |last4=Andronick
 |first4=June
 |last5=Cock
 |first5=David
 |last6=Derrin
 |first6=Philip
 |last7=Elkaduwe
 |first7=Dhammika
 |last8=Engelhardt
 |first8=Kai
 |last9=Kolanski
 |first9=Rafal
 |last10=Norrish
 |first10=Michael
 |last11=Sewell
 |first11=Thomas
 |last12=Tuch
 |first12=Harvey
 |last13=Winwood
 |first13=Simon
 |title=seL4: Formal verification of an OS kernel
 |book-title=22nd ACM Symposium on Operating System Principles
 |pages=207–200
 |date=October 2009
 |location=Big Sky, Montana, US
 |url=http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
}}</ref> the seL4 (secure embedded [[L4 microkernel family|L4]]) [[microkernel]]. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 7,500 lines of C. The verification covers code, design, and implementation, and the main theorem states that the C code correctly implements the formal specification of the kernel. The proof uncovered 144 bugs in an early version of the C code of the seL4 kernel, and about 150 issues in each of design and specification.

* The definition of the programming language [[Lightweight Java]] was proven [[Type soundness|type-sound]] in Isabelle.<ref>{{Cite journal |last1=Strniša |first1=Rok |last2=Parkinson |first2=Matthew |date=7 February 2011 |title=Lightweight Java |url=https://www.isa-afp.org/entries/LightweightJava.html |access-date=2019-11-25 |journal=Archive of Formal Proofs |edition=February 2011 |issn=2150-914X}}</ref>

==Alternatives==
{{Further|Proof assistant#System comparison}}
Several languages and systems provide similar functions:
* [[Agda (programming language)|Agda]], written in [[Haskell]]
* [[Rocq (software)|Rocq]] (previously known as ''Coq''), written in [[OCaml]]
* [[Lean (proof assistant)|Lean]], written in [[Lean (proof assistant)|Lean]] itself and [[C++]]
* [[LEGO (proof assistant)|LEGO]], written in [[Standard ML of New Jersey]]
* [[Mizar system]], written in [[Free Pascal]]
* [[Metamath]], written in [[ANSI C]]
* [[Prover9]], written in [[C (programming language)|C]], with a GUI written in [[Python (programming language)|Python]]
* [[Twelf]], written in [[Standard ML]]

==Notes==
{{Notelist}}

==References==
{{Reflist}}

==Further reading==
{{refbegin}}
* [[Lawrence C. Paulson]], [https://arxiv.org/abs/cs/9301105 "The Foundation of a Generic Theorem Prover"], ''Journal of Automated Reasoning'', Volume 5, Issue 3 (September 1989), pages: 363–397, {{issn|0168-7433}}.
* Lawrence C. Paulson and [[Tobias Nipkow]], [https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-189.pdf "Isabelle Tutorial and User's Manual"], 1990.
* M. A. Ozols, K. A. Eastaughffe, and A. Cant, [https://link.springer.com/chapter/10.1007/BFb0000502 "DOVE: A Tool for Design Oriented Verification and Evaluation"], ''Proceedings of AMAST 97'', M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
* Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel, [https://isabelle.in.tum.de/doc/tutorial.pdf "Isabelle/HOL – A Proof Assistant for Higher-Order Logic"], 2020.
{{refend}}

==External links==
{{Portal|Free and open-source software}}
* {{Official website|isabelle.in.tum.de}}
* [https://stackoverflow.com/tags/isabelle/ Isabelle on Stack Overflow]
* [https://www.isa-afp.org/ The Archive of Formal Proofs]
* [https://isarmathlib.org IsarMathLib]

{{ML programming}}

[[Category:Proof assistants]]
[[Category:Free theorem provers]]
[[Category:Software using the BSD license]]