# HG changeset patch
# User haftmann
# Date 1240212727 -7200
# Node ID 7ab2716dd93b480af62accb0a6dc04254c0fc5d5
# Parent  a6e26a248f03cd8136a3f436d03bcd4df60151de
power operation on functions with syntax o^; power operation on relations with syntax ^^

diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Bali/Trans.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -359,7 +359,7 @@
 
 abbreviation
   stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
-  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^n"
+  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n"
 
 abbreviation
   steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
@@ -370,25 +370,6 @@
   Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
 *)
 
-lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
-proof -
-  assume "p \<in> R\<^sup>*"
-  moreover obtain x y where p: "p = (x,y)" by (cases p)
-  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
-  hence "\<exists>n. (x,y) \<in> R^n"
-  proof induct
-    fix a have "(a,a) \<in> R^0" by simp
-    thus "\<exists>n. (a,a) \<in> R ^ n" ..
-  next
-    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
-    then obtain n where "(a,b) \<in> R^n" ..
-    moreover assume "(b,c) \<in> R"
-    ultimately have "(a,c) \<in> R^(Suc n)" by auto
-    thus "\<exists>n. (a,c) \<in> R^n" ..
-  qed
-  with p show ?thesis by hypsubst
-qed  
-
 (*
 lemma imp_eval_trans:
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Apr 20 09:32:07 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^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)"
+  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)"
 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^n) s) (f n)"
+  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ 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^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)"
+  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)"
   (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 ^ 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))"
+    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))"
       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 ^ 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)"
+    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)"
       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^n) s) (f n)"
+  assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ 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^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")
+  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")
 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^n) s) (f n)"
+  assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ 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^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")
+  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")
 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.simps uminus_float.simps times_float.simps algebra_simps)
@@ -104,13 +104,13 @@
 
   have move_minus: "Ifloat (-x) = -1 * Ifloat x" by auto
 
-  have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j) = 
+  have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j) = 
     (\<Sum>j = 0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j)"
   proof (rule setsum_cong, simp)
     fix j assume "j \<in> {0 ..< n}"
     show "1 / real (f (j' + j)) * Ifloat x ^ j = -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j"
       unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
-      unfolding real_mult_commute unfolding real_mult_assoc[of "-1^j", symmetric] power_mult_distrib[symmetric]
+      unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
       by auto
   qed
 
@@ -160,21 +160,21 @@
                                             else (0, (max (-l) u) ^ n))"
 
 lemma float_power_bnds: assumes "(l1, u1) = float_power_bnds n l u" and "x \<in> {Ifloat l .. Ifloat u}"
-  shows "x^n \<in> {Ifloat l1..Ifloat u1}"
+  shows "x ^ n \<in> {Ifloat l1..Ifloat u1}"
 proof (cases "even n")
   case True 
   show ?thesis
   proof (cases "0 < l")
     case True hence "odd n \<or> 0 < l" and "0 \<le> Ifloat l" unfolding less_float_def by auto
     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
-    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
+    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
     thus ?thesis using assms `0 < l` unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
   next
     case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
     show ?thesis
     proof (cases "u < 0")
       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
-      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] 
+      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] 
 	unfolding power_minus_even[OF `even n`] by auto
       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
       ultimately show ?thesis using float_power by auto
@@ -194,11 +194,11 @@
 next
   case False hence "odd n \<or> 0 < l" by auto
   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
-  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
+  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
   thus ?thesis unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
 qed
 
-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"
+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"
   using float_power_bnds by auto
 
 section "Square root"
@@ -794,8 +794,8 @@
   let "?f n" = "fact (2 * n)"
 
   { fix n 
-    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)"
+    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)"
       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, 
@@ -811,7 +811,7 @@
   have "0 < x * x" using `0 < x` unfolding less_float_def Ifloat_mult Ifloat_0
     using mult_pos_pos[where a="Ifloat x" and b="Ifloat x"] by auto
 
