# HG changeset patch
# User wenzelm
# Date 1484661407 -3600
# Node ID 3a9eb793fa105c9f2af4d909b5d4ec23b8cf9778
# Parent  68f0465d956b25113b71b10c4ba1935ccd2fb561
more symbols;

diff -r 68f0465d956b -r 3a9eb793fa10 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Jan 17 14:56:15 2017 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Tue Jan 17 14:56:47 2017 +0100
@@ -59,13 +59,13 @@
 definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
   where "UP R = \<lparr>
    carrier = up R,
-   mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
-   one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
-   zero = (%i. \<zero>\<^bsub>R\<^esub>),
-   add = (%p:up R. %q:up R. %i. p i \<oplus>\<^bsub>R\<^esub> q i),
-   smult = (%a:carrier R. %p:up R. %i. a \<otimes>\<^bsub>R\<^esub> p i),
-   monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
-   coeff = (%p:up R. %n. p n)\<rparr>"
+   mult = (\<lambda>p\<in>up R. \<lambda>q\<in>up R. \<lambda>n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
+   one = (\<lambda>i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
+   zero = (\<lambda>i. \<zero>\<^bsub>R\<^esub>),
+   add = (\<lambda>p\<in>up R. \<lambda>q\<in>up R. \<lambda>i. p i \<oplus>\<^bsub>R\<^esub> q i),
+   smult = (\<lambda>a\<in>carrier R. \<lambda>p\<in>up R. \<lambda>i. a \<otimes>\<^bsub>R\<^esub> p i),
+   monom = (\<lambda>a\<in>carrier R. \<lambda>n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
+   coeff = (\<lambda>p\<in>up R. \<lambda>n. p n)\<rparr>"
 
 text \<open>
   Properties of the set of polynomials @{term up}.
@@ -84,12 +84,12 @@
 
 lemma bound_upD [dest]: "f \<in> up R ==> EX n. bound \<zero> n f" by (simp add: up_def)
 
-lemma up_one_closed: "(%n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force
+lemma up_one_closed: "(\<lambda>n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force
 
-lemma up_smult_closed: "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R" by force
+lemma up_smult_closed: "[| a \<in> carrier R; p \<in> up R |] ==> (\<lambda>i. a \<otimes> p i) \<in> up R" by force
 
 lemma up_add_closed:
-  "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
+  "[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<oplus> q i) \<in> up R"
 proof
   fix n
   assume "p \<in> up R" and "q \<in> up R"
@@ -97,11 +97,11 @@
     by auto
 next
   assume UP: "p \<in> up R" "q \<in> up R"
-  show "EX n. bound \<zero> n (%i. p i \<oplus> q i)"
+  show "EX n. bound \<zero> n (\<lambda>i. p i \<oplus> q i)"
   proof -
     from UP obtain n where boundn: "bound \<zero> n p" by fast
     from UP obtain m where boundm: "bound \<zero> m q" by fast
-    have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
+    have "bound \<zero> (max n m) (\<lambda>i. p i \<oplus> q i)"
     proof
       fix i
       assume "max n m < i"
@@ -112,22 +112,22 @@
 qed
 
 lemma up_a_inv_closed:
-  "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
+  "p \<in> up R ==> (\<lambda>i. \<ominus> (p i)) \<in> up R"
 proof
   assume R: "p \<in> up R"
   then obtain n where "bound \<zero> n p" by auto
-  then have "bound \<zero> n (%i. \<ominus> p i)" by auto
-  then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
+  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
+  then show "EX n. bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
 qed auto
 
 lemma up_minus_closed:
-  "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<ominus> q i) \<in> up R"
+  "[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<ominus> q i) \<in> up R"
   using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R]
   by auto
 
 lemma up_mult_closed:
   "[| p \<in> up R; q \<in> up R |] ==>
-  (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
+  (\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
 proof
   fix n
   assume "p \<in> up R" "q \<in> up R"
@@ -135,11 +135,11 @@
     by (simp add: mem_upD  funcsetI)
 next
   assume UP: "p \<in> up R" "q \<in> up R"
-  show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
+  show "EX n. bound \<zero> n (\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
   proof -
     from UP obtain n where boundn: "bound \<zero> n p" by fast
     from UP obtain m where boundm: "bound \<zero> m q" by fast
-    have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
+    have "bound \<zero> (n + m) (\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
     proof
       fix k assume bound: "n + m < k"
       {
@@ -206,7 +206,7 @@
 
 end
 
-context UP_ring 
+context UP_ring
 begin
 
 (* Theorems generalised from commutative rings to rings by Jesus Aransay. *)
@@ -215,7 +215,7 @@
   "a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)"
 proof -
   assume R: "a \<in> carrier R"
-  then have "(%n. if n = m then a else \<zero>) \<in> up R"
+  then have "(\<lambda>n. if n = m then a else \<zero>) \<in> up R"
     using up_def by force
   with R show ?thesis by (simp add: UP_def)
 qed
@@ -286,7 +286,7 @@
   assumes R: "p \<in> carrier P"
   shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
 proof -
-  let ?q = "%i. \<ominus> (p i)"
+  let ?q = "\<lambda>i. \<ominus> (p i)"
   from R have closed: "?q \<in> carrier P"
     by (simp add: UP_def P_def up_a_inv_closed)
   from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
@@ -337,7 +337,7 @@
   fix n
   show "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) n = coeff P p n"
   proof (cases n)
-    case 0 
+    case 0
     {
       with R show ?thesis by simp
     }
@@ -354,7 +354,7 @@
         also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
         proof -
           have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
-            using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R 
+            using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R
             unfolding Pi_def by simp
           also have "\<dots> = \<zero>" by simp
           finally show ?thesis using r_zero R by simp
@@ -366,7 +366,7 @@
     }
   qed
 qed (simp_all add: R)
-  
+
 lemma UP_l_one [simp]:
   assumes R: "p \<in> carrier P"
   shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
@@ -422,8 +422,8 @@
   }
   note l = this
   from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
-    unfolding coeff_mult [OF R1 R2, of n] 
-    unfolding coeff_mult [OF R2 R1, of n] 
+    unfolding coeff_mult [OF R1 R2, of n]
+    unfolding coeff_mult [OF R2 R1, of n]
     using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
 qed (simp_all add: R1 R2)
 
@@ -637,7 +637,7 @@
   }
 qed
 
-text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"} 
+text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"}
   and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
 
 corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
@@ -664,16 +664,16 @@
   assumes a_in_R: "a \<in> carrier R" and b_in_R: "b \<in> carrier R"
   shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
 proof (rule up_eqI)
-  fix k 
+  fix k
   show "coeff P (monom P (a \<otimes> b) (n + m)) k = coeff P (monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m) k"
   proof (cases "n + m = k")
-    case True 
+    case True
     {
       show ?thesis
         unfolding True [symmetric]
-          coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"] 
+          coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"]
           coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m]
-        using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m - i then b else \<zero>))" 
+        using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m - i then b else \<zero>))"
           "(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"]
           a_in_R b_in_R
         unfolding simp_implies_def
