author wenzelm Tue Jul 12 20:03:18 2016 +0200 (2016-07-12) changeset 63465 d7610beb98bc parent 63464 9d4dbb7a548a child 63466 2100fbbdc3f1
misc tuning and modernization;
     1.1 --- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Tue Jul 12 19:12:17 2016 +0200
1.2 +++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Tue Jul 12 20:03:18 2016 +0200
1.3 @@ -11,36 +11,38 @@
1.4
1.5  subsection \<open>Abstract\<close>
1.6
1.7 -text \<open>The following document presents a proof that the Continuum is
1.8 -uncountable. It is formalised in the Isabelle/Isar theorem proving
1.9 -system.
1.10 +text \<open>
1.11 +  The following document presents a proof that the Continuum is uncountable.
1.12 +  It is formalised in the Isabelle/Isar theorem proving system.
1.13
1.14 -{\em Theorem:} The Continuum \<open>\<real>\<close> is not denumerable. In other
1.15 -words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is
1.16 -surjective.
1.17 +  \<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
1.18 +  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective.
1.19 +
1.20 +  \<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
1.21 +  Diagonalisation argument. The proof presented here is not this one.
1.22
1.23 -{\em Outline:} An elegant informal proof of this result uses Cantor's
1.24 -Diagonalisation argument. The proof presented here is not this
1.25 -one. First we formalise some properties of closed intervals, then we
1.26 -prove the Nested Interval Property. This property relies on the
1.27 -completeness of the Real numbers and is the foundation for our
1.28 -argument. Informally it states that an intersection of countable
1.29 -closed intervals (where each successive interval is a subset of the
1.30 -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
1.31 -by generating a sequence of closed intervals then using the NIP.\<close>
1.32 +  First we formalise some properties of closed intervals, then we prove the
1.33 +  Nested Interval Property. This property relies on the completeness of the
1.34 +  Real numbers and is the foundation for our argument. Informally it states
1.35 +  that an intersection of countable closed intervals (where each successive
1.36 +  interval is a subset of the last) is non-empty. We then assume a surjective
1.37 +  function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
1.38 +  range of \<open>f\<close> by generating a sequence of closed intervals then using the
1.39 +  NIP.
1.40 +\<close>
1.41
1.42 -theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
1.43 +theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
1.44  proof
1.45    assume "\<exists>f::nat \<Rightarrow> real. surj f"
1.46    then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
1.47
1.48    txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
1.49
1.50 -  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})"
1.51 +  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
1.52      by (auto simp add: not_le cong: conj_cong)
1.53 -       (metis dense le_less_linear less_linear less_trans order_refl)
1.54 +      (metis dense le_less_linear less_linear less_trans order_refl)
1.55    then obtain i j where ij:
1.56 -      "a < b \<Longrightarrow> i a b c < j a b c"
1.57 +    "a < b \<Longrightarrow> i a b c < j a b c"
1.58        "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
1.59        "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
1.60      for a b c :: real
1.61 @@ -50,29 +52,31 @@
1.62      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)))"
1.63    define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n
1.64
1.65 -  have ivl[simp]:
1.66 +  have ivl [simp]:
1.67      "ivl 0 = (f 0 + 1, f 0 + 2)"
1.68      "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
1.69      unfolding ivl_def by simp_all
1.70
1.71    txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
1.72
1.73 -  { fix n have "fst (ivl n) < snd (ivl n)"
1.74 -      by (induct n) (auto intro!: ij) }
1.75 -  note less = this
1.76 +  have less: "fst (ivl n) < snd (ivl n)" for n
1.77 +    by (induct n) (auto intro!: ij)
1.78
1.79    have "decseq I"
1.80 -    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
1.81 +    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv
1.82 +    by (intro ij allI less)
1.83
1.84    txt \<open>Now we apply the finite intersection property of compact sets.\<close>
1.85
1.86    have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
1.87    proof (rule compact_imp_fip_image)
1.88 -    fix S :: "nat set" assume fin: "finite S"
1.89 +    fix S :: "nat set"
1.90 +    assume fin: "finite S"
1.91      have "{} \<subset> I (Max (insert 0 S))"
1.92        unfolding I_def using less[of "Max (insert 0 S)"] by auto
1.93      also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
1.94 -      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
1.95 +      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"]
1.96 +      by (auto simp: Max_ge_iff)
1.97      also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
1.98        by auto
1.99      finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
1.100 @@ -88,7 +92,7 @@
1.101      unfolding I_def ivl fst_conv snd_conv by auto
1.102  qed
1.103
1.104 -lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
1.105 +lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)"
1.106    using real_non_denum unfolding uncountable_def by auto
1.107
1.108  lemma bij_betw_open_intervals:
1.109 @@ -97,31 +101,29 @@
1.110    shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
1.111  proof -
1.112    define f where "f a b c d x = (d - c)/(b - a) * (x - a) + c" for a b c d x :: real
1.113 -  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
1.114 +  {
1.115 +    fix a b c d x :: real
1.116 +    assume *: "a < b" "c < d" "a < x" "x < b"
1.117      moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
1.118        by (intro mult_strict_left_mono) simp_all
1.119      moreover from * have "0 < (d - c) * (x - a) / (b - a)"
1.120        by simp
1.121      ultimately have "f a b c d x < d" "c < f a b c d x"
1.122 -      by (simp_all add: f_def field_simps) }
1.123 +      by (simp_all add: f_def field_simps)
1.124 +  }
1.125    with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
1.126      by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
1.127 -  thus ?thesis by auto
1.128 +  then show ?thesis by auto
1.129  qed
1.130
1.131  lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
1.132    using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
1.133
1.134 -lemma uncountable_open_interval:
1.135 -  fixes a b :: real
1.136 -  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
1.137 +lemma uncountable_open_interval: "uncountable {a<..<b} \<longleftrightarrow> a < b" for a b :: real
1.138  proof
1.139 -  assume "uncountable {a<..<b}"
1.140 -  then show "a < b"
1.141 -    using uncountable_def by force
1.142 -next
1.143 -  assume "a < b"
1.144 -  show "uncountable {a<..<b}"
1.145 +  show "a < b" if "uncountable {a<..<b}"
1.146 +    using uncountable_def that by force
1.147 +  show "uncountable {a<..<b}" if "a < b"
1.148    proof -
1.149      obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
1.150        using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
1.151 @@ -130,38 +132,44 @@
1.152    qed
1.153  qed
1.154
1.155 -lemma uncountable_half_open_interval_1:
1.156 -  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
1.157 +lemma uncountable_half_open_interval_1: "uncountable {a..<b} \<longleftrightarrow> a < b" for a b :: real
1.158    apply auto
1.159 -  using atLeastLessThan_empty_iff apply fastforce
1.160 +  using atLeastLessThan_empty_iff
1.161 +  apply fastforce
1.162    using uncountable_open_interval [of a b]
1.163 -  by (metis countable_Un_iff ivl_disj_un_singleton(3))
1.164 +  apply (metis countable_Un_iff ivl_disj_un_singleton(3))
1.165 +  done
1.166
1.167 -lemma uncountable_half_open_interval_2:
1.168 -  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
1.169 +lemma uncountable_half_open_interval_2: "uncountable {a<..b} \<longleftrightarrow> a < b" for a b :: real
1.170    apply auto
1.171 -  using atLeastLessThan_empty_iff apply fastforce
1.172 +  using atLeastLessThan_empty_iff
1.173 +  apply fastforce
1.174    using uncountable_open_interval [of a b]
1.175 -  by (metis countable_Un_iff ivl_disj_un_singleton(4))
1.176 +  apply (metis countable_Un_iff ivl_disj_un_singleton(4))
1.177 +  done
1.178
1.179  lemma real_interval_avoid_countable_set:
1.180    fixes a b :: real and A :: "real set"
1.181    assumes "a < b" and "countable A"
1.182    shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
1.183  proof -
1.184 -  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto
1.185 -  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
1.186 +  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})"
1.187 +    by auto
1.188 +  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
1.190 -  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
1.191 -  hence "A \<inter> {a<..<b} \<subset> {a<..<b}"
1.192 -    by (intro psubsetI, auto)
1.193 -  hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
1.194 +  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
1.195 +    by auto
1.196 +  then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
1.197 +    by (intro psubsetI) auto
1.198 +  then have "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
1.199      by (rule psubset_imp_ex_mem)
1.200 -  thus ?thesis by auto
1.201 +  then show ?thesis
1.202 +    by auto
1.203  qed
1.204
1.205  lemma open_minus_countable:
1.206 -  fixes S A :: "real set" assumes "countable A" "S \<noteq> {}" "open S"
1.207 +  fixes S A :: "real set"
1.208 +  assumes "countable A" "S \<noteq> {}" "open S"
1.209    shows "\<exists>x\<in>S. x \<notin> A"
1.210  proof -
1.211    obtain x where "x \<in> S"

     2.1 --- a/src/HOL/Library/Prefix_Order.thy	Tue Jul 12 19:12:17 2016 +0200
