# HG changeset patch
# User wenzelm
# Date 1393365261 -3600
# Node ID c90cc76ec8558b5dfc28eb8f41849090c1ec7093
# Parent  30312334445923310ad206107693d5efd310d360# Parent  43d0e2a34c9d36e8ccd981e08ade6cb088869eda
merged

diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -928,6 +928,11 @@
 
 hide_const (open) Nat
 
+lifting_update integer.lifting
+lifting_forget integer.lifting
+
+lifting_update natural.lifting
+lifting_forget natural.lifting
 
 code_reflect Code_Numeral
   datatypes natural = _
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Complex.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -557,6 +557,109 @@
   bounded_linear.isCont [OF bounded_linear_cnj]
 
 
+subsection{*Basic Lemmas*}
+
+lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
+  by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff)
+
+lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
+by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
+
+lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
+apply (cases z, auto)
+by (metis complex_of_real_def of_real_add of_real_power power2_eq_square)
+
+lemma complex_div_eq_0: 
+    "(Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0) & (Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0)"
+proof (cases "b=0")
+  case True then show ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof (cases b)
+    case (Complex x y)
+    then have "x\<^sup>2 + y\<^sup>2 > 0"
+      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
+    then have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
+      by (metis add_divide_distrib)
+    with Complex False show ?thesis
+      by (auto simp: complex_divide_def)
+  qed
+qed
+
+lemma re_complex_div_eq_0: "Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0"
+  and im_complex_div_eq_0: "Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0"
+using complex_div_eq_0 by auto
+
+
+lemma complex_div_gt_0: 
+    "(Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0) & (Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0)"
+proof (cases "b=0")
+  case True then show ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof (cases b)
+    case (Complex x y)
+    then have "x\<^sup>2 + y\<^sup>2 > 0"
+      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
+    moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
+      by (metis add_divide_distrib)
+    ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
+      apply (simp add: complex_divide_def  zero_less_divide_iff less_divide_eq)
+      apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
+      done
+  qed
+qed
+
+lemma re_complex_div_gt_0: "Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0"
+  and im_complex_div_gt_0: "Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0"
+using complex_div_gt_0 by auto
+
+lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+  by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
+
+lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+  by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
+
+lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+  by (smt re_complex_div_eq_0 re_complex_div_gt_0)
+
+lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+  by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
+
+lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+  by (metis not_le re_complex_div_gt_0)
+
+lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+  by (metis im_complex_div_gt_0 not_le)
+
+lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
+  by (induct s rule: finite_induct) auto
+
+lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
+  by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
+  by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
+  by (metis Complex_setsum')
+
+lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
+  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
+
+lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
+by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj 
+          complex_of_real_def equal_neg_zero)
+
+lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
+  by (metis Reals_of_real complex_of_real_def)
+
+lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
+  by (metis Re_complex_of_real Reals_cases norm_of_real)
+
+
 subsection{*Finally! Polar Form for Complex Numbers*}
 
 subsubsection {* $\cos \theta + i \sin \theta$ *}
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -12,6 +12,10 @@
 
 declare [[code drop: integer_of_int]]
 
+context
+includes integer.lifting
+begin
+
 lemma [code]:
   "integer_of_int (int_of_integer k) = k"
   by transfer rule
@@ -86,6 +90,7 @@
 lemma [code]:
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
+end
 
 lemma (in ring_1) of_int_code_if:
   "of_int k = (if k = 0 then 0
@@ -105,7 +110,7 @@
 
 lemma [code]:
   "nat = nat_of_integer \<circ> of_int"
-  by transfer (simp add: fun_eq_iff)
+  including integer.lifting by transfer (simp add: fun_eq_iff)
 
 code_identifier
   code_module Code_Target_Int \<rightharpoonup>
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -10,6 +10,10 @@
 
 subsection {* Implementation for @{typ nat} *}
 
+context
+includes natural.lifting integer.lifting
+begin
+
 lift_definition Nat :: "integer \<Rightarrow> nat"
   is nat
   .
