src/HOL/Nat.thy
changeset 30954 cf50e67bc1d1
parent 30686 47a32dd1b86e
child 30966 55104c664185
     1.1 --- a/src/HOL/Nat.thy	Mon Apr 20 09:32:09 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Apr 20 09:32:40 2009 +0200
     1.3 @@ -1164,6 +1164,37 @@
     1.4  end
     1.5  
     1.6  
     1.7 +subsection {* Natural operation of natural numbers on functions *}
     1.8 +
     1.9 +text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    1.10 +
    1.11 +primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.12 +    "funpow 0 f = id"
    1.13 +  | "funpow (Suc n) f = f o funpow n f"
    1.14 +
    1.15 +abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where
    1.16 +  "f o^ n \<equiv> funpow n f"
    1.17 +
    1.18 +notation (latex output)
    1.19 +  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.20 +
    1.21 +notation (HTML output)
    1.22 +  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.23 +
    1.24 +lemma funpow_add:
    1.25 +  "f o^ (m + n) = f o^ m \<circ> f o^ n"
    1.26 +  by (induct m) simp_all
    1.27 +
    1.28 +lemma funpow_swap1:
    1.29 +  "f ((f o^ n) x) = (f o^ n) (f x)"
    1.30 +proof -
    1.31 +  have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp
    1.32 +  also have "\<dots>  = (f o^ n o f o^ 1) x" by (simp only: funpow_add)
    1.33 +  also have "\<dots> = (f o^ n) (f x)" by simp
    1.34 +  finally show ?thesis .
    1.35 +qed
    1.36 +
    1.37 +
    1.38  subsection {* Embedding of the Naturals into any
    1.39    @{text semiring_1}: @{term of_nat} *}
    1.40