2.2 +++ b/src/HOL/Library/Prefix_Order.thy	Tue Jul 12 20:03:18 2016 +0200
2.3 @@ -11,16 +11,16 @@
2.4  instantiation list :: (type) order
2.5  begin
2.6
2.7 -definition "(xs::'a list) \<le> ys \<equiv> prefix xs ys"
2.8 -definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
2.9 +definition "xs \<le> ys \<equiv> prefix xs ys" for xs ys :: "'a list"
2.10 +definition "xs < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" for xs ys :: "'a list"
2.11
2.12  instance
2.13    by standard (auto simp: less_eq_list_def less_list_def)
2.14
2.15  end
2.16
2.17 -lemma less_list_def': "(xs::'a list) < ys \<longleftrightarrow> strict_prefix xs ys"
2.18 -by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
2.19 +lemma less_list_def': "xs < ys \<longleftrightarrow> strict_prefix xs ys" for xs ys :: "'a list"
2.20 +  by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
2.21
2.22  lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
2.23  lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]

     3.1 --- a/src/HOL/Library/Preorder.thy	Tue Jul 12 19:12:17 2016 +0200
3.2 +++ b/src/HOL/Library/Preorder.thy	Tue Jul 12 20:03:18 2016 +0200
3.3 @@ -9,24 +9,21 @@
3.4  class preorder_equiv = preorder
3.5  begin
3.6
3.7 -definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
3.8 -  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
3.9 +definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
3.10 +  where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
3.11
3.12  notation
3.13    equiv ("op \<approx>") and
3.14    equiv ("(_/ \<approx> _)"  [51, 51] 50)
3.15
3.16 -lemma refl [iff]:
3.17 -  "x \<approx> x"
3.18 -  unfolding equiv_def by simp
3.19 +lemma refl [iff]: "x \<approx> x"
3.20 +  by (simp add: equiv_def)
3.21
3.22 -lemma trans:
3.23 -  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
3.24 -  unfolding equiv_def by (auto intro: order_trans)
3.25 +lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
3.26 +  by (auto simp: equiv_def intro: order_trans)
3.27
3.28 -lemma antisym:
3.29 -  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
3.30 -  unfolding equiv_def ..
3.31 +lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
3.32 +  by (simp only: equiv_def)
3.33
3.34  lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
3.35    by (auto simp add: equiv_def less_le_not_le)

     4.1 --- a/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jul 12 19:12:17 2016 +0200