-  { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i))
+  { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
     = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
   proof -
     have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
@@ -905,8 +905,8 @@
   let "?f n" = "fact (2 * n + 1)"
 
   { fix n 
-    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)"
+    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)"
       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) ^ 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
+    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
     
   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]
@@ -1631,10 +1631,10 @@
 
 lemma ln_bounds:
   assumes "0 \<le> x" and "x < 1"
-  shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x^(Suc i)) \<le> ln (x + 1)" (is "?lb")
-  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x^(Suc i))" (is "?ub")
+  shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
+  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
 proof -
-  let "?a n" = "(1/real (n +1)) * x^(Suc n)"
+  let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
 
   have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
     using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
@@ -2479,7 +2479,7 @@
     fun lift_var (Free (varname, _)) = (case AList.lookup (op =) bound_eqs varname of
                                           SOME bound => bound
                                         | NONE => raise TERM ("No bound equations found for " ^ varname, []))
-      | lift_var t = raise TERM ("Can not convert expression " ^ 
+      | lift_var t = raise TERM ("Can not convert expression " ^
                                  (Syntax.string_of_term ctxt t), [t])
 
     val _ $ vs = HOLogic.dest_Trueprop (Logic.strip_imp_concl goal')
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/HoareParallel/OG_Tran.thy
--- a/src/HOL/HoareParallel/OG_Tran.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/HoareParallel/OG_Tran.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -74,7 +74,7 @@
 abbreviation
   ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) 
                            \<Rightarrow> bool"  ("_ -_\<rightarrow> _"[81,81] 100)  where
-  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition^n"
+  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition ^^ n"
 
 abbreviation
   ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
@@ -84,7 +84,7 @@
 abbreviation
   transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"  
                           ("_ -P_\<rightarrow> _"[81,81,81] 100)  where
-  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition^n"
+  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition ^^ n"
 
 subsection {* Definition of Semantics *}
 
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Compiler0.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -45,7 +45,7 @@
 abbreviation
   stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
     ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)  where
-  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)"
+  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : (stepa1 P ^^ i)"
 
 subsection "The compiler"
 
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Machines.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -1,7 +1,6 @@
-
-(* $Id$ *)
-
-theory Machines imports Natural begin
+theory Machines
+imports Natural
+begin
 
 lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
   by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
@@ -11,20 +10,22 @@
 
 lemmas converse_rel_powE = rel_pow_E2
 
-lemma R_O_Rn_commute: "R O R^n = R^n O R"
+lemma R_O_Rn_commute: "R O R ^^ n = R ^^ n O R"
   by (induct n) (simp, simp add: O_assoc [symmetric])
 
 lemma converse_in_rel_pow_eq:
-  "((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))"
+  "((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))"
 apply(rule iffI)
  apply(blast elim:converse_rel_powE)
 apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
 done
 
-lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
+lemma rel_pow_plus:
+  "R ^^ (m+n) = R ^^ n O R ^^ m"
   by (induct n) (simp, simp add: O_assoc)
 
-lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
+lemma rel_pow_plusI:
+  "\<lbrakk> (x,y) \<in> R ^^ m; (y,z) \<in> R ^^ n \<rbrakk> \<Longrightarrow> (x,z) \<in> R ^^ (m+n)"
   by (simp add: rel_pow_plus rel_compI)
 
 subsection "Instructions"
@@ -57,7 +58,7 @@
 abbreviation
   exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
     ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
-  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^n"
+  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n"
 
 subsection "M0 with lists"
 
@@ -89,7 +90,7 @@
 abbreviation
   stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
     ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
-  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^i)"
+  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)"
 
 inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
 
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Transition.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:        HOL/IMP/Transition.thy
-    ID:           $Id$
     Author:       Tobias Nipkow & Robert Sandner, TUM
     Isar Version: Gerwin Klein, 2001
     Copyright     1996 TUM
