equal
deleted
inserted
replaced
10 |
10 |
11 defaultsort pcpo |
11 defaultsort pcpo |
12 |
12 |
13 subsection {* Iteration *} |
13 subsection {* Iteration *} |
14 |
14 |
15 consts |
15 primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where |
16 iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" |
16 "iterate 0 = (\<Lambda> F x. x)" |
17 |
17 | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))" |
18 primrec |
|
19 "iterate 0 = (\<Lambda> F x. x)" |
|
20 "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))" |
|
21 |
18 |
22 text {* Derive inductive properties of iterate from primitive recursion *} |
19 text {* Derive inductive properties of iterate from primitive recursion *} |
23 |
20 |
24 lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x" |
21 lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x" |
25 by simp |
22 by simp |