@@ -698,7 +698,7 @@
   by (rule up_eqI) simp_all
 
 lemma monom_inj:
-  "inj_on (%a. monom P a n) (carrier R)"
+  "inj_on (\<lambda>a. monom P a n) (carrier R)"
 proof (rule inj_onI)
   fix x y
   assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
@@ -725,7 +725,7 @@
 (*
 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
 proof -
-  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+  have "(\<lambda>n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   then show ?thesis ..
 qed
@@ -733,7 +733,7 @@
 lemma bound_coeff_obtain:
   assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
 proof -
-  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+  have "(\<lambda>n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   with prem show P .
 qed
@@ -925,7 +925,7 @@
   assume "p \<in> carrier P" " q \<in> carrier P"
   then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
 next
-  let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
+  let ?s = "(\<lambda>i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
   assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
   have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
   show "deg R p + deg R q <= deg R (p \<otimes>\<^bsub>P\<^esub> q)"
@@ -964,7 +964,7 @@
   assumes R: "p \<in> carrier P"
   shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
 proof (rule up_eqI)
-  let ?s = "(%i. monom P (coeff P p i) i)"
+  let ?s = "(\<lambda>i. monom P (coeff P p i) i)"
   fix k
   from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
     by simp
@@ -999,7 +999,7 @@
   "[| deg R p <= n; p \<in> carrier P |] ==>
   (\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p"
 proof -
-  let ?s = "(%i. monom P (coeff P p i) i)"
+  let ?s = "(\<lambda>i. monom P (coeff P p i) i)"
   assume R: "p \<in> carrier P" and "deg R p <= n"
   then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} \<union> {deg R p<..n})"
     by (simp only: ivl_disj_un_one)