@@ -69,7 +68,7 @@
 abbreviation
   evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
     ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)  where
-  "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^n"
+  "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n"
 
 abbreviation
   evalc' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
@@ -77,28 +76,9 @@
   "cs \<longrightarrow>\<^sub>1\<^sup>* cs' == (cs,cs') \<in> evalc1^*"
 
 (*<*)
-(* fixme: move to Relation_Power.thy *)
-lemma rel_pow_Suc_E2 [elim!]:
-  "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
-  by (blast dest: rel_pow_Suc_D2)
+declare rel_pow_Suc_E2 [elim!]
+(*>*)
 
-lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
-proof (induct p)
-  fix x y
-  assume "(x, y) \<in> R\<^sup>*"
-  thus "\<exists>n. (x, y) \<in> R^n"
-  proof induct
-    fix a have "(a, a) \<in> R^0" by simp
-    thus "\<exists>n. (a, a) \<in> R ^ n" ..
-  next
-    fix a b c assume "\<exists>n. (a, b) \<in> R ^ n"
-    then obtain n where "(a, b) \<in> R^n" ..
-    moreover assume "(b, c) \<in> R"
-    ultimately have "(a, c) \<in> R^(Suc n)" by auto
-    thus "\<exists>n. (a, c) \<in> R^n" ..
-  qed
-qed
-(*>*)
 text {*
   As for the big step semantics you can read these rules in a
   syntax directed way:
@@ -189,8 +169,8 @@
 (*<*)
 (* FIXME: relpow.simps don't work *)
 lemmas [simp del] = relpow.simps
-lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by (simp add: relpow.simps)
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by (simp add: relpow.simps)
+lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps)
+lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps)
 
 (*>*)
 lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Import/HOL/HOL4Base.thy
--- a/src/HOL/Import/HOL/HOL4Base.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -2794,8 +2794,8 @@
   by (import numeral numeral_fact)
 
 lemma numeral_funpow: "ALL n::nat.
-   ((f::'a::type => 'a::type) ^ n) (x::'a::type) =
-   (if n = 0 then x else (f ^ (n - 1)) (f x))"
+   ((f::'a::type => 'a::type) o^ n) (x::'a::type) =
+   (if n = 0 then x else (f o^ (n - 1)) (f x))"
   by (import numeral numeral_funpow)
 
 ;end_setup
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Import/HOL/HOL4Word32.thy
--- a/src/HOL/Import/HOL/HOL4Word32.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Mon Apr 20 09:32:07 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 ^ n) (f x) = f ((f ^ n) x)"
+   (f o^ n) (f x) = f ((f o^ n) x)"
   by (import word32 FUNPOW_THM)
 
 lemma FUNPOW_THM2: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
-   (f ^ Suc n) x = f ((f ^ n) x)"
+   (f o^ Suc n) x = f ((f o^ n) x)"
   by (import word32 FUNPOW_THM2)
 
 lemma FUNPOW_COMP: "ALL (f::'a::type => 'a::type) (m::nat) (n::nat) a::'a::type.
-   (f ^ m) ((f ^ n) a) = (f ^ (m + n)) a"
+   (f o^ m) ((f o^ n) a) = (f o^ (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 ^ n) a"
+  "word_lsr == %(a::word32) n::nat. (word_lsr1 o^ n) a"
 
-lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 ^ n) a"
+lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 o^ n) a"
   by (import word32 word_lsr)
 
 constdefs
   word_asr :: "word32 => nat => word32" 
-  "word_asr == %(a::word32) n::nat. (word_asr1 ^ n) a"
+  "word_asr == %(a::word32) n::nat. (word_asr1 o^ n) a"
 
-lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 ^ n) a"
+lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 o^ n) a"
   by (import word32 word_asr)
 
 constdefs
   word_ror :: "word32 => nat => word32" 