@@ -96,6 +100,8 @@
   "num_of_nat = num_of_integer \<circ> of_nat"
   by transfer (simp add: fun_eq_iff)
 
+end
+
 lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
@@ -120,7 +126,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
-  by transfer auto
+  including integer.lifting by transfer auto
 
 lemma term_of_nat_code [code]:
   -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
@@ -139,7 +145,7 @@
   "nat_of_integer 0 = 0"
   "nat_of_integer 1 = 1"
   "nat_of_integer (numeral k) = numeral k"
-  by (transfer, simp)+
+  including integer.lifting by (transfer, simp)+
 
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -176,16 +176,8 @@
 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 
   parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
 
-lemma compose_rel_to_Domainp:
-  assumes "left_unique R"
-  assumes "(R ===> op=) P P'"
-  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) x y \<longleftrightarrow> Domainp R x \<and> P x \<and> x = y"
-using assms unfolding OO_def conversep_iff Domainp_iff left_unique_def fun_rel_def invariant_def
-by blast
-
 lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer 
-by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset 
-  simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq)
+by (simp add: finite_subset)
 
 lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
 
@@ -194,13 +186,10 @@
 
 lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
 
-(* FIXME why is not invariant here unfolded ? *)
-lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
-unfolding invariant_def Set.bind_def by clarsimp metis
+lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer 
+by (simp add: Set.bind_def)
 
-lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer
-by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer])
-  (auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def)
+lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
 
 lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
 lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -7,6 +7,7 @@
 begin
 
 subsection {* Square root of complex numbers *}
+
 definition csqrt :: "complex \<Rightarrow> complex" where
 "csqrt z = (if Im z = 0 then
             if 0 \<le> Re z then Complex (sqrt(Re z)) 0
@@ -54,6 +55,39 @@
   ultimately show ?thesis by blast
 qed
 
+lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
+  by (simp add: csqrt_def)
+
+lemma csqrt_0 [simp]: "csqrt 0 = 0"
+  by (simp add: csqrt_def)
+
+lemma csqrt_1 [simp]: "csqrt 1 = 1"
+  by (simp add: csqrt_def)
+
+lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
+proof (cases z)
+  case (Complex x y)
+  then show ?thesis
+    using real_sqrt_sum_squares_ge1 [of "x" y]
+          real_sqrt_sum_squares_ge1 [of "-x" y]
+          real_sqrt_sum_squares_eq_cancel [of x y]
+    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
+    apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
+    by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
+qed
+
+lemma Re_csqrt: "0 \<le> Re(csqrt z)"
+  by (metis csqrt_principal le_less)
+
+lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
+  using csqrt [of "z^2"] csqrt_principal [of "z^2"]
+  by (cases z) (auto simp: power2_eq_iff)
+
+lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
+  by auto (metis csqrt power_eq_0_iff)
+
+lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
+  by auto (metis csqrt power2_eq_1_iff)
 
 subsection{* More lemmas about module of complex numbers *}
 
@@ -64,27 +98,29 @@
 lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
   using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
 
-subsection{* Basic lemmas about complex polynomials *}
+subsection{* Basic lemmas about polynomials *}
 
 lemma poly_bound_exists:
-  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
+  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly" 
+  shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z <= r \<longrightarrow> norm (poly p z) \<le> m)"
 proof(induct p)
   case 0 thus ?case by (rule exI[where x=1], simp)
 next
   case (pCons c cs)
-  from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
+  from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
     by blast
-  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
+  let ?k = " 1 + norm c + \<bar>r * m\<bar>"
   have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
