# HG changeset patch
# User wenzelm
# Date 1468346598 -7200
# Node ID d7610beb98bc978edb8b8721d7755d77f6b28fe4
# Parent  9d4dbb7a548a9939ed903a32f43625545fb09cae
misc tuning and modernization;

diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Continuum_Not_Denumerable.thy
--- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Tue Jul 12 19:12:17 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Tue Jul 12 20:03:18 2016 +0200
@@ -11,36 +11,38 @@
 
 subsection \<open>Abstract\<close>
 
-text \<open>The following document presents a proof that the Continuum is
-uncountable. It is formalised in the Isabelle/Isar theorem proving
-system.
+text \<open>
+  The following document presents a proof that the Continuum is uncountable.
+  It is formalised in the Isabelle/Isar theorem proving system.
 
-{\em Theorem:} The Continuum \<open>\<real>\<close> is not denumerable. In other
-words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is
-surjective.
+  \<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
+  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective.
+
+  \<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
+  Diagonalisation argument. The proof presented here is not this one.
 
-{\em Outline:} An elegant informal proof of this result uses Cantor's
-Diagonalisation argument. The proof presented here is not this
-one. First we formalise some properties of closed intervals, then we
-prove the Nested Interval Property. This property relies on the
-completeness of the Real numbers and is the foundation for our
-argument. Informally it states that an intersection of countable
-closed intervals (where each successive interval is a subset of the
-last) is non-empty. We then assume a surjective function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real x such that x is not in the range of f
-by generating a sequence of closed intervals then using the NIP.\<close>
+  First we formalise some properties of closed intervals, then we prove the
+  Nested Interval Property. This property relies on the completeness of the
+  Real numbers and is the foundation for our argument. Informally it states
+  that an intersection of countable closed intervals (where each successive
+  interval is a subset of the last) is non-empty. We then assume a surjective
+  function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
+  range of \<open>f\<close> by generating a sequence of closed intervals then using the
+  NIP.
+\<close>
 
-theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
+theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
 proof
   assume "\<exists>f::nat \<Rightarrow> real. surj f"
   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
 
   txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
 
-  have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
+  have "a < b \<Longrightarrow> \<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}" for a b c :: real
     by (auto simp add: not_le cong: conj_cong)
-       (metis dense le_less_linear less_linear less_trans order_refl)
+      (metis dense le_less_linear less_linear less_trans order_refl)
   then obtain i j where ij:
-      "a < b \<Longrightarrow> i a b c < j a b c"
+    "a < b \<Longrightarrow> i a b c < j a b c"
       "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
       "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
     for a b c :: real
@@ -50,29 +52,31 @@
     rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
   define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n
 
-  have ivl[simp]:
+  have ivl [simp]:
     "ivl 0 = (f 0 + 1, f 0 + 2)"
     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
     unfolding ivl_def by simp_all
 
   txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
 
-  { fix n have "fst (ivl n) < snd (ivl n)"
-      by (induct n) (auto intro!: ij) }
-  note less = this
+  have less: "fst (ivl n) < snd (ivl n)" for n
+    by (induct n) (auto intro!: ij)
 
   have "decseq I"
-    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
+    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv
+    by (intro ij allI less)
 
   txt \<open>Now we apply the finite intersection property of compact sets.\<close>
 
   have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
   proof (rule compact_imp_fip_image)
-    fix S :: "nat set" assume fin: "finite S"
+    fix S :: "nat set"
+    assume fin: "finite S"
     have "{} \<subset> I (Max (insert 0 S))"
       unfolding I_def using less[of "Max (insert 0 S)"] by auto
     also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
-      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
+      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"]
+      by (auto simp: Max_ge_iff)
     also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
       by auto
     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
@@ -88,7 +92,7 @@
     unfolding I_def ivl fst_conv snd_conv by auto
 qed
 
-lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
+lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)"
   using real_non_denum unfolding uncountable_def by auto
 
 lemma bij_betw_open_intervals:
@@ -97,31 +101,29 @@
   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
 proof -
   define f where "f a b c d x = (d - c)/(b - a) * (x - a) + c" for a b c d x :: real
-  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
+  {
+    fix a b c d x :: real
+    assume *: "a < b" "c < d" "a < x" "x < b"
     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
       by (intro mult_strict_left_mono) simp_all
     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
       by simp
     ultimately have "f a b c d x < d" "c < f a b c d x"
-      by (simp_all add: f_def field_simps) }
+      by (simp_all add: f_def field_simps)
+  }
   with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
     by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
-  thus ?thesis by auto
+  then show ?thesis by auto
 qed
 
 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
   using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
 