-  "word_ror == %(a::word32) n::nat. (word_ror1 ^ n) a"
+  "word_ror == %(a::word32) n::nat. (word_ror1 o^ n) a"
 
-lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 ^ n) a"
+lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 o^ n) a"
   by (import word32 word_ror)
 
 consts
@@ -1583,4 +1583,3 @@
 ;end_setup
 
 end
-
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -202,19 +202,13 @@
 
 constdefs
   FUNPOW :: "('a => 'a) => nat => 'a => 'a"
-  "FUNPOW f n == f ^ n"
+  "FUNPOW f n == f o^ n"
 
-lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
-  (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
-proof auto
-  fix f n x
-  have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
-    by (induct n,auto)
-  thus "f ((f ^ n) x) = (f ^ n) (f x)"
-    ..
-qed
+lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
+  (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
+  by (simp add: funpow_swap1)
 
-lemma [hol4rew]: "FUNPOW f n = f ^ n"
+lemma [hol4rew]: "FUNPOW f n = f o^ n"
   by (simp add: FUNPOW_def)
 
 lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
@@ -224,7 +218,7 @@
   by simp
 
 lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
-  by (simp, arith)
+  by (simp) arith
 
 lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   by (simp add: max_def)
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -786,7 +786,7 @@
 
 lemma funpow_lmap:
   fixes f :: "'a \<Rightarrow> 'a"
-  shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)"
+  shows "(lmap f o^ n) (LCons b l) = LCons ((f o^ n) b) ((lmap f o^ n) l)"
   by (induct n) simp_all
 
 
@@ -796,35 +796,35 @@
 proof
   fix x
   have "(h x, iterates f x) \<in>
-      {((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}"
+      {((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u)) | u n. True}"
   proof -
-    have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))"
+    have "(h x, iterates f x) = ((lmap f o^ 0) (h x), (lmap f o^ 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 ^ n) (h u), (lmap f ^ n) (iterates f u))"
+    then obtain u n where "q = ((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u))"
         (is "_ = (?q1, ?q2)")
       by auto
-    also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))"
+    also have "?q1 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (h u))"
     proof -
-      have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))"
+      have "?q1 = (lmap f o^ n) (LCons u (lmap f (h u)))"
         by (subst h) rule
-      also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))"
+      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (lmap f (h u)))"
         by (rule funpow_lmap)
-      also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)"
+      also have "(lmap f o^ n) (lmap f (h u)) = (lmap f o^ Suc n) (h u)"
         by (simp add: funpow_swap1)
       finally show ?thesis .
     qed
-    also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))"
+    also have "?q2 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (iterates f u))"
     proof -
-      have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))"
+      have "?q2 = (lmap f o^ n) (LCons u (iterates f (f u)))"
         by (subst iterates) rule
-      also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))"
+      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (iterates f (f u)))"
         by (rule funpow_lmap)
-      also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)"
+      also have "(lmap f o^ n) (iterates f (f u)) = (lmap f o^ Suc n) (iterates f u)"
         by (simp add: lmap_iterates funpow_swap1)
       finally show ?thesis .
     qed
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Continuity.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -5,7 +5,7 @@
 header {* Continuity and iterations (of set transformers) *}
 
 theory Continuity
-imports Relation_Power Main
+imports Transitive_Closure Main
 begin
 
 subsection {* Continuity for complete lattices *}
@@ -48,25 +48,25 @@
 qed
 
 lemma continuous_lfp:
- assumes "continuous F" shows "lfp F = (SUP i. (F^^i) bot)"
+ assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
 proof -
   note mono = continuous_mono[OF `continuous F`]
