23 lines
524 B
Text
23 lines
524 B
Text
|
theory Scratch
|
|||
|
|
imports Main
|
|||
|
|
begin
|
|||
|
|
|
|||
|
|
text‹if-then-else›
|
|||
|
|
lemma "(if True then 42 else 0) = 42" by simp
|
|||
|
|
|
|||
|
|
text‹case statement with pattern matching, which evaluates to the True-case›
|
|||
|
|
lemma "case [42] of
|
|||
|
|
Nil ⇒ False
|
|||
|
|
| [x] ⇒ True
|
|||
|
|
| x#xs ⇒ False" by simp
|
|||
|
|
|
|||
|
|
text‹Loops are implemented via recursive functions›
|
|||
|
|
fun recurse :: "nat ⇒ nat" where
|
|||
|
|
"recurse 0 = 0"
|
|||
|
|
| "recurse (Suc n) = recurse n"
|
|||
|
|
|
|||
|
|
text‹The function always returns zero.›
|
|||
|
|
lemma "recurse n = 0" by(induction n) simp+
|
|||
|
|
|
|||
|
|
end
|