@@ -1168,7 +1168,7 @@
 end
 
 lemma (in UP_ring) const_ring_hom:
-  "(%a. monom P a 0) \<in> ring_hom R P"
+  "(\<lambda>a. monom P a 0) \<in> ring_hom R P"
   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
 
 definition
@@ -1202,7 +1202,7 @@
   defines Eval_def: "Eval == eval R S h s"
 
 text\<open>JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.\<close>
-text\<open>JE: I was considering using it in \<open>eval_ring_hom\<close>, but that property does not hold for non commutative rings, so 
+text\<open>JE: I was considering using it in \<open>eval_ring_hom\<close>, but that property does not hold for non commutative rings, so
   maybe it is not that necessary.\<close>
 
 lemma (in ring_hom_ring) hom_finsum [simp]:
@@ -1455,14 +1455,14 @@
 
 abbreviation lcoeff :: "(nat =>'a) => 'a" where "lcoeff p == coeff P p (deg R p)"
 
-lemma lcoeff_nonzero2: assumes p_in_R: "p \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>" 
+lemma lcoeff_nonzero2: assumes p_in_R: "p \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>"
   using lcoeff_nonzero [OF p_not_zero p_in_R] .
 
 
 subsection\<open>The long division algorithm: some previous facts.\<close>
 
 lemma coeff_minus [simp]:
-  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n" 
+  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
   unfolding a_minus_def [OF p q] unfolding coeff_add [OF p a_inv_closed [OF q]] unfolding coeff_a_inv [OF q]
   using coeff_closed [OF p, of n] using coeff_closed [OF q, of n] by algebra
 
@@ -1472,14 +1472,14 @@
 lemma deg_smult_decr: assumes a_in_R: "a \<in> carrier R" and f_in_P: "f \<in> carrier P" shows "deg R (a \<odot>\<^bsub>P\<^esub> f) \<le> deg R f"
   using deg_smult_ring [OF a_in_R f_in_P] by (cases "a = \<zero>", auto)
 
-lemma coeff_monom_mult: assumes R: "c \<in> carrier R" and P: "p \<in> carrier P" 
+lemma coeff_monom_mult: assumes R: "c \<in> carrier R" and P: "p \<in> carrier P"
   shows "coeff P (monom P c n \<otimes>\<^bsub>P\<^esub> p) (m + n) = c \<otimes> (coeff P p m)"
 proof -
   have "coeff P (monom P c n \<otimes>\<^bsub>P\<^esub> p) (m + n) = (\<Oplus>i\<in>{..m + n}. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i))"
     unfolding coeff_mult [OF monom_closed [OF R, of n] P, of "m + n"] unfolding coeff_monom [OF R, of n] by simp
-  also have "(\<Oplus>i\<in>{..m + n}. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i)) = 
+  also have "(\<Oplus>i\<in>{..m + n}. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i)) =
     (\<Oplus>i\<in>{..m + n}. (if n = i then c \<otimes> coeff P p (m + n - i) else \<zero>))"
-    using  R.finsum_cong [of "{..m + n}" "{..m + n}" "(\<lambda>i::nat. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i))" 
+    using  R.finsum_cong [of "{..m + n}" "{..m + n}" "(\<lambda>i::nat. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i))"
       "(\<lambda>i::nat. (if n = i then c \<otimes> coeff P p (m + n - i) else \<zero>))"]
     using coeff_closed [OF P] unfolding Pi_def simp_implies_def using R by auto
   also have "\<dots> = c \<otimes> coeff P p m" using R.finsum_singleton [of n "{..m + n}" "(\<lambda>i. c \<otimes> coeff P p (m + n - i))"]
@@ -1487,10 +1487,10 @@
   finally show ?thesis by simp
 qed
 
-lemma deg_lcoeff_cancel: 
-  assumes p_in_P: "p \<in> carrier P" and q_in_P: "q \<in> carrier P" and r_in_P: "r \<in> carrier P" 
+lemma deg_lcoeff_cancel:
+  assumes p_in_P: "p \<in> carrier P" and q_in_P: "q \<in> carrier P" and r_in_P: "r \<in> carrier P"
   and deg_r_nonzero: "deg R r \<noteq> 0"
-  and deg_R_p: "deg R p \<le> deg R r" and deg_R_q: "deg R q \<le> deg R r" 
+  and deg_R_p: "deg R p \<le> deg R r" and deg_R_q: "deg R q \<le> deg R r"
   and coeff_R_p_eq_q: "coeff P p (deg R r) = \<ominus>\<^bsub>R\<^esub> (coeff P q (deg R r))"
   shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) < deg R r"
 proof -
