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