Renamed (^) to [^] in preparation of the move from "op X" to (X)
authornipkow
Fri Jan 05 18:41:42 2018 +0100 (18 months ago)
changeset 67341df79ef3b3a41
parent 67340 150d40a25622
child 67342 7905adb28bdc
Renamed (^) to [^] in preparation of the move from "op X" to (X)
NEWS
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/More_Finite_Product.thy
src/HOL/Algebra/More_Group.thy
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Decision_Procs/Algebra_Aux.thy
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Reflective_Field.thy
src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
src/HOL/Number_Theory/Prime_Powers.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Quotient_Examples/Int_Pow.thy
     1.1 --- a/NEWS	Fri Jan 05 15:24:57 2018 +0100
     1.2 +++ b/NEWS	Fri Jan 05 18:41:42 2018 +0100
     1.3 @@ -166,6 +166,8 @@
     1.4  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* HOL-Algebra: renamed (^) to [^]
     1.8 +
     1.9  * Session HOL-Analysis: Moebius functions and the Riemann mapping
    1.10  theorem.
    1.11  
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jan 05 15:24:57 2018 +0100
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Jan 05 18:41:42 2018 +0100
     2.3 @@ -502,12 +502,12 @@
     2.4  
     2.5  lemma finprod_const:
     2.6    assumes a [simp]: "a : carrier G"
     2.7 -    shows "finprod G (%x. a) A = a (^) card A"
     2.8 +    shows "finprod G (%x. a) A = a [^] card A"
     2.9  proof (induct A rule: infinite_finite_induct)
    2.10    case (insert b A)
    2.11    show ?case 
    2.12    proof (subst finprod_insert[OF insert(1-2)])
    2.13 -    show "a \<otimes> (\<Otimes>x\<in>A. a) = a (^) card (insert b A)"
    2.14 +    show "a \<otimes> (\<Otimes>x\<in>A. a) = a [^] card (insert b A)"
    2.15        by (insert insert, auto, subst m_comm, auto)
    2.16    qed auto
    2.17  qed auto
     3.1 --- a/src/HOL/Algebra/Group.thy	Fri Jan 05 15:24:57 2018 +0100
     3.2 +++ b/src/HOL/Algebra/Group.thy	Fri Jan 05 18:41:42 2018 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4    where "Units G = {y. y \<in> carrier G \<and> (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
     3.5  
     3.6  consts
     3.7 -  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "'(^')\<index>" 75)
     3.8 +  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "[^]\<index>" 75)
     3.9  
    3.10  overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
    3.11  begin
    3.12 @@ -44,7 +44,7 @@
    3.13      in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
    3.14  end
    3.15  
    3.16 -lemma int_pow_int: "x (^)\<^bsub>G\<^esub> (int n) = x (^)\<^bsub>G\<^esub> n"
    3.17 +lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
    3.18  by(simp add: int_pow_def nat_pow_def)
    3.19  
    3.20  locale monoid =
    3.21 @@ -196,27 +196,27 @@
    3.22  text \<open>Power\<close>
    3.23  
    3.24  lemma (in monoid) nat_pow_closed [intro, simp]:
    3.25 -  "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
    3.26 +  "x \<in> carrier G ==> x [^] (n::nat) \<in> carrier G"
    3.27    by (induct n) (simp_all add: nat_pow_def)
    3.28  
    3.29  lemma (in monoid) nat_pow_0 [simp]:
    3.30 -  "x (^) (0::nat) = \<one>"
    3.31 +  "x [^] (0::nat) = \<one>"
    3.32    by (simp add: nat_pow_def)
    3.33  
    3.34  lemma (in monoid) nat_pow_Suc [simp]:
    3.35 -  "x (^) (Suc n) = x (^) n \<otimes> x"
    3.36 +  "x [^] (Suc n) = x [^] n \<otimes> x"
    3.37    by (simp add: nat_pow_def)
    3.38  
    3.39  lemma (in monoid) nat_pow_one [simp]:
    3.40 -  "\<one> (^) (n::nat) = \<one>"
    3.41 +  "\<one> [^] (n::nat) = \<one>"
    3.42    by (induct n) simp_all
    3.43  
    3.44  lemma (in monoid) nat_pow_mult:
    3.45 -  "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
    3.46 +  "x \<in> carrier G ==> x [^] (n::nat) \<otimes> x [^] m = x [^] (n + m)"
    3.47    by (induct m) (simp_all add: m_assoc [THEN sym])
    3.48  
    3.49  lemma (in monoid) nat_pow_pow:
    3.50 -  "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
    3.51 +  "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
    3.52    by (induct m) (simp, simp add: nat_pow_mult add.commute)
    3.53  
    3.54  
    3.55 @@ -406,33 +406,33 @@
    3.56  text \<open>Power\<close>
    3.57  
    3.58  lemma (in group) int_pow_def2:
    3.59 -  "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
    3.60 +  "a [^] (z::int) = (if z < 0 then inv (a [^] (nat (-z))) else a [^] (nat z))"
    3.61    by (simp add: int_pow_def nat_pow_def Let_def)
    3.62  
    3.63  lemma (in group) int_pow_0 [simp]:
    3.64 -  "x (^) (0::int) = \<one>"
    3.65 +  "x [^] (0::int) = \<one>"
    3.66    by (simp add: int_pow_def2)
    3.67  
    3.68  lemma (in group) int_pow_one [simp]:
    3.69 -  "\<one> (^) (z::int) = \<one>"
    3.70 +  "\<one> [^] (z::int) = \<one>"
    3.71    by (simp add: int_pow_def2)
    3.72  
    3.73  (* The following are contributed by Joachim Breitner *)
    3.74  
    3.75  lemma (in group) int_pow_closed [intro, simp]:
    3.76 -  "x \<in> carrier G ==> x (^) (i::int) \<in> carrier G"
    3.77 +  "x \<in> carrier G ==> x [^] (i::int) \<in> carrier G"
    3.78    by (simp add: int_pow_def2)
    3.79  
    3.80  lemma (in group) int_pow_1 [simp]:
    3.81 -  "x \<in> carrier G \<Longrightarrow> x (^) (1::int) = x"
    3.82 +  "x \<in> carrier G \<Longrightarrow> x [^] (1::int) = x"
    3.83    by (simp add: int_pow_def2)
    3.84  
    3.85  lemma (in group) int_pow_neg:
    3.86 -  "x \<in> carrier G \<Longrightarrow> x (^) (-i::int) = inv (x (^) i)"
    3.87 +  "x \<in> carrier G \<Longrightarrow> x [^] (-i::int) = inv (x [^] i)"
    3.88    by (simp add: int_pow_def2)
    3.89  
    3.90  lemma (in group) int_pow_mult:
    3.91 -  "x \<in> carrier G \<Longrightarrow> x (^) (i + j::int) = x (^) i \<otimes> x (^) j"
    3.92 +  "x \<in> carrier G \<Longrightarrow> x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
    3.93  proof -
    3.94    have [simp]: "-i - j = -j - i" by simp
    3.95    assume "x : carrier G" then
    3.96 @@ -441,7 +441,7 @@
    3.97  qed
    3.98  
    3.99  lemma (in group) int_pow_diff:
   3.100 -  "x \<in> carrier G \<Longrightarrow> x (^) (n - m :: int) = x (^) n \<otimes> inv (x (^) m)"
   3.101 +  "x \<in> carrier G \<Longrightarrow> x [^] (n - m :: int) = x [^] n \<otimes> inv (x [^] m)"
   3.102  by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
   3.103  
   3.104  lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"
   3.105 @@ -676,7 +676,7 @@
   3.106  
   3.107  (* Contributed by Joachim Breitner *)
   3.108  lemma (in group) int_pow_is_hom:
   3.109 -  "x \<in> carrier G \<Longrightarrow> (op(^) x) \<in> hom \<lparr> carrier = UNIV, mult = op +, one = 0::int \<rparr> G "
   3.110 +  "x \<in> carrier G \<Longrightarrow> (op[^] x) \<in> hom \<lparr> carrier = UNIV, mult = op +, one = 0::int \<rparr> G "
   3.111    unfolding hom_def by (simp add: int_pow_mult)
   3.112  
   3.113  
   3.114 @@ -737,7 +737,7 @@
   3.115  
   3.116  lemma (in comm_monoid) nat_pow_distr:
   3.117    "[| x \<in> carrier G; y \<in> carrier G |] ==>
   3.118 -  (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   3.119 +  (x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
   3.120    by (induct n) (simp, simp add: m_ac)
   3.121  
   3.122  locale comm_group = comm_monoid + group
     4.1 --- a/src/HOL/Algebra/More_Finite_Product.thy	Fri Jan 05 15:24:57 2018 +0100
     4.2 +++ b/src/HOL/Algebra/More_Finite_Product.thy	Fri Jan 05 18:41:42 2018 +0100
     4.3 @@ -82,14 +82,14 @@
     4.4  
     4.5  lemma (in monoid) units_of_pow:
     4.6    fixes n :: nat
     4.7 -  shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
     4.8 +  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
     4.9    apply (induct n)
    4.10    apply (auto simp add: units_group group.is_monoid
    4.11      monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
    4.12    done
    4.13  
    4.14  lemma (in cring) units_power_order_eq_one:
    4.15 -  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a (^) card(Units R) = \<one>"
    4.16 +  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
    4.17    apply (subst units_of_carrier [symmetric])
    4.18    apply (subst units_of_one [symmetric])
    4.19    apply (subst units_of_pow [symmetric])
     5.1 --- a/src/HOL/Algebra/More_Group.thy	Fri Jan 05 15:24:57 2018 +0100
     5.2 +++ b/src/HOL/Algebra/More_Group.thy	Fri Jan 05 18:41:42 2018 +0100
     5.3 @@ -113,14 +113,14 @@
     5.4  lemma (in comm_group) power_order_eq_one:
     5.5    assumes fin [simp]: "finite (carrier G)"
     5.6      and a [simp]: "a \<in> carrier G"
     5.7 -  shows "a (^) card(carrier G) = one G"
     5.8 +  shows "a [^] card(carrier G) = one G"
     5.9  proof -
    5.10    have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
    5.11      by (subst (2) finprod_reindex [symmetric],
    5.12        auto simp add: Pi_def inj_on_const_mult surj_const_mult)
    5.13    also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
    5.14      by (auto simp add: finprod_multf Pi_def)
    5.15 -  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
    5.16 +  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
    5.17      by (auto simp add: finprod_const)
    5.18    finally show ?thesis
    5.19  (* uses the preceeding lemma *)
     6.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Fri Jan 05 15:24:57 2018 +0100
     6.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Fri Jan 05 18:41:42 2018 +0100
     6.3 @@ -84,7 +84,7 @@
     6.4  
     6.5  lemma evalRR_monom:
     6.6    assumes a: "a \<in> carrier R" and x: "x \<in> carrier R"
     6.7 -  shows "eval R R id x (monom P a d) = a \<otimes> x (^) d"
     6.8 +  shows "eval R R id x (monom P a d) = a \<otimes> x [^] d"
     6.9  proof -
    6.10    interpret UP_pre_univ_prop R R id by unfold_locales simp
    6.11    show ?thesis using assms by (simp add: eval_monom)
    6.12 @@ -271,33 +271,33 @@
    6.13  lemma pow_eq_div2 :
    6.14    fixes m n :: nat
    6.15    assumes x_car: "x \<in> carrier G"
    6.16 -  assumes pow_eq: "x (^) m = x (^) n"
    6.17 -  shows "x (^) (m - n) = \<one>"
    6.18 +  assumes pow_eq: "x [^] m = x [^] n"
    6.19 +  shows "x [^] (m - n) = \<one>"
    6.20  proof (cases "m < n")
    6.21    case False
    6.22 -  have "\<one> \<otimes> x (^) m = x (^) m" by (simp add: x_car)
    6.23 -  also have "\<dots> = x (^) (m - n) \<otimes> x (^) n"
    6.24 +  have "\<one> \<otimes> x [^] m = x [^] m" by (simp add: x_car)
    6.25 +  also have "\<dots> = x [^] (m - n) \<otimes> x [^] n"
    6.26      using False by (simp add: nat_pow_mult x_car)
    6.27 -  also have "\<dots> = x (^) (m - n) \<otimes> x (^) m"
    6.28 +  also have "\<dots> = x [^] (m - n) \<otimes> x [^] m"
    6.29      by (simp add: pow_eq)
    6.30    finally show ?thesis by (simp add: x_car)
    6.31  qed simp
    6.32  
    6.33 -definition ord where "ord a = Min {d \<in> {1 .. order G} . a (^) d = \<one>}"
    6.34 +definition ord where "ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
    6.35  
    6.36  lemma
    6.37    assumes finite:"finite (carrier G)"
    6.38    assumes a:"a \<in> carrier G"
    6.39    shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"
    6.40 -    and pow_ord_eq_1: "a (^) ord a = \<one>"
    6.41 +    and pow_ord_eq_1: "a [^] ord a = \<one>"
    6.42  proof -
    6.43 -  have "\<not>inj_on (\<lambda>x. a (^) x) {0 .. order G}"
    6.44 +  have "\<not>inj_on (\<lambda>x. a [^] x) {0 .. order G}"
    6.45    proof (rule notI)
    6.46 -    assume A: "inj_on (\<lambda>x. a (^) x) {0 .. order G}"
    6.47 +    assume A: "inj_on (\<lambda>x. a [^] x) {0 .. order G}"
    6.48      have "order G + 1 = card {0 .. order G}" by simp
    6.49 -    also have "\<dots> = card ((\<lambda>x. a (^) x) ` {0 .. order G})" (is "_ = card ?S")
    6.50 +    also have "\<dots> = card ((\<lambda>x. a [^] x) ` {0 .. order G})" (is "_ = card ?S")
    6.51        using A by (simp add: card_image)
    6.52 -    also have "?S = {a (^) x | x. x \<in> {0 .. order G}}" by blast
    6.53 +    also have "?S = {a [^] x | x. x \<in> {0 .. order G}}" by blast
    6.54      also have "\<dots> \<subseteq> carrier G" (is "?S \<subseteq> _") using a by blast
    6.55      then have "card ?S \<le> order G" unfolding order_def
    6.56        by (rule card_mono[OF finite])
    6.57 @@ -305,8 +305,8 @@
    6.58    qed
    6.59  
    6.60    then obtain x y where x_y:"x \<noteq> y" "x \<in> {0 .. order G}" "y \<in> {0 .. order G}"
    6.61 -                        "a (^) x = a (^) y" unfolding inj_on_def by blast
    6.62 -  obtain d where "1 \<le> d" "a (^) d = \<one>" "d \<le> order G"
    6.63 +                        "a [^] x = a [^] y" unfolding inj_on_def by blast
    6.64 +  obtain d where "1 \<le> d" "a [^] d = \<one>" "d \<le> order G"
    6.65    proof cases
    6.66      assume "y < x" with x_y show ?thesis
    6.67        by (intro that[where d="x - y"]) (auto simp add: pow_eq_div2[OF a])
    6.68 @@ -314,22 +314,22 @@
    6.69      assume "\<not>y < x" with x_y show ?thesis
    6.70        by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])
    6.71    qed
    6.72 -  hence "ord a \<in> {d \<in> {1 .. order G} . a (^) d = \<one>}"
    6.73 -    unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a (^) d = \<one>}"]
    6.74 +  hence "ord a \<in> {d \<in> {1 .. order G} . a [^] d = \<one>}"
    6.75 +    unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a [^] d = \<one>}"]
    6.76      by fastforce
    6.77 -  then show "1 \<le> ord a" and "ord a \<le> order G" and "a (^) ord a = \<one>"
    6.78 +  then show "1 \<le> ord a" and "ord a \<le> order G" and "a [^] ord a = \<one>"
    6.79      by (auto simp: order_def)
    6.80  qed
    6.81  
    6.82  lemma finite_group_elem_finite_ord :
    6.83    assumes "finite (carrier G)" "x \<in> carrier G"
    6.84 -  shows "\<exists> d::nat. d \<ge> 1 \<and> x (^) d = \<one>"
    6.85 +  shows "\<exists> d::nat. d \<ge> 1 \<and> x [^] d = \<one>"
    6.86    using assms ord_ge_1 pow_ord_eq_1 by auto
    6.87  
    6.88  lemma ord_min:
    6.89 -  assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
    6.90 +  assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a [^] d = \<one>" shows "ord a \<le> d"
    6.91  proof -
    6.92 -  define Ord where "Ord = {d \<in> {1..order G}. a (^) d = \<one>}"
    6.93 +  define Ord where "Ord = {d \<in> {1..order G}. a [^] d = \<one>}"
    6.94    have fin: "finite Ord" by (auto simp: Ord_def)
    6.95    have in_ord: "ord a \<in> Ord"
    6.96      using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
    6.97 @@ -350,22 +350,22 @@
    6.98  lemma ord_inj :
    6.99    assumes finite: "finite (carrier G)"
   6.100    assumes a: "a \<in> carrier G"
   6.101 -  shows "inj_on (\<lambda> x . a (^) x) {0 .. ord a - 1}"
   6.102 +  shows "inj_on (\<lambda> x . a [^] x) {0 .. ord a - 1}"
   6.103  proof (rule inj_onI, rule ccontr)
   6.104 -  fix x y assume A: "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}" "a (^) x= a (^) y" "x \<noteq> y"
   6.105 +  fix x y assume A: "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}" "a [^] x= a [^] y" "x \<noteq> y"
   6.106  
   6.107 -  have "finite {d \<in> {1..order G}. a (^) d = \<one>}" by auto
   6.108 +  have "finite {d \<in> {1..order G}. a [^] d = \<one>}" by auto
   6.109  
   6.110    { fix x y assume A: "x < y" "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}"
   6.111 -        "a (^) x = a (^) y"
   6.112 +        "a [^] x = a [^] y"
   6.113      hence "y - x < ord a" by auto
   6.114      also have "\<dots> \<le> order G" using assms by (simp add: ord_le_group_order)
   6.115      finally have y_x_range:"y - x \<in> {1 .. order G}" using A by force
   6.116 -    have "a (^) (y-x) = \<one>" using a A by (simp add: pow_eq_div2)
   6.117 +    have "a [^] (y-x) = \<one>" using a A by (simp add: pow_eq_div2)
   6.118  
   6.119 -    hence y_x:"y - x \<in> {d \<in> {1.. order G}. a (^) d = \<one>}" using y_x_range by blast
   6.120 +    hence y_x:"y - x \<in> {d \<in> {1.. order G}. a [^] d = \<one>}" using y_x_range by blast
   6.121      have "min (y - x) (ord a) = ord a"
   6.122 -      using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a (^) d = \<one>}\<close> y_x] ord_def by auto
   6.123 +      using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a [^] d = \<one>}\<close> y_x] ord_def by auto
   6.124      with \<open>y - x < ord a\<close> have False by linarith
   6.125    }
   6.126    note X = this
   6.127 @@ -382,22 +382,22 @@
   6.128  lemma ord_inj' :
   6.129    assumes finite: "finite (carrier G)"
   6.130    assumes a: "a \<in> carrier G"
   6.131 -  shows "inj_on (\<lambda> x . a (^) x) {1 .. ord a}"
   6.132 +  shows "inj_on (\<lambda> x . a [^] x) {1 .. ord a}"
   6.133  proof (rule inj_onI, rule ccontr)
   6.134    fix x y :: nat
   6.135 -  assume A:"x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a (^) x = a (^) y" "x\<noteq>y"
   6.136 +  assume A:"x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a [^] x = a [^] y" "x\<noteq>y"
   6.137    { assume "x < ord a" "y < ord a"
   6.138      hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
   6.139    }
   6.140    moreover
   6.141    { assume "x = ord a" "y < ord a"
   6.142 -    hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   6.143 +    hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   6.144      hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
   6.145      hence False using A by fastforce
   6.146    }
   6.147    moreover
   6.148    { assume "y = ord a" "x < ord a"
   6.149 -    hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   6.150 +    hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   6.151      hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
   6.152      hence False using A by fastforce
   6.153    }
   6.154 @@ -406,35 +406,35 @@
   6.155  
   6.156  lemma ord_elems :
   6.157    assumes "finite (carrier G)" "a \<in> carrier G"
   6.158 -  shows "{a(^)x | x. x \<in> (UNIV :: nat set)} = {a(^)x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
   6.159 +  shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
   6.160  proof
   6.161    show "?R \<subseteq> ?L" by blast
   6.162    { fix y assume "y \<in> ?L"
   6.163 -    then obtain x::nat where x:"y = a(^)x" by auto
   6.164 +    then obtain x::nat where x:"y = a[^]x" by auto
   6.165      define r where "r = x mod ord a"
   6.166      then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
   6.167 -    hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
   6.168 +    hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
   6.169        using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
   6.170 -    hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1)
   6.171 +    hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
   6.172      have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
   6.173      hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
   6.174 -    hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a(^)r\<close> by blast
   6.175 +    hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
   6.176    }
   6.177    thus "?L \<subseteq> ?R" by auto
   6.178  qed
   6.179  
   6.180  lemma ord_dvd_pow_eq_1 :
   6.181 -  assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
   6.182 +  assumes "finite (carrier G)" "a \<in> carrier G" "a [^] k = \<one>"
   6.183    shows "ord a dvd k"
   6.184  proof -
   6.185    define r where "r = k mod ord a"
   6.186    then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
   6.187 -  hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
   6.188 +  hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"
   6.189        using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
   6.190 -  hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1)
   6.191 -  hence "a(^)r = \<one>" using assms(3) by simp
   6.192 +  hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)
   6.193 +  hence "a[^]r = \<one>" using assms(3) by simp
   6.194    have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
   6.195 -  hence "r = 0" using \<open>a(^)r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith
   6.196 +  hence "r = 0" using \<open>a[^]r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith
   6.197    thus ?thesis using q by simp
   6.198  qed
   6.199  
   6.200 @@ -450,14 +450,14 @@
   6.201  lemma ord_pow_dvd_ord_elem :
   6.202    assumes finite[simp]: "finite (carrier G)"
   6.203    assumes a[simp]:"a \<in> carrier G"
   6.204 -  shows "ord (a(^)n) = ord a div gcd n (ord a)"
   6.205 +  shows "ord (a[^]n) = ord a div gcd n (ord a)"
   6.206  proof -
   6.207 -  have "(a(^)n) (^) ord a = (a (^) ord a) (^) n"
   6.208 +  have "(a[^]n) [^] ord a = (a [^] ord a) [^] n"
   6.209      by (simp add: mult.commute nat_pow_pow)
   6.210 -  hence "(a(^)n) (^) ord a = \<one>" by (simp add: pow_ord_eq_1)
   6.211 +  hence "(a[^]n) [^] ord a = \<one>" by (simp add: pow_ord_eq_1)
   6.212    obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)
   6.213 -  hence "(a(^)n) (^) (ord a div gcd n (ord a)) = (a (^) ord a)(^)q"  by (simp add : nat_pow_pow)
   6.214 -  hence pow_eq_1: "(a(^)n) (^) (ord a div gcd n (ord a)) = \<one>"
   6.215 +  hence "(a[^]n) [^] (ord a div gcd n (ord a)) = (a [^] ord a)[^]q"  by (simp add : nat_pow_pow)
   6.216 +  hence pow_eq_1: "(a[^]n) [^] (ord a div gcd n (ord a)) = \<one>"
   6.217       by (auto simp add : pow_ord_eq_1[of a])
   6.218    have "ord a \<ge> 1" using ord_ge_1 by simp
   6.219    have ge_1:"ord a div gcd n (ord a) \<ge> 1"
   6.220 @@ -471,12 +471,12 @@
   6.221      have "ord a div gcd n (ord a) \<le> ord a" by simp
   6.222      thus ?thesis using \<open>ord a \<le> order G\<close> by linarith
   6.223    qed
   6.224 -  hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
   6.225 +  hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}"
   6.226      using ge_1 pow_eq_1 by force
   6.227    { fix d :: nat
   6.228 -    assume d_elem:"d \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
   6.229 +    assume d_elem:"d \<in> {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}"
   6.230      assume d_lt:"d < ord a div gcd n (ord a)"
   6.231 -    hence pow_nd:"a(^)(n*d)  = \<one>" using d_elem
   6.232 +    hence pow_nd:"a[^](n*d)  = \<one>" using d_elem
   6.233        by (simp add : nat_pow_pow)
   6.234      hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)
   6.235      then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)
   6.236 @@ -500,9 +500,9 @@
   6.237      have "d > 0" using d_elem by simp
   6.238      hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
   6.239      hence False using d_lt by simp
   6.240 -  } hence ord_gcd_min: "\<And> d . d \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}
   6.241 +  } hence ord_gcd_min: "\<And> d . d \<in> {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}
   6.242                          \<Longrightarrow> d\<ge>ord a div gcd n (ord a)" by fastforce
   6.243 -  have fin:"finite {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}" by auto
   6.244 +  have fin:"finite {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}" by auto
   6.245    thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]
   6.246      unfolding ord_def by simp
   6.247  qed
   6.248 @@ -519,33 +519,33 @@
   6.249  lemma element_generates_subgroup:
   6.250    assumes finite[simp]: "finite (carrier G)"
   6.251    assumes a[simp]: "a \<in> carrier G"
   6.252 -  shows "subgroup {a (^) i | i. i \<in> {0 .. ord a - 1}} G"
   6.253 +  shows "subgroup {a [^] i | i. i \<in> {0 .. ord a - 1}} G"
   6.254  proof
   6.255 -  show "{a(^)i | i. i \<in> {0 .. ord a - 1} } \<subseteq> carrier G" by auto
   6.256 +  show "{a[^]i | i. i \<in> {0 .. ord a - 1} } \<subseteq> carrier G" by auto
   6.257  next
   6.258    fix x y
   6.259 -  assume A: "x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" "y \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   6.260 -  obtain i::nat where i:"x = a(^)i" and i2:"i \<in> UNIV" using A by auto
   6.261 -  obtain j::nat where j:"y = a(^)j" and j2:"j \<in> UNIV" using A by auto
   6.262 -  have "a(^)(i+j) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto
   6.263 -  thus "x \<otimes> y \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   6.264 +  assume A: "x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" "y \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
   6.265 +  obtain i::nat where i:"x = a[^]i" and i2:"i \<in> UNIV" using A by auto
   6.266 +  obtain j::nat where j:"y = a[^]j" and j2:"j \<in> UNIV" using A by auto
   6.267 +  have "a[^](i+j) \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto
   6.268 +  thus "x \<otimes> y \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
   6.269      using i j a ord_elems assms by (auto simp add: nat_pow_mult)
   6.270  next
   6.271 -  show "\<one> \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" by force
   6.272 +  show "\<one> \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" by force
   6.273  next
   6.274 -  fix x assume x: "x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   6.275 +  fix x assume x: "x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
   6.276    hence x_in_carrier: "x \<in> carrier G" by auto
   6.277 -  then obtain d::nat where d:"x (^) d = \<one>" and "d\<ge>1"
   6.278 +  then obtain d::nat where d:"x [^] d = \<one>" and "d\<ge>1"
   6.279      using finite_group_elem_finite_ord by auto
   6.280 -  have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using \<open>d\<ge>1\<close> d nat_pow_Suc[of x "d - 1"] by simp
   6.281 -  have elem:"x (^) (d - 1) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   6.282 +  have inv_1:"x[^](d - 1) \<otimes> x = \<one>" using \<open>d\<ge>1\<close> d nat_pow_Suc[of x "d - 1"] by simp
   6.283 +  have elem:"x [^] (d - 1) \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"
   6.284    proof -
   6.285 -    obtain i::nat where i:"x = a(^)i" using x by auto
   6.286 -    hence "x(^)(d - 1) \<in> {a(^)i | i. i \<in> (UNIV::nat set)}" by (auto simp add: nat_pow_pow)
   6.287 +    obtain i::nat where i:"x = a[^]i" using x by auto
   6.288 +    hence "x[^](d - 1) \<in> {a[^]i | i. i \<in> (UNIV::nat set)}" by (auto simp add: nat_pow_pow)
   6.289      thus ?thesis using ord_elems[of a] by auto
   6.290    qed
   6.291 -  have inv:"inv x = x(^)(d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast
   6.292 -  thus "inv x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" using elem inv by auto
   6.293 +  have inv:"inv x = x[^](d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast
   6.294 +  thus "inv x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" using elem inv by auto
   6.295  qed
   6.296  
   6.297  lemma ord_dvd_group_order :
   6.298 @@ -553,13 +553,13 @@
   6.299    assumes a[simp]: "a \<in> carrier G"
   6.300    shows "ord a dvd order G"
   6.301  proof -
   6.302 -  have card_dvd:"card {a(^)i | i. i \<in> {0 .. ord a - 1}} dvd card (carrier G)"
   6.303 +  have card_dvd:"card {a[^]i | i. i \<in> {0 .. ord a - 1}} dvd card (carrier G)"
   6.304      using lagrange_dvd element_generates_subgroup unfolding order_def by simp
   6.305 -  have "inj_on (\<lambda> i . a(^)i) {0..ord a - 1}" using ord_inj by simp
   6.306 -  hence cards_eq:"card ( (\<lambda> i . a(^)i) ` {0..ord a - 1}) = card {0..ord a - 1}"
   6.307 -    using card_image[of "\<lambda> i . a(^)i" "{0..ord a - 1}"] by auto
   6.308 -  have "(\<lambda> i . a(^)i) ` {0..ord a - 1} = {a(^)i | i. i \<in> {0..ord a - 1}}" by auto
   6.309 -  hence "card {a(^)i | i. i \<in> {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp
   6.310 +  have "inj_on (\<lambda> i . a[^]i) {0..ord a - 1}" using ord_inj by simp
   6.311 +  hence cards_eq:"card ( (\<lambda> i . a[^]i) ` {0..ord a - 1}) = card {0..ord a - 1}"
   6.312 +    using card_image[of "\<lambda> i . a[^]i" "{0..ord a - 1}"] by auto
   6.313 +  have "(\<lambda> i . a[^]i) ` {0..ord a - 1} = {a[^]i | i. i \<in> {0..ord a - 1}}" by auto
   6.314 +  hence "card {a[^]i | i. i \<in> {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp
   6.315    also have "\<dots> = ord a" using ord_ge_1[of a] by simp
   6.316    finally show ?thesis using card_dvd by (simp add: order_def)
   6.317  qed
   6.318 @@ -580,7 +580,7 @@
   6.319  lemma mult_mult_of: "mult (mult_of R) = mult R"
   6.320   by (simp add: mult_of_def)
   6.321  
   6.322 -lemma nat_pow_mult_of: "op (^)\<^bsub>mult_of R\<^esub> = (op (^)\<^bsub>R\<^esub> :: _ \<Rightarrow> nat \<Rightarrow> _)"
   6.323 +lemma nat_pow_mult_of: "op [^]\<^bsub>mult_of R\<^esub> = (op [^]\<^bsub>R\<^esub> :: _ \<Rightarrow> nat \<Rightarrow> _)"
   6.324    by (simp add: mult_of_def fun_eq_iff nat_pow_def)
   6.325  
   6.326  lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
   6.327 @@ -609,7 +609,7 @@
   6.328  lemma (in monoid) Units_pow_closed :
   6.329    fixes d :: nat
   6.330    assumes "x \<in> Units G"
   6.331 -  shows "x (^) d \<in> Units G"
   6.332 +  shows "x [^] d \<in> Units G"
   6.333      by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)
   6.334  
   6.335  lemma (in comm_monoid) is_monoid:
   6.336 @@ -644,7 +644,7 @@
   6.337    have "\<And>x. eval R R id x f \<noteq> \<zero>"
   6.338    proof -
   6.339      fix x
   6.340 -    have "(\<Oplus>i\<in>{..deg R f}. id (coeff P f i) \<otimes> x (^) i) \<noteq> \<zero>"
   6.341 +    have "(\<Oplus>i\<in>{..deg R f}. id (coeff P f i) \<otimes> x [^] i) \<noteq> \<zero>"
   6.342        using 0 lcoeff_nonzero_nonzero[where p = f] by simp
   6.343      thus "eval R R id x f \<noteq> \<zero>" using 0 unfolding eval_def P_def by simp
   6.344    qed
   6.345 @@ -697,7 +697,7 @@
   6.346    fixes p d :: nat
   6.347    assumes finite:"finite (carrier R)"
   6.348    assumes d_neq_zero : "d \<noteq> 0"
   6.349 -  shows "card {x \<in> carrier R. x (^) d = \<one>} \<le> d"
   6.350 +  shows "card {x \<in> carrier R. x [^] d = \<one>} \<le> d"
   6.351  proof -
   6.352    let ?f = "monom (UP R) \<one>\<^bsub>R\<^esub> d \<ominus>\<^bsub> (UP R)\<^esub> monom (UP R) \<one>\<^bsub>R\<^esub> 0"
   6.353    have one_in_carrier:"\<one> \<in> carrier R" by simp
   6.354 @@ -708,9 +708,9 @@
   6.355    have roots_bound:"finite {a \<in> carrier R . eval R R id a ?f = \<zero>} \<and>
   6.356                      card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"
   6.357                      using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
   6.358 -  have subs:"{x \<in> carrier R. x (^) d = \<one>} \<subseteq> {a \<in> carrier R . eval R R id a ?f = \<zero>}"
   6.359 +  have subs:"{x \<in> carrier R. x [^] d = \<one>} \<subseteq> {a \<in> carrier R . eval R R id a ?f = \<zero>}"
   6.360      by (auto simp: R.evalRR_simps)
   6.361 -  then have "card {x \<in> carrier R. x (^) d = \<one>} \<le>
   6.362 +  then have "card {x \<in> carrier R. x [^] d = \<one>} \<le>
   6.363          card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
   6.364    thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith
   6.365  qed
   6.366 @@ -728,7 +728,7 @@
   6.367  \<close>
   6.368  
   6.369  lemma (in group) pow_order_eq_1:
   6.370 -  assumes "finite (carrier G)" "x \<in> carrier G" shows "x (^) order G = \<one>"
   6.371 +  assumes "finite (carrier G)" "x \<in> carrier G" shows "x [^] order G = \<one>"
   6.372    using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)
   6.373  
   6.374  (* XXX remove in AFP devel, replaced by div_eq_dividend_iff *)
   6.375 @@ -742,7 +742,7 @@
   6.376  lemma (in group)
   6.377    assumes finite': "finite (carrier G)"
   6.378    assumes "a \<in> carrier G"
   6.379 -  shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
   6.380 +  shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
   6.381  proof
   6.382    assume A: ?L then show ?R
   6.383      using assms ord_ge_1 [OF assms]
   6.384 @@ -762,32 +762,32 @@
   6.385    note mult_of_simps[simp]
   6.386    have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
   6.387  
   6.388 -  interpret G:group "mult_of R" rewrites "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
   6.389 +  interpret G:group "mult_of R" rewrites "op [^]\<^bsub>mult_of R\<^esub> = (op [^] :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
   6.390      by (rule field_mult_group) simp_all
   6.391  
   6.392    from exists
   6.393    obtain a where a:"a \<in> carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
   6.394      by (auto simp add: card_gt_0_iff)
   6.395  
   6.396 -  have set_eq1:"{a(^)n| n. n \<in> {1 .. d}} = {x \<in> carrier (mult_of R). x (^) d = \<one>}"
   6.397 +  have set_eq1:"{a[^]n| n. n \<in> {1 .. d}} = {x \<in> carrier (mult_of R). x [^] d = \<one>}"
   6.398    proof (rule card_seteq)
   6.399 -    show "finite {x \<in> carrier (mult_of R). x (^) d = \<one>}" using finite by auto
   6.400 +    show "finite {x \<in> carrier (mult_of R). x [^] d = \<one>}" using finite by auto
   6.401  
   6.402 -    show "{a(^)n| n. n \<in> {1 ..d}} \<subseteq> {x \<in> carrier (mult_of R). x(^)d = \<one>}"
   6.403 +    show "{a[^]n| n. n \<in> {1 ..d}} \<subseteq> {x \<in> carrier (mult_of R). x[^]d = \<one>}"
   6.404      proof
   6.405 -      fix x assume "x \<in> {a(^)n | n. n \<in> {1 .. d}}"
   6.406 -      then obtain n where n:"x = a(^)n \<and> n \<in> {1 .. d}" by auto
   6.407 -      have "x(^)d =(a(^)d)(^)n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
   6.408 -      hence "x(^)d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce
   6.409 -      thus "x \<in> {x \<in> carrier (mult_of R). x(^)d = \<one>}" using G.nat_pow_closed[OF a] n by blast
   6.410 +      fix x assume "x \<in> {a[^]n | n. n \<in> {1 .. d}}"
   6.411 +      then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" by auto
   6.412 +      have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
   6.413 +      hence "x[^]d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce
   6.414 +      thus "x \<in> {x \<in> carrier (mult_of R). x[^]d = \<one>}" using G.nat_pow_closed[OF a] n by blast
   6.415      qed
   6.416  
   6.417 -    show "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {a(^)n | n. n \<in> {1 .. d}}"
   6.418 +    show "card {x \<in> carrier (mult_of R). x [^] d = \<one>} \<le> card {a[^]n | n. n \<in> {1 .. d}}"
   6.419      proof -
   6.420 -      have *:"{a(^)n | n. n \<in> {1 .. d }} = ((\<lambda> n. a(^)n) ` {1 .. d})" by auto
   6.421 +      have *:"{a[^]n | n. n \<in> {1 .. d }} = ((\<lambda> n. a[^]n) ` {1 .. d})" by auto
   6.422        have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
   6.423          using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)
   6.424 -      have "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {x \<in> carrier R. x (^) d = \<one>}"
   6.425 +      have "card {x \<in> carrier (mult_of R). x [^] d = \<one>} \<le> card {x \<in> carrier R. x [^] d = \<one>}"
   6.426          using finite by (auto intro: card_mono)
   6.427        also have "\<dots> \<le> d" using \<open>0 < order (mult_of R)\<close> num_roots_le_deg[OF finite, of d]
   6.428          by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])
   6.429 @@ -796,20 +796,20 @@
   6.430    qed
   6.431  
   6.432    have set_eq2:"{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}
   6.433 -                = (\<lambda> n . a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d}" (is "?L = ?R")
   6.434 +                = (\<lambda> n . a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
   6.435    proof
   6.436      { fix x assume x:"x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
   6.437 -      hence "x \<in> {x \<in> carrier (mult_of R). x (^) d = \<one>}"
   6.438 +      hence "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
   6.439          by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])
   6.440 -      then obtain n where n:"x = a(^)n \<and> n \<in> {1 .. d}" using set_eq1 by blast
   6.441 +      then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" using set_eq1 by blast
   6.442        hence "x \<in> ?R" using x by fast
   6.443      } thus "?L \<subseteq> ?R" by blast
   6.444      show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
   6.445    qed
   6.446 -  have "inj_on (\<lambda> n . a(^)n) {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d}"
   6.447 +  have "inj_on (\<lambda> n . a[^]n) {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
   6.448      using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast
   6.449 -  hence "card ((\<lambda>n. a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d})
   6.450 -         = card {k \<in> {1 .. d}. group.ord (mult_of R) (a(^)k) = d}"
   6.451 +  hence "card ((\<lambda>n. a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d})
   6.452 +         = card {k \<in> {1 .. d}. group.ord (mult_of R) (a[^]k) = d}"
   6.453           using card_image by blast
   6.454    thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \<open>a \<in> _\<close>, unfolded ord_a]
   6.455      by (simp add: phi'_def)
   6.456 @@ -820,13 +820,13 @@
   6.457  
   6.458  theorem (in field) finite_field_mult_group_has_gen :
   6.459    assumes finite:"finite (carrier R)"
   6.460 -  shows "\<exists> a \<in> carrier (mult_of R) . carrier (mult_of R) = {a(^)i | i::nat . i \<in> UNIV}"
   6.461 +  shows "\<exists> a \<in> carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i \<in> UNIV}"
   6.462  proof -
   6.463    note mult_of_simps[simp]
   6.464    have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
   6.465  
   6.466    interpret G: group "mult_of R" rewrites
   6.467 -      "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
   6.468 +      "op [^]\<^bsub>mult_of R\<^esub> = (op [^] :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
   6.469      by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)
   6.470  
   6.471    let ?N = "\<lambda> x . card {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = x}"
   6.472 @@ -888,17 +888,17 @@
   6.473    hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
   6.474    then obtain a where a:"a \<in> carrier (mult_of R)" and a_ord:"group.ord (mult_of R) a = order (mult_of R)"
   6.475      by (auto simp add: card_gt_0_iff)
   6.476 -  hence set_eq:"{a(^)i | i::nat. i \<in> UNIV} = (\<lambda>x. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}"
   6.477 +  hence set_eq:"{a[^]i | i::nat. i \<in> UNIV} = (\<lambda>x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}"
   6.478      using G.ord_elems[OF finite'] by auto
   6.479 -  have card_eq:"card ((\<lambda>x. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
   6.480 +  have card_eq:"card ((\<lambda>x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
   6.481      by (intro card_image G.ord_inj finite' a)
   6.482 -  hence "card ((\<lambda> x . a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
   6.483 +  hence "card ((\<lambda> x . a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
   6.484      using assms by (simp add: card_eq a_ord)
   6.485 -  hence card_R_minus_1:"card {a(^)i | i::nat. i \<in> UNIV} =  order (mult_of R)"
   6.486 +  hence card_R_minus_1:"card {a[^]i | i::nat. i \<in> UNIV} =  order (mult_of R)"
   6.487      using * by (subst set_eq) auto
   6.488 -  have **:"{a(^)i | i::nat. i \<in> UNIV} \<subseteq> carrier (mult_of R)"
   6.489 +  have **:"{a[^]i | i::nat. i \<in> UNIV} \<subseteq> carrier (mult_of R)"
   6.490      using G.nat_pow_closed[OF a] by auto
   6.491 -  with _ have "carrier (mult_of R) = {a(^)i|i::nat. i \<in> UNIV}"
   6.492 +  with _ have "carrier (mult_of R) = {a[^]i|i::nat. i \<in> UNIV}"
   6.493      by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
   6.494    thus ?thesis using a by blast
   6.495  qed
     7.1 --- a/src/HOL/Algebra/Ring.thy	Fri Jan 05 15:24:57 2018 +0100
     7.2 +++ b/src/HOL/Algebra/Ring.thy	Fri Jan 05 18:41:42 2018 +0100
     7.3 @@ -146,13 +146,13 @@
     7.4  
     7.5  lemmas finsum_reindex = add.finprod_reindex
     7.6  
     7.7 -(* The following would be wrong.  Needed is the equivalent of (^) for addition,
     7.8 +(* The following would be wrong.  Needed is the equivalent of [^] for addition,
     7.9    or indeed the canonical embedding from Nat into the monoid.
    7.10  
    7.11  lemma finsum_const:
    7.12    assumes fin [simp]: "finite A"
    7.13        and a [simp]: "a : carrier G"
    7.14 -    shows "finsum G (%x. a) A = a (^) card A"
    7.15 +    shows "finsum G (%x. a) A = a [^] card A"
    7.16    using fin apply induct
    7.17    apply force
    7.18    apply (subst finsum_insert)
    7.19 @@ -427,7 +427,7 @@
    7.20    a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
    7.21  
    7.22  lemma (in semiring) nat_pow_zero:
    7.23 -  "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> (^) n = \<zero>"
    7.24 +  "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> [^] n = \<zero>"
    7.25    by (induct n) simp_all
    7.26  
    7.27  context semiring begin
     8.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Jan 05 15:24:57 2018 +0100
     8.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Jan 05 18:41:42 2018 +0100
     8.3 @@ -1175,7 +1175,7 @@
     8.4    eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
     8.5             'a => 'b, 'b, nat => 'a] => 'b"
     8.6    where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
     8.7 -    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
     8.8 +    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
     8.9  
    8.10  context UP
    8.11  begin
    8.12 @@ -1183,7 +1183,7 @@
    8.13  lemma eval_on_carrier:
    8.14    fixes S (structure)
    8.15    shows "p \<in> carrier P ==>
    8.16 -  eval R S phi s p = (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.17 +  eval R S phi s p = (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.18    by (unfold eval_def, fold P_def) simp
    8.19  
    8.20  lemma eval_extensional:
    8.21 @@ -1227,35 +1227,35 @@
    8.22    then show "eval R S h s (p \<oplus>\<^bsub>P\<^esub> q) = eval R S h s p \<oplus>\<^bsub>S\<^esub> eval R S h s q"
    8.23    proof (simp only: eval_on_carrier P.a_closed)
    8.24      from S R have
    8.25 -      "(\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
    8.26 +      "(\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
    8.27        (\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<oplus>\<^bsub>P\<^esub> q)<..max (deg R p) (deg R q)}.
    8.28 -        h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.29 +        h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.30        by (simp cong: S.finsum_cong
    8.31          add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def del: coeff_add)
    8.32      also from R have "... =
    8.33          (\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}.
    8.34 -          h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.35 +          h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.36        by (simp add: ivl_disj_un_one)
    8.37      also from R S have "... =
    8.38 -      (\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.39 -      (\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.40 +      (\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.41 +      (\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.42        by (simp cong: S.finsum_cong
    8.43          add: S.l_distr deg_aboveD ivl_disj_int_one Pi_def)
    8.44      also have "... =
    8.45          (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
    8.46 -          h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.47 +          h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.48          (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
    8.49 -          h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.50 +          h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.51        by (simp only: ivl_disj_un_one max.cobounded1 max.cobounded2)
    8.52      also from R S have "... =
    8.53 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.54 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.55 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.56 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.57        by (simp cong: S.finsum_cong
    8.58          add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def)
    8.59      finally show
    8.60 -      "(\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
    8.61 -      (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.62 -      (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
    8.63 +      "(\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
    8.64 +      (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    8.65 +      (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)" .
    8.66    qed
    8.67  next
    8.68    show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>"
    8.69 @@ -1266,31 +1266,31 @@
    8.70    then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q"
    8.71    proof (simp only: eval_on_carrier UP_mult_closed)
    8.72      from R S have
    8.73 -      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
    8.74 +      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
    8.75        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}.
    8.76 -        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.77 +        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.78        by (simp cong: S.finsum_cong
    8.79          add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
    8.80          del: coeff_mult)
    8.81      also from R have "... =
    8.82 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.83 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.84        by (simp only: ivl_disj_un_one deg_mult_ring)
    8.85      also from R S have "... =
    8.86        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
    8.87           \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
    8.88             h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
    8.89 -           (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
    8.90 +           (s [^]\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> (i - k)))"
    8.91        by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
    8.92          S.m_ac S.finsum_rdistr)
    8.93      also from R S have "... =
    8.94 -      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
    8.95 -      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
    8.96 +      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
    8.97 +      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    8.98        by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
    8.99          Pi_def)
   8.100      finally show
   8.101 -      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
   8.102 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
   8.103 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
   8.104 +      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
   8.105 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
   8.106 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)" .
   8.107    qed
   8.108  qed
   8.109  
   8.110 @@ -1314,13 +1314,13 @@
   8.111    shows "eval R S h s (monom P \<one> 1) = s"
   8.112  proof (simp only: eval_on_carrier monom_closed R.one_closed)
   8.113     from S have
   8.114 -    "(\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
   8.115 +    "(\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
   8.116      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
   8.117 -      h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
   8.118 +      h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
   8.119      by (simp cong: S.finsum_cong del: coeff_monom
   8.120        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def)
   8.121    also have "... =
   8.122 -    (\<Oplus>\<^bsub>S\<^esub> i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
   8.123 +    (\<Oplus>\<^bsub>S\<^esub> i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
   8.124      by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
   8.125    also have "... = s"
   8.126    proof (cases "s = \<zero>\<^bsub>S\<^esub>")
   8.127 @@ -1329,7 +1329,7 @@
   8.128      case False then show ?thesis by (simp add: S Pi_def)
   8.129    qed
   8.130    finally show "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (monom P \<one> 1)}.
   8.131 -    h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" .
   8.132 +    h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) = s" .
   8.133  qed
   8.134  
   8.135  end
   8.136 @@ -1342,7 +1342,7 @@
   8.137  
   8.138  lemma (in UP_cring) monom_pow:
   8.139    assumes R: "a \<in> carrier R"
   8.140 -  shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)"
   8.141 +  shows "(monom P a n) [^]\<^bsub>P\<^esub> m = monom P (a [^] m) (n * m)"
   8.142  proof (induct m)
   8.143    case 0 from R show ?case by simp
   8.144  next
   8.145 @@ -1351,25 +1351,25 @@
   8.146  qed
   8.147  
   8.148  lemma (in ring_hom_cring) hom_pow [simp]:
   8.149 -  "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^bsub>S\<^esub> (n::nat)"
   8.150 +  "x \<in> carrier R ==> h (x [^] n) = h x [^]\<^bsub>S\<^esub> (n::nat)"
   8.151    by (induct n) simp_all
   8.152  
   8.153  lemma (in UP_univ_prop) Eval_monom:
   8.154 -  "r \<in> carrier R ==> Eval (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
   8.155 +  "r \<in> carrier R ==> Eval (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> n"
   8.156  proof -
   8.157    assume R: "r \<in> carrier R"
   8.158 -  from R have "Eval (monom P r n) = Eval (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) (^)\<^bsub>P\<^esub> n)"
   8.159 +  from R have "Eval (monom P r n) = Eval (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) [^]\<^bsub>P\<^esub> n)"
   8.160      by (simp del: monom_mult add: monom_mult [THEN sym] monom_pow)
   8.161    also
   8.162    from R eval_monom1 [where s = s, folded Eval_def]
   8.163 -  have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
   8.164 +  have "... = h r \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> n"
   8.165      by (simp add: eval_const [where s = s, folded Eval_def])
   8.166    finally show ?thesis .
   8.167  qed
   8.168  
   8.169  lemma (in UP_pre_univ_prop) eval_monom:
   8.170    assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
   8.171 -  shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
   8.172 +  shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> n"
   8.173  proof -
   8.174    interpret UP_univ_prop R S h P s "eval R S h s"
   8.175      using UP_pre_univ_prop_axioms P_def R S
   8.176 @@ -1411,11 +1411,11 @@
   8.177    interpret ring_hom_cring P S Phi by fact
   8.178    interpret ring_hom_cring P S Psi by fact
   8.179    have "Phi p =
   8.180 -      Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
   8.181 +      Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 [^]\<^bsub>P\<^esub> i)"
   8.182      by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
   8.183    also
   8.184    have "... =
   8.185 -      Psi (\<Oplus>\<^bsub>P \<^esub>i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
   8.186 +      Psi (\<Oplus>\<^bsub>P \<^esub>i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 [^]\<^bsub>P\<^esub> i)"
   8.187      by (simp add: Phi Psi P Pi_def comp_def)
   8.188    also have "... = Psi p"
   8.189      by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
   8.190 @@ -1445,7 +1445,7 @@
   8.191  context monoid
   8.192  begin
   8.193  
   8.194 -lemma nat_pow_eone[simp]: assumes x_in_G: "x \<in> carrier G" shows "x (^) (1::nat) = x"
   8.195 +lemma nat_pow_eone[simp]: assumes x_in_G: "x \<in> carrier G" shows "x [^] (1::nat) = x"
   8.196    using nat_pow_Suc [of x 0] unfolding nat_pow_0 [of x] unfolding l_one [OF x_in_G] by simp
   8.197  
   8.198  end
   8.199 @@ -1550,14 +1550,14 @@
   8.200  lemma long_div_theorem:
   8.201    assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
   8.202    and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
   8.203 -  shows "\<exists>q r (k::nat). (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R g)"
   8.204 +  shows "\<exists>q r (k::nat). (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)[^]\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R g)"
   8.205    using f_in_P
   8.206  proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
   8.207    case (1 f)
   8.208    note f_in_P [simp] = "1.prems"
   8.209    let ?pred = "(\<lambda> q r (k::nat).
   8.210      (q \<in> carrier P) \<and> (r \<in> carrier P)
   8.211 -    \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R g))"
   8.212 +    \<and> (lcoeff g)[^]\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R g))"
   8.213    let ?lg = "lcoeff g" and ?lf = "lcoeff f"
   8.214    show ?case
   8.215    proof (cases "deg R f < deg R g")
   8.216 @@ -1585,7 +1585,7 @@
   8.217        next
   8.218          case False note deg_f_nzero = False
   8.219          {
   8.220 -          have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1"
   8.221 +          have exist: "lcoeff g [^] ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1"
   8.222              by (simp add: minus_add r_neg sym [
   8.223                OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]])
   8.224            have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?f1) < deg R f"
   8.225 @@ -1611,28 +1611,28 @@
   8.226              qed (simp_all add: deg_f_nzero)
   8.227            qed
   8.228            then obtain q' r' k'
   8.229 -            where rem_desc: "?lg (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?f1) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
   8.230 +            where rem_desc: "?lg [^] (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?f1) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
   8.231              and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
   8.232              and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
   8.233              using "1.hyps" using f1_in_carrier by blast
   8.234            show ?thesis
   8.235 -          proof (rule exI3 [of _ "((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
   8.236 -            show "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
   8.237 +          proof (rule exI3 [of _ "((?lg [^] k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
   8.238 +            show "(?lg [^] (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((?lg [^] k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
   8.239              proof -
   8.240 -              have "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1)"
   8.241 +              have "(?lg [^] (Suc k')) \<odot>\<^bsub>P\<^esub> f = (?lg [^] k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1)"
   8.242                  using smult_assoc1 [OF _ _ f_in_P] using exist by simp
   8.243 -              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?f1))"
   8.244 +              also have "\<dots> = (?lg [^] k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((?lg [^] k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?f1))"
   8.245                  using UP_smult_r_distr by simp
   8.246 -              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
   8.247 +              also have "\<dots> = (?lg [^] k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
   8.248                  unfolding rem_desc ..
   8.249 -              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
   8.250 -                using sym [OF a_assoc [of "?lg (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
   8.251 +              also have "\<dots> = (?lg [^] k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
   8.252 +                using sym [OF a_assoc [of "?lg [^] k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
   8.253                  using r'_in_carrier q'_in_carrier by simp
   8.254 -              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
   8.255 +              also have "\<dots> = (?lg [^] k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
   8.256                  using q'_in_carrier by (auto simp add: m_comm)
   8.257 -              also have "\<dots> = (((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
   8.258 +              also have "\<dots> = (((?lg [^] k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
   8.259                  using smult_assoc2 q'_in_carrier "1.prems" by auto
   8.260 -              also have "\<dots> = ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
   8.261 +              also have "\<dots> = ((?lg [^] k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
   8.262                  using sym [OF l_distr] and q'_in_carrier by auto
   8.263                finally show ?thesis using m_comm q'_in_carrier by auto
   8.264              qed
   8.265 @@ -1740,7 +1740,7 @@
   8.266    from deg_minus_monom [OF a R_not_trivial]
   8.267    have deg_g_nzero: "deg R ?g \<noteq> 0" by simp
   8.268    have "\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and>
   8.269 -    lcoeff ?g (^) k \<odot>\<^bsub>P\<^esub> f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R ?g)"
   8.270 +    lcoeff ?g [^] k \<odot>\<^bsub>P\<^esub> f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R ?g)"
   8.271      using long_div_theorem [OF _ f deg_nzero_nzero [OF deg_g_nzero]] a
   8.272      by auto
   8.273    then show ?thesis
     9.1 --- a/src/HOL/Decision_Procs/Algebra_Aux.thy	Fri Jan 05 15:24:57 2018 +0100
     9.2 +++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Fri Jan 05 18:41:42 2018 +0100
     9.3 @@ -190,7 +190,7 @@
     9.4    with assms show "x \<ominus> y = \<zero>" by (simp add: minus_eq r_neg)
     9.5  qed
     9.6  
     9.7 -lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x (^) (2::nat) = x \<otimes> x"
     9.8 +lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x [^] (2::nat) = x \<otimes> x"
     9.9    by (simp add: numeral_eq_Suc)
    9.10  
    9.11  lemma eq_neg_iff_add_eq_0:
    9.12 @@ -230,7 +230,7 @@
    9.13  
    9.14  end
    9.15  
    9.16 -lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> (^) n"
    9.17 +lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> [^] n"
    9.18    by (induct n) (simp_all add: m_ac)
    9.19  
    9.20  definition cring_class_ops :: "'a::comm_ring_1 ring"
    9.21 @@ -267,7 +267,7 @@
    9.22  lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
    9.23    by (simp add: a_minus_def carrier_class plus_class uminus_class)
    9.24  
    9.25 -lemma power_class: "x (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    9.26 +lemma power_class: "x [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    9.27    by (induct n) (simp_all add: one_class times_class
    9.28      monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
    9.29      monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])
    9.30 @@ -288,14 +288,14 @@
    9.31      and "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
    9.32      and "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x"
    9.33      and "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
    9.34 -    and "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    9.35 +    and "(x::'a) [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    9.36      and "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
    9.37      and "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i"
    9.38      and "(Int.of_int (numeral m)::'a) = numeral m"
    9.39    by (simp_all add: cring_class class_simps)
    9.40  
    9.41  lemma (in domain) nat_pow_eq_0_iff [simp]:
    9.42 -  "a \<in> carrier R \<Longrightarrow> (a (^) (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
    9.43 +  "a \<in> carrier R \<Longrightarrow> (a [^] (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
    9.44    by (induct n) (auto simp add: integral_iff)
    9.45  
    9.46  lemma (in domain) square_eq_iff:
    9.47 @@ -446,7 +446,7 @@
    9.48  
    9.49  lemma nonzero_power_divide:
    9.50    "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow>
    9.51 -    (a \<oslash> b) (^) (n::nat) = a (^) n \<oslash> b (^) n"
    9.52 +    (a \<oslash> b) [^] (n::nat) = a [^] n \<oslash> b [^] n"
    9.53    by (induct n) (simp_all add: nonzero_divide_divide_eq_left)
    9.54  
    9.55  lemma r_diff_distr:
    9.56 @@ -504,7 +504,7 @@
    9.57      and "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
    9.58      and "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x"
    9.59      and "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
    9.60 -    and "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    9.61 +    and "(x::'a) [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    9.62      and "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
    9.63      and "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i"
    9.64      and "(x::'a) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y"
    10.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Jan 05 15:24:57 2018 +0100
    10.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Jan 05 18:41:42 2018 +0100
    10.3 @@ -58,7 +58,7 @@
    10.4    where
    10.5      "Ipol l (Pc c) = \<guillemotleft>c\<guillemotright>"
    10.6    | "Ipol l (Pinj i P) = Ipol (drop i l) P"
    10.7 -  | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l (^) x \<oplus> Ipol (drop 1 l) Q"
    10.8 +  | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l [^] x \<oplus> Ipol (drop 1 l) Q"
    10.9  
   10.10  lemma Ipol_Pc:
   10.11    "Ipol l (Pc 0) = \<zero>"
   10.12 @@ -77,7 +77,7 @@
   10.13    | "Ipolex l (Add P Q) = Ipolex l P \<oplus> Ipolex l Q"
   10.14    | "Ipolex l (Sub P Q) = Ipolex l P \<ominus> Ipolex l Q"
   10.15    | "Ipolex l (Mul P Q) = Ipolex l P \<otimes> Ipolex l Q"
   10.16 -  | "Ipolex l (Pow p n) = Ipolex l p (^) n"
   10.17 +  | "Ipolex l (Pow p n) = Ipolex l p [^] n"
   10.18    | "Ipolex l (Neg P) = \<ominus> Ipolex l P"
   10.19  
   10.20  lemma Ipolex_Const:
   10.21 @@ -302,7 +302,7 @@
   10.22         a_ac m_ac nat_pow_mult [symmetric] of_int_2)
   10.23  
   10.24  text \<open>Power\<close>
   10.25 -lemma pow_ci: "in_carrier ls \<Longrightarrow> Ipol ls (pow n P) = Ipol ls P (^) n"
   10.26 +lemma pow_ci: "in_carrier ls \<Longrightarrow> Ipol ls (pow n P) = Ipol ls P [^] n"
   10.27  proof (induct n arbitrary: P rule: less_induct)
   10.28    case (less k)
   10.29    consider "k = 0" | "k > 0" by arith
   10.30 @@ -313,7 +313,7 @@
   10.31    next
   10.32      case 2
   10.33      then have "k div 2 < k" by arith
   10.34 -    with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) (^) (k div 2)"
   10.35 +    with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) [^] (k div 2)"
   10.36        by simp
   10.37      show ?thesis
   10.38      proof (cases "even k")
   10.39 @@ -358,7 +358,7 @@
   10.40    where
   10.41      "Imon l (Mc c) = \<guillemotleft>c\<guillemotright>"
   10.42    | "Imon l (Minj i M) = Imon (drop i l) M"
   10.43 -  | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l (^) x"
   10.44 +  | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l [^] x"
   10.45  
   10.46  lemma (in cring) Imon_closed [simp]: "in_carrier l \<Longrightarrow> Imon l m \<in> carrier R"
   10.47    by (induct m arbitrary: l) simp_all
   10.48 @@ -385,7 +385,7 @@
   10.49  lemma (in cring) Minj_pred_correct: "0 < i \<Longrightarrow> Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)"
   10.50    by (simp add: Minj_pred_def mkMinj_correct)
   10.51  
   10.52 -lemma (in cring) mkMX_correct: "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l (^) i"
   10.53 +lemma (in cring) mkMX_correct: "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l [^] i"
   10.54    by (induct M)
   10.55      (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split)
   10.56  
   10.57 @@ -485,18 +485,18 @@
   10.58  next
   10.59    case (PX_MX P i Q j M)
   10.60    from \<open>in_carrier l\<close>
   10.61 -  have eq1: "(Imon (drop (Suc 0) l) M \<otimes> head l (^) (j - i)) \<otimes>
   10.62 -    Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes> head l (^) i =
   10.63 +  have eq1: "(Imon (drop (Suc 0) l) M \<otimes> head l [^] (j - i)) \<otimes>
   10.64 +    Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes> head l [^] i =
   10.65      Imon (drop (Suc 0) l) M \<otimes>
   10.66      Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes>
   10.67 -    (head l (^) (j - i) \<otimes> head l (^) i)"
   10.68 +    (head l [^] (j - i) \<otimes> head l [^] i)"
   10.69      by (simp add: m_ac)
   10.70    from \<open>in_carrier l\<close>
   10.71 -  have eq2: "(Imon (drop (Suc 0) l) M \<otimes> head l (^) j) \<otimes>
   10.72 -    (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes> head l (^) (i - j)) =
   10.73 +  have eq2: "(Imon (drop (Suc 0) l) M \<otimes> head l [^] j) \<otimes>
   10.74 +    (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes> head l [^] (i - j)) =
   10.75      Imon (drop (Suc 0) l) M \<otimes>
   10.76      Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes>
   10.77 -    (head l (^) (i - j) \<otimes> head l (^) j)"
   10.78 +    (head l [^] (i - j) \<otimes> head l [^] j)"
   10.79      by (simp add: m_ac)
   10.80    from PX_MX \<open>in_carrier l\<close> show ?case
   10.81      by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult)
    11.1 --- a/src/HOL/Decision_Procs/Reflective_Field.thy	Fri Jan 05 15:24:57 2018 +0100
    11.2 +++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Fri Jan 05 18:41:42 2018 +0100
    11.3 @@ -39,7 +39,7 @@
    11.4    | "feval xs (FMul a b) = feval xs a \<otimes> feval xs b"
    11.5    | "feval xs (FNeg a) = \<ominus> feval xs a"
    11.6    | "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b"
    11.7 -  | "feval xs (FPow a n) = feval xs a (^) n"
    11.8 +  | "feval xs (FPow a n) = feval xs a [^] n"
    11.9  
   11.10  lemma (in field) feval_Cnst:
   11.11    "feval xs (FCnst 0) = \<zero>"
   11.12 @@ -96,7 +96,7 @@
   11.13    | "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b"
   11.14    | "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a"
   11.15    | "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b"
   11.16 -  | "peval xs (PExpr2 (PPow a n)) = peval xs a (^) n"
   11.17 +  | "peval xs (PExpr2 (PPow a n)) = peval xs a [^] n"
   11.18  
   11.19  lemma (in field) peval_Cnst:
   11.20    "peval xs (PExpr1 (PCnst 0)) = \<zero>"
   11.21 @@ -264,7 +264,7 @@
   11.22  
   11.23  lemma (in field) isin_correct':
   11.24    "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow>
   11.25 -    peval xs e' = peval xs e (^) (n - p) \<otimes> peval xs e''"
   11.26 +    peval xs e' = peval xs e [^] (n - p) \<otimes> peval xs e''"
   11.27    "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> p \<le> n"
   11.28    using isin_correct [where m = 1] by simp_all
   11.29  
    12.1 --- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Fri Jan 05 15:24:57 2018 +0100
    12.2 +++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Fri Jan 05 18:41:42 2018 +0100
    12.3 @@ -13,8 +13,8 @@
    12.4  
    12.5  lemma (in cring)
    12.6    assumes "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
    12.7 -  shows "\<guillemotleft>4\<guillemotright> \<otimes> x (^) (5::nat) \<otimes> y (^) (3::nat) \<otimes> x (^) (2::nat) \<otimes> \<guillemotleft>3\<guillemotright> \<oplus> x \<otimes> z \<oplus> \<guillemotleft>3\<guillemotright> (^) (5::nat) =
    12.8 -    \<guillemotleft>12\<guillemotright> \<otimes> x (^) (7::nat) \<otimes> y (^) (3::nat) \<oplus> z \<otimes> x \<oplus> \<guillemotleft>243\<guillemotright>"
    12.9 +  shows "\<guillemotleft>4\<guillemotright> \<otimes> x [^] (5::nat) \<otimes> y [^] (3::nat) \<otimes> x [^] (2::nat) \<otimes> \<guillemotleft>3\<guillemotright> \<oplus> x \<otimes> z \<oplus> \<guillemotleft>3\<guillemotright> [^] (5::nat) =
   12.10 +    \<guillemotleft>12\<guillemotright> \<otimes> x [^] (7::nat) \<otimes> y [^] (3::nat) \<oplus> z \<otimes> x \<oplus> \<guillemotleft>243\<guillemotright>"
   12.11    by ring
   12.12  
   12.13  lemma "((x::int) + y) ^ 2  = x ^ 2 + y ^ 2 + 2 * x * y"
   12.14 @@ -22,7 +22,7 @@
   12.15  
   12.16  lemma (in cring)
   12.17    assumes "x \<in> carrier R" "y \<in> carrier R"
   12.18 -  shows "(x \<oplus> y) (^) (2::nat)  = x (^) (2::nat) \<oplus> y (^) (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
   12.19 +  shows "(x \<oplus> y) [^] (2::nat)  = x [^] (2::nat) \<oplus> y [^] (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
   12.20    by ring
   12.21  
   12.22  lemma "((x::int) + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x ^ 2 * y + 3 * y ^ 2 * x"
   12.23 @@ -30,8 +30,8 @@
   12.24  
   12.25  lemma (in cring)
   12.26    assumes "x \<in> carrier R" "y \<in> carrier R"
   12.27 -  shows "(x \<oplus> y) (^) (3::nat) =
   12.28 -    x (^) (3::nat) \<oplus> y (^) (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x (^) (2::nat) \<otimes> y \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> y (^) (2::nat) \<otimes> x"
   12.29 +  shows "(x \<oplus> y) [^] (3::nat) =
   12.30 +    x [^] (3::nat) \<oplus> y [^] (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x [^] (2::nat) \<otimes> y \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> y [^] (2::nat) \<otimes> x"
   12.31    by ring
   12.32  
   12.33  lemma "((x::int) - y) ^ 3 = x ^ 3 + 3 * x * y ^ 2 + (- 3) * y * x ^ 2 - y ^ 3"
   12.34 @@ -39,8 +39,8 @@
   12.35  
   12.36  lemma (in cring)
   12.37    assumes "x \<in> carrier R" "y \<in> carrier R"
   12.38 -  shows "(x \<ominus> y) (^) (3::nat) =
   12.39 -    x (^) (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x \<otimes> y (^) (2::nat) \<oplus> (\<ominus> \<guillemotleft>3\<guillemotright>) \<otimes> y \<otimes> x (^) (2::nat) \<ominus> y (^) (3::nat)"
   12.40 +  shows "(x \<ominus> y) [^] (3::nat) =
   12.41 +    x [^] (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x \<otimes> y [^] (2::nat) \<oplus> (\<ominus> \<guillemotleft>3\<guillemotright>) \<otimes> y \<otimes> x [^] (2::nat) \<ominus> y [^] (3::nat)"
   12.42    by ring
   12.43  
   12.44  lemma "((x::int) - y) ^ 2 = x ^ 2 + y ^ 2 - 2 * x * y"
   12.45 @@ -48,7 +48,7 @@
   12.46  
   12.47  lemma (in cring)
   12.48    assumes "x \<in> carrier R" "y \<in> carrier R"
   12.49 -  shows "(x \<ominus> y) (^) (2::nat) = x (^) (2::nat) \<oplus> y (^) (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
   12.50 +  shows "(x \<ominus> y) [^] (2::nat) = x [^] (2::nat) \<oplus> y [^] (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
   12.51    by ring
   12.52  
   12.53  lemma " ((a::int) + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * b * c + 2 * a * c"
   12.54 @@ -56,8 +56,8 @@
   12.55  
   12.56  lemma (in cring)
   12.57    assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
   12.58 -  shows " (a \<oplus> b \<oplus> c) (^) (2::nat) =
   12.59 -    a (^) (2::nat) \<oplus> b (^) (2::nat) \<oplus> c (^) (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
   12.60 +  shows " (a \<oplus> b \<oplus> c) [^] (2::nat) =
   12.61 +    a [^] (2::nat) \<oplus> b [^] (2::nat) \<oplus> c [^] (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
   12.62    by ring
   12.63  
   12.64  lemma "((a::int) - b - c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 - 2 * a * b + 2 * b * c - 2 * a * c"
   12.65 @@ -65,8 +65,8 @@
   12.66  
   12.67  lemma (in cring)
   12.68    assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
   12.69 -  shows "(a \<ominus> b \<ominus> c) (^) (2::nat) =
   12.70 -    a (^) (2::nat) \<oplus> b (^) (2::nat) \<oplus> c (^) (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
   12.71 +  shows "(a \<ominus> b \<ominus> c) [^] (2::nat) =
   12.72 +    a [^] (2::nat) \<oplus> b [^] (2::nat) \<oplus> c [^] (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
   12.73    by ring
   12.74  
   12.75  lemma "(a::int) * b + a * c = a * (b + c)"
   12.76 @@ -82,7 +82,7 @@
   12.77  
   12.78  lemma (in cring)
   12.79    assumes "a \<in> carrier R" "b \<in> carrier R"
   12.80 -  shows "a (^) (2::nat) \<ominus> b (^) (2::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b)"
   12.81 +  shows "a [^] (2::nat) \<ominus> b [^] (2::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b)"
   12.82    by ring
   12.83  
   12.84  lemma "(a::int) ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2)"
   12.85 @@ -90,7 +90,7 @@
   12.86  
   12.87  lemma (in cring)
   12.88    assumes "a \<in> carrier R" "b \<in> carrier R"
   12.89 -  shows "a (^) (3::nat) \<ominus> b (^) (3::nat) = (a \<ominus> b) \<otimes> (a (^) (2::nat) \<oplus> a \<otimes> b \<oplus> b (^) (2::nat))"
   12.90 +  shows "a [^] (3::nat) \<ominus> b [^] (3::nat) = (a \<ominus> b) \<otimes> (a [^] (2::nat) \<oplus> a \<otimes> b \<oplus> b [^] (2::nat))"
   12.91    by ring
   12.92  
   12.93  lemma "(a::int) ^ 3 + b ^ 3 = (a + b) * (a ^ 2 - a * b + b ^ 2)"
   12.94 @@ -98,7 +98,7 @@
   12.95  
   12.96  lemma (in cring)
   12.97    assumes "a \<in> carrier R" "b \<in> carrier R"
   12.98 -  shows "a (^) (3::nat) \<oplus> b (^) (3::nat) = (a \<oplus> b) \<otimes> (a (^) (2::nat) \<ominus> a \<otimes> b \<oplus> b (^) (2::nat))"
   12.99 +  shows "a [^] (3::nat) \<oplus> b [^] (3::nat) = (a \<oplus> b) \<otimes> (a [^] (2::nat) \<ominus> a \<otimes> b \<oplus> b [^] (2::nat))"
  12.100    by ring
  12.101  
  12.102  lemma "(a::int) ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2)"
  12.103 @@ -106,7 +106,7 @@
  12.104  
  12.105  lemma (in cring)
  12.106    assumes "a \<in> carrier R" "b \<in> carrier R"
  12.107 -  shows "a (^) (4::nat) \<ominus> b (^) (4::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b) \<otimes> (a (^) (2::nat) \<oplus> b (^) (2::nat))"
  12.108 +  shows "a [^] (4::nat) \<ominus> b [^] (4::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b) \<otimes> (a [^] (2::nat) \<oplus> b [^] (2::nat))"
  12.109    by ring
  12.110  
  12.111  lemma "(a::int) ^ 10 - b ^ 10 =
  12.112 @@ -116,11 +116,11 @@
  12.113  
  12.114  lemma (in cring)
  12.115    assumes "a \<in> carrier R" "b \<in> carrier R"
  12.116 -  shows "a (^) (10::nat) \<ominus> b (^) (10::nat) =
  12.117 -  (a \<ominus> b) \<otimes> (a (^) (9::nat) \<oplus> a (^) (8::nat) \<otimes> b \<oplus> a (^) (7::nat) \<otimes> b (^) (2::nat) \<oplus>
  12.118 -    a (^) (6::nat) \<otimes> b (^) (3::nat) \<oplus> a (^) (5::nat) \<otimes> b (^) (4::nat) \<oplus>
  12.119 -    a (^) (4::nat) \<otimes> b (^) (5::nat) \<oplus> a (^) (3::nat) \<otimes> b (^) (6::nat) \<oplus>
  12.120 -    a (^) (2::nat) \<otimes> b (^) (7::nat) \<oplus> a \<otimes> b (^) (8::nat) \<oplus> b (^) (9::nat))"
  12.121 +  shows "a [^] (10::nat) \<ominus> b [^] (10::nat) =
  12.122 +  (a \<ominus> b) \<otimes> (a [^] (9::nat) \<oplus> a [^] (8::nat) \<otimes> b \<oplus> a [^] (7::nat) \<otimes> b [^] (2::nat) \<oplus>
  12.123 +    a [^] (6::nat) \<otimes> b [^] (3::nat) \<oplus> a [^] (5::nat) \<otimes> b [^] (4::nat) \<oplus>
  12.124 +    a [^] (4::nat) \<otimes> b [^] (5::nat) \<oplus> a [^] (3::nat) \<otimes> b [^] (6::nat) \<oplus>
  12.125 +    a [^] (2::nat) \<otimes> b [^] (7::nat) \<oplus> a \<otimes> b [^] (8::nat) \<oplus> b [^] (9::nat))"
  12.126    by ring
  12.127  
  12.128  lemma "(x::'a::field) \<noteq> 0 \<Longrightarrow> (1 - 1 / x) * x - x + 1 = 0"
    13.1 --- a/src/HOL/Number_Theory/Prime_Powers.thy	Fri Jan 05 15:24:57 2018 +0100
    13.2 +++ b/src/HOL/Number_Theory/Prime_Powers.thy	Fri Jan 05 18:41:42 2018 +0100
    13.3 @@ -510,4 +510,4 @@
    13.4    finally show ?thesis .
    13.5  qed (insert assms, auto simp: mangoldt_def)
    13.6  
    13.7 -end
    13.8 \ No newline at end of file
    13.9 +end
    14.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jan 05 15:24:57 2018 +0100
    14.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jan 05 18:41:42 2018 +0100
    14.3 @@ -149,7 +149,7 @@
    14.4    using m_gt_one by (auto simp: R_def residue_ring_def)
    14.5  
    14.6  (* FIXME revise algebra library to use 1? *)
    14.7 -lemma pow_cong: "(x mod m) (^) n = x^n mod m"
    14.8 +lemma pow_cong: "(x mod m) [^] n = x^n mod m"
    14.9    using m_gt_one
   14.10    apply (induct n)
   14.11    apply (auto simp add: nat_pow_def one_cong)
   14.12 @@ -413,12 +413,12 @@
   14.13    have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}"
   14.14      by (auto simp add: R.zero_cong R.res_carrier_eq)
   14.15  
   14.16 -  have "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)"
   14.17 +  have "x [^]\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)"
   14.18      if "x \<in> {1 .. int p - 1}" for x and i :: nat
   14.19      using that R.pow_cong[of x i] by auto
   14.20    moreover
   14.21    obtain a where a: "a \<in> {1 .. int p - 1}"
   14.22 -    and a_gen: "{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
   14.23 +    and a_gen: "{1 .. int p - 1} = {a[^]\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
   14.24      using field.finite_field_mult_group_has_gen[OF R.is_field]
   14.25      by (auto simp add: car[symmetric] carrier_mult_of)
   14.26    moreover
    15.1 --- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jan 05 15:24:57 2018 +0100
    15.2 +++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jan 05 18:41:42 2018 +0100
    15.3 @@ -20,7 +20,7 @@
    15.4  (* first some additional lemmas that are missing in monoid *)
    15.5  
    15.6  lemma Units_nat_pow_Units [intro, simp]:
    15.7 -  "a \<in> Units G \<Longrightarrow> a (^) (c :: nat) \<in> Units G" by (induct c) auto
    15.8 +  "a \<in> Units G \<Longrightarrow> a [^] (c :: nat) \<in> Units G" by (induct c) auto
    15.9  
   15.10  lemma Units_r_cancel [simp]:
   15.11    "[| z \<in> Units G; x \<in> carrier G; y \<in> carrier G |] ==>
   15.12 @@ -49,14 +49,14 @@
   15.13  
   15.14  lemma mult_same_comm:
   15.15    assumes [simp, intro]: "a \<in> Units G"
   15.16 -  shows "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> a (^) m"
   15.17 +  shows "a [^] (m::nat) \<otimes> inv (a [^] (n::nat)) = inv (a [^] n) \<otimes> a [^] m"
   15.18  proof (cases "m\<ge>n")
   15.19    have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> by (rule Units_closed)
   15.20    case True
   15.21      then obtain k where *:"m = k + n" and **:"m = n + k" by (metis le_iff_add add.commute)
   15.22 -    have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = a (^) k"
   15.23 +    have "a [^] (m::nat) \<otimes> inv (a [^] (n::nat)) = a [^] k"
   15.24        using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
   15.25 -    also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
   15.26 +    also have "\<dots> = inv (a [^] n) \<otimes> a [^] m"
   15.27        using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric])
   15.28      finally show ?thesis .
   15.29  next
   15.30 @@ -64,15 +64,15 @@
   15.31    case False
   15.32      then obtain k where *:"n = k + m" and **:"n = m + k"
   15.33        by (metis le_iff_add add.commute nat_le_linear)
   15.34 -    have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv(a (^) k)"
   15.35 +    have "a [^] (m::nat) \<otimes> inv (a [^] (n::nat)) = inv(a [^] k)"
   15.36        using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
   15.37 -    also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
   15.38 +    also have "\<dots> = inv (a [^] n) \<otimes> a [^] m"
   15.39        using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc inv_mult_units)
   15.40      finally show ?thesis .
   15.41  qed
   15.42  
   15.43  lemma mult_inv_same_comm:
   15.44 -  "a \<in> Units G \<Longrightarrow> inv (a (^) (m::nat)) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> inv (a (^) m)"
   15.45 +  "a \<in> Units G \<Longrightarrow> inv (a [^] (m::nat)) \<otimes> inv (a [^] (n::nat)) = inv (a [^] n) \<otimes> inv (a [^] m)"
   15.46  by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)
   15.47  
   15.48  context
   15.49 @@ -82,15 +82,15 @@
   15.50  lemma int_pow_rsp:
   15.51    assumes eq: "(b::nat) + e = d + c"
   15.52    assumes a_in_G [simp, intro]: "a \<in> Units G"
   15.53 -  shows "a (^) b \<otimes> inv (a (^) c) = a (^) d \<otimes> inv (a (^) e)"
   15.54 +  shows "a [^] b \<otimes> inv (a [^] c) = a [^] d \<otimes> inv (a [^] e)"
   15.55  proof(cases "b\<ge>c")
   15.56    have [simp]: "a \<in> carrier G" using \<open>a \<in> _\<close> by (rule Units_closed)
   15.57    case True
   15.58      then obtain n where "b = n + c" by (metis le_iff_add add.commute)
   15.59      then have "d = n + e" using eq by arith
   15.60 -    from \<open>b = _\<close> have "a (^) b \<otimes> inv (a (^) c) = a (^) n"
   15.61 +    from \<open>b = _\<close> have "a [^] b \<otimes> inv (a [^] c) = a [^] n"
   15.62        by (auto simp add: nat_pow_mult[symmetric] m_assoc)
   15.63 -    also from \<open>d = _\<close>  have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
   15.64 +    also from \<open>d = _\<close>  have "\<dots> = a [^] d \<otimes> inv (a [^] e)"
   15.65        by (auto simp add: nat_pow_mult[symmetric] m_assoc)
   15.66      finally show ?thesis .
   15.67  next
   15.68 @@ -98,20 +98,20 @@
   15.69    case False
   15.70      then obtain n where "c = n + b" by (metis le_iff_add add.commute nat_le_linear)
   15.71      then have "e = n + d" using eq by arith
   15.72 -    from \<open>c = _\<close> have "a (^) b \<otimes> inv (a (^) c) = inv (a (^) n)"
   15.73 +    from \<open>c = _\<close> have "a [^] b \<otimes> inv (a [^] c) = inv (a [^] n)"
   15.74        by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
   15.75 -    also from \<open>e = _\<close> have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
   15.76 +    also from \<open>e = _\<close> have "\<dots> = a [^] d \<otimes> inv (a [^] e)"
   15.77        by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
   15.78      finally show ?thesis .
   15.79  qed
   15.80  
   15.81  (*
   15.82    This definition is more convinient than the definition in HOL/Algebra/Group because
   15.83 -  it doesn't contain a test z < 0 when a (^) z is being defined.
   15.84 +  it doesn't contain a test z < 0 when a [^] z is being defined.
   15.85  *)
   15.86  
   15.87  lift_definition int_pow :: "('a, 'm) monoid_scheme \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a" is
   15.88 -  "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a (^)\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a (^)\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>"
   15.89 +  "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a [^]\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>"
   15.90  unfolding intrel_def by (auto intro: monoid.int_pow_rsp)
   15.91  
   15.92  (*
   15.93 @@ -125,12 +125,12 @@
   15.94  proof -
   15.95    {
   15.96      fix k l m :: nat
   15.97 -    have "a (^) l \<otimes> (inv (a (^) m) \<otimes> inv (a (^) k)) = (a (^) l \<otimes> inv (a (^) k)) \<otimes> inv (a (^) m)"
   15.98 +    have "a [^] l \<otimes> (inv (a [^] m) \<otimes> inv (a [^] k)) = (a [^] l \<otimes> inv (a [^] k)) \<otimes> inv (a [^] m)"
   15.99        (is "?lhs = _")
  15.100        by (simp add: mult_inv_same_comm m_assoc Units_closed)
  15.101 -    also have "\<dots> = (inv (a (^) k) \<otimes> a (^) l) \<otimes> inv (a (^) m)"
  15.102 +    also have "\<dots> = (inv (a [^] k) \<otimes> a [^] l) \<otimes> inv (a [^] m)"
  15.103        by (simp add: mult_same_comm)
  15.104 -    also have "\<dots> = inv (a (^) k) \<otimes> (a (^) l \<otimes> inv (a (^) m))" (is "_ = ?rhs")
  15.105 +    also have "\<dots> = inv (a [^] k) \<otimes> (a [^] l \<otimes> inv (a [^] m))" (is "_ = ?rhs")
  15.106        by (simp add: m_assoc Units_closed)
  15.107      finally have "?lhs = ?rhs" .
  15.108    }