-  {fix z
-    assume H: "cmod z \<le> r"
-    from m H have th: "cmod (poly cs z) \<le> m" by blast
+  {fix z :: 'a 
+    assume H: "norm z \<le> r"
+    from m H have th: "norm (poly cs z) \<le> m" by blast
     from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
-    have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
+    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z* poly cs z)"
       using norm_triangle_ineq[of c "z* poly cs z"] by simp
-    also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
+    also have "\<dots> \<le> norm c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
+      by (simp add: norm_mult)
     also have "\<dots> \<le> ?k" by simp
-    finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
+    finally have "norm (poly (pCons c cs) z) \<le> ?k" .}
   with kp show ?case by blast
 qed
 
@@ -140,7 +176,9 @@
 lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
   unfolding psize_def by simp
 
-lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
+lemma poly_offset: 
+  fixes p:: "('a::comm_ring_1) poly" 
+  shows "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
 proof (intro exI conjI)
   show "psize (offset_poly p a) = psize p"
     unfolding psize_def
@@ -297,8 +335,9 @@
 text{* Polynomial is continuous. *}
 
 lemma poly_cont:
+  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly" 
   assumes ep: "e > 0"
-  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
+  shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
 proof-
   obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
   proof
@@ -316,7 +355,7 @@
   next
     case (pCons c cs)
     from poly_bound_exists[of 1 "cs"]
-    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
+    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" by blast
     from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
     have one0: "1 > (0::real)"  by arith
     from real_lbound_gt_zero[OF one0 em0]
@@ -326,12 +365,12 @@
     show ?case
       proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
         fix d w
-        assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
-        hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
+        assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "norm (w-z) < d"
+        hence d1: "norm (w-z) \<le> 1" "d \<ge> 0" by simp_all
         from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
-        from H have th: "cmod (w-z) \<le> d" by simp
+        from H have th: "norm (w-z) \<le> d" by simp
         from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
-        show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
+        show "norm (w - z) * norm (poly cs (w - z)) < e" by simp
       qed
     qed
 qed
@@ -448,41 +487,42 @@
 text {* Nonzero polynomial in z goes to infinity as z does. *}
 
 lemma poly_infinity:
+  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly" 
   assumes ex: "p \<noteq> 0"
-  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
+  shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
 using ex
 proof(induct p arbitrary: a d)
   case (pCons c cs a d)
   {assume H: "cs \<noteq> 0"
-    with pCons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (pCons c cs) z)" by blast
+    with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)" by blast
     let ?r = "1 + \<bar>r\<bar>"
-    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
-      have r0: "r \<le> cmod z" using h by arith
+    {fix z::'a assume h: "1 + \<bar>r\<bar> \<le> norm z"
+      have r0: "r \<le> norm z" using h by arith
       from r[rule_format, OF r0]
-      have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
-      from h have z1: "cmod z \<ge> 1" by arith
+      have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)" by arith
+      from h have z1: "norm z \<ge> 1" by arith
       from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
-      have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
+      have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
         unfolding norm_mult by (simp add: algebra_simps)
-      from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
-      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
+      from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
+      have th2: "norm(z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
         by (simp add: algebra_simps)
-      from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
+      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"  by arith}
     hence ?case by blast}
   moreover
   {assume cs0: "\<not> (cs \<noteq> 0)"
     with pCons.prems have c0: "c \<noteq> 0" by simp
     from cs0 have cs0': "cs = 0" by simp
-    {fix z
-      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
-      from c0 have "cmod c > 0" by simp
-      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
+    {fix z::'a
+      assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
+      from c0 have "norm c > 0" by simp
+      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z*c)"
         by (simp add: field_simps norm_mult)
       have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
-      from complex_mod_triangle_sub[of "z*c" a ]
-      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
+      from norm_diff_ineq[of "z*c" a ]
+      have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
         by (simp add: algebra_simps)
-      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
+      from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
         using cs0' by simp}
     then have ?case  by blast}
   ultimately show ?case by blast
@@ -816,7 +856,7 @@
               from h have "poly p x = 0" by (subst s, simp)
               with pq0 have "poly q x = 0" by blast
               with r xa have "poly r x = 0"
-                by (auto simp add: uminus_add_conv_diff)}
+                by auto}
             note impth = this
             from IH[rule_format, OF dsn, of s r] impth ds0
             have "s dvd (r ^ (degree s))" by blast
