equal
deleted
inserted
replaced
1162 intro: order_less_imp_le antisym elim!: order_trans order_less_trans) |
1162 intro: order_less_imp_le antisym elim!: order_trans order_less_trans) |
1163 |
1163 |
1164 end |
1164 end |
1165 |
1165 |
1166 |
1166 |
|
1167 subsection {* Natural operation of natural numbers on functions *} |
|
1168 |
|
1169 text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *} |
|
1170 |
|
1171 primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
1172 "funpow 0 f = id" |
|
1173 | "funpow (Suc n) f = f o funpow n f" |
|
1174 |
|
1175 abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where |
|
1176 "f o^ n \<equiv> funpow n f" |
|
1177 |
|
1178 notation (latex output) |
|
1179 funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
|
1180 |
|
1181 notation (HTML output) |
|
1182 funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
|
1183 |
|
1184 lemma funpow_add: |
|
1185 "f o^ (m + n) = f o^ m \<circ> f o^ n" |
|
1186 by (induct m) simp_all |
|
1187 |
|
1188 lemma funpow_swap1: |
|
1189 "f ((f o^ n) x) = (f o^ n) (f x)" |
|
1190 proof - |
|
1191 have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp |
|
1192 also have "\<dots> = (f o^ n o f o^ 1) x" by (simp only: funpow_add) |
|
1193 also have "\<dots> = (f o^ n) (f x)" by simp |
|
1194 finally show ?thesis . |
|
1195 qed |
|
1196 |
|
1197 |
1167 subsection {* Embedding of the Naturals into any |
1198 subsection {* Embedding of the Naturals into any |
1168 @{text semiring_1}: @{term of_nat} *} |
1199 @{text semiring_1}: @{term of_nat} *} |
1169 |
1200 |
1170 context semiring_1 |
1201 context semiring_1 |
1171 begin |
1202 begin |