@@ -1504,7 +1504,7 @@
       then have max_sl: "max (deg R p) (deg R q) < m" by simp
       then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) < m" using deg_add [OF p_in_P q_in_P] by arith
       with deg_R_p deg_R_q show ?thesis using coeff_add [OF p_in_P q_in_P, of m]
-        using deg_aboveD [of "p \<oplus>\<^bsub>P\<^esub> q" m] using p_in_P q_in_P by simp 
+        using deg_aboveD [of "p \<oplus>\<^bsub>P\<^esub> q" m] using p_in_P q_in_P by simp
     qed
   qed (simp add: p_in_P q_in_P)
   moreover have deg_ne: "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<noteq> deg R r"
@@ -1519,16 +1519,16 @@
   ultimately show ?thesis by simp
 qed
 
-lemma monom_deg_mult: 
+lemma monom_deg_mult:
   assumes f_in_P: "f \<in> carrier P" and g_in_P: "g \<in> carrier P" and deg_le: "deg R g \<le> deg R f"
   and a_in_R: "a \<in> carrier R"
   shows "deg R (g \<otimes>\<^bsub>P\<^esub> monom P a (deg R f - deg R g)) \<le> deg R f"
   using deg_mult_ring [OF g_in_P monom_closed [OF a_in_R, of "deg R f - deg R g"]]
-  apply (cases "a = \<zero>") using g_in_P apply simp 
+  apply (cases "a = \<zero>") using g_in_P apply simp
   using deg_monom [OF _ a_in_R, of "deg R f - deg R g"] using deg_le by simp
 
 lemma deg_zero_impl_monom:
-  assumes f_in_P: "f \<in> carrier P" and deg_f: "deg R f = 0" 
+  assumes f_in_P: "f \<in> carrier P" and deg_f: "deg R f = 0"
   shows "f = monom P (coeff P f 0) 0"
   apply (rule up_eqI) using coeff_monom [OF coeff_closed [OF f_in_P], of 0 0]
   using f_in_P deg_f using deg_aboveD [of f _] by auto
@@ -1541,13 +1541,13 @@
 context UP_cring
 begin
 
-lemma exI3: assumes exist: "Pred x y z" 
+lemma exI3: assumes exist: "Pred x y z"
   shows "\<exists> x y z. Pred x y z"
   using exist by blast
 
 text \<open>Jacobson's Theorem 2.14\<close>
 
-lemma long_div_theorem: 
+lemma long_div_theorem:
   assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
   and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
   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> | deg R r < deg R g)"
@@ -1556,7 +1556,7 @@
   case (1 f)
   note f_in_P [simp] = "1.prems"
   let ?pred = "(\<lambda> q r (k::nat).
-    (q \<in> carrier P) \<and> (r \<in> carrier P) 
+    (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> | deg R r < deg R g))"
   let ?lg = "lcoeff g" and ?lf = "lcoeff f"
   show ?case
@@ -1598,13 +1598,13 @@
               show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
                 by (simp add: monom_deg_mult [OF f_in_P g_in_P deg_g_le_deg_f, of ?lf])
               show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
-                unfolding coeff_mult [OF g_in_P monom_closed 
-                  [OF lcoeff_closed [OF f_in_P], 
+                unfolding coeff_mult [OF g_in_P monom_closed
+                  [OF lcoeff_closed [OF f_in_P],
                     of "deg R f - deg R g"], of "deg R f"]
-                unfolding coeff_monom [OF lcoeff_closed 
+                unfolding coeff_monom [OF lcoeff_closed
                   [OF f_in_P], of "(deg R f - deg R g)"]
-                using R.finsum_cong' [of "{..deg R f}" "{..deg R f}" 
-                  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))" 
+                using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
+                  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))"
                   "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> ?lf else \<zero>)"]
                 using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> ?lf)"]
                 unfolding Pi_def using deg_g_le_deg_f by force