@@ -911,44 +951,38 @@
 (* Arithmetic operations on multivariate polynomials.                        *)
 
 lemma mpoly_base_conv:
-  "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
+  fixes x :: "'a::comm_ring_1" 
+  shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
+  by simp_all
 
 lemma mpoly_norm_conv:
-  "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
+  fixes x :: "'a::comm_ring_1" 
+  shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x" by simp_all
 
 lemma mpoly_sub_conv:
-  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
+  fixes x :: "'a::comm_ring_1" 
+  shows "poly p x - poly q x = poly p x + -1 * poly q x"
   by simp
 
-lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
+lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = 0" by simp
 
-lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
-
-lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
+lemma poly_cancel_eq_conv:
+  fixes x :: "'a::field" 
+  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)" 
+  by auto
 
 lemma poly_divides_pad_rule:
-  fixes p q :: "complex poly"
+  fixes p:: "('a::comm_ring_1) poly" 
   assumes pq: "p dvd q"
-  shows "p dvd (pCons (0::complex) q)"
+shows "p dvd (pCons 0 q)"
 proof-
   have "pCons 0 q = q * [:0,1:]" by simp
   then have "q dvd (pCons 0 q)" ..
   with pq show ?thesis by (rule dvd_trans)
 qed
 
-lemma poly_divides_pad_const_rule:
-  fixes p q :: "complex poly"
-  assumes pq: "p dvd q"
-  shows "p dvd (smult a q)"
-proof-
-  have "smult a q = q * [:a:]" by simp
-  then have "q dvd smult a q" ..
-  with pq show ?thesis by (rule dvd_trans)
-qed
-
-
 lemma poly_divides_conv0:
-  fixes p :: "complex poly"
+  fixes p:: "('a::field) poly" 
   assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
   shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
 proof-
@@ -969,9 +1003,10 @@
 qed
 
 lemma poly_divides_conv1:
-  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
+  fixes p:: "('a::field) poly" 
+  assumes a0: "a\<noteq> 0" and pp': "p dvd p'"
   and qrp': "smult a q - p' \<equiv> r"
-  shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
+  shows "p dvd q \<equiv> p dvd r" (is "?lhs \<equiv> ?rhs")
 proof-
   {
   from pp' obtain t where t: "p' = p * t" ..
@@ -1034,8 +1069,9 @@
   thus "p dvd (q ^ n) \<longleftrightarrow> p dvd r" by simp
 qed
 
-lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
-
-lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
+lemma poly_const_conv:
+  fixes x :: "'a::comm_ring_1" 
+  shows "poly [:c:] x = y \<longleftrightarrow> c = y" by simp
 
 end
+
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Lifting.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -296,7 +296,10 @@
   shows "x = y"
 using assms by (simp add: invariant_def)
 
-lemma fun_rel_eq_invariant:
+lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
+unfolding invariant_def fun_rel_def by auto
+
+lemma fun_rel_invariant_rel:
   shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
 by (auto simp add: invariant_def fun_rel_def)
 
@@ -591,6 +594,21 @@
 
 subsection {* Domains *}
 
+lemma composed_equiv_rel_invariant:
+  assumes "left_unique R"
+  assumes "(R ===> op=) P P'"
+  assumes "Domainp R = P''"
+  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
+fun_eq_iff by blast
+
+lemma composed_equiv_rel_eq_invariant:
+  assumes "left_unique R"
+  assumes "Domainp R = P"
+  shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
+fun_eq_iff is_equality_def by metis
+
 lemma pcr_Domainp_par_left_total:
   assumes "Domainp B = P"
   assumes "left_total A"
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -45,19 +45,7 @@
 
 lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
 
-lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
-proof -
-  {
-    fix x y
-    have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
-      unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
-  }
-  note cr = this
-  fix x :: "'a list list" and y :: "'a list list"
-  assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
-  then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
-  then show "?thesis x y" unfolding Lifting.invariant_def by auto
-qed
+lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto
 
 text {* We can export code: *}
 
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -71,7 +71,7 @@
   using Quotient_rel [OF Quotient_fset] by simp
 
 lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat parametric concat_transfer
-proof -
+proof (simp only: fset.pcr_cr_eq)
   fix xss yss :: "'a list list"
   assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss"
   then obtain uss vss where
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 22:54:21 2014 +0100
@@ -29,7 +29,7 @@
 
 fun mono_eq_prover ctxt prop =
   let
-    val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+    val rules = Lifting_Info.get_reflexivity_rules ctxt
   in
     SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
       handle ERROR _ => NONE
@@ -443,20 +443,81 @@
       |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
   end
 
+local
+  val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
+    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
+      @{thm pcr_Domainp}]
+in
 fun mk_readable_rsp_thm_eq tm lthy =
   let
     val ctm = cterm_of (Proof_Context.theory_of lthy) tm
     
