mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
d9f17a65dd
Also, Isabelle is very polular in academia. See for example http://scholar.google.de/scholar?q=isabelle%2FHOL In around 40 days, the seL4 microkernel [1] with its Isabelle proofs is (probably) released on github [2]. [1] http://sel4.systems/ [2] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-June/msg00011.html
47 lines
1.2 KiB
Plaintext
47 lines
1.2 KiB
Plaintext
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
|