misc tuning and modernization;
authorwenzelm
Tue Jul 12 20:03:18 2016 +0200 (2016-07-12)
changeset 63465d7610beb98bc
parent 63464 9d4dbb7a548a
child 63466 2100fbbdc3f1
misc tuning and modernization;
src/HOL/Library/Continuum_Not_Denumerable.thy
src/HOL/Library/Prefix_Order.thy
src/HOL/Library/Preorder.thy
src/HOL/Library/Quadratic_Discriminant.thy
src/HOL/Library/Sublist_Order.thy
     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.189      by (simp add: uncountable_open_interval)
   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')