-  { fix i have "(F^^i) bot \<le> lfp F"
+  { fix i have "(F o^ i) bot \<le> lfp F"
     proof (induct i)
-      show "(F^^0) bot \<le> lfp F" by simp
+      show "(F o^ 0) bot \<le> lfp F" by simp
     next
       case (Suc i)
-      have "(F^^(Suc i)) bot = F((F^^i) bot)" by simp
+      have "(F o^ Suc i) bot = F((F o^ 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^^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
-  moreover have "lfp F \<le> (SUP i. (F^^i) bot)" (is "_ \<le> ?U")
+  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")
   proof (rule lfp_lowerbound)
-    have "chain(%i. (F^^i) bot)"
+    have "chain(%i. (F o^ i) bot)"
     proof -
-      { fix i have "(F^^i) bot \<le> (F^^(Suc i)) bot"
+      { fix i have "(F o^ i) bot \<le> (F o^ (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^^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
+    hence "F ?U = (SUP i. (F o^ (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^^n) {}"
+  "up_iterate f n = (f o^ 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^^n) UNIV"
+  "down_iterate f n = (f o^ n) UNIV"
 
 lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   by (simp add: down_iterate_def)
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -1022,13 +1022,15 @@
 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)"
   by simp
 
-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)"
+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)"
   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 ^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)
+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)"
+  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}*}
 subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -5441,7 +5441,7 @@
   have "1 - c > 0" using c by auto
 
   from s(2) obtain z0 where "z0 \<in> s" by auto
-  def z \<equiv> "\<lambda> n::nat. fun_pow n f z0"
+  def z \<equiv> "\<lambda> n::nat. funpow n f z0"
   { fix n::nat
     have "z n \<in> s" unfolding z_def
     proof(induct n) case 0 thus ?case using `z0 \<in>s` by auto
@@ -5580,7 +5580,7 @@
       using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
   def y \<equiv> "g x"
   have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
-  def f \<equiv> "\<lambda> n. fun_pow n g"
+  def f \<equiv> "\<lambda> n. funpow n g"
   have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
   have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
   { fix n::nat and z assume "z\<in>s"
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/List.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Plain Relation_Power Presburger Recdef ATP_Linkup
+imports Plain Presburger Recdef ATP_Linkup
 uses "Tools/string_syntax.ML"
 begin
 
@@ -198,7 +198,7 @@
 
 definition
   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "rotate n = rotate1 ^^ n"
+  "rotate n = rotate1 o^ n"
 
 definition
   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/SizeChange/Interpretation.thy
--- a/src/HOL/SizeChange/Interpretation.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/SizeChange/Interpretation.thy	Mon Apr 20 09:32:07 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 ^ i) x"
+  let ?s = "\<lambda>i. (f o^ i) x"
   
   {
 	fix i
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/UNITY/Comp.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -15,14 +15,22 @@
 
 header{*Composition: Basic Primitives*}
 
-theory Comp imports Union begin
+theory Comp
+imports Union
+begin
 
-instance program :: (type) ord ..
+instantiation program :: (type) ord
+begin
 
-defs
-  component_def:          "F \<le> H == \<exists>G. F\<squnion>G = H"
-  strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
+definition
+  component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
 
+definition
+  strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
+
+instance ..
+
+end
 
 constdefs
   component_of :: "'a program =>'a program=> bool"
@@ -114,7 +122,7 @@
 by (auto simp add: stable_def component_constrains)
 
 (*Used in Guar.thy to show that programs are partially ordered*)
-lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
+lemmas program_less_le = strict_component_def
 
 
 subsection{*The preserves property*}
@@ -229,8 +237,7 @@
 apply (blast intro: Join_assoc [symmetric])
 done
 
-lemmas strict_component_of_eq =
-    strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
+lemmas strict_component_of_eq = strict_component_of_def
 
 (** localize **)
 lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Mon Apr 20 09:32:07 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)^i) B"
+    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
 
   wens_single :: "[('a*'a) set, 'a set] => 'a set"  
-    "wens_single act B == \<Union>i. ((wp act)^i) B"
+    "wens_single act B == \<Union>i. (wp act o^ i) B"
 
 lemma wens_single_Un_eq:
       "single_valued act
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -38,7 +38,7 @@
     if y then rbl_add ws x else ws)"
 
 lemma butlast_power:
-  "(butlast ^ n) bl = take (length bl - n) bl"
+  "(butlast o^ 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 ^ k) w) n = bin_nth w (n + k)"
+  "ALL n. bin_nth ((bin_rest o^ 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 ^ (n - m)) w)" 
+  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest o^ (n - m)) w)" 
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -822,8 +822,8 @@
   by (induct n) auto
 
 lemma bin_rest_power_trunc [rule_format] :
-  "(bin_rest ^ k) (bintrunc n bin) = 
-    bintrunc (n - k) ((bin_rest ^ k) bin)"
+  "(bin_rest o^ k) (bintrunc n bin) = 
+    bintrunc (n - k) ((bin_rest o^ 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) ^ n = g ^ n o f"
+  "f o g o f = g o f ==> f o (g o f) o^ n = g o^ 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) ^ n o f = f o (g o f) ^ n"
+lemma rco_alt: "(f o g) o^ n o f = f o (g o f) o^ n"
   apply (rule ext)
   apply (induct n)
    apply (simp_all add: o_def)
@@ -891,8 +891,9 @@
 
 subsection {* Miscellaneous lemmas *}
 
-lemmas funpow_minus_simp = 
-  trans [OF gen_minus [where f = "power f"] funpow_Suc, standard]
+lemma funpow_minus_simp:
+  "0 < n \<Longrightarrow> f o^ n = f \<circ> f o^ (n - 1)"
+  by (cases n) simp_all
 
 lemmas funpow_pred_simp [simp] =
   funpow_minus_simp [of "number_of bin", simplified nobm1, standard]
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/TdThs.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -110,7 +110,7 @@
   done
 
 lemma fn_comm_power:
-  "fa o tr = tr o fr ==> fa ^ n o tr = tr o fr ^ n" 
+  "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n" 
   apply (rule ext) 
   apply (induct n)
    apply (auto dest: fun_cong)
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -207,10 +207,10 @@
   "shiftr1 w = word_of_int (bin_rest (uint w))"
 
 definition
-  shiftl_def: "w << n = (shiftl1 ^ n) w"
+  shiftl_def: "w << n = (shiftl1 o^ n) w"
 
 definition
-  shiftr_def: "w >> n = (shiftr1 ^ n) w"
+  shiftr_def: "w >> n = (shiftr1 o^ n) w"
 
 instance ..
 
@@ -245,7 +245,7 @@
   "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
 
   sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
-  "w >>> n == (sshiftr1 ^ n) w"
+  "w >>> n == (sshiftr1 o^ n) w"
 
   mask :: "nat => 'a::len word"
   "mask n == (1 << n) - 1"
@@ -268,7 +268,7 @@
     case ys of [] => [] | x # xs => last ys # butlast ys"
 
   rotater :: "nat => 'a list => 'a list"
-  "rotater n == rotater1 ^ n"
+  "rotater n == rotater1 o^ n"
 
   word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
   "word_rotr n w == of_bl (rotater n (to_bl w))"
@@ -303,7 +303,7 @@
 constdefs
   -- "Largest representable machine integer."
   max_word :: "'a::len word"
-  "max_word \<equiv> word_of_int (2^len_of TYPE('a) - 1)"
+  "max_word \<equiv> word_of_int (2 ^ len_of TYPE('a) - 1)"
 
 consts 
   of_bool :: "bool \<Rightarrow> 'a::len word"
diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/WordShift.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -361,14 +361,14 @@
 
 lemma shiftr_no': 
   "w = number_of bin ==> 
-  (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
+  (w::'a::len0 word) >> n = number_of ((bin_rest o^ 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 ^ n) 
+  "w = number_of bin ==> w >>> n = number_of ((bin_rest o^ n) 
     (sbintrunc (size w - 1) bin))"
   apply clarsimp
   apply (rule word_eqI)