23 lines
524 B
Plaintext
23 lines
524 B
Plaintext
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
|