4.2 +++ b/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jul 12 20:03:18 2016 +0200
4.3 @@ -10,8 +10,8 @@
4.4  imports Complex_Main
4.5  begin
4.6
4.7 -definition discrim :: "[real,real,real] \<Rightarrow> real" where
4.8 -  "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
4.9 +definition discrim :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
4.10 +  where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
4.11
4.12  lemma complete_square:
4.13    fixes a b c x :: "real"
4.14 @@ -23,20 +23,22 @@
4.15    with \<open>a \<noteq> 0\<close>
4.16    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"
4.17      by simp
4.18 -  thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
4.19 -    unfolding discrim_def
4.20 -    by (simp add: power2_eq_square algebra_simps)
4.21 +  then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
4.22 +    by (simp add: discrim_def power2_eq_square algebra_simps)
4.23  qed
4.24
4.25  lemma discriminant_negative:
4.26    fixes a b c x :: real
4.27    assumes "a \<noteq> 0"
4.28 -  and "discrim a b c < 0"
4.29 +    and "discrim a b c < 0"
4.30    shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
4.31  proof -
4.32 -  have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
4.33 -  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
4.34 -  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
4.35 +  have "(2 * a * x + b)\<^sup>2 \<ge> 0"
4.36 +    by simp
4.37 +  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
4.38 +    by arith
4.39 +  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0"
4.40 +    by simp
4.41  qed
4.42
4.43  lemma plus_or_minus_sqrt:
4.44 @@ -45,13 +47,18 @@
4.45    shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
4.46  proof
4.47    assume "x\<^sup>2 = y"
4.48 -  hence "sqrt (x\<^sup>2) = sqrt y" by simp
4.49 -  hence "sqrt y = \<bar>x\<bar>" by simp
4.50 -  thus "x = sqrt y \<or> x = - sqrt y" by auto
4.51 +  then have "sqrt (x\<^sup>2) = sqrt y"
4.52 +    by simp
4.53 +  then have "sqrt y = \<bar>x\<bar>"
4.54 +    by simp
4.55 +  then show "x = sqrt y \<or> x = - sqrt y"
4.56 +    by auto
4.57  next
4.58    assume "x = sqrt y \<or> x = - sqrt y"
4.59 -  hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
4.60 -  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y" by simp
4.61 +  then have "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2"
4.62 +    by auto
4.63 +  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y"
4.64 +    by simp
4.65  qed
4.66
4.67  lemma divide_non_zero:
4.68 @@ -59,20 +66,19 @@
4.69    assumes "x \<noteq> 0"
4.70    shows "x * y = z \<longleftrightarrow> y = z / x"
4.71  proof
4.72 -  assume "x * y = z"
4.73 -  with \<open>x \<noteq> 0\<close> show "y = z / x" by (simp add: field_simps)
4.74 -next
4.75 -  assume "y = z / x"
4.76 -  with \<open>x \<noteq> 0\<close> show "x * y = z" by simp
4.77 +  show "y = z / x" if "x * y = z"
4.78 +    using \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
4.79 +  show "x * y = z" if "y = z / x"
4.80 +    using \<open>x \<noteq> 0\<close> that by simp
4.81  qed
4.82
4.83  lemma discriminant_nonneg:
4.84    fixes a b c x :: real
4.85    assumes "a \<noteq> 0"
4.86 -  and "discrim a b c \<ge> 0"
4.87 +    and "discrim a b c \<ge> 0"
4.88    shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
4.89 -  x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.90 -  x = (-b - sqrt (discrim a b c)) / (2 * a)"
4.91 +    x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.92 +    x = (-b - sqrt (discrim a b c)) / (2 * a)"
4.93  proof -
4.94    from complete_square and plus_or_minus_sqrt and assms
4.95    have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
4.96 @@ -94,88 +100,93 @@
4.97  lemma discriminant_zero:
4.98    fixes a b c x :: real
4.99    assumes "a \<noteq> 0"
4.100 -  and "discrim a b c = 0"
4.101 +    and "discrim a b c = 0"
4.102    shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
4.103 -  using discriminant_nonneg and assms
4.104 -  by simp
4.105 +  by (simp add: discriminant_nonneg assms)
4.106
4.107  theorem discriminant_iff:
4.108    fixes a b c x :: real
4.109    assumes "a \<noteq> 0"
4.110    shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
4.111 -  discrim a b c \<ge> 0 \<and>
4.112 -  (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.113 -  x = (-b - sqrt (discrim a b c)) / (2 * a))"
4.114 +    discrim a b c \<ge> 0 \<and>
4.115 +    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.116 +     x = (-b - sqrt (discrim a b c)) / (2 * a))"
4.117  proof
4.118    assume "a * x\<^sup>2 + b * x + c = 0"
4.119 -  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)" by auto
4.120 -  hence "discrim a b c \<ge> 0" by simp
4.121 +  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
4.122 +    by auto
4.123 +  then have "discrim a b c \<ge> 0"
4.124 +    by simp
4.125    with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
4.126    have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.127 -    x = (-b - sqrt (discrim a b c)) / (2 * a)"
4.128 +      x = (-b - sqrt (discrim a b c)) / (2 * a)"
4.129      by simp
4.130    with \<open>discrim a b c \<ge> 0\<close>
4.131    show "discrim a b c \<ge> 0 \<and>
4.132      (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.133 -    x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
4.134 +     x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
4.135  next
4.136    assume "discrim a b c \<ge> 0 \<and>
4.137      (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.138 -    x = (-b - sqrt (discrim a b c)) / (2 * a))"
4.139 -  hence "discrim a b c \<ge> 0" and
4.140 +     x = (-b - sqrt (discrim a b c)) / (2 * a))"
4.141 +  then have "discrim a b c \<ge> 0" and
4.142      "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
4.143 -    x = (-b - sqrt (discrim a b c)) / (2 * a)"
4.144 +     x = (-b - sqrt (discrim a b c)) / (2 * a)"
4.145      by simp_all
4.146 -  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0" by simp
4.147 +  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0"
4.148 +    by simp
4.149  qed
4.150
4.151  lemma discriminant_nonneg_ex:
4.152    fixes a b c :: real
4.153    assumes "a \<noteq> 0"
4.154 -  and "discrim a b c \<ge> 0"
4.155 +    and "discrim a b c \<ge> 0"
4.156    shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
4.157 -  using discriminant_nonneg and assms
4.158 -  by auto
4.159 +  by (auto simp: discriminant_nonneg assms)
4.160
4.161  lemma discriminant_pos_ex:
4.162    fixes a b c :: real
4.163    assumes "a \<noteq> 0"
4.164 -  and "discrim a b c > 0"
4.165 -  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"
4.166 +    and "discrim a b c > 0"
4.167 +  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"
4.168  proof -
4.169    let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
4.170    let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
4.171 -  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0" by simp
4.172 -  hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
4.173 -  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y" by simp
4.174 -  moreover
4.175 -  from discriminant_nonneg [of a b c ?x]
4.176 -    and discriminant_nonneg [of a b c ?y]
4.177 -    and assms
4.178 -  have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
4.179 -  ultimately
4.180 -  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
4.181 +  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
4.182 +    by simp
4.183 +  then have "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)"
4.184 +    by arith
4.185 +  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y"
4.186 +    by simp
4.187 +  moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0"
4.188 +    using discriminant_nonneg [of a b c ?x]
4.189 +      and discriminant_nonneg [of a b c ?y]
4.190 +    by simp_all
4.191 +  ultimately show ?thesis
4.192 +    by blast
4.193  qed
4.194
4.195  lemma discriminant_pos_distinct:
4.196    fixes a b c x :: real
4.197 -  assumes "a \<noteq> 0" and "discrim a b c > 0"
4.198 +  assumes "a \<noteq> 0"
4.199 +    and "discrim a b c > 0"
4.200    shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
4.201  proof -
4.202    from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
4.203    obtain w and z where "w \<noteq> z"
4.204      and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
4.205      by blast
4.206 -  show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
4.207 -  proof cases
4.208 -    assume "x = w"
4.209 -    with \<open>w \<noteq> z\<close> have "x \<noteq> z" by simp
4.210 -    with \<open>a * z\<^sup>2 + b * z + c = 0\<close>
4.211 -    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
4.212 +  show "\<exists>y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
4.213 +  proof (cases "x = w")
4.214 +    case True
4.215 +    with \<open>w \<noteq> z\<close> have "x \<noteq> z"
4.216 +      by simp
4.217 +    with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
4.218 +      by auto
4.219    next
4.220 -    assume "x \<noteq> w"
4.221 -    with \<open>a * w\<^sup>2 + b * w + c = 0\<close>
4.222 -    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
4.223 +    case False
4.224 +    with \<open>a * w\<^sup>2 + b * w + c = 0\<close> show ?thesis
4.225 +      by auto
4.226    qed
4.227  qed
4.228

     5.1 --- a/src/HOL/Library/Sublist_Order.thy	Tue Jul 12 19:12:17 2016 +0200