@@ -1630,7 +1630,7 @@
                 using r'_in_carrier q'_in_carrier by simp
               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'"
                 using q'_in_carrier by (auto simp add: m_comm)
-              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'" 
+              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'"
                 using smult_assoc2 q'_in_carrier "1.prems" by auto
               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'"
                 using sym [OF l_distr] and q'_in_carrier by auto
@@ -1660,8 +1660,8 @@
   have "deg R ?g \<le> 1"
   proof (rule deg_aboveI)
     fix m
-    assume "(1::nat) < m" 
-    then show "coeff P ?g m = \<zero>" 
+    assume "(1::nat) < m"
+    then show "coeff P ?g m = \<zero>"
       using coeff_minus using a by auto algebra
   qed (simp add: a)
   moreover have "deg R ?g \<ge> 1"
@@ -1691,15 +1691,15 @@
 proof -
   have "deg R ?g \<le> 1"
   proof (rule deg_aboveI)
-    fix m::nat assume "1 < m" then show "coeff P ?g m = \<zero>" 
-      using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of m] 
+    fix m::nat assume "1 < m" then show "coeff P ?g m = \<zero>"
+      using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of m]
       using coeff_monom [OF R.one_closed, of 1 m] using coeff_monom [OF a, of 0 m] by auto algebra
   qed (simp add: a)
   moreover have "1 \<le> deg R ?g"
   proof (rule deg_belowI)
-    show "coeff P ?g 1 \<noteq> \<zero>" 
+    show "coeff P ?g 1 \<noteq> \<zero>"
       using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of 1]
-      using coeff_monom [OF R.one_closed, of 1 1] using coeff_monom [OF a, of 0 1] 
+      using coeff_monom [OF R.one_closed, of 1 1] using coeff_monom [OF a, of 0 1]
       using R_not_trivial using R.carrier_one_not_zero
       by auto algebra
   qed (simp add: a)
@@ -1714,14 +1714,14 @@
   interpret UP_pre_univ_prop R R id by unfold_locales simp
   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
   interpret ring_hom_cring P R "eval R R id a" by unfold_locales (rule eval_ring_hom)
-  have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
-    and mon0_closed: "monom P a 0 \<in> carrier P" 
+  have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
+    and mon0_closed: "monom P a 0 \<in> carrier P"
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
     using a R.a_inv_closed by auto
   have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
     unfolding P.minus_eq [OF mon1_closed mon0_closed]
     unfolding hom_add [OF mon1_closed min_mon0_closed]
-    unfolding hom_a_inv [OF mon0_closed] 
+    unfolding hom_a_inv [OF mon0_closed]
     using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
   also have "\<dots> = a \<ominus> a"
     using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
@@ -1766,21 +1766,21 @@
   also have "\<dots> = ((eval R R id a ?g) \<otimes> (eval R R id a q)) \<oplus>\<^bsub>R\<^esub> eval R R id a r"
     using ring_hom_mult [OF eval_ring_hom] by auto
   also have "\<dots> = \<zero> \<oplus> eval R R id a r"
-    unfolding eval_monom_expr [OF a] using eval_ring_hom 
+    unfolding eval_monom_expr [OF a] using eval_ring_hom
     unfolding ring_hom_def using q unfolding Pi_def by simp
   also have "\<dots> = eval R R id a r"
     using eval_ring_hom unfolding ring_hom_def using r unfolding Pi_def by simp
   finally have eval_eq: "eval R R id a f = eval R R id a r" by simp
   from deg_zero_impl_monom [OF r deg_r_0]
   have "r = monom P (coeff P r 0) 0" by simp
-  with eval_const [OF a, of "coeff P r 0"] eval_eq 
+  with eval_const [OF a, of "coeff P r 0"] eval_eq
   show ?thesis by auto
 qed
 
 corollary remainder_theorem:
   assumes f [simp]: "f \<in> carrier P" and a [simp]: "a \<in> carrier R"
   and R_not_trivial: "carrier R \<noteq> {\<zero>}"
