Isabelle - Programming language

Isabelle is an open source programming language created in 1986.

#496on PLDB

38Years Old

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

Tags: programming language
There are at least 839 Isabelle repos on GitHub
Early development of Isabelle happened in University of Cambridge and Technische Universität München
The Google BigQuery Public Dataset GitHub snapshot shows 115 users using Isabelle in 137 repos on GitHub
Isabelle LSP implementation
Pygments supports syntax highlighting for Isabelle
GitHub supports syntax highlighting for Isabelle
See also: (2 related languages) Standard ML, Coq
Read more about Isabelle on the web: 1.

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	X