5.2 +++ b/src/HOL/Library/Sublist_Order.thy	Tue Jul 12 20:03:18 2016 +0200
5.3 @@ -1,6 +1,7 @@
5.4  (*  Title:      HOL/Library/Sublist_Order.thy
5.5 -    Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
5.6 -                Florian Haftmann, Tobias Nipkow, TU Muenchen
5.7 +    Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
5.8 +    Author:     Florian Haftmann, , TU Muenchen
5.9 +    Author:     Tobias Nipkow, TU Muenchen
5.10  *)
5.11
5.12  section \<open>Sublist Ordering\<close>
5.13 @@ -10,9 +11,8 @@
5.14  begin
5.15
5.16  text \<open>
5.17 -  This theory defines sublist ordering on lists.
5.18 -  A list \<open>ys\<close> is a sublist of a list \<open>xs\<close>,
5.19 -  iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
5.20 +  This theory defines sublist ordering on lists. A list \<open>ys\<close> is a sublist of a
5.21 +  list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
5.22  \<close>
5.23
5.24  subsection \<open>Definitions and basic lemmas\<close>
5.25 @@ -20,11 +20,8 @@
5.26  instantiation list :: (type) ord
5.27  begin
5.28
5.29 -definition
5.30 -  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
5.31 -
5.32 -definition
5.33 -  "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
5.34 +definition "xs \<le> ys \<longleftrightarrow> sublisteq xs ys" for xs ys :: "'a list"
5.35 +definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
5.36
5.37  instance ..
5.38
5.39 @@ -32,19 +29,15 @@
5.40
5.41  instance list :: (type) order
5.42  proof
5.43 -  fix xs ys :: "'a list"
5.44 -  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def ..
5.45 -next
5.46 -  fix xs :: "'a list"
5.47 -  show "xs \<le> xs" by (simp add: less_eq_list_def)
5.48 -next
5.49 -  fix xs ys :: "'a list"
5.50 -  assume "xs <= ys" and "ys <= xs"
5.51 -  thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
5.52 -next
5.53    fix xs ys zs :: "'a list"
5.54 -  assume "xs <= ys" and "ys <= zs"
5.55 -  thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
5.56 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
5.57 +    unfolding less_list_def ..
5.58 +  show "xs \<le> xs"
5.59 +    by (simp add: less_eq_list_def)
5.60 +  show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
5.61 +    using that unfolding less_eq_list_def by (rule sublisteq_antisym)
5.62 +  show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
5.63 +    using that unfolding less_eq_list_def by (rule sublisteq_trans)
5.64  qed
5.65
5.66  lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
5.67 @@ -71,7 +64,8 @@
5.68    by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
5.69
5.70  lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
5.71 -  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
5.72 +  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le
5.73 +      self_append_conv2 less_eq_list_def)
5.74
5.75  lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
5.76    by (metis less_list_def less_eq_list_def sublisteq_append')