power operation on functions with syntax o^; power operation on relations with syntax ^^
authorhaftmann
Mon Apr 20 09:32:07 2009 +0200 (2009-04-20)
changeset 309527ab2716dd93b
parent 30951 a6e26a248f03
child 30953 d5f5ab29d769
power operation on functions with syntax o^; power operation on relations with syntax ^^
src/HOL/Bali/Trans.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/HoareParallel/OG_Tran.thy
src/HOL/IMP/Compiler0.thy
src/HOL/IMP/Machines.thy
src/HOL/IMP/Transition.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/Library/Topology_Euclidean_Space.thy
src/HOL/List.thy
src/HOL/SizeChange/Interpretation.thy
src/HOL/UNITY/Comp.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/src/HOL/Bali/Trans.thy	Fri Apr 17 16:41:31 2009 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Mon Apr 20 09:32:07 2009 +0200
     1.3 @@ -359,7 +359,7 @@
     1.4  
     1.5  abbreviation
     1.6    stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
     1.7 -  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^n"
     1.8 +  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n"
     1.9  
    1.10  abbreviation
    1.11    steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
    1.12 @@ -370,25 +370,6 @@
    1.13    Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
    1.14  *)
    1.15  
    1.16 -lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
    1.17 -proof -
    1.18 -  assume "p \<in> R\<^sup>*"
    1.19 -  moreover obtain x y where p: "p = (x,y)" by (cases p)
    1.20 -  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
    1.21 -  hence "\<exists>n. (x,y) \<in> R^n"
    1.22 -  proof induct
    1.23 -    fix a have "(a,a) \<in> R^0" by simp
    1.24 -    thus "\<exists>n. (a,a) \<in> R ^ n" ..
    1.25 -  next
    1.26 -    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
    1.27 -    then obtain n where "(a,b) \<in> R^n" ..
    1.28 -    moreover assume "(b,c) \<in> R"
    1.29 -    ultimately have "(a,c) \<in> R^(Suc n)" by auto
    1.30 -    thus "\<exists>n. (a,c) \<in> R^n" ..
    1.31 -  qed
    1.32 -  with p show ?thesis by hypsubst
    1.33 -qed  
    1.34 -
    1.35  (*
    1.36  lemma imp_eval_trans:
    1.37    assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 17 16:41:31 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Apr 20 09:32:07 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^n) s) (f n)"
     2.8 -  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.9 +  assumes f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
    2.10 +  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.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^n) s) (f n)"
    2.19 +  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ 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^j') s) (f j') x) \<le> horner F G n ((F^j') s) (f j') (Ifloat x) \<and> 
    2.25 -         horner F G n ((F^j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F^j') s) (f j') x)"
    2.26 +  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.27 +         horner F G n ((F o^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F o^ 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 ^ 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.36 +    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.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 ^ j') s)) (G ((F ^ j') s) (f j')) (Ifloat x)) \<le> 
    2.44 -          - Ifloat (x * lb n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) x)"
    2.45 +    show "- (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x)) \<le> 
    2.46 +          - Ifloat (x * lb n (F ((F o^ j') s)) (G ((F o^ 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^n) s) (f n)"
    2.55 +  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ 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^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^j') s) (f j') x)" (is "?ub")
    2.62 +  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.63 +    "(\<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.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^n) s) (f n)"
    2.72 +  assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ 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^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^j') s) (f j') x)" (is "?ub")
    2.79 +  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.80 +    "(\<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.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.simps uminus_float.simps times_float.simps algebra_simps)
    2.84 @@ -104,13 +104,13 @@
    2.85  
    2.86    have move_minus: "Ifloat (-x) = -1 * Ifloat x" by auto
    2.87  
    2.88 -  have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j) = 
    2.89 +  have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j) = 
    2.90      (\<Sum>j = 0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j)"
    2.91    proof (rule setsum_cong, simp)
    2.92      fix j assume "j \<in> {0 ..< n}"
    2.93      show "1 / real (f (j' + j)) * Ifloat x ^ j = -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j"
    2.94        unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
    2.95 -      unfolding real_mult_commute unfolding real_mult_assoc[of "-1^j", symmetric] power_mult_distrib[symmetric]
    2.96 +      unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
    2.97        by auto
    2.98    qed
    2.99  
   2.100 @@ -160,21 +160,21 @@
   2.101                                              else (0, (max (-l) u) ^ n))"
   2.102  
   2.103  lemma float_power_bnds: assumes "(l1, u1) = float_power_bnds n l u" and "x \<in> {Ifloat l .. Ifloat u}"
   2.104 -  shows "x^n \<in> {Ifloat l1..Ifloat u1}"
   2.105 +  shows "x ^ n \<in> {Ifloat l1..Ifloat u1}"
   2.106  proof (cases "even n")
   2.107    case True 
   2.108    show ?thesis
   2.109    proof (cases "0 < l")
   2.110      case True hence "odd n \<or> 0 < l" and "0 \<le> Ifloat l" unfolding less_float_def by auto
   2.111      have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
   2.112 -    have "Ifloat l^n \<le> x^n" and "x^n \<le> Ifloat u^n " using `0 \<le> Ifloat l` and assms unfolding atLeastAtMost_iff using power_mono[of "Ifloat l" x] power_mono[of x "Ifloat u"] by auto
   2.113 +    have "Ifloat l ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat u ^ n " using `0 \<le> Ifloat l` and assms unfolding atLeastAtMost_iff using power_mono[of "Ifloat l" x] power_mono[of x "Ifloat u"] by auto
   2.114      thus ?thesis using assms `0 < l` unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
   2.115    next
   2.116      case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
   2.117      show ?thesis
   2.118      proof (cases "u < 0")
   2.119        case True hence "0 \<le> - Ifloat u" and "- Ifloat u \<le> - x" and "0 \<le> - x" and "-x \<le> - Ifloat l" using assms unfolding less_float_def by auto
   2.120 -      hence "Ifloat u^n \<le> x^n" and "x^n \<le> Ifloat l^n" using power_mono[of  "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n] 
   2.121 +      hence "Ifloat u ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat l ^ n" using power_mono[of  "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n] 
   2.122  	unfolding power_minus_even[OF `even n`] by auto
   2.123        moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
   2.124        ultimately show ?thesis using float_power by auto
   2.125 @@ -194,11 +194,11 @@
   2.126  next
   2.127    case False hence "odd n \<or> 0 < l" by auto
   2.128    have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
   2.129 -  have "Ifloat l^n \<le> x^n" and "x^n \<le> Ifloat u^n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
   2.130 +  have "Ifloat l ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat u ^ n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
   2.131    thus ?thesis unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
   2.132  qed
   2.133  
   2.134 -lemma bnds_power: "\<forall> x l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {Ifloat l .. Ifloat u} \<longrightarrow> Ifloat l1 \<le> x^n \<and> x^n \<le> Ifloat u1"
   2.135 +lemma bnds_power: "\<forall> x l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {Ifloat l .. Ifloat u} \<longrightarrow> Ifloat l1 \<le> x ^ n \<and> x ^ n \<le> Ifloat u1"
   2.136    using float_power_bnds by auto
   2.137  
   2.138  section "Square root"
   2.139 @@ -794,8 +794,8 @@
   2.140    let "?f n" = "fact (2 * n)"
   2.141  
   2.142    { fix n 
   2.143 -    have F: "\<And>m. ((\<lambda>i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
   2.144 -    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^ n) 1 * (((\<lambda>i. i + 2) ^ n) 1 + 1)"
   2.145 +    have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
   2.146 +    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 1 * (((\<lambda>i. i + 2) o^ n) 1 + 1)"
   2.147        unfolding F by auto } note f_eq = this
   2.148      
   2.149    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0, 
   2.150 @@ -811,7 +811,7 @@
   2.151    have "0 < x * x" using `0 < x` unfolding less_float_def Ifloat_mult Ifloat_0
   2.152      using mult_pos_pos[where a="Ifloat x" and b="Ifloat x"] by auto
   2.153  
   2.154 -  { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i))
   2.155 +  { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
   2.156      = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
   2.157    proof -
   2.158      have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
   2.159 @@ -905,8 +905,8 @@
   2.160    let "?f n" = "fact (2 * n + 1)"
   2.161  
   2.162    { fix n 
   2.163 -    have F: "\<And>m. ((\<lambda>i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
   2.164 -    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^ n) 2 * (((\<lambda>i. i + 2) ^ n) 2 + 1)"
   2.165 +    have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
   2.166 +    have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 2 * (((\<lambda>i. i + 2) o^ n) 2 + 1)"
   2.167        unfolding F by auto } note f_eq = this
   2.168      
   2.169    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
   2.170 @@ -1382,8 +1382,8 @@
   2.171    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.172  proof -
   2.173    { fix n
   2.174 -    have F: "\<And> m. ((\<lambda>i. i + 1) ^ n) m = n + m" by (induct n, auto)
   2.175 -    have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^ n) 1" unfolding F by auto } note f_eq = this
   2.176 +    have F: "\<And> m. ((\<lambda>i. i + 1) o^ n) m = n + m" by (induct n, auto)
   2.177 +    have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) o^ n) 1" unfolding F by auto } note f_eq = this
   2.178      
   2.179    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.180      OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
   2.181 @@ -1631,10 +1631,10 @@
   2.182  
   2.183  lemma ln_bounds:
   2.184    assumes "0 \<le> x" and "x < 1"
   2.185 -  shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x^(Suc i)) \<le> ln (x + 1)" (is "?lb")
   2.186 -  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x^(Suc i))" (is "?ub")
   2.187 +  shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
   2.188 +  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
   2.189  proof -
   2.190 -  let "?a n" = "(1/real (n +1)) * x^(Suc n)"
   2.191 +  let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
   2.192  
   2.193    have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
   2.194      using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
   2.195 @@ -2479,7 +2479,7 @@
   2.196      fun lift_var (Free (varname, _)) = (case AList.lookup (op =) bound_eqs varname of
   2.197                                            SOME bound => bound
   2.198                                          | NONE => raise TERM ("No bound equations found for " ^ varname, []))
   2.199 -      | lift_var t = raise TERM ("Can not convert expression " ^ 
   2.200 +      | lift_var t = raise TERM ("Can not convert expression " ^
   2.201                                   (Syntax.string_of_term ctxt t), [t])
   2.202  
   2.203      val _ $ vs = HOLogic.dest_Trueprop (Logic.strip_imp_concl goal')
     3.1 --- a/src/HOL/HoareParallel/OG_Tran.thy	Fri Apr 17 16:41:31 2009 +0200
     3.2 +++ b/src/HOL/HoareParallel/OG_Tran.thy	Mon Apr 20 09:32:07 2009 +0200
     3.3 @@ -74,7 +74,7 @@
     3.4  abbreviation
     3.5    ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) 
     3.6                             \<Rightarrow> bool"  ("_ -_\<rightarrow> _"[81,81] 100)  where
     3.7 -  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition^n"
     3.8 +  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition ^^ n"
     3.9  
    3.10  abbreviation
    3.11    ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
    3.12 @@ -84,7 +84,7 @@
    3.13  abbreviation
    3.14    transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"  
    3.15                            ("_ -P_\<rightarrow> _"[81,81,81] 100)  where
    3.16 -  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition^n"
    3.17 +  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition ^^ n"
    3.18  
    3.19  subsection {* Definition of Semantics *}
    3.20  
     4.1 --- a/src/HOL/IMP/Compiler0.thy	Fri Apr 17 16:41:31 2009 +0200
     4.2 +++ b/src/HOL/IMP/Compiler0.thy	Mon Apr 20 09:32:07 2009 +0200
     4.3 @@ -45,7 +45,7 @@
     4.4  abbreviation
     4.5    stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
     4.6      ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)  where
     4.7 -  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)"
     4.8 +  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : (stepa1 P ^^ i)"
     4.9  
    4.10  subsection "The compiler"
    4.11  
     5.1 --- a/src/HOL/IMP/Machines.thy	Fri Apr 17 16:41:31 2009 +0200
     5.2 +++ b/src/HOL/IMP/Machines.thy	Mon Apr 20 09:32:07 2009 +0200
     5.3 @@ -1,7 +1,6 @@
     5.4 -
     5.5 -(* $Id$ *)
     5.6 -
     5.7 -theory Machines imports Natural begin
     5.8 +theory Machines
     5.9 +imports Natural
    5.10 +begin
    5.11  
    5.12  lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
    5.13    by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
    5.14 @@ -11,20 +10,22 @@
    5.15  
    5.16  lemmas converse_rel_powE = rel_pow_E2
    5.17  
    5.18 -lemma R_O_Rn_commute: "R O R^n = R^n O R"
    5.19 +lemma R_O_Rn_commute: "R O R ^^ n = R ^^ n O R"
    5.20    by (induct n) (simp, simp add: O_assoc [symmetric])
    5.21  
    5.22  lemma converse_in_rel_pow_eq:
    5.23 -  "((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
    5.24 +  "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
    5.25  apply(rule iffI)
    5.26   apply(blast elim:converse_rel_powE)
    5.27  apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
    5.28  done
    5.29  
    5.30 -lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
    5.31 +lemma rel_pow_plus:
    5.32 +  "R ^^ (m+n) = R ^^ n O R ^^ m"
    5.33    by (induct n) (simp, simp add: O_assoc)
    5.34  
    5.35 -lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
    5.36 +lemma rel_pow_plusI:
    5.37 +  "\<lbrakk> (x,y) \<in> R ^^ m; (y,z) \<in> R ^^ n \<rbrakk> \<Longrightarrow> (x,z) \<in> R ^^ (m+n)"
    5.38    by (simp add: rel_pow_plus rel_compI)
    5.39  
    5.40  subsection "Instructions"
    5.41 @@ -57,7 +58,7 @@
    5.42  abbreviation
    5.43    exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    5.44      ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
    5.45 -  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^n"
    5.46 +  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n"
    5.47  
    5.48  subsection "M0 with lists"
    5.49  
    5.50 @@ -89,7 +90,7 @@
    5.51  abbreviation
    5.52    stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
    5.53      ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
    5.54 -  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^i)"
    5.55 +  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)"
    5.56  
    5.57  inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
    5.58  
     6.1 --- a/src/HOL/IMP/Transition.thy	Fri Apr 17 16:41:31 2009 +0200
     6.2 +++ b/src/HOL/IMP/Transition.thy	Mon Apr 20 09:32:07 2009 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:        HOL/IMP/Transition.thy
     6.5 -    ID:           $Id$
     6.6      Author:       Tobias Nipkow & Robert Sandner, TUM
     6.7      Isar Version: Gerwin Klein, 2001
     6.8      Copyright     1996 TUM
     6.9 @@ -69,7 +68,7 @@
    6.10  abbreviation
    6.11    evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    6.12      ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)  where
    6.13 -  "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^n"
    6.14 +  "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n"
    6.15  
    6.16  abbreviation
    6.17    evalc' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.18 @@ -77,28 +76,9 @@
    6.19    "cs \<longrightarrow>\<^sub>1\<^sup>* cs' == (cs,cs') \<in> evalc1^*"
    6.20  
    6.21  (*<*)
    6.22 -(* fixme: move to Relation_Power.thy *)
    6.23 -lemma rel_pow_Suc_E2 [elim!]:
    6.24 -  "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
    6.25 -  by (blast dest: rel_pow_Suc_D2)
    6.26 +declare rel_pow_Suc_E2 [elim!]
    6.27 +(*>*)
    6.28  
    6.29 -lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
    6.30 -proof (induct p)
    6.31 -  fix x y
    6.32 -  assume "(x, y) \<in> R\<^sup>*"
    6.33 -  thus "\<exists>n. (x, y) \<in> R^n"
    6.34 -  proof induct
    6.35 -    fix a have "(a, a) \<in> R^0" by simp
    6.36 -    thus "\<exists>n. (a, a) \<in> R ^ n" ..
    6.37 -  next
    6.38 -    fix a b c assume "\<exists>n. (a, b) \<in> R ^ n"
    6.39 -    then obtain n where "(a, b) \<in> R^n" ..
    6.40 -    moreover assume "(b, c) \<in> R"
    6.41 -    ultimately have "(a, c) \<in> R^(Suc n)" by auto
    6.42 -    thus "\<exists>n. (a, c) \<in> R^n" ..
    6.43 -  qed
    6.44 -qed
    6.45 -(*>*)
    6.46  text {*
    6.47    As for the big step semantics you can read these rules in a
    6.48    syntax directed way:
    6.49 @@ -189,8 +169,8 @@
    6.50  (*<*)
    6.51  (* FIXME: relpow.simps don't work *)
    6.52  lemmas [simp del] = relpow.simps
    6.53 -lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by (simp add: relpow.simps)
    6.54 -lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by (simp add: relpow.simps)
    6.55 +lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps)
    6.56 +lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps)
    6.57  
    6.58  (*>*)
    6.59  lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
     7.1 --- a/src/HOL/Import/HOL/HOL4Base.thy	Fri Apr 17 16:41:31 2009 +0200
     7.2 +++ b/src/HOL/Import/HOL/HOL4Base.thy	Mon Apr 20 09:32:07 2009 +0200
     7.3 @@ -2794,8 +2794,8 @@
     7.4    by (import numeral numeral_fact)
     7.5  
     7.6  lemma numeral_funpow: "ALL n::nat.
     7.7 -   ((f::'a::type => 'a::type) ^ n) (x::'a::type) =
     7.8 -   (if n = 0 then x else (f ^ (n - 1)) (f x))"
     7.9 +   ((f::'a::type => 'a::type) o^ n) (x::'a::type) =
    7.10 +   (if n = 0 then x else (f o^ (n - 1)) (f x))"
    7.11    by (import numeral numeral_funpow)
    7.12  
    7.13  ;end_setup
     8.1 --- a/src/HOL/Import/HOL/HOL4Word32.thy	Fri Apr 17 16:41:31 2009 +0200
     8.2 +++ b/src/HOL/Import/HOL/HOL4Word32.thy	Mon Apr 20 09:32:07 2009 +0200
     8.3 @@ -434,15 +434,15 @@
     8.4    by (import word32 EQUIV_QT)
     8.5  
     8.6  lemma FUNPOW_THM: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
     8.7 -   (f ^ n) (f x) = f ((f ^ n) x)"
     8.8 +   (f o^ n) (f x) = f ((f o^ n) x)"
     8.9    by (import word32 FUNPOW_THM)
    8.10  
    8.11  lemma FUNPOW_THM2: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
    8.12 -   (f ^ Suc n) x = f ((f ^ n) x)"
    8.13 +   (f o^ Suc n) x = f ((f o^ n) x)"
    8.14    by (import word32 FUNPOW_THM2)
    8.15  
    8.16  lemma FUNPOW_COMP: "ALL (f::'a::type => 'a::type) (m::nat) (n::nat) a::'a::type.
    8.17 -   (f ^ m) ((f ^ n) a) = (f ^ (m + n)) a"
    8.18 +   (f o^ m) ((f o^ n) a) = (f o^ (m + n)) a"
    8.19    by (import word32 FUNPOW_COMP)
    8.20  
    8.21  lemma INw_MODw: "ALL n::nat. INw (MODw n)"
    8.22 @@ -1170,23 +1170,23 @@
    8.23  
    8.24  constdefs
    8.25    word_lsr :: "word32 => nat => word32" 
    8.26 -  "word_lsr == %(a::word32) n::nat. (word_lsr1 ^ n) a"
    8.27 +  "word_lsr == %(a::word32) n::nat. (word_lsr1 o^ n) a"
    8.28  
    8.29 -lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 ^ n) a"
    8.30 +lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 o^ n) a"
    8.31    by (import word32 word_lsr)
    8.32  
    8.33  constdefs
    8.34    word_asr :: "word32 => nat => word32" 
    8.35 -  "word_asr == %(a::word32) n::nat. (word_asr1 ^ n) a"
    8.36 +  "word_asr == %(a::word32) n::nat. (word_asr1 o^ n) a"
    8.37  
    8.38 -lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 ^ n) a"
    8.39 +lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 o^ n) a"
    8.40    by (import word32 word_asr)
    8.41  
    8.42  constdefs
    8.43    word_ror :: "word32 => nat => word32" 
    8.44 -  "word_ror == %(a::word32) n::nat. (word_ror1 ^ n) a"
    8.45 +  "word_ror == %(a::word32) n::nat. (word_ror1 o^ n) a"
    8.46  
    8.47 -lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 ^ n) a"
    8.48 +lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 o^ n) a"
    8.49    by (import word32 word_ror)
    8.50  
    8.51  consts
    8.52 @@ -1583,4 +1583,3 @@
    8.53  ;end_setup
    8.54  
    8.55  end
    8.56 -
     9.1 --- a/src/HOL/Import/HOL4Compat.thy	Fri Apr 17 16:41:31 2009 +0200
     9.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Apr 20 09:32:07 2009 +0200
     9.3 @@ -202,19 +202,13 @@
     9.4  
     9.5  constdefs
     9.6    FUNPOW :: "('a => 'a) => nat => 'a => 'a"
     9.7 -  "FUNPOW f n == f ^ n"
     9.8 +  "FUNPOW f n == f o^ n"
     9.9  
    9.10 -lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
    9.11 -  (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
    9.12 -proof auto
    9.13 -  fix f n x
    9.14 -  have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
    9.15 -    by (induct n,auto)
    9.16 -  thus "f ((f ^ n) x) = (f ^ n) (f x)"
    9.17 -    ..
    9.18 -qed
    9.19 +lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
    9.20 +  (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
    9.21 +  by (simp add: funpow_swap1)
    9.22  
    9.23 -lemma [hol4rew]: "FUNPOW f n = f ^ n"
    9.24 +lemma [hol4rew]: "FUNPOW f n = f o^ n"
    9.25    by (simp add: FUNPOW_def)
    9.26  
    9.27  lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
    9.28 @@ -224,7 +218,7 @@
    9.29    by simp
    9.30  
    9.31  lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
    9.32 -  by (simp, arith)
    9.33 +  by (simp) arith
    9.34  
    9.35  lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
    9.36    by (simp add: max_def)
    10.1 --- a/src/HOL/Library/Coinductive_List.thy	Fri Apr 17 16:41:31 2009 +0200
    10.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Apr 20 09:32:07 2009 +0200
    10.3 @@ -786,7 +786,7 @@
    10.4  
    10.5  lemma funpow_lmap:
    10.6    fixes f :: "'a \<Rightarrow> 'a"
    10.7 -  shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)"
    10.8 +  shows "(lmap f o^ n) (LCons b l) = LCons ((f o^ n) b) ((lmap f o^ n) l)"
    10.9    by (induct n) simp_all
   10.10  
   10.11  
   10.12 @@ -796,35 +796,35 @@
   10.13  proof
   10.14    fix x
   10.15    have "(h x, iterates f x) \<in>
   10.16 -      {((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}"
   10.17 +      {((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u)) | u n. True}"
   10.18    proof -
   10.19 -    have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))"
   10.20 +    have "(h x, iterates f x) = ((lmap f o^ 0) (h x), (lmap f o^ 0) (iterates f x))"
   10.21        by simp
   10.22      then show ?thesis by blast
   10.23    qed
   10.24    then show "h x = iterates f x"
   10.25    proof (coinduct rule: llist_equalityI)
   10.26      case (Eqllist q)
   10.27 -    then obtain u n where "q = ((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u))"
   10.28 +    then obtain u n where "q = ((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u))"
   10.29          (is "_ = (?q1, ?q2)")
   10.30        by auto
   10.31 -    also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))"
   10.32 +    also have "?q1 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (h u))"
   10.33      proof -
   10.34 -      have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))"
   10.35 +      have "?q1 = (lmap f o^ n) (LCons u (lmap f (h u)))"
   10.36          by (subst h) rule
   10.37 -      also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))"
   10.38 +      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (lmap f (h u)))"
   10.39          by (rule funpow_lmap)
   10.40 -      also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)"
   10.41 +      also have "(lmap f o^ n) (lmap f (h u)) = (lmap f o^ Suc n) (h u)"
   10.42          by (simp add: funpow_swap1)
   10.43        finally show ?thesis .
   10.44      qed
   10.45 -    also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))"
   10.46 +    also have "?q2 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (iterates f u))"
   10.47      proof -
   10.48 -      have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))"
   10.49 +      have "?q2 = (lmap f o^ n) (LCons u (iterates f (f u)))"
   10.50          by (subst iterates) rule
   10.51 -      also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))"
   10.52 +      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (iterates f (f u)))"
   10.53          by (rule funpow_lmap)
   10.54 -      also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)"
   10.55 +      also have "(lmap f o^ n) (iterates f (f u)) = (lmap f o^ Suc n) (iterates f u)"
   10.56          by (simp add: lmap_iterates funpow_swap1)
   10.57        finally show ?thesis .
   10.58      qed
    11.1 --- a/src/HOL/Library/Continuity.thy	Fri Apr 17 16:41:31 2009 +0200
    11.2 +++ b/src/HOL/Library/Continuity.thy	Mon Apr 20 09:32:07 2009 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  header {* Continuity and iterations (of set transformers) *}
    11.5  
    11.6  theory Continuity
    11.7 -imports Relation_Power Main
    11.8 +imports Transitive_Closure Main
    11.9  begin
   11.10  
   11.11  subsection {* Continuity for complete lattices *}
   11.12 @@ -48,25 +48,25 @@
   11.13  qed
   11.14  
   11.15  lemma continuous_lfp:
   11.16 - assumes "continuous F" shows "lfp F = (SUP i. (F^^i) bot)"
   11.17 + assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
   11.18  proof -
   11.19    note mono = continuous_mono[OF `continuous F`]
   11.20 -  { fix i have "(F^^i) bot \<le> lfp F"
   11.21 +  { fix i have "(F o^ i) bot \<le> lfp F"
   11.22      proof (induct i)
   11.23 -      show "(F^^0) bot \<le> lfp F" by simp
   11.24 +      show "(F o^ 0) bot \<le> lfp F" by simp
   11.25      next
   11.26        case (Suc i)
   11.27 -      have "(F^^(Suc i)) bot = F((F^^i) bot)" by simp
   11.28 +      have "(F o^ Suc i) bot = F((F o^ i) bot)" by simp
   11.29        also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
   11.30        also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
   11.31        finally show ?case .
   11.32      qed }
   11.33 -  hence "(SUP i. (F^^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
   11.34 -  moreover have "lfp F \<le> (SUP i. (F^^i) bot)" (is "_ \<le> ?U")
   11.35 +  hence "(SUP i. (F o^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
   11.36 +  moreover have "lfp F \<le> (SUP i. (F o^ i) bot)" (is "_ \<le> ?U")
   11.37    proof (rule lfp_lowerbound)
   11.38 -    have "chain(%i. (F^^i) bot)"
   11.39 +    have "chain(%i. (F o^ i) bot)"
   11.40      proof -
   11.41 -      { fix i have "(F^^i) bot \<le> (F^^(Suc i)) bot"
   11.42 +      { fix i have "(F o^ i) bot \<le> (F o^ (Suc i)) bot"
   11.43  	proof (induct i)
   11.44  	  case 0 show ?case by simp
   11.45  	next
   11.46 @@ -74,7 +74,7 @@
   11.47  	qed }
   11.48        thus ?thesis by(auto simp add:chain_def)
   11.49      qed
   11.50 -    hence "F ?U = (SUP i. (F^^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
   11.51 +    hence "F ?U = (SUP i. (F o^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
   11.52      also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
   11.53      finally show "F ?U \<le> ?U" .
   11.54    qed
   11.55 @@ -193,7 +193,7 @@
   11.56  
   11.57  definition
   11.58    up_iterate :: "('a set => 'a set) => nat => 'a set" where
   11.59 -  "up_iterate f n = (f^^n) {}"
   11.60 +  "up_iterate f n = (f o^ n) {}"
   11.61  
   11.62  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   11.63    by (simp add: up_iterate_def)
   11.64 @@ -245,7 +245,7 @@
   11.65  
   11.66  definition
   11.67    down_iterate :: "('a set => 'a set) => nat => 'a set" where
   11.68 -  "down_iterate f n = (f^^n) UNIV"
   11.69 +  "down_iterate f n = (f o^ n) UNIV"
   11.70  
   11.71  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   11.72    by (simp add: down_iterate_def)
    12.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 17 16:41:31 2009 +0200
    12.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 20 09:32:07 2009 +0200
    12.3 @@ -1022,13 +1022,15 @@
    12.4  lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)"
    12.5    by simp
    12.6  
    12.7 -lemma XDN_linear: "(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)"
    12.8 +lemma XDN_linear:
    12.9 +  "(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)"
   12.10    by (induct n, simp_all)
   12.11  
   12.12  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)
   12.13  
   12.14 -lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   12.15 -by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
   12.16 +lemma fps_mult_XD_shift:
   12.17 +  "(XD o^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   12.18 +  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
   12.19  
   12.20  subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
   12.21  subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
    13.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Apr 17 16:41:31 2009 +0200
    13.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Apr 20 09:32:07 2009 +0200
    13.3 @@ -5441,7 +5441,7 @@
    13.4    have "1 - c > 0" using c by auto
    13.5  
    13.6    from s(2) obtain z0 where "z0 \<in> s" by auto
    13.7 -  def z \<equiv> "\<lambda> n::nat. fun_pow n f z0"
    13.8 +  def z \<equiv> "\<lambda> n::nat. funpow n f z0"
    13.9    { fix n::nat
   13.10      have "z n \<in> s" unfolding z_def
   13.11      proof(induct n) case 0 thus ?case using `z0 \<in>s` by auto
   13.12 @@ -5580,7 +5580,7 @@
   13.13        using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
   13.14    def y \<equiv> "g x"
   13.15    have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
   13.16 -  def f \<equiv> "\<lambda> n. fun_pow n g"
   13.17 +  def f \<equiv> "\<lambda> n. funpow n g"
   13.18    have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
   13.19    have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
   13.20    { fix n::nat and z assume "z\<in>s"
    14.1 --- a/src/HOL/List.thy	Fri Apr 17 16:41:31 2009 +0200
    14.2 +++ b/src/HOL/List.thy	Mon Apr 20 09:32:07 2009 +0200
    14.3 @@ -5,7 +5,7 @@
    14.4  header {* The datatype of finite lists *}
    14.5  
    14.6  theory List
    14.7 -imports Plain Relation_Power Presburger Recdef ATP_Linkup
    14.8 +imports Plain Presburger Recdef ATP_Linkup
    14.9  uses "Tools/string_syntax.ML"
   14.10  begin
   14.11  
   14.12 @@ -198,7 +198,7 @@
   14.13  
   14.14  definition
   14.15    rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   14.16 -  "rotate n = rotate1 ^^ n"
   14.17 +  "rotate n = rotate1 o^ n"
   14.18  
   14.19  definition
   14.20    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
    15.1 --- a/src/HOL/SizeChange/Interpretation.thy	Fri Apr 17 16:41:31 2009 +0200
    15.2 +++ b/src/HOL/SizeChange/Interpretation.thy	Mon Apr 20 09:32:07 2009 +0200
    15.3 @@ -35,7 +35,7 @@
    15.4  	and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)"
    15.5  	by blast
    15.6    
    15.7 -  let ?s = "\<lambda>i. (f ^ i) x"
    15.8 +  let ?s = "\<lambda>i. (f o^ i) x"
    15.9    
   15.10    {
   15.11  	fix i
    16.1 --- a/src/HOL/UNITY/Comp.thy	Fri Apr 17 16:41:31 2009 +0200
    16.2 +++ b/src/HOL/UNITY/Comp.thy	Mon Apr 20 09:32:07 2009 +0200
    16.3 @@ -15,14 +15,22 @@
    16.4  
    16.5  header{*Composition: Basic Primitives*}
    16.6  
    16.7 -theory Comp imports Union begin
    16.8 +theory Comp
    16.9 +imports Union
   16.10 +begin
   16.11  
   16.12 -instance program :: (type) ord ..
   16.13 +instantiation program :: (type) ord
   16.14 +begin
   16.15  
   16.16 -defs
   16.17 -  component_def:          "F \<le> H == \<exists>G. F\<squnion>G = H"
   16.18 -  strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
   16.19 +definition
   16.20 +  component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
   16.21  
   16.22 +definition
   16.23 +  strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
   16.24 +
   16.25 +instance ..
   16.26 +
   16.27 +end
   16.28  
   16.29  constdefs
   16.30    component_of :: "'a program =>'a program=> bool"
   16.31 @@ -114,7 +122,7 @@
   16.32  by (auto simp add: stable_def component_constrains)
   16.33  
   16.34  (*Used in Guar.thy to show that programs are partially ordered*)
   16.35 -lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
   16.36 +lemmas program_less_le = strict_component_def
   16.37  
   16.38  
   16.39  subsection{*The preserves property*}
   16.40 @@ -229,8 +237,7 @@
   16.41  apply (blast intro: Join_assoc [symmetric])
   16.42  done
   16.43  
   16.44 -lemmas strict_component_of_eq =
   16.45 -    strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
   16.46 +lemmas strict_component_of_eq = strict_component_of_def
   16.47  
   16.48  (** localize **)
   16.49  lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
    17.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Apr 17 16:41:31 2009 +0200
    17.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Apr 20 09:32:07 2009 +0200
    17.3 @@ -338,10 +338,10 @@
    17.4  
    17.5  constdefs
    17.6    wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"  
    17.7 -    "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
    17.8 +    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
    17.9  
   17.10    wens_single :: "[('a*'a) set, 'a set] => 'a set"  
   17.11 -    "wens_single act B == \<Union>i. ((wp act)^i) B"
   17.12 +    "wens_single act B == \<Union>i. (wp act o^ i) B"
   17.13  
   17.14  lemma wens_single_Un_eq:
   17.15        "single_valued act
    18.1 --- a/src/HOL/Word/BinBoolList.thy	Fri Apr 17 16:41:31 2009 +0200
    18.2 +++ b/src/HOL/Word/BinBoolList.thy	Mon Apr 20 09:32:07 2009 +0200
    18.3 @@ -38,7 +38,7 @@
    18.4      if y then rbl_add ws x else ws)"
    18.5  
    18.6  lemma butlast_power:
    18.7 -  "(butlast ^ n) bl = take (length bl - n) bl"
    18.8 +  "(butlast o^ n) bl = take (length bl - n) bl"
    18.9    by (induct n) (auto simp: butlast_take)
   18.10  
   18.11  lemma bin_to_bl_aux_Pls_minus_simp [simp]:
   18.12 @@ -370,14 +370,14 @@
   18.13    done
   18.14  
   18.15  lemma nth_rest_power_bin [rule_format] :
   18.16 -  "ALL n. bin_nth ((bin_rest ^ k) w) n = bin_nth w (n + k)"
   18.17 +  "ALL n. bin_nth ((bin_rest o^ k) w) n = bin_nth w (n + k)"
   18.18    apply (induct k, clarsimp)
   18.19    apply clarsimp
   18.20    apply (simp only: bin_nth.Suc [symmetric] add_Suc)
   18.21    done
   18.22  
   18.23  lemma take_rest_power_bin:
   18.24 -  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^ (n - m)) w)" 
   18.25 +  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest o^ (n - m)) w)" 
   18.26    apply (rule nth_equalityI)
   18.27     apply simp
   18.28    apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
    19.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Apr 17 16:41:31 2009 +0200
    19.2 +++ b/src/HOL/Word/BinGeneral.thy	Mon Apr 20 09:32:07 2009 +0200
    19.3 @@ -822,8 +822,8 @@
    19.4    by (induct n) auto
    19.5  
    19.6  lemma bin_rest_power_trunc [rule_format] :
    19.7 -  "(bin_rest ^ k) (bintrunc n bin) = 
    19.8 -    bintrunc (n - k) ((bin_rest ^ k) bin)"
    19.9 +  "(bin_rest o^ k) (bintrunc n bin) = 
   19.10 +    bintrunc (n - k) ((bin_rest o^ k) bin)"
   19.11    by (induct k) (auto simp: bin_rest_trunc)
   19.12  
   19.13  lemma bin_rest_trunc_i:
   19.14 @@ -857,7 +857,7 @@
   19.15    by (rule ext) auto
   19.16  
   19.17  lemma rco_lem:
   19.18 -  "f o g o f = g o f ==> f o (g o f) ^ n = g ^ n o f"
   19.19 +  "f o g o f = g o f ==> f o (g o f) o^ n = g o^ n o f"
   19.20    apply (rule ext)
   19.21    apply (induct_tac n)
   19.22     apply (simp_all (no_asm))
   19.23 @@ -867,7 +867,7 @@
   19.24    apply simp
   19.25    done
   19.26  
   19.27 -lemma rco_alt: "(f o g) ^ n o f = f o (g o f) ^ n"
   19.28 +lemma rco_alt: "(f o g) o^ n o f = f o (g o f) o^ n"
   19.29    apply (rule ext)
   19.30    apply (induct n)
   19.31     apply (simp_all add: o_def)
   19.32 @@ -891,8 +891,9 @@
   19.33  
   19.34  subsection {* Miscellaneous lemmas *}
   19.35  
   19.36 -lemmas funpow_minus_simp = 
   19.37 -  trans [OF gen_minus [where f = "power f"] funpow_Suc, standard]
   19.38 +lemma funpow_minus_simp:
   19.39 +  "0 < n \<Longrightarrow> f o^ n = f \<circ> f o^ (n - 1)"
   19.40 +  by (cases n) simp_all
   19.41  
   19.42  lemmas funpow_pred_simp [simp] =
   19.43    funpow_minus_simp [of "number_of bin", simplified nobm1, standard]
    20.1 --- a/src/HOL/Word/TdThs.thy	Fri Apr 17 16:41:31 2009 +0200
    20.2 +++ b/src/HOL/Word/TdThs.thy	Mon Apr 20 09:32:07 2009 +0200
    20.3 @@ -110,7 +110,7 @@
    20.4    done
    20.5  
    20.6  lemma fn_comm_power:
    20.7 -  "fa o tr = tr o fr ==> fa ^ n o tr = tr o fr ^ n" 
    20.8 +  "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n" 
    20.9    apply (rule ext) 
   20.10    apply (induct n)
   20.11     apply (auto dest: fun_cong)
    21.1 --- a/src/HOL/Word/WordDefinition.thy	Fri Apr 17 16:41:31 2009 +0200
    21.2 +++ b/src/HOL/Word/WordDefinition.thy	Mon Apr 20 09:32:07 2009 +0200
    21.3 @@ -207,10 +207,10 @@
    21.4    "shiftr1 w = word_of_int (bin_rest (uint w))"
    21.5  
    21.6  definition
    21.7 -  shiftl_def: "w << n = (shiftl1 ^ n) w"
    21.8 +  shiftl_def: "w << n = (shiftl1 o^ n) w"
    21.9  
   21.10  definition
   21.11 -  shiftr_def: "w >> n = (shiftr1 ^ n) w"
   21.12 +  shiftr_def: "w >> n = (shiftr1 o^ n) w"
   21.13  
   21.14  instance ..
   21.15  
   21.16 @@ -245,7 +245,7 @@
   21.17    "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
   21.18  
   21.19    sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
   21.20 -  "w >>> n == (sshiftr1 ^ n) w"
   21.21 +  "w >>> n == (sshiftr1 o^ n) w"
   21.22  
   21.23    mask :: "nat => 'a::len word"
   21.24    "mask n == (1 << n) - 1"
   21.25 @@ -268,7 +268,7 @@
   21.26      case ys of [] => [] | x # xs => last ys # butlast ys"
   21.27  
   21.28    rotater :: "nat => 'a list => 'a list"
   21.29 -  "rotater n == rotater1 ^ n"
   21.30 +  "rotater n == rotater1 o^ n"
   21.31  
   21.32    word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
   21.33    "word_rotr n w == of_bl (rotater n (to_bl w))"
   21.34 @@ -303,7 +303,7 @@
   21.35  constdefs
   21.36    -- "Largest representable machine integer."
   21.37    max_word :: "'a::len word"
   21.38 -  "max_word \<equiv> word_of_int (2^len_of TYPE('a) - 1)"
   21.39 +  "max_word \<equiv> word_of_int (2 ^ len_of TYPE('a) - 1)"
   21.40  
   21.41  consts 
   21.42    of_bool :: "bool \<Rightarrow> 'a::len word"
    22.1 --- a/src/HOL/Word/WordShift.thy	Fri Apr 17 16:41:31 2009 +0200
    22.2 +++ b/src/HOL/Word/WordShift.thy	Mon Apr 20 09:32:07 2009 +0200
    22.3 @@ -361,14 +361,14 @@
    22.4  
    22.5  lemma shiftr_no': 
    22.6    "w = number_of bin ==> 
    22.7 -  (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
    22.8 +  (w::'a::len0 word) >> n = number_of ((bin_rest o^ n) (bintrunc (size w) bin))"
    22.9    apply clarsimp
   22.10    apply (rule word_eqI)
   22.11    apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
   22.12    done
   22.13  
   22.14  lemma sshiftr_no': 
   22.15 -  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n) 
   22.16 +  "w = number_of bin ==> w >>> n = number_of ((bin_rest o^ n) 
   22.17      (sbintrunc (size w - 1) bin))"
   22.18    apply clarsimp
   22.19    apply (rule word_eqI)