PLDB
Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon

Isabelle

Isabelle

Isabelle is a pl created in 1986.

#269on PLDB 36Years Old 576Users
0Books 4Papers 839Repos

The Isabelle theorem prover is an interactive theorem prover, a Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core to ease logical correctness. 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). Read more on Wikipedia...


Example from Linguist:
theory HelloWorld imports Main begin section{*Playing around with Isabelle*} text{* creating a lemma with the name hello_world*} lemma hello_world: "True" by simp (*inspecting it*) thm hello_world text{* defining a string constant HelloWorld *} definition HelloWorld :: "string" where "HelloWorld \<equiv> ''Hello World!''" (*reversing HelloWorld twice yilds HelloWorld again*) theorem "rev (rev HelloWorld) = HelloWorld" by (fact List.rev_rev_ident) text{*now we delete the already proven List.rev_rev_ident lema and show it by hand*} declare List.rev_rev_ident[simp del] hide_fact List.rev_rev_ident (*It's trivial since we can just 'execute' it*) corollary "rev (rev HelloWorld) = HelloWorld" apply(simp add: HelloWorld_def) done text{*does it hold in general?*} theorem rev_rev_ident:"rev (rev l) = l" proof(induction l) case Nil thus ?case by simp next case (Cons l ls) assume IH: "rev (rev ls) = ls" have "rev (l#ls) = (rev ls) @ [l]" by simp hence "rev (rev (l#ls)) = rev ((rev ls) @ [l])" by simp also have "\<dots> = [l] @ rev (rev ls)" by simp finally show "rev (rev (l#ls)) = l#ls" using IH by simp qed corollary "\<forall>(l::string). rev (rev l) = l" by(fastforce intro: rev_rev_ident) end
Example from Wikipedia:
theorem sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" proof let ?x = "sqrt (real 2)" assume "?x ∈ ℚ" then obtain m n :: nat where sqrt_rat: "¦?x¦ = real m / real n" and lowest_terms: "coprime m n" by (rule Rats_abs_nat_div_natE) hence "real (m^2) = ?x^2 * real (n^2)" by (auto simp add: power2_eq_square) hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce hence "2 dvd m^2" by simp hence "2 dvd m" by simp have "2 dvd n" proof- from ‹2 dvd m› obtain k where "m = 2 * k" .. with eq have "2 * n^2 = 2^2 * k^2" by simp hence "2 dvd n^2" by simp thus "2 dvd n" by simp qed with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp thus False using odd_one by blast qed

Language features

Feature Supported Example Token
Binary Literals
Hexadecimals
Octals
Booleans True False
Comments
(* A comment
*)
MultiLine Comments
(* A comment
*)
(* *)
Semantic Indentation ϴ

Publications about Isabelle from Semantic Scholar

title authors year citations influentialCitations
General Bindings and Alpha-Equivalence in Nominal Isabelle Christian Urban and C. Kaliszyk 2011 66 12
Smart Testing of Functional Programs in Isabelle Lukas Bulwahn 2012 26 4
A Formalization of the C99 Standard in HOL, Isabelle and Coq R. Krebbers and F. Wiedijk 2011 14 0
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions C. Kaliszyk and Karol Pak 2017 5 0
c--.html · isabelle.html · wren.html

View source

PLDB - Build the next great programming language · v2022 · Day 32 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub · feedback@pldb.com