-lemma uncountable_open_interval:
-  fixes a b :: real 
-  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
+lemma uncountable_open_interval: "uncountable {a<..<b} \<longleftrightarrow> a < b" for a b :: real
 proof
-  assume "uncountable {a<..<b}"
-  then show "a < b"
-    using uncountable_def by force
-next 
-  assume "a < b"
-  show "uncountable {a<..<b}"
+  show "a < b" if "uncountable {a<..<b}"
+    using uncountable_def that by force
+  show "uncountable {a<..<b}" if "a < b"
   proof -
     obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
       using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
@@ -130,38 +132,44 @@
   qed
 qed
 
-lemma uncountable_half_open_interval_1:
-  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
+lemma uncountable_half_open_interval_1: "uncountable {a..<b} \<longleftrightarrow> a < b" for a b :: real
   apply auto
-  using atLeastLessThan_empty_iff apply fastforce
+  using atLeastLessThan_empty_iff
+  apply fastforce
   using uncountable_open_interval [of a b]
-  by (metis countable_Un_iff ivl_disj_un_singleton(3))
+  apply (metis countable_Un_iff ivl_disj_un_singleton(3))
+  done
 
-lemma uncountable_half_open_interval_2:
-  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
+lemma uncountable_half_open_interval_2: "uncountable {a<..b} \<longleftrightarrow> a < b" for a b :: real
   apply auto
-  using atLeastLessThan_empty_iff apply fastforce
+  using atLeastLessThan_empty_iff
+  apply fastforce
   using uncountable_open_interval [of a b]
-  by (metis countable_Un_iff ivl_disj_un_singleton(4))
+  apply (metis countable_Un_iff ivl_disj_un_singleton(4))
+  done
 
 lemma real_interval_avoid_countable_set:
   fixes a b :: real and A :: "real set"
   assumes "a < b" and "countable A"
   shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
 proof -
-  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto
-  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}" 
+  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})"
+    by auto
+  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
     by (simp add: uncountable_open_interval)
-  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
-  hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 
-    by (intro psubsetI, auto)
-  hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
+  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
+    by auto
+  then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
+    by (intro psubsetI) auto
+  then have "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
     by (rule psubset_imp_ex_mem)
-  thus ?thesis by auto
+  then show ?thesis
+    by auto
 qed
 
 lemma open_minus_countable:
-  fixes S A :: "real set" assumes "countable A" "S \<noteq> {}" "open S"
+  fixes S A :: "real set"
+  assumes "countable A" "S \<noteq> {}" "open S"
   shows "\<exists>x\<in>S. x \<notin> A"
 proof -
   obtain x where "x \<in> S"
diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Prefix_Order.thy
--- a/src/HOL/Library/Prefix_Order.thy	Tue Jul 12 19:12:17 2016 +0200
+++ b/src/HOL/Library/Prefix_Order.thy	Tue Jul 12 20:03:18 2016 +0200
@@ -11,16 +11,16 @@
 instantiation list :: (type) order
 begin
 
-definition "(xs::'a list) \<le> ys \<equiv> prefix xs ys"
-definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
+definition "xs \<le> ys \<equiv> prefix xs ys" for xs ys :: "'a list"
+definition "xs < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" for xs ys :: "'a list"
 
 instance
   by standard (auto simp: less_eq_list_def less_list_def)
 
 end
 
-lemma less_list_def': "(xs::'a list) < ys \<longleftrightarrow> strict_prefix xs ys"
-by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
+lemma less_list_def': "xs < ys \<longleftrightarrow> strict_prefix xs ys" for xs ys :: "'a list"
+  by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
 
 lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
 lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]
diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Tue Jul 12 19:12:17 2016 +0200
+++ b/src/HOL/Library/Preorder.thy	Tue Jul 12 20:03:18 2016 +0200
@@ -9,24 +9,21 @@
 class preorder_equiv = preorder
 begin
 
-definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
-  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
+definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
 
 notation
   equiv ("op \<approx>") and
   equiv ("(_/ \<approx> _)"  [51, 51] 50)
 
-lemma refl [iff]:
-  "x \<approx> x"
-  unfolding equiv_def by simp
+lemma refl [iff]: "x \<approx> x"
+  by (simp add: equiv_def)
 
-lemma trans:
-  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
-  unfolding equiv_def by (auto intro: order_trans)
+lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
+  by (auto simp: equiv_def intro: order_trans)
 
-lemma antisym:
-  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
-  unfolding equiv_def ..
+lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
+  by (simp only: equiv_def)
 
 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
   by (auto simp add: equiv_def less_le_not_le)
diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Quadratic_Discriminant.thy
--- a/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jul 12 19:12:17 2016 +0200
+++ b/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jul 12 20:03:18 2016 +0200
@@ -10,8 +10,8 @@
 imports Complex_Main
 begin
 
-definition discrim :: "[real,real,real] \<Rightarrow> real" where
-  "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
+definition discrim :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
+  where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
 
 lemma complete_square:
   fixes a b c x :: "real"
@@ -23,20 +23,22 @@
   with \<open>a \<noteq> 0\<close>
   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0"
     by simp
-  thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
-    unfolding discrim_def
-    by (simp add: power2_eq_square algebra_simps)
+  then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
+    by (simp add: discrim_def power2_eq_square algebra_simps)
 qed
 
 lemma discriminant_negative:
   fixes a b c x :: real
   assumes "a \<noteq> 0"
-  and "discrim a b c < 0"
+    and "discrim a b c < 0"
   shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
 proof -
-  have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
-  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
-  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
+  have "(2 * a * x + b)\<^sup>2 \<ge> 0"
+    by simp
+  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
+    by arith
+  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0"
+    by simp
 qed
 
 lemma plus_or_minus_sqrt:
@@ -45,13 +47,18 @@
   shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
 proof
   assume "x\<^sup>2 = y"
-  hence "sqrt (x\<^sup>2) = sqrt y" by simp
-  hence "sqrt y = \<bar>x\<bar>" by simp
-  thus "x = sqrt y \<or> x = - sqrt y" by auto
+  then have "sqrt (x\<^sup>2) = sqrt y"
+    by simp
+  then have "sqrt y = \<bar>x\<bar>"
+    by simp
+  then show "x = sqrt y \<or> x = - sqrt y"
+    by auto
 next
   assume "x = sqrt y \<or> x = - sqrt y"
-  hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
-  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y" by simp
+  then have "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2"
+    by auto
+  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y"
+    by simp
 qed
 
 lemma divide_non_zero:
@@ -59,20 +66,19 @@
   assumes "x \<noteq> 0"
   shows "x * y = z \<longleftrightarrow> y = z / x"
 proof
-  assume "x * y = z"
-  with \<open>x \<noteq> 0\<close> show "y = z / x" by (simp add: field_simps)
-next
-  assume "y = z / x"
-  with \<open>x \<noteq> 0\<close> show "x * y = z" by simp
+  show "y = z / x" if "x * y = z"
+    using \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
+  show "x * y = z" if "y = z / x"
+    using \<open>x \<noteq> 0\<close> that by simp
 qed
 
 lemma discriminant_nonneg:
   fixes a b c x :: real
   assumes "a \<noteq> 0"
-  and "discrim a b c \<ge> 0"
+    and "discrim a b c \<ge> 0"
   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
-  x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
-  x = (-b - sqrt (discrim a b c)) / (2 * a)"
+    x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a)"
 proof -
   from complete_square and plus_or_minus_sqrt and assms
   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
@@ -94,88 +100,93 @@
 lemma discriminant_zero:
   fixes a b c x :: real
   assumes "a \<noteq> 0"
-  and "discrim a b c = 0"
+    and "discrim a b c = 0"
   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
-  using discriminant_nonneg and assms
-  by simp
+  by (simp add: discriminant_nonneg assms)
 
 theorem discriminant_iff:
   fixes a b c x :: real
   assumes "a \<noteq> 0"
   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
-  discrim a b c \<ge> 0 \<and>
-  (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
-  x = (-b - sqrt (discrim a b c)) / (2 * a))"
+    discrim a b c \<ge> 0 \<and>
+    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+     x = (-b - sqrt (discrim a b c)) / (2 * a))"
 proof
   assume "a * x\<^sup>2 + b * x + c = 0"
-  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)" by auto
-  hence "discrim a b c \<ge> 0" by simp
+  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
+    by auto
+  then have "discrim a b c \<ge> 0"
+    by simp
   with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
   have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
-    x = (-b - sqrt (discrim a b c)) / (2 * a)"
+      x = (-b - sqrt (discrim a b c)) / (2 * a)"
     by simp
   with \<open>discrim a b c \<ge> 0\<close>
   show "discrim a b c \<ge> 0 \<and>
     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
-    x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
+     x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
 next
   assume "discrim a b c \<ge> 0 \<and>
     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
-    x = (-b - sqrt (discrim a b c)) / (2 * a))"
-  hence "discrim a b c \<ge> 0" and
+     x = (-b - sqrt (discrim a b c)) / (2 * a))"
+  then have "discrim a b c \<ge> 0" and
     "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
