--- a/NEWS Fri Apr 24 08:24:54 2009 +0200
+++ b/NEWS Fri Apr 24 17:45:15 2009 +0200
@@ -18,13 +18,9 @@
theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
div_mult_mult1 is now [simp] by default. INCOMPATIBILITY.
-* Power operations on relations and functions are now dedicated constants:
-
- relpow with infix syntax "^^"
- funpow with infix syntax "^o"
-
- Power operations on algebraic structures retains syntax "^" and is now defined
- generic in class recpower; class power disappeared. INCOMPATIBILITY.
+* Power operations on relations and functions are now one dedicate constant compow with
+infix syntax "^^". Power operations on multiplicative monoids retains syntax "^"
+and is now defined generic in class recpower; class power disappeared. INCOMPATIBILITY.
* ML antiquotation @{code_datatype} inserts definition of a datatype generated
by the code generator; see Predicate.thy for an example.
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Apr 24 17:45:15 2009 +0200
@@ -23,8 +23,8 @@
qed
lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
- assumes f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
- shows "horner F G n ((F o^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / real (f (j' + j))) * x ^ j)"
+ assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
+ shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / real (f (j' + j))) * x ^ j)"
proof (induct n arbitrary: i k j')
case (Suc n)
@@ -33,13 +33,13 @@
qed auto
lemma horner_bounds':
- assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
+ assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
and lb_0: "\<And> i k x. lb 0 i k x = 0"
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
- shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> horner F G n ((F o^ j') s) (f j') (Ifloat x) \<and>
- horner F G n ((F o^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)"
+ shows "Ifloat (lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') (Ifloat x) \<and>
+ horner F G n ((F ^^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F ^^ j') s) (f j') x)"
(is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
proof (induct n arbitrary: j')
case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
@@ -49,15 +49,15 @@
proof (rule add_mono)
show "Ifloat (lapprox_rat prec 1 (int (f j'))) \<le> 1 / real (f j')" using lapprox_rat[of prec 1 "int (f j')"] by auto
from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> Ifloat x`
- show "- Ifloat (x * ub n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x) \<le> - (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x))"
+ show "- Ifloat (x * ub n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x) \<le> - (Ifloat x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (Ifloat x))"
unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
qed
moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps Ifloat_sub diff_def
proof (rule add_mono)
show "1 / real (f j') \<le> Ifloat (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> Ifloat x`
- show "- (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x)) \<le>
- - Ifloat (x * lb n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x)"
+ show "- (Ifloat x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (Ifloat x)) \<le>
+ - Ifloat (x * lb n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x)"
unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
qed
ultimately show ?case by blast
@@ -73,13 +73,13 @@
*}
lemma horner_bounds: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
+ assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
and lb_0: "\<And> i k x. lb 0 i k x = 0"
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
- shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
- "(\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
+ shows "Ifloat (lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
+ "(\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
proof -
have "?lb \<and> ?ub"
using horner_bounds'[where lb=lb, OF `0 \<le> Ifloat x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
@@ -88,13 +88,13 @@
qed
lemma horner_bounds_nonpos: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
+ assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
and lb_0: "\<And> i k x. lb 0 i k x = 0"
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) + x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) + x * (lb n (F i) (G i k) x)"
- shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
- "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
+ shows "Ifloat (lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
+ "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
proof -
{ fix x y z :: float have "x - y * z = x + - y * z"
by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def uminus_float.simps times_float.simps algebra_simps)
@@ -794,8 +794,8 @@
let "?f n" = "fact (2 * n)"
{ fix n
- have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
- have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 1 * (((\<lambda>i. i + 2) o^ n) 1 + 1)"
+ have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
+ have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 1 * (((\<lambda>i. i + 2) ^^ n) 1 + 1)"
unfolding F by auto } note f_eq = this
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
@@ -905,8 +905,8 @@
let "?f n" = "fact (2 * n + 1)"
{ fix n
- have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
- have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 2 * (((\<lambda>i. i + 2) o^ n) 2 + 1)"
+ have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
+ have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
unfolding F by auto } note f_eq = this
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
@@ -1382,8 +1382,8 @@
shows "exp (Ifloat x) \<in> { Ifloat (lb_exp_horner prec (get_even n) 1 1 x) .. Ifloat (ub_exp_horner prec (get_odd n) 1 1 x) }"
proof -
{ fix n
- have F: "\<And> m. ((\<lambda>i. i + 1) o^ n) m = n + m" by (induct n, auto)
- have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) o^ n) 1" unfolding F by auto } note f_eq = this
+ have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
+ have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^^ n) 1" unfolding F by auto } note f_eq = this
note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
--- a/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 24 17:45:15 2009 +0200
@@ -2794,8 +2794,8 @@
by (import numeral numeral_fact)
lemma numeral_funpow: "ALL n::nat.
- ((f::'a::type => 'a::type) o^ n) (x::'a::type) =
- (if n = 0 then x else (f o^ (n - 1)) (f x))"
+ ((f::'a::type => 'a::type) ^^ n) (x::'a::type) =
+ (if n = 0 then x else (f ^^ (n - 1)) (f x))"
by (import numeral numeral_funpow)
;end_setup
--- a/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 24 17:45:15 2009 +0200
@@ -434,15 +434,15 @@
by (import word32 EQUIV_QT)
lemma FUNPOW_THM: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
- (f o^ n) (f x) = f ((f o^ n) x)"
+ (f ^^ n) (f x) = f ((f ^^ n) x)"
by (import word32 FUNPOW_THM)
lemma FUNPOW_THM2: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
- (f o^ Suc n) x = f ((f o^ n) x)"
+ (f ^^ Suc n) x = f ((f ^^ n) x)"
by (import word32 FUNPOW_THM2)
lemma FUNPOW_COMP: "ALL (f::'a::type => 'a::type) (m::nat) (n::nat) a::'a::type.
- (f o^ m) ((f o^ n) a) = (f o^ (m + n)) a"
+ (f ^^ m) ((f ^^ n) a) = (f ^^ (m + n)) a"
by (import word32 FUNPOW_COMP)
lemma INw_MODw: "ALL n::nat. INw (MODw n)"
@@ -1170,23 +1170,23 @@
constdefs
word_lsr :: "word32 => nat => word32"
- "word_lsr == %(a::word32) n::nat. (word_lsr1 o^ n) a"
+ "word_lsr == %(a::word32) n::nat. (word_lsr1 ^^ n) a"
-lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 o^ n) a"
+lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 ^^ n) a"
by (import word32 word_lsr)
constdefs
word_asr :: "word32 => nat => word32"
- "word_asr == %(a::word32) n::nat. (word_asr1 o^ n) a"
+ "word_asr == %(a::word32) n::nat. (word_asr1 ^^ n) a"
-lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 o^ n) a"
+lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 ^^ n) a"
by (import word32 word_asr)
constdefs
word_ror :: "word32 => nat => word32"
- "word_ror == %(a::word32) n::nat. (word_ror1 o^ n) a"
+ "word_ror == %(a::word32) n::nat. (word_ror1 ^^ n) a"
-lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 o^ n) a"
+lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 ^^ n) a"
by (import word32 word_ror)
consts
--- a/src/HOL/Import/HOL4Compat.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Fri Apr 24 17:45:15 2009 +0200
@@ -202,13 +202,13 @@
constdefs
FUNPOW :: "('a => 'a) => nat => 'a => 'a"
- "FUNPOW f n == f o^ n"
+ "FUNPOW f n == f ^^ n"
-lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
- (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
+lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
+ (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))"
by (simp add: funpow_swap1)
-lemma [hol4rew]: "FUNPOW f n = f o^ n"
+lemma [hol4rew]: "FUNPOW f n = f ^^ n"
by (simp add: FUNPOW_def)
lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
--- a/src/HOL/Library/Coinductive_List.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy Fri Apr 24 17:45:15 2009 +0200
@@ -786,7 +786,7 @@
lemma funpow_lmap:
fixes f :: "'a \<Rightarrow> 'a"
- shows "(lmap f o^ n) (LCons b l) = LCons ((f o^ n) b) ((lmap f o^ n) l)"
+ shows "(lmap f ^^ n) (LCons b l) = LCons ((f ^^ n) b) ((lmap f ^^ n) l)"
by (induct n) simp_all
@@ -796,35 +796,35 @@
proof
fix x
have "(h x, iterates f x) \<in>
- {((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u)) | u n. True}"
+ {((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u)) | u n. True}"
proof -
- have "(h x, iterates f x) = ((lmap f o^ 0) (h x), (lmap f o^ 0) (iterates f x))"
+ have "(h x, iterates f x) = ((lmap f ^^ 0) (h x), (lmap f ^^ 0) (iterates f x))"
by simp
then show ?thesis by blast
qed
then show "h x = iterates f x"
proof (coinduct rule: llist_equalityI)
case (Eqllist q)
- then obtain u n where "q = ((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u))"
+ then obtain u n where "q = ((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u))"
(is "_ = (?q1, ?q2)")
by auto
- also have "?q1 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (h u))"
+ also have "?q1 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (h u))"
proof -
- have "?q1 = (lmap f o^ n) (LCons u (lmap f (h u)))"
+ have "?q1 = (lmap f ^^ n) (LCons u (lmap f (h u)))"
by (subst h) rule
- also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (lmap f (h u)))"
+ also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (lmap f (h u)))"
by (rule funpow_lmap)
- also have "(lmap f o^ n) (lmap f (h u)) = (lmap f o^ Suc n) (h u)"
+ also have "(lmap f ^^ n) (lmap f (h u)) = (lmap f ^^ Suc n) (h u)"
by (simp add: funpow_swap1)
finally show ?thesis .
qed
- also have "?q2 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (iterates f u))"
+ also have "?q2 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (iterates f u))"
proof -
- have "?q2 = (lmap f o^ n) (LCons u (iterates f (f u)))"
+ have "?q2 = (lmap f ^^ n) (LCons u (iterates f (f u)))"
by (subst iterates) rule
- also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (iterates f (f u)))"
+ also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (iterates f (f u)))"
by (rule funpow_lmap)
- also have "(lmap f o^ n) (iterates f (f u)) = (lmap f o^ Suc n) (iterates f u)"
+ also have "(lmap f ^^ n) (iterates f (f u)) = (lmap f ^^ Suc n) (iterates f u)"
by (simp add: lmap_iterates funpow_swap1)
finally show ?thesis .
qed
--- a/src/HOL/Library/Continuity.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Library/Continuity.thy Fri Apr 24 17:45:15 2009 +0200
@@ -48,25 +48,25 @@
qed
lemma continuous_lfp:
- assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
+ assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)"
proof -
note mono = continuous_mono[OF `continuous F`]
- { fix i have "(F o^ i) bot \<le> lfp F"
+ { fix i have "(F ^^ i) bot \<le> lfp F"
proof (induct i)
- show "(F o^ 0) bot \<le> lfp F" by simp
+ show "(F ^^ 0) bot \<le> lfp F" by simp
next
case (Suc i)
- have "(F o^ Suc i) bot = F((F o^ i) bot)" by simp
+ have "(F ^^ Suc i) bot = F((F ^^ i) bot)" by simp
also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
finally show ?case .
qed }
- hence "(SUP i. (F o^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
- moreover have "lfp F \<le> (SUP i. (F o^ i) bot)" (is "_ \<le> ?U")
+ hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
+ moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
proof (rule lfp_lowerbound)
- have "chain(%i. (F o^ i) bot)"
+ have "chain(%i. (F ^^ i) bot)"
proof -
- { fix i have "(F o^ i) bot \<le> (F o^ (Suc i)) bot"
+ { fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
proof (induct i)
case 0 show ?case by simp
next
@@ -74,7 +74,7 @@
qed }
thus ?thesis by(auto simp add:chain_def)
qed
- hence "F ?U = (SUP i. (F o^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
+ hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
finally show "F ?U \<le> ?U" .
qed
@@ -193,7 +193,7 @@
definition
up_iterate :: "('a set => 'a set) => nat => 'a set" where
- "up_iterate f n = (f o^ n) {}"
+ "up_iterate f n = (f ^^ n) {}"
lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
by (simp add: up_iterate_def)
@@ -245,7 +245,7 @@
definition
down_iterate :: "('a set => 'a set) => nat => 'a set" where
- "down_iterate f n = (f o^ n) UNIV"
+ "down_iterate f n = (f ^^ n) UNIV"
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
by (simp add: down_iterate_def)
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Apr 24 17:45:15 2009 +0200
@@ -1007,13 +1007,13 @@
by simp
lemma XDN_linear:
- "(XD o^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD o^ n) a + fps_const d * (XD o^ n) (b :: ('a::comm_ring_1) fps)"
+ "(XD ^^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)"
by (induct n, simp_all)
lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
lemma fps_mult_XD_shift:
- "(XD o^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+ "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
--- a/src/HOL/List.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/List.thy Fri Apr 24 17:45:15 2009 +0200
@@ -198,7 +198,7 @@
definition
rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "rotate n = rotate1 o^ n"
+ "rotate n = rotate1 ^^ n"
definition
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
--- a/src/HOL/Nat.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Nat.thy Fri Apr 24 17:45:15 2009 +0200
@@ -1166,31 +1166,58 @@
subsection {* Natural operation of natural numbers on functions *}
-text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *}
+text {*
+ We use the same logical constant for the power operations on
+ functions and relations, in order to share the same syntax.
+*}
+
+consts compow :: "nat \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+
+abbreviation compower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80) where
+ "f ^^ n \<equiv> compow n f"
+
+notation (latex output)
+ compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+
+notation (HTML output)
+ compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+
+text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
+
+overloading
+ funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
+begin
primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
"funpow 0 f = id"
| "funpow (Suc n) f = f o funpow n f"
-abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where
- "f o^ n \<equiv> funpow n f"
+end
+
+text {* for code generation *}
+
+definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ funpow_code_def [code post]: "funpow = compow"
-notation (latex output)
- funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+lemmas [code inline] = funpow_code_def [symmetric]
-notation (HTML output)
- funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+lemma [code]:
+ "funpow 0 f = id"
+ "funpow (Suc n) f = f o funpow n f"
+ unfolding funpow_code_def by simp_all
+
+definition "foo = id ^^ (1 + 1)"
lemma funpow_add:
- "f o^ (m + n) = f o^ m \<circ> f o^ n"
+ "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
by (induct m) simp_all
lemma funpow_swap1:
- "f ((f o^ n) x) = (f o^ n) (f x)"
+ "f ((f ^^ n) x) = (f ^^ n) (f x)"
proof -
- have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp
- also have "\<dots> = (f o^ n o f o^ 1) x" by (simp only: funpow_add)
- also have "\<dots> = (f o^ n) (f x)" by simp
+ have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
+ also have "\<dots> = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
+ also have "\<dots> = (f ^^ n) (f x)" by simp
finally show ?thesis .
qed
--- a/src/HOL/SizeChange/Interpretation.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/SizeChange/Interpretation.thy Fri Apr 24 17:45:15 2009 +0200
@@ -35,7 +35,7 @@
and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)"
by blast
- let ?s = "\<lambda>i. (f o^ i) x"
+ let ?s = "\<lambda>i. (f ^^ i) x"
{
fix i
--- a/src/HOL/Transitive_Closure.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri Apr 24 17:45:15 2009 +0200
@@ -634,18 +634,19 @@
text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
-primrec relpow :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set" (infixr "^^" 80) where
- "R ^^ 0 = Id"
- | "R ^^ Suc n = R O (R ^^ n)"
+overloading
+ relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
+begin
-notation (latex output)
- relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
+ "relpow 0 R = Id"
+ | "relpow (Suc n) R = R O (R ^^ n)"
-notation (HTML output)
- relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+end
lemma rel_pow_1 [simp]:
- "R ^^ 1 = R"
+ fixes R :: "('a \<times> 'a) set"
+ shows "R ^^ 1 = R"
by simp
lemma rel_pow_0_I:
@@ -741,7 +742,7 @@
apply (rule iffI)
apply (drule tranclD2)
apply (clarsimp simp: rtrancl_is_UN_rel_pow)
- apply (rule_tac x="Suc x" in exI)
+ apply (rule_tac x="Suc n" in exI)
apply (clarsimp simp: rel_comp_def)
apply fastsimp
apply clarsimp
--- a/src/HOL/UNITY/Transformers.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Fri Apr 24 17:45:15 2009 +0200
@@ -338,10 +338,10 @@
constdefs
wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"
- "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
+ "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
wens_single :: "[('a*'a) set, 'a set] => 'a set"
- "wens_single act B == \<Union>i. (wp act o^ i) B"
+ "wens_single act B == \<Union>i. (wp act ^^ i) B"
lemma wens_single_Un_eq:
"single_valued act
--- a/src/HOL/Word/BinBoolList.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy Fri Apr 24 17:45:15 2009 +0200
@@ -38,7 +38,7 @@
if y then rbl_add ws x else ws)"
lemma butlast_power:
- "(butlast o^ n) bl = take (length bl - n) bl"
+ "(butlast ^^ n) bl = take (length bl - n) bl"
by (induct n) (auto simp: butlast_take)
lemma bin_to_bl_aux_Pls_minus_simp [simp]:
@@ -370,14 +370,14 @@
done
lemma nth_rest_power_bin [rule_format] :
- "ALL n. bin_nth ((bin_rest o^ k) w) n = bin_nth w (n + k)"
+ "ALL n. bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
apply (induct k, clarsimp)
apply clarsimp
apply (simp only: bin_nth.Suc [symmetric] add_Suc)
done
lemma take_rest_power_bin:
- "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest o^ (n - m)) w)"
+ "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
--- a/src/HOL/Word/BinGeneral.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Apr 24 17:45:15 2009 +0200
@@ -822,8 +822,8 @@
by (induct n) auto
lemma bin_rest_power_trunc [rule_format] :
- "(bin_rest o^ k) (bintrunc n bin) =
- bintrunc (n - k) ((bin_rest o^ k) bin)"
+ "(bin_rest ^^ k) (bintrunc n bin) =
+ bintrunc (n - k) ((bin_rest ^^ k) bin)"
by (induct k) (auto simp: bin_rest_trunc)
lemma bin_rest_trunc_i:
@@ -857,7 +857,7 @@
by (rule ext) auto
lemma rco_lem:
- "f o g o f = g o f ==> f o (g o f) o^ n = g o^ n o f"
+ "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f"
apply (rule ext)
apply (induct_tac n)
apply (simp_all (no_asm))
@@ -867,7 +867,7 @@
apply simp
done
-lemma rco_alt: "(f o g) o^ n o f = f o (g o f) o^ n"
+lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n"
apply (rule ext)
apply (induct n)
apply (simp_all add: o_def)
@@ -892,7 +892,7 @@
subsection {* Miscellaneous lemmas *}
lemma funpow_minus_simp:
- "0 < n \<Longrightarrow> f o^ n = f \<circ> f o^ (n - 1)"
+ "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
by (cases n) simp_all
lemmas funpow_pred_simp [simp] =
--- a/src/HOL/Word/TdThs.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Word/TdThs.thy Fri Apr 24 17:45:15 2009 +0200
@@ -110,7 +110,7 @@
done
lemma fn_comm_power:
- "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n"
+ "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n"
apply (rule ext)
apply (induct n)
apply (auto dest: fun_cong)
--- a/src/HOL/Word/WordDefinition.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy Fri Apr 24 17:45:15 2009 +0200
@@ -203,10 +203,10 @@
"shiftr1 w = word_of_int (bin_rest (uint w))"
definition
- shiftl_def: "w << n = (shiftl1 o^ n) w"
+ shiftl_def: "w << n = (shiftl1 ^^ n) w"
definition
- shiftr_def: "w >> n = (shiftr1 o^ n) w"
+ shiftr_def: "w >> n = (shiftr1 ^^ n) w"
instance ..
@@ -241,7 +241,7 @@
"bshiftr1 b w == of_bl (b # butlast (to_bl w))"
sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
- "w >>> n == (sshiftr1 o^ n) w"
+ "w >>> n == (sshiftr1 ^^ n) w"
mask :: "nat => 'a::len word"
"mask n == (1 << n) - 1"
@@ -264,7 +264,7 @@
case ys of [] => [] | x # xs => last ys # butlast ys"
rotater :: "nat => 'a list => 'a list"
- "rotater n == rotater1 o^ n"
+ "rotater n == rotater1 ^^ n"
word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
"word_rotr n w == of_bl (rotater n (to_bl w))"
--- a/src/HOL/Word/WordShift.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Word/WordShift.thy Fri Apr 24 17:45:15 2009 +0200
@@ -361,14 +361,14 @@
lemma shiftr_no':
"w = number_of bin ==>
- (w::'a::len0 word) >> n = number_of ((bin_rest o^ n) (bintrunc (size w) bin))"
+ (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
apply clarsimp
apply (rule word_eqI)
apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
done
lemma sshiftr_no':
- "w = number_of bin ==> w >>> n = number_of ((bin_rest o^ n)
+ "w = number_of bin ==> w >>> n = number_of ((bin_rest ^^ n)
(sbintrunc (size w - 1) bin))"
apply clarsimp
apply (rule word_eqI)