-  shows "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> 
+  shows "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and>
      f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> monom P (eval R R id a f) 0"
   (is "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> monom P (eval R R id a f) 0")
 proof -
diff -r 68f0465d956b -r 3a9eb793fa10 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Tue Jan 17 14:56:15 2017 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Tue Jan 17 14:56:47 2017 +0100
@@ -34,17 +34,17 @@
                           (\<forall>y \<in> pset po. P y --> (y,x): order po)"
 
 definition lub  :: "['a set, 'a potype] => 'a" where
-  "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
+  "lub S po == least (\<lambda>x. \<forall>y\<in>S. (y,x): order po) po"
 
 definition glb  :: "['a set, 'a potype] => 'a" where
-  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
+  "glb S po == greatest (\<lambda>x. \<forall>y\<in>S. (x,y): order po) po"
 
 definition isLub :: "['a set, 'a potype, 'a] => bool" where
-  "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
+  "isLub S po == \<lambda>L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
                    (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
 
 definition isGlb :: "['a set, 'a potype, 'a] => bool" where
-  "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
+  "isGlb S po == \<lambda>G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
                  (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
 
 definition "fix"    :: "[('a => 'a), 'a set] => 'a set" where
@@ -54,10 +54,10 @@
   "interval r a b == {x. (a,x): r & (x,b): r}"
 
 definition Bot :: "'a potype => 'a" where
-  "Bot po == least (%x. True) po"
+  "Bot po == least (\<lambda>x. True) po"
 
 definition Top :: "'a potype => 'a" where
-  "Top po == greatest (%x. True) po"
+  "Top po == greatest (\<lambda>x. True) po"
 
 definition PartialOrder :: "('a potype) set" where
   "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
@@ -113,7 +113,7 @@
     Y_ss: "Y \<subseteq> P"
   defines
     intY1_def: "intY1 == interval r (lub Y cl) (Top cl)"
-    and v_def: "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r &
+    and v_def: "v == glb {x. ((\<lambda>x \<in> intY1. f x) x, x): induced intY1 r &
                              x: intY1}
                       (| pset=intY1, order=induced intY1 r|)"
 
@@ -442,7 +442,7 @@
 by (simp add: fix_def)
 
 lemma fixf_subset:
-     "[| A \<subseteq> B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B"
+     "[| A \<subseteq> B; x \<in> fix (\<lambda>y \<in> A. f y) A |] ==> x \<in> fix f B"
 by (simp add: fix_def, auto)
 
 subsection \<open>lemmas for Tarski, lub\<close>
@@ -517,7 +517,7 @@
     by (metis Collect_conj_eq Collect_mem_eq)
   have F3: "\<forall>x v. {R. v R \<in> x} = v -` x" by (metis vimage_def)
   hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
-  hence F5: "(f (lub H cl), lub H cl) \<in> r" 
+  hence F5: "(f (lub H cl), lub H cl) \<in> r"
     by (metis A1 flubH_le_lubH)
   have F6: "(lub H cl, f (lub H cl)) \<in> r"
     by (metis A1 lubH_le_flubH)
@@ -904,14 +904,14 @@
 done
 
 
-lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 \<rightarrow> intY1"
+lemma (in Tarski) intY1_func: "(\<lambda>x \<in> intY1. f x) \<in> intY1 \<rightarrow> intY1"
 apply (rule restrict_in_funcset)
 apply (metis intY1_f_closed restrict_in_funcset)
 done
 
 
 lemma (in Tarski) intY1_mono:
-     "monotone (%x: intY1. f x) intY1 (induced intY1 r)"
+     "monotone (\<lambda>x \<in> intY1. f x) intY1 (induced intY1 r)"
 (*sledgehammer *)
 apply (auto simp add: monotone_def induced_def intY1_f_closed)
 apply (blast intro: intY1_elem monotone_f [THEN monotoneE])
@@ -957,7 +957,7 @@
 
 
 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
-      ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r"
+      ==> ((\<lambda>x \<in> intY1. f x) z, z) \<in> induced intY1 r"
 using P_def fix_imp_eq indI intY1_elem reflE z_in_interval by fastforce
 
 (*never proved, 2007-01-22*)