-    x = (-b - sqrt (discrim a b c)) / (2 * a)"
+     x = (-b - sqrt (discrim a b c)) / (2 * a)"
     by simp_all
-  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0" by simp
+  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0"
+    by simp
 qed
 
 lemma discriminant_nonneg_ex:
   fixes a b c :: real
   assumes "a \<noteq> 0"
-  and "discrim a b c \<ge> 0"
+    and "discrim a b c \<ge> 0"
   shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
-  using discriminant_nonneg and assms
-  by auto
+  by (auto simp: discriminant_nonneg assms)
 
 lemma discriminant_pos_ex:
   fixes a b c :: real
   assumes "a \<noteq> 0"
-  and "discrim a b c > 0"
-  shows "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
+    and "discrim a b c > 0"
+  shows "\<exists>x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
 proof -
   let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
   let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
-  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0" by simp
-  hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
-  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y" by simp
-  moreover
-  from discriminant_nonneg [of a b c ?x]
-    and discriminant_nonneg [of a b c ?y]
-    and assms
-  have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
-  ultimately
-  show "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0" by blast
+  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
+    by simp
+  then have "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)"
+    by arith
+  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y"
+    by simp
+  moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0"
+    using discriminant_nonneg [of a b c ?x]
+      and discriminant_nonneg [of a b c ?y]
+    by simp_all
+  ultimately show ?thesis
+    by blast
 qed
 
 lemma discriminant_pos_distinct:
   fixes a b c x :: real
-  assumes "a \<noteq> 0" and "discrim a b c > 0"
+  assumes "a \<noteq> 0"
+    and "discrim a b c > 0"
   shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
 proof -
   from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
   obtain w and z where "w \<noteq> z"
     and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
     by blast
-  show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
-  proof cases
-    assume "x = w"
-    with \<open>w \<noteq> z\<close> have "x \<noteq> z" by simp
-    with \<open>a * z\<^sup>2 + b * z + c = 0\<close>
-    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
+  show "\<exists>y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
+  proof (cases "x = w")
+    case True
+    with \<open>w \<noteq> z\<close> have "x \<noteq> z"
+      by simp
+    with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
+      by auto
   next
-    assume "x \<noteq> w"
-    with \<open>a * w\<^sup>2 + b * w + c = 0\<close>
-    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
+    case False
+    with \<open>a * w\<^sup>2 + b * w + c = 0\<close> show ?thesis
+      by auto
   qed
 qed
 
diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Tue Jul 12 19:12:17 2016 +0200
+++ b/src/HOL/Library/Sublist_Order.thy	Tue Jul 12 20:03:18 2016 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Library/Sublist_Order.thy
-    Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
-                Florian Haftmann, Tobias Nipkow, TU Muenchen
+    Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
+    Author:     Florian Haftmann, , TU Muenchen
+    Author:     Tobias Nipkow, TU Muenchen
 *)
 
 section \<open>Sublist Ordering\<close>
@@ -10,9 +11,8 @@
 begin
 
 text \<open>
-  This theory defines sublist ordering on lists.
-  A list \<open>ys\<close> is a sublist of a list \<open>xs\<close>,
-  iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
+  This theory defines sublist ordering on lists. A list \<open>ys\<close> is a sublist of a
+  list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
 \<close>
 
 subsection \<open>Definitions and basic lemmas\<close>
@@ -20,11 +20,8 @@
 instantiation list :: (type) ord
 begin
 
-definition
-  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
-
-definition
-  "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+definition "xs \<le> ys \<longleftrightarrow> sublisteq xs ys" for xs ys :: "'a list"
+definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
 
 instance ..
 
@@ -32,19 +29,15 @@
 
 instance list :: (type) order
 proof
-  fix xs ys :: "'a list"
-  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
-next
-  fix xs :: "'a list"
-  show "xs \<le> xs" by (simp add: less_eq_list_def)
-next
-  fix xs ys :: "'a list"
-  assume "xs <= ys" and "ys <= xs"
-  thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
-next
   fix xs ys zs :: "'a list"
-  assume "xs <= ys" and "ys <= zs"
-  thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
+  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+    unfolding less_list_def ..
+  show "xs \<le> xs"
+    by (simp add: less_eq_list_def)
+  show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
+    using that unfolding less_eq_list_def by (rule sublisteq_antisym)
+  show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
+    using that unfolding less_eq_list_def by (rule sublisteq_trans)
 qed
 
 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
@@ -71,7 +64,8 @@
   by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
 
 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
-  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
+  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le
+      self_append_conv2 less_eq_list_def)
 
 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   by (metis less_list_def less_eq_list_def sublisteq_append')