src/HOLCF/Fix.thy
 changeset 27270 6a353260735e parent 27185 0407630909ef child 27316 9e74019041d4
equal inserted replaced
27269:1e9c05cddc64 27270:6a353260735e
`    31 by simp`
`    31 by simp`
`    32 `
`    32 `
`    33 declare iterate.simps [simp del]`
`    33 declare iterate.simps [simp del]`
`    34 `
`    34 `
`    35 lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"`
`    35 lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"`
`    36 by (induct_tac n, auto)`
`    36 by (induct n) simp_all`
`       `
`    37 `
`       `
`    38 lemma iterate_iterate:`
`       `
`    39   "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"`
`       `
`    40 by (induct m) simp_all`
`    37 `
`    41 `
`    38 text {*`
`    42 text {*`
`    39   The sequence of function iterations is a chain.`
`    43   The sequence of function iterations is a chain.`
`    40   This property is essential since monotonicity of iterate makes no sense.`
`    44   This property is essential since monotonicity of iterate makes no sense.`
`    41 *}`
`    45 *}`