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