funpow and relpow with shared "^^" syntax
authorhaftmann
Fri Apr 24 17:45:15 2009 +0200 (2009-04-24)
changeset 309717fbebf75b3ef
parent 30970 3fe2e418a071
child 30972 5b65835ccc92
funpow and relpow with shared "^^" syntax
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Import/HOL/HOL4Base.thy
src/HOL/Import/HOL/HOL4Word32.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/SizeChange/Interpretation.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Transformers.thy
src/HOL/Word/BinBoolList.thy
src/HOL/Word/BinGeneral.thy
src/HOL/Word/TdThs.thy
src/HOL/Word/WordDefinition.thy
src/HOL/Word/WordShift.thy
     1.1 --- a/NEWS	Fri Apr 24 08:24:54 2009 +0200
     1.2 +++ b/NEWS	Fri Apr 24 17:45:15 2009 +0200
     1.3 @@ -18,13 +18,9 @@
     1.4  theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
     1.5  div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
     1.6  
     1.7 -* Power operations on relations and functions are now dedicated constants:
     1.8 -
     1.9 -    relpow with infix syntax "^^"
    1.10 -    funpow with infix syntax "^o"
    1.11 -
    1.12 -  Power operations on algebraic structures retains syntax "^" and is now defined
    1.13 -  generic in class recpower; class power disappeared.  INCOMPATIBILITY.
    1.14 +* Power operations on relations and functions are now one dedicate constant compow with
    1.15 +infix syntax "^^".  Power operations on multiplicative monoids retains syntax "^"
    1.16 +and is now defined generic in class recpower; class power disappeared.  INCOMPATIBILITY.
    1.17  
    1.18  * ML antiquotation @{code_datatype} inserts definition of a datatype generated
    1.19  by the code generator; see Predicate.thy for an example.
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 24 08:24:54 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 24 17:45:15 2009 +0200
     2.3 @@ -23,8 +23,8 @@
     2.4  qed
     2.5  
     2.6  lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
     2.7 -  assumes f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
     2.8 -  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)"
     2.9 +  assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    2.10 +  shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / real (f (j' + j))) * x ^ j)"
    2.11  proof (induct n arbitrary: i k j')
    2.12    case (Suc n)
    2.13  
    2.14 @@ -33,13 +33,13 @@
    2.15  qed auto
    2.16  
    2.17  lemma horner_bounds':
    2.18 -  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
    2.19 +  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    2.20    and lb_0: "\<And> i k x. lb 0 i k x = 0"
    2.21    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)"
    2.22    and ub_0: "\<And> i k x. ub 0 i k x = 0"
    2.23    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)"
    2.24 -  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> 
    2.25 -         horner F G n ((F o^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)"
    2.26 +  shows "Ifloat (lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') (Ifloat x) \<and> 
    2.27 +         horner F G n ((F ^^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F ^^ j') s) (f j') x)"
    2.28    (is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
    2.29  proof (induct n arbitrary: j')
    2.30    case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
    2.31 @@ -49,15 +49,15 @@
    2.32    proof (rule add_mono)
    2.33      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
    2.34      from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> Ifloat x`
    2.35 -    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))"
    2.36 +    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))"
    2.37        unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
    2.38    qed
    2.39    moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps Ifloat_sub diff_def
    2.40    proof (rule add_mono)
    2.41      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
    2.42      from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> Ifloat x`
    2.43 -    show "- (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x)) \<le> 
    2.44 -          - Ifloat (x * lb n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x)"
    2.45 +    show "- (Ifloat x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (Ifloat x)) \<le> 
    2.46 +          - Ifloat (x * lb n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x)"
    2.47        unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
    2.48    qed
    2.49    ultimately show ?case by blast
    2.50 @@ -73,13 +73,13 @@
    2.51  *}
    2.52  
    2.53  lemma horner_bounds: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.54 -  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
    2.55 +  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    2.56    and lb_0: "\<And> i k x. lb 0 i k x = 0"
    2.57    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)"
    2.58    and ub_0: "\<And> i k x. ub 0 i k x = 0"
    2.59    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)"
    2.60 -  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 
    2.61 -    "(\<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")
    2.62 +  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 
    2.63 +    "(\<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")
    2.64  proof -
    2.65    have "?lb  \<and> ?ub" 
    2.66      using horner_bounds'[where lb=lb, OF `0 \<le> Ifloat x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
    2.67 @@ -88,13 +88,13 @@
    2.68  qed
    2.69  
    2.70  lemma horner_bounds_nonpos: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.71 -  assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
    2.72 +  assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    2.73    and lb_0: "\<And> i k x. lb 0 i k x = 0"
    2.74    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)"
    2.75    and ub_0: "\<And> i k x. ub 0 i k x = 0"
    2.76    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)"
    2.77 -  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 
    2.78 -    "(\<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")
    2.79 +  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 
    2.80 +    "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
    2.81  proof -
    2.82    { fix x y z :: float have "x - y * z = x + - y * z"
    2.83        by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def uminus_float.simps times_float.simps algebra_simps)
    2.84 @@ -794,8 +794,8 @@
    2.85    let "?f n" = "fact (2 * n)"
    2.86  
    2.87    { fix n 
    2.88 -    have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
    2.89 -    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 1 * (((\<lambda>i. i + 2) o^ n) 1 + 1)"
    2.90 +    have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
    2.91 +    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 1 * (((\<lambda>i. i + 2) ^^ n) 1 + 1)"
    2.92        unfolding F by auto } note f_eq = this
    2.93      
    2.94    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0, 
    2.95 @@ -905,8 +905,8 @@
    2.96    let "?f n" = "fact (2 * n + 1)"
    2.97  
    2.98    { fix n 
    2.99 -    have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
   2.100 -    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 2 * (((\<lambda>i. i + 2) o^ n) 2 + 1)"
   2.101 +    have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
   2.102 +    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
   2.103        unfolding F by auto } note f_eq = this
   2.104      
   2.105    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
   2.106 @@ -1382,8 +1382,8 @@
   2.107    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) }"
   2.108  proof -
   2.109    { fix n
   2.110 -    have F: "\<And> m. ((\<lambda>i. i + 1) o^ n) m = n + m" by (induct n, auto)
   2.111 -    have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) o^ n) 1" unfolding F by auto } note f_eq = this
   2.112 +    have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
   2.113 +    have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^^ n) 1" unfolding F by auto } note f_eq = this
   2.114      
   2.115    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,
   2.116      OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
     3.1 --- a/src/HOL/Import/HOL/HOL4Base.thy	Fri Apr 24 08:24:54 2009 +0200
     3.2 +++ b/src/HOL/Import/HOL/HOL4Base.thy	Fri Apr 24 17:45:15 2009 +0200
     3.3 @@ -2794,8 +2794,8 @@
     3.4    by (import numeral numeral_fact)
     3.5  
     3.6  lemma numeral_funpow: "ALL n::nat.
     3.7 -   ((f::'a::type => 'a::type) o^ n) (x::'a::type) =
     3.8 -   (if n = 0 then x else (f o^ (n - 1)) (f x))"
     3.9 +   ((f::'a::type => 'a::type) ^^ n) (x::'a::type) =
    3.10 +   (if n = 0 then x else (f ^^ (n - 1)) (f x))"
    3.11    by (import numeral numeral_funpow)
    3.12  
    3.13  ;end_setup
     4.1 --- a/src/HOL/Import/HOL/HOL4Word32.thy	Fri Apr 24 08:24:54 2009 +0200
     4.2 +++ b/src/HOL/Import/HOL/HOL4Word32.thy	Fri Apr 24 17:45:15 2009 +0200
     4.3 @@ -434,15 +434,15 @@
     4.4    by (import word32 EQUIV_QT)
     4.5  
     4.6  lemma FUNPOW_THM: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
     4.7 -   (f o^ n) (f x) = f ((f o^ n) x)"
     4.8 +   (f ^^ n) (f x) = f ((f ^^ n) x)"
     4.9    by (import word32 FUNPOW_THM)
    4.10  
    4.11  lemma FUNPOW_THM2: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
    4.12 -   (f o^ Suc n) x = f ((f o^ n) x)"
    4.13 +   (f ^^ Suc n) x = f ((f ^^ n) x)"
    4.14    by (import word32 FUNPOW_THM2)
    4.15  
    4.16  lemma FUNPOW_COMP: "ALL (f::'a::type => 'a::type) (m::nat) (n::nat) a::'a::type.
    4.17 -   (f o^ m) ((f o^ n) a) = (f o^ (m + n)) a"
    4.18 +   (f ^^ m) ((f ^^ n) a) = (f ^^ (m + n)) a"
    4.19    by (import word32 FUNPOW_COMP)
    4.20  
    4.21  lemma INw_MODw: "ALL n::nat. INw (MODw n)"
    4.22 @@ -1170,23 +1170,23 @@
    4.23  
    4.24  constdefs
    4.25    word_lsr :: "word32 => nat => word32" 
    4.26 -  "word_lsr == %(a::word32) n::nat. (word_lsr1 o^ n) a"
    4.27 +  "word_lsr == %(a::word32) n::nat. (word_lsr1 ^^ n) a"
    4.28  
    4.29 -lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 o^ n) a"
    4.30 +lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 ^^ n) a"
    4.31    by (import word32 word_lsr)
    4.32  
    4.33  constdefs
    4.34    word_asr :: "word32 => nat => word32" 
    4.35 -  "word_asr == %(a::word32) n::nat. (word_asr1 o^ n) a"
    4.36 +  "word_asr == %(a::word32) n::nat. (word_asr1 ^^ n) a"
    4.37  
    4.38 -lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 o^ n) a"
    4.39 +lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 ^^ n) a"
    4.40    by (import word32 word_asr)
    4.41  
    4.42  constdefs
    4.43    word_ror :: "word32 => nat => word32" 
    4.44 -  "word_ror == %(a::word32) n::nat. (word_ror1 o^ n) a"
    4.45 +  "word_ror == %(a::word32) n::nat. (word_ror1 ^^ n) a"
    4.46  
    4.47 -lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 o^ n) a"
    4.48 +lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 ^^ n) a"
    4.49    by (import word32 word_ror)
    4.50  
    4.51  consts
     5.1 --- a/src/HOL/Import/HOL4Compat.thy	Fri Apr 24 08:24:54 2009 +0200
     5.2 +++ b/src/HOL/Import/HOL4Compat.thy	Fri Apr 24 17:45:15 2009 +0200
     5.3 @@ -202,13 +202,13 @@
     5.4  
     5.5  constdefs
     5.6    FUNPOW :: "('a => 'a) => nat => 'a => 'a"
     5.7 -  "FUNPOW f n == f o^ n"
     5.8 +  "FUNPOW f n == f ^^ n"
     5.9  
    5.10 -lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
    5.11 -  (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
    5.12 +lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
    5.13 +  (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))"
    5.14    by (simp add: funpow_swap1)
    5.15  
    5.16 -lemma [hol4rew]: "FUNPOW f n = f o^ n"
    5.17 +lemma [hol4rew]: "FUNPOW f n = f ^^ n"
    5.18    by (simp add: FUNPOW_def)
    5.19  
    5.20  lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
     6.1 --- a/src/HOL/Library/Coinductive_List.thy	Fri Apr 24 08:24:54 2009 +0200
     6.2 +++ b/src/HOL/Library/Coinductive_List.thy	Fri Apr 24 17:45:15 2009 +0200
     6.3 @@ -786,7 +786,7 @@
     6.4  
     6.5  lemma funpow_lmap:
     6.6    fixes f :: "'a \<Rightarrow> 'a"
     6.7 -  shows "(lmap f o^ n) (LCons b l) = LCons ((f o^ n) b) ((lmap f o^ n) l)"
     6.8 +  shows "(lmap f ^^ n) (LCons b l) = LCons ((f ^^ n) b) ((lmap f ^^ n) l)"
     6.9    by (induct n) simp_all
    6.10  
    6.11  
    6.12 @@ -796,35 +796,35 @@
    6.13  proof
    6.14    fix x
    6.15    have "(h x, iterates f x) \<in>
    6.16 -      {((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u)) | u n. True}"
    6.17 +      {((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u)) | u n. True}"
    6.18    proof -
    6.19 -    have "(h x, iterates f x) = ((lmap f o^ 0) (h x), (lmap f o^ 0) (iterates f x))"
    6.20 +    have "(h x, iterates f x) = ((lmap f ^^ 0) (h x), (lmap f ^^ 0) (iterates f x))"
    6.21        by simp
    6.22      then show ?thesis by blast
    6.23    qed
    6.24    then show "h x = iterates f x"
    6.25    proof (coinduct rule: llist_equalityI)
    6.26      case (Eqllist q)
    6.27 -    then obtain u n where "q = ((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u))"
    6.28 +    then obtain u n where "q = ((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u))"
    6.29          (is "_ = (?q1, ?q2)")
    6.30        by auto
    6.31 -    also have "?q1 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (h u))"
    6.32 +    also have "?q1 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (h u))"
    6.33      proof -
    6.34 -      have "?q1 = (lmap f o^ n) (LCons u (lmap f (h u)))"
    6.35 +      have "?q1 = (lmap f ^^ n) (LCons u (lmap f (h u)))"
    6.36          by (subst h) rule
    6.37 -      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (lmap f (h u)))"
    6.38 +      also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (lmap f (h u)))"
    6.39          by (rule funpow_lmap)
    6.40 -      also have "(lmap f o^ n) (lmap f (h u)) = (lmap f o^ Suc n) (h u)"
    6.41 +      also have "(lmap f ^^ n) (lmap f (h u)) = (lmap f ^^ Suc n) (h u)"
    6.42          by (simp add: funpow_swap1)
    6.43        finally show ?thesis .
    6.44      qed
    6.45 -    also have "?q2 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (iterates f u))"
    6.46 +    also have "?q2 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (iterates f u))"
    6.47      proof -
    6.48 -      have "?q2 = (lmap f o^ n) (LCons u (iterates f (f u)))"
    6.49 +      have "?q2 = (lmap f ^^ n) (LCons u (iterates f (f u)))"
    6.50          by (subst iterates) rule
    6.51 -      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (iterates f (f u)))"
    6.52 +      also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (iterates f (f u)))"
    6.53          by (rule funpow_lmap)
    6.54 -      also have "(lmap f o^ n) (iterates f (f u)) = (lmap f o^ Suc n) (iterates f u)"
    6.55 +      also have "(lmap f ^^ n) (iterates f (f u)) = (lmap f ^^ Suc n) (iterates f u)"
    6.56          by (simp add: lmap_iterates funpow_swap1)
    6.57        finally show ?thesis .
    6.58      qed
     7.1 --- a/src/HOL/Library/Continuity.thy	Fri Apr 24 08:24:54 2009 +0200
     7.2 +++ b/src/HOL/Library/Continuity.thy	Fri Apr 24 17:45:15 2009 +0200
     7.3 @@ -48,25 +48,25 @@
     7.4  qed
     7.5  
     7.6  lemma continuous_lfp:
     7.7 - assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
     7.8 + assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)"
     7.9  proof -
    7.10    note mono = continuous_mono[OF `continuous F`]
    7.11 -  { fix i have "(F o^ i) bot \<le> lfp F"
    7.12 +  { fix i have "(F ^^ i) bot \<le> lfp F"
    7.13      proof (induct i)
    7.14 -      show "(F o^ 0) bot \<le> lfp F" by simp
    7.15 +      show "(F ^^ 0) bot \<le> lfp F" by simp
    7.16      next
    7.17        case (Suc i)
    7.18 -      have "(F o^ Suc i) bot = F((F o^ i) bot)" by simp
    7.19 +      have "(F ^^ Suc i) bot = F((F ^^ i) bot)" by simp
    7.20        also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
    7.21        also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    7.22        finally show ?case .
    7.23      qed }
    7.24 -  hence "(SUP i. (F o^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    7.25 -  moreover have "lfp F \<le> (SUP i. (F o^ i) bot)" (is "_ \<le> ?U")
    7.26 +  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    7.27 +  moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
    7.28    proof (rule lfp_lowerbound)
    7.29 -    have "chain(%i. (F o^ i) bot)"
    7.30 +    have "chain(%i. (F ^^ i) bot)"
    7.31      proof -
    7.32 -      { fix i have "(F o^ i) bot \<le> (F o^ (Suc i)) bot"
    7.33 +      { fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
    7.34  	proof (induct i)
    7.35  	  case 0 show ?case by simp
    7.36  	next
    7.37 @@ -74,7 +74,7 @@
    7.38  	qed }
    7.39        thus ?thesis by(auto simp add:chain_def)
    7.40      qed
    7.41 -    hence "F ?U = (SUP i. (F o^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    7.42 +    hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    7.43      also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
    7.44      finally show "F ?U \<le> ?U" .
    7.45    qed
    7.46 @@ -193,7 +193,7 @@
    7.47  
    7.48  definition
    7.49    up_iterate :: "('a set => 'a set) => nat => 'a set" where
    7.50 -  "up_iterate f n = (f o^ n) {}"
    7.51 +  "up_iterate f n = (f ^^ n) {}"
    7.52  
    7.53  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
    7.54    by (simp add: up_iterate_def)
    7.55 @@ -245,7 +245,7 @@
    7.56  
    7.57  definition
    7.58    down_iterate :: "('a set => 'a set) => nat => 'a set" where
    7.59 -  "down_iterate f n = (f o^ n) UNIV"
    7.60 +  "down_iterate f n = (f ^^ n) UNIV"
    7.61  
    7.62  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
    7.63    by (simp add: down_iterate_def)
     8.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 24 08:24:54 2009 +0200
     8.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 24 17:45:15 2009 +0200
     8.3 @@ -1007,13 +1007,13 @@
     8.4    by simp
     8.5  
     8.6  lemma XDN_linear:
     8.7 -  "(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)"
     8.8 +  "(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)"
     8.9    by (induct n, simp_all)
    8.10  
    8.11  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)
    8.12  
    8.13  lemma fps_mult_XD_shift:
    8.14 -  "(XD o^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
    8.15 +  "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
    8.16    by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
    8.17  
    8.18  subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
     9.1 --- a/src/HOL/List.thy	Fri Apr 24 08:24:54 2009 +0200
     9.2 +++ b/src/HOL/List.thy	Fri Apr 24 17:45:15 2009 +0200
     9.3 @@ -198,7 +198,7 @@
     9.4  
     9.5  definition
     9.6    rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     9.7 -  "rotate n = rotate1 o^ n"
     9.8 +  "rotate n = rotate1 ^^ n"
     9.9  
    9.10  definition
    9.11    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
    10.1 --- a/src/HOL/Nat.thy	Fri Apr 24 08:24:54 2009 +0200
    10.2 +++ b/src/HOL/Nat.thy	Fri Apr 24 17:45:15 2009 +0200
    10.3 @@ -1166,31 +1166,58 @@
    10.4  
    10.5  subsection {* Natural operation of natural numbers on functions *}
    10.6  
    10.7 -text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    10.8 +text {*
    10.9 +  We use the same logical constant for the power operations on
   10.10 +  functions and relations, in order to share the same syntax.
   10.11 +*}
   10.12 +
   10.13 +consts compow :: "nat \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
   10.14 +
   10.15 +abbreviation compower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80) where
   10.16 +  "f ^^ n \<equiv> compow n f"
   10.17 +
   10.18 +notation (latex output)
   10.19 +  compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   10.20 +
   10.21 +notation (HTML output)
   10.22 +  compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   10.23 +
   10.24 +text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
   10.25 +
   10.26 +overloading
   10.27 +  funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
   10.28 +begin
   10.29  
   10.30  primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   10.31      "funpow 0 f = id"
   10.32    | "funpow (Suc n) f = f o funpow n f"
   10.33  
   10.34 -abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where
   10.35 -  "f o^ n \<equiv> funpow n f"
   10.36 +end
   10.37 +
   10.38 +text {* for code generation *}
   10.39 +
   10.40 +definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   10.41 +  funpow_code_def [code post]: "funpow = compow"
   10.42  
   10.43 -notation (latex output)
   10.44 -  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   10.45 +lemmas [code inline] = funpow_code_def [symmetric]
   10.46  
   10.47 -notation (HTML output)
   10.48 -  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   10.49 +lemma [code]:
   10.50 +  "funpow 0 f = id"
   10.51 +  "funpow (Suc n) f = f o funpow n f"
   10.52 +  unfolding funpow_code_def by simp_all
   10.53 +
   10.54 +definition "foo = id ^^ (1 + 1)"
   10.55  
   10.56  lemma funpow_add:
   10.57 -  "f o^ (m + n) = f o^ m \<circ> f o^ n"
   10.58 +  "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
   10.59    by (induct m) simp_all
   10.60  
   10.61  lemma funpow_swap1:
   10.62 -  "f ((f o^ n) x) = (f o^ n) (f x)"
   10.63 +  "f ((f ^^ n) x) = (f ^^ n) (f x)"
   10.64  proof -
   10.65 -  have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp
   10.66 -  also have "\<dots>  = (f o^ n o f o^ 1) x" by (simp only: funpow_add)
   10.67 -  also have "\<dots> = (f o^ n) (f x)" by simp
   10.68 +  have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
   10.69 +  also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
   10.70 +  also have "\<dots> = (f ^^ n) (f x)" by simp
   10.71    finally show ?thesis .
   10.72  qed
   10.73  
    11.1 --- a/src/HOL/SizeChange/Interpretation.thy	Fri Apr 24 08:24:54 2009 +0200
    11.2 +++ b/src/HOL/SizeChange/Interpretation.thy	Fri Apr 24 17:45:15 2009 +0200
    11.3 @@ -35,7 +35,7 @@
    11.4  	and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)"
    11.5  	by blast
    11.6    
    11.7 -  let ?s = "\<lambda>i. (f o^ i) x"
    11.8 +  let ?s = "\<lambda>i. (f ^^ i) x"
    11.9    
   11.10    {
   11.11  	fix i
    12.1 --- a/src/HOL/Transitive_Closure.thy	Fri Apr 24 08:24:54 2009 +0200
    12.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Apr 24 17:45:15 2009 +0200
    12.3 @@ -634,18 +634,19 @@
    12.4  
    12.5  text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
    12.6  
    12.7 -primrec relpow :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set" (infixr "^^" 80) where
    12.8 -    "R ^^ 0 = Id"
    12.9 -  | "R ^^ Suc n = R O (R ^^ n)"
   12.10 +overloading
   12.11 +  relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
   12.12 +begin
   12.13  
   12.14 -notation (latex output)
   12.15 -  relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   12.16 +primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
   12.17 +    "relpow 0 R = Id"
   12.18 +  | "relpow (Suc n) R = R O (R ^^ n)"
   12.19  
   12.20 -notation (HTML output)
   12.21 -  relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   12.22 +end
   12.23  
   12.24  lemma rel_pow_1 [simp]:
   12.25 -  "R ^^ 1 = R"
   12.26 +  fixes R :: "('a \<times> 'a) set"
   12.27 +  shows "R ^^ 1 = R"
   12.28    by simp
   12.29  
   12.30  lemma rel_pow_0_I: 
   12.31 @@ -741,7 +742,7 @@
   12.32    apply (rule iffI)
   12.33     apply (drule tranclD2)
   12.34     apply (clarsimp simp: rtrancl_is_UN_rel_pow)
   12.35 -   apply (rule_tac x="Suc x" in exI)
   12.36 +   apply (rule_tac x="Suc n" in exI)
   12.37     apply (clarsimp simp: rel_comp_def)
   12.38     apply fastsimp
   12.39    apply clarsimp
    13.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Apr 24 08:24:54 2009 +0200
    13.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Apr 24 17:45:15 2009 +0200
    13.3 @@ -338,10 +338,10 @@
    13.4  
    13.5  constdefs
    13.6    wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"  
    13.7 -    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
    13.8 +    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
    13.9  
   13.10    wens_single :: "[('a*'a) set, 'a set] => 'a set"  
   13.11 -    "wens_single act B == \<Union>i. (wp act o^ i) B"
   13.12 +    "wens_single act B == \<Union>i. (wp act ^^ i) B"
   13.13  
   13.14  lemma wens_single_Un_eq:
   13.15        "single_valued act
    14.1 --- a/src/HOL/Word/BinBoolList.thy	Fri Apr 24 08:24:54 2009 +0200
    14.2 +++ b/src/HOL/Word/BinBoolList.thy	Fri Apr 24 17:45:15 2009 +0200
    14.3 @@ -38,7 +38,7 @@
    14.4      if y then rbl_add ws x else ws)"
    14.5  
    14.6  lemma butlast_power:
    14.7 -  "(butlast o^ n) bl = take (length bl - n) bl"
    14.8 +  "(butlast ^^ n) bl = take (length bl - n) bl"
    14.9    by (induct n) (auto simp: butlast_take)
   14.10  
   14.11  lemma bin_to_bl_aux_Pls_minus_simp [simp]:
   14.12 @@ -370,14 +370,14 @@
   14.13    done
   14.14  
   14.15  lemma nth_rest_power_bin [rule_format] :
   14.16 -  "ALL n. bin_nth ((bin_rest o^ k) w) n = bin_nth w (n + k)"
   14.17 +  "ALL n. bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
   14.18    apply (induct k, clarsimp)
   14.19    apply clarsimp
   14.20    apply (simp only: bin_nth.Suc [symmetric] add_Suc)
   14.21    done
   14.22  
   14.23  lemma take_rest_power_bin:
   14.24 -  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest o^ (n - m)) w)" 
   14.25 +  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" 
   14.26    apply (rule nth_equalityI)
   14.27     apply simp
   14.28    apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
    15.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Apr 24 08:24:54 2009 +0200
    15.2 +++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 24 17:45:15 2009 +0200
    15.3 @@ -822,8 +822,8 @@
    15.4    by (induct n) auto
    15.5  
    15.6  lemma bin_rest_power_trunc [rule_format] :
    15.7 -  "(bin_rest o^ k) (bintrunc n bin) = 
    15.8 -    bintrunc (n - k) ((bin_rest o^ k) bin)"
    15.9 +  "(bin_rest ^^ k) (bintrunc n bin) = 
   15.10 +    bintrunc (n - k) ((bin_rest ^^ k) bin)"
   15.11    by (induct k) (auto simp: bin_rest_trunc)
   15.12  
   15.13  lemma bin_rest_trunc_i:
   15.14 @@ -857,7 +857,7 @@
   15.15    by (rule ext) auto
   15.16  
   15.17  lemma rco_lem:
   15.18 -  "f o g o f = g o f ==> f o (g o f) o^ n = g o^ n o f"
   15.19 +  "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f"
   15.20    apply (rule ext)
   15.21    apply (induct_tac n)
   15.22     apply (simp_all (no_asm))
   15.23 @@ -867,7 +867,7 @@
   15.24    apply simp
   15.25    done
   15.26  
   15.27 -lemma rco_alt: "(f o g) o^ n o f = f o (g o f) o^ n"
   15.28 +lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n"
   15.29    apply (rule ext)
   15.30    apply (induct n)
   15.31     apply (simp_all add: o_def)
   15.32 @@ -892,7 +892,7 @@
   15.33  subsection {* Miscellaneous lemmas *}
   15.34  
   15.35  lemma funpow_minus_simp:
   15.36 -  "0 < n \<Longrightarrow> f o^ n = f \<circ> f o^ (n - 1)"
   15.37 +  "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
   15.38    by (cases n) simp_all
   15.39  
   15.40  lemmas funpow_pred_simp [simp] =
    16.1 --- a/src/HOL/Word/TdThs.thy	Fri Apr 24 08:24:54 2009 +0200
    16.2 +++ b/src/HOL/Word/TdThs.thy	Fri Apr 24 17:45:15 2009 +0200
    16.3 @@ -110,7 +110,7 @@
    16.4    done
    16.5  
    16.6  lemma fn_comm_power:
    16.7 -  "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n" 
    16.8 +  "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n" 
    16.9    apply (rule ext) 
   16.10    apply (induct n)
   16.11     apply (auto dest: fun_cong)
    17.1 --- a/src/HOL/Word/WordDefinition.thy	Fri Apr 24 08:24:54 2009 +0200
    17.2 +++ b/src/HOL/Word/WordDefinition.thy	Fri Apr 24 17:45:15 2009 +0200
    17.3 @@ -203,10 +203,10 @@
    17.4    "shiftr1 w = word_of_int (bin_rest (uint w))"
    17.5  
    17.6  definition
    17.7 -  shiftl_def: "w << n = (shiftl1 o^ n) w"
    17.8 +  shiftl_def: "w << n = (shiftl1 ^^ n) w"
    17.9  
   17.10  definition
   17.11 -  shiftr_def: "w >> n = (shiftr1 o^ n) w"
   17.12 +  shiftr_def: "w >> n = (shiftr1 ^^ n) w"
   17.13  
   17.14  instance ..
   17.15  
   17.16 @@ -241,7 +241,7 @@
   17.17    "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
   17.18  
   17.19    sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
   17.20 -  "w >>> n == (sshiftr1 o^ n) w"
   17.21 +  "w >>> n == (sshiftr1 ^^ n) w"
   17.22  
   17.23    mask :: "nat => 'a::len word"
   17.24    "mask n == (1 << n) - 1"
   17.25 @@ -264,7 +264,7 @@
   17.26      case ys of [] => [] | x # xs => last ys # butlast ys"
   17.27  
   17.28    rotater :: "nat => 'a list => 'a list"
   17.29 -  "rotater n == rotater1 o^ n"
   17.30 +  "rotater n == rotater1 ^^ n"
   17.31  
   17.32    word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
   17.33    "word_rotr n w == of_bl (rotater n (to_bl w))"
    18.1 --- a/src/HOL/Word/WordShift.thy	Fri Apr 24 08:24:54 2009 +0200
    18.2 +++ b/src/HOL/Word/WordShift.thy	Fri Apr 24 17:45:15 2009 +0200
    18.3 @@ -361,14 +361,14 @@
    18.4  
    18.5  lemma shiftr_no': 
    18.6    "w = number_of bin ==> 
    18.7 -  (w::'a::len0 word) >> n = number_of ((bin_rest o^ n) (bintrunc (size w) bin))"
    18.8 +  (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
    18.9    apply clarsimp
   18.10    apply (rule word_eqI)
   18.11    apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
   18.12    done
   18.13  
   18.14  lemma sshiftr_no': 
   18.15 -  "w = number_of bin ==> w >>> n = number_of ((bin_rest o^ n) 
   18.16 +  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^^ n) 
   18.17      (sbintrunc (size w - 1) bin))"
   18.18    apply clarsimp
   18.19    apply (rule word_eqI)