Isabelle is a programming language created in 1986.
#269on PLDB  37Years Old  576Users 
0Books  4Papers  839Repos 
The Isabelle theorem prover is an interactive theorem prover, a Higher Order Logic (HOL) theorem prover. It is an LCFstyle 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 metalogic (a weak type theory), which is used to encode object logics like firstorder logic (FOL), higherorder logic (HOL) or Zermeloâ€“Fraenkel set theory (ZFC). Read more on Wikipedia...
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
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
Feature  Supported  Token  Example 

Binary Literals  âœ“  
Hexadecimals  âœ“  
Octals  âœ“  
Booleans  âœ“  True False  
Comments  âœ“  (* A comment *) 

MultiLine Comments  âœ“  (* *)  (* A comment *) 
Semantic Indentation  X 
title  authors  year  citations  influentialCitations 

General Bindings and AlphaEquivalence 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 