theory Scratch
  imports Main
begin

text‹
Given the function we want to execute multiple times is of
type \<^typ>‹unit ⇒ unit›.
›
fun pure_repeat :: "(unit ⇒ unit) ⇒ nat ⇒ unit" where
  "pure_repeat _ 0 = ()"
| "pure_repeat f (Suc n) = f (pure_repeat f n)"

text‹
Functions are pure in Isabelle. They don't have side effects.
This means, the \<^const>‹pure_repeat› we implemented is always equal
to \<^term>‹() :: unit›, independent of the function \<^typ>‹unit ⇒ unit›
or \<^typ>‹nat›.
Technically, functions are not even "executed", but only evaluated.
›
lemma "pure_repeat f n = ()" by simp

text‹
But we can repeat a value of \<^typ>‹'a› \<^term>‹n› times and return the result
in a list of length \<^term>‹n›
›
fun repeat :: "'a ⇒ nat ⇒ 'a list" where
  "repeat _ 0 = []"
| "repeat f (Suc n) = f # (repeat f n)"

lemma "repeat ''Hello'' 4 = [''Hello'', ''Hello'', ''Hello'', ''Hello'']"
  by code_simp

lemma "length (repeat a n) = n" by(induction n) simp+

text‹
Technically, \<^typ>‹'a› is not a function. We can wrap it in a dummy function
which takes a \<^typ>‹unit› as first argument. This gives a function of type
\<^typ>‹unit ⇒ 'a›.
›

fun fun_repeat :: "(unit ⇒ 'a) ⇒ nat ⇒ 'a list" where
  "fun_repeat _ 0 = []"
| "fun_repeat f (Suc n) = (f ()) # (fun_repeat f n)"

lemma "fun_repeat (λ_. ''Hello'') 4 =
       [''Hello'', ''Hello'', ''Hello'', ''Hello'']"
  by code_simp

text‹
Yet, \<^const>‹fun_repeat› with the dummy function \<^typ>‹unit ⇒ 'a› is
equivalent to \<^const>‹repeat› with the value \<^typ>‹'a› directly.
›
lemma "fun_repeat (λ_. a) n = repeat a n" by(induction n) simp+

end