src/HOL/Nat.thy
changeset 30971 7fbebf75b3ef
parent 30966 55104c664185
child 30975 b2fa60d56735
     1.1 --- a/src/HOL/Nat.thy	Fri Apr 24 08:24:54 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Apr 24 17:45:15 2009 +0200
     1.3 @@ -1166,31 +1166,58 @@
     1.4  
     1.5  subsection {* Natural operation of natural numbers on functions *}
     1.6  
     1.7 -text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *}
     1.8 +text {*
     1.9 +  We use the same logical constant for the power operations on
    1.10 +  functions and relations, in order to share the same syntax.
    1.11 +*}
    1.12 +
    1.13 +consts compow :: "nat \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.14 +
    1.15 +abbreviation compower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80) where
    1.16 +  "f ^^ n \<equiv> compow n f"
    1.17 +
    1.18 +notation (latex output)
    1.19 +  compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.20 +
    1.21 +notation (HTML output)
    1.22 +  compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.23 +
    1.24 +text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    1.25 +
    1.26 +overloading
    1.27 +  funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.28 +begin
    1.29  
    1.30  primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.31      "funpow 0 f = id"
    1.32    | "funpow (Suc n) f = f o funpow n f"
    1.33  
    1.34 -abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where
    1.35 -  "f o^ n \<equiv> funpow n f"
    1.36 +end
    1.37 +
    1.38 +text {* for code generation *}
    1.39 +
    1.40 +definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.41 +  funpow_code_def [code post]: "funpow = compow"
    1.42  
    1.43 -notation (latex output)
    1.44 -  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.45 +lemmas [code inline] = funpow_code_def [symmetric]
    1.46  
    1.47 -notation (HTML output)
    1.48 -  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.49 +lemma [code]:
    1.50 +  "funpow 0 f = id"
    1.51 +  "funpow (Suc n) f = f o funpow n f"
    1.52 +  unfolding funpow_code_def by simp_all
    1.53 +
    1.54 +definition "foo = id ^^ (1 + 1)"
    1.55  
    1.56  lemma funpow_add:
    1.57 -  "f o^ (m + n) = f o^ m \<circ> f o^ n"
    1.58 +  "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
    1.59    by (induct m) simp_all
    1.60  
    1.61  lemma funpow_swap1:
    1.62 -  "f ((f o^ n) x) = (f o^ n) (f x)"
    1.63 +  "f ((f ^^ n) x) = (f ^^ n) (f x)"
    1.64  proof -
    1.65 -  have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp
    1.66 -  also have "\<dots>  = (f o^ n o f o^ 1) x" by (simp only: funpow_add)
    1.67 -  also have "\<dots> = (f o^ n) (f x)" by simp
    1.68 +  have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
    1.69 +  also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
    1.70 +  also have "\<dots> = (f ^^ n) (f x)" by simp
    1.71    finally show ?thesis .
    1.72  qed
    1.73