+    (* This is not very cheap way of getting the rules but we have only few active
+      liftings in the current setting *)
+    fun get_cr_pcr_eqs ctxt =
+      let
+        fun collect (data : Lifting_Info.quotient) l =
+          if is_some (#pcr_info data) 
+          then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) 
+          else l
+        val table = Lifting_Info.get_quotients ctxt
+      in
+        Symtab.fold (fn (_, data) => fn l => collect data l) table []
+      end
+
+    fun assms_rewr_conv tactic rule ct =
+      let
+        fun prove_extra_assms thm =
+          let
+            val assms = cprems_of thm
+            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
+            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
+          in
+            map_interrupt prove assms
+          end
+    
+        fun cconl_of thm = Drule.strip_imp_concl (cprop_of thm)
+        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
+        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
+        val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+        val lhs = lhs_of rule1;
+        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
+        val rule3 =
+          Thm.instantiate (Thm.match (lhs, ct)) rule2
+            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
+        val proved_assms = prove_extra_assms rule3
+      in
+        case proved_assms of
+          SOME proved_assms =>
+            let
+              val rule3 = proved_assms MRSL rule3
+              val rule4 =
+                if lhs_of rule3 aconvc ct then rule3
+                else
+                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
+                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
+            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
+          | NONE => Conv.no_conv ct
+      end
+
+    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
+
     fun simp_arrows_conv ctm =
       let
         val unfold_conv = Conv.rewrs_conv 
           [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, 
+            @{thm fun_rel_invariant_rel[THEN eq_reflection]},
             @{thm fun_rel_eq[THEN eq_reflection]},
             @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
             @{thm fun_rel_def[THEN eq_reflection]}]
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+        val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
+            invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
+        val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) 
+          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
         val invariant_commute_conv = Conv.bottom_conv
