Isabelle is an open source programming language created in 1986.
| #498on 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...
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 | Example | Token |
|---|---|---|---|
| Binary Literals | ✓ | ||
| Hexadecimals | ✓ | ||
| Octals | ✓ | ||
| Booleans | ✓ | True False | |
| Comments | ✓ | (* A comment *) | |
| MultiLine Comments | ✓ | (* A comment *) | (* *) |
| Semantic Indentation | X |