56 lines
1.7 KiB
Plaintext
56 lines
1.7 KiB
Plaintext
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
|