-          (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
+          (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac
+            (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
         val relator_eq_conv = Conv.bottom_conv
           (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
       in
@@ -467,8 +528,9 @@
       end
     
     val unfold_ret_val_invs = Conv.bottom_conv 
-      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
-    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
+      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
+    val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
+    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv))
     val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
     val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
     val beta_conv = Thm.beta_conversion true
@@ -477,6 +539,7 @@
   in
     Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end
+end
 
 fun rename_to_tnames ctxt term =
   let
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 25 22:54:21 2014 +0100
@@ -516,6 +516,11 @@
   #> relfexivity_rule_setup
   #> relator_distr_attribute_setup
 
+(* setup fixed invariant rules *)
+
+val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
+  [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
+
 (* outer syntax commands *)
 
 val _ =
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Feb 25 22:54:21 2014 +0100
@@ -447,16 +447,6 @@
    end
   
   fun rewrs_imp rules = first_imp (map rewr_imp rules)
-
-  fun map_interrupt f l =
-    let
-      fun map_interrupt' _ [] l = SOME (rev l)
-       | map_interrupt' f (x::xs) l = (case f x of
-        NONE => NONE
-        | SOME v => map_interrupt' f xs (v::l))
-    in
-      map_interrupt' f l []
-    end
 in
 
   (*
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Tue Feb 25 22:54:21 2014 +0100
@@ -31,6 +31,7 @@
   val relation_types: typ -> typ * typ
   val mk_HOL_eq: thm -> thm
   val safe_HOL_meta_eq: thm -> thm
+  val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
 end
 
 
@@ -121,4 +122,14 @@
 
 fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
 
+fun map_interrupt f l =
+  let
+    fun map_interrupt' _ [] l = SOME (rev l)
+     | map_interrupt' f (x::xs) l = (case f x of
+      NONE => NONE
+      | SOME v => map_interrupt' f xs (v::l))
+  in
+    map_interrupt' f l []
+  end
+
 end
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Tools/transfer.ML	Tue Feb 25 22:54:21 2014 +0100
@@ -25,10 +25,13 @@
   val transfer_raw_del: thm -> Context.generic -> Context.generic
   val transferred_attribute: thm list -> attribute
   val untransferred_attribute: thm list -> attribute
+  val prep_transfer_domain_thm: Proof.context -> thm -> thm
   val transfer_domain_add: attribute
   val transfer_domain_del: attribute
   val transfer_rule_of_term: Proof.context -> bool -> term -> thm
   val transfer_rule_of_lhs: Proof.context -> term -> thm
+  val eq_tac: Proof.context -> int -> tactic
+  val transfer_step_tac: Proof.context -> int -> tactic
   val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic
   val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
@@ -346,11 +349,14 @@
 
 (** Adding transfer domain rules **)
 
-fun add_transfer_domain_thm thm ctxt = 
-  (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+fun prep_transfer_domain_thm ctxt thm = 
+  (abstract_equalities_domain ctxt o detect_transfer_rules) thm 
 
-fun del_transfer_domain_thm thm ctxt = 
-  (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o 
+  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
+
+fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o 
+  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
 
 (** Transfer proof method **)
 
@@ -571,7 +577,13 @@
       |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
-fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
+fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) 
+  THEN_ALL_NEW rtac @{thm is_equality_eq}
+
+fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+
+fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt)) 
+  THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
 
 fun transfer_tac equiv ctxt i =
   let
@@ -587,7 +599,7 @@
       rtac start_rule i THEN
       (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
         THEN_ALL_NEW
-          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
+          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
             ORELSE' end_tac)) (i + 1)
         handle TERM (_, ts) => raise TERM (err_msg, ts)
   in
@@ -612,7 +624,7 @@
        rtac @{thm transfer_prover_start} i,
        ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
         THEN_ALL_NEW
-         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1),
+         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
        rtac @{thm refl} i]
   end)
 
@@ -640,7 +652,7 @@
       (rtac rule
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
-            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
@@ -676,7 +688,7 @@
       (rtac rule
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
-            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -1706,6 +1706,11 @@
   unfolding continuous_on_open_invariant
   by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
 
+corollary continuous_imp_open_vimage:
+  assumes "continuous_on s f" "open s" "open B" "f -` B \<subseteq> s"
+    shows "open (f -` B)"
+by (metis assms continuous_on_open_vimage le_iff_inf)
+
 lemma continuous_on_closed_invariant:
   "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
 proof -
diff -r 43d0e2a34c9d -r c90cc76ec855 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Feb 25 22:13:57 2014 +0100
+++ b/src/HOL/Transcendental.thy	Tue Feb 25 22:54:21 2014 +0100
@@ -52,6 +52,12 @@
   finally show ?case .
 qed
 
+corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows   "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
+using lemma_realpow_diff_sumr2[of x "n - 1" y]
+by (cases "n = 0") (simp_all add: field_simps)
+
 lemma lemma_realpow_rev_sumr:
    "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
     (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"