tuned proofs;
authorwenzelm
Tue Apr 29 22:50:55 2014 +0200 (2014-04-29)
changeset 567969f84219715a7
parent 56795 e8cce2bd23e5
child 56797 32963b43a538
tuned proofs;
src/HOL/Library/BigO.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Finite_Lattice.thy
src/HOL/Library/Permutation.thy
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Apr 29 21:54:26 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Tue Apr 29 22:50:55 2014 +0200
     1.3 @@ -390,7 +390,7 @@
     1.4      also have "\<dots> \<subseteq> O(g) + O(g)"
     1.5      proof -
     1.6        from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
     1.7 -      thus ?thesis by (auto del: subsetI)
     1.8 +      then show ?thesis by (auto del: subsetI)
     1.9      qed
    1.10      also have "\<dots> \<subseteq> O(g)" by simp
    1.11      finally show ?thesis .
     2.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Apr 29 21:54:26 2014 +0200
     2.2 +++ b/src/HOL/Library/ContNotDenum.thy	Tue Apr 29 22:50:55 2014 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4 -(*  Title       : HOL/ContNonDenum
     2.5 -    Author      : Benjamin Porter, Monash University, NICTA, 2005
     2.6 +(*  Title:      HOL/Library/ContNonDenum.thy
     2.7 +    Author:     Benjamin Porter, Monash University, NICTA, 2005
     2.8  *)
     2.9  
    2.10  header {* Non-denumerability of the Continuum. *}
    2.11 @@ -15,7 +15,7 @@
    2.12  system.
    2.13  
    2.14  {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    2.15 -words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    2.16 +words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
    2.17  surjective.
    2.18  
    2.19  {\em Outline:} An elegant informal proof of this result uses Cantor's
    2.20 @@ -25,41 +25,50 @@
    2.21  completeness of the Real numbers and is the foundation for our
    2.22  argument. Informally it states that an intersection of countable
    2.23  closed intervals (where each successive interval is a subset of the
    2.24 -last) is non-empty. We then assume a surjective function f:@{text
    2.25 -"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    2.26 +last) is non-empty. We then assume a surjective function @{text
    2.27 +"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
    2.28  by generating a sequence of closed intervals then using the NIP. *}
    2.29  
    2.30 +
    2.31  subsection {* Closed Intervals *}
    2.32  
    2.33  subsection {* Nested Interval Property *}
    2.34  
    2.35  theorem NIP:
    2.36 -  fixes f::"nat \<Rightarrow> real set"
    2.37 +  fixes f :: "nat \<Rightarrow> real set"
    2.38    assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    2.39 -  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    2.40 +    and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    2.41    shows "(\<Inter>n. f n) \<noteq> {}"
    2.42  proof -
    2.43    let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
    2.44 -  { fix n 
    2.45 +  {
    2.46 +    fix n
    2.47      from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
    2.48        by auto
    2.49      then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
    2.50 -      by auto }
    2.51 +      by auto
    2.52 +  }
    2.53    note f_eq = this
    2.54 -  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
    2.55 -      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
    2.56 +  {
    2.57 +    fix n m :: nat
    2.58 +    assume "n \<le> m"
    2.59 +    then have "f m \<subseteq> f n"
    2.60 +      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
    2.61 +  }
    2.62    note subset' = this
    2.63  
    2.64    have "compact (f 0)"
    2.65      by (subst f_eq) (rule compact_Icc)
    2.66    then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
    2.67    proof (rule compact_imp_fip_image)
    2.68 -    fix I :: "nat set" assume I: "finite I"
    2.69 +    fix I :: "nat set"
    2.70 +    assume I: "finite I"
    2.71      have "{} \<subset> f (Max (insert 0 I))"
    2.72        using f_eq[of "Max (insert 0 I)"] by auto
    2.73      also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
    2.74      proof (rule INF_greatest)
    2.75 -      fix i assume "i \<in> insert 0 I"
    2.76 +      fix i
    2.77 +      assume "i \<in> insert 0 I"
    2.78        with I show "f (Max (insert 0 I)) \<subseteq> f i"
    2.79          by (intro subset') auto
    2.80      qed
    2.81 @@ -70,6 +79,7 @@
    2.82      by auto
    2.83  qed
    2.84  
    2.85 +
    2.86  subsection {* Generating the intervals *}
    2.87  
    2.88  subsubsection {* Existence of non-singleton closed intervals *}
    2.89 @@ -80,7 +90,7 @@
    2.90  non-singleton itself. *}
    2.91  
    2.92  lemma closed_subset_ex:
    2.93 -  fixes c::real
    2.94 +  fixes c :: real
    2.95    assumes "a < b"
    2.96    shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
    2.97  proof (cases "c < b")
    2.98 @@ -90,39 +100,45 @@
    2.99      case True
   2.100      with `a < b` `c < b` have "c \<notin> {a..b}"
   2.101        by auto
   2.102 -    with `a < b` show ?thesis by auto
   2.103 +    with `a < b` show ?thesis
   2.104 +      by auto
   2.105    next
   2.106      case False
   2.107      then have "a \<le> c" by simp
   2.108      def ka \<equiv> "(c + b)/2"
   2.109 -
   2.110 -    from ka_def `c < b` have kalb: "ka < b" by auto
   2.111 -    moreover from ka_def `c < b` have kagc: "ka > c" by simp
   2.112 -    ultimately have "c\<notin>{ka..b}" by auto
   2.113 -    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
   2.114 -    hence "{ka..b} \<subseteq> {a..b}" by auto
   2.115 -    ultimately have
   2.116 -      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   2.117 -      using kalb by auto
   2.118 +    from ka_def `c < b` have "ka < b"
   2.119 +      by auto
   2.120 +    moreover from ka_def `c < b` have "ka > c"
   2.121 +      by simp
   2.122 +    ultimately have "c \<notin> {ka..b}"
   2.123 +      by auto
   2.124 +    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
   2.125 +      by simp
   2.126 +    then have "{ka..b} \<subseteq> {a..b}"
   2.127 +      by auto
   2.128 +    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   2.129 +      using `ka < b` by auto
   2.130      then show ?thesis
   2.131        by auto
   2.132    qed
   2.133  next
   2.134    case False
   2.135    then have "c \<ge> b" by simp
   2.136 -
   2.137    def kb \<equiv> "(a + b)/2"
   2.138    with `a < b` have "kb < b" by auto
   2.139 -  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
   2.140 +  with kb_def `c \<ge> b` have "a < kb" "kb < c"
   2.141 +    by auto
   2.142    from `kb < c` have c: "c \<notin> {a..kb}"
   2.143      by auto
   2.144    with `kb < b` have "{a..kb} \<subseteq> {a..b}"
   2.145      by auto
   2.146    with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
   2.147      by simp
   2.148 -  then show ?thesis by auto
   2.149 +  then show ?thesis
   2.150 +    by auto
   2.151  qed
   2.152  
   2.153 +
   2.154  subsection {* newInt: Interval generation *}
   2.155  
   2.156  text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   2.157 @@ -130,17 +146,19 @@
   2.158  does not contain @{text "f (Suc n)"}. With the base case defined such
   2.159  that @{text "(f 0)\<notin>newInt 0 f"}. *}
   2.160  
   2.161 +
   2.162  subsubsection {* Definition *}
   2.163  
   2.164 -primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   2.165 +primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
   2.166 +where
   2.167    "newInt 0 f = {f 0 + 1..f 0 + 2}"
   2.168 -  | "newInt (Suc n) f =
   2.169 -      (SOME e. (\<exists>e1 e2.
   2.170 -       e1 < e2 \<and>
   2.171 -       e = {e1..e2} \<and>
   2.172 -       e \<subseteq> newInt n f \<and>
   2.173 -       f (Suc n) \<notin> e)
   2.174 -      )"
   2.175 +| "newInt (Suc n) f =
   2.176 +    (SOME e.
   2.177 +      (\<exists>e1 e2.
   2.178 +         e1 < e2 \<and>
   2.179 +         e = {e1..e2} \<and>
   2.180 +         e \<subseteq> newInt n f \<and>
   2.181 +         f (Suc n) \<notin> e))"
   2.182  
   2.183  
   2.184  subsubsection {* Properties *}
   2.185 @@ -150,81 +168,76 @@
   2.186  
   2.187  lemma newInt_ex:
   2.188    "\<exists>a b. a < b \<and>
   2.189 -   newInt (Suc n) f = {a..b} \<and>
   2.190 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.191 -   f (Suc n) \<notin> newInt (Suc n) f"
   2.192 +    newInt (Suc n) f = {a..b} \<and>
   2.193 +    newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.194 +    f (Suc n) \<notin> newInt (Suc n) f"
   2.195  proof (induct n)
   2.196    case 0
   2.197 -
   2.198    let ?e = "SOME e. \<exists>e1 e2.
   2.199 -   e1 < e2 \<and>
   2.200 -   e = {e1..e2} \<and>
   2.201 -   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   2.202 -   f (Suc 0) \<notin> e"
   2.203 +    e1 < e2 \<and>
   2.204 +    e = {e1..e2} \<and>
   2.205 +    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   2.206 +    f (Suc 0) \<notin> e"
   2.207  
   2.208    have "newInt (Suc 0) f = ?e" by auto
   2.209    moreover
   2.210    have "f 0 + 1 < f 0 + 2" by simp
   2.211 -  with closed_subset_ex have
   2.212 -    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   2.213 -     f (Suc 0) \<notin> {ka..kb}" .
   2.214 -  hence
   2.215 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   2.216 -     e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
   2.217 -  hence
   2.218 -    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   2.219 +  with closed_subset_ex
   2.220 +  have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
   2.221 +  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e"
   2.222 +    by simp
   2.223 +  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   2.224      by (rule someI_ex)
   2.225    ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   2.226 -   newInt (Suc 0) f = {e1..e2} \<and>
   2.227 -   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   2.228 -   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   2.229 -  thus
   2.230 -    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   2.231 -     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   2.232 +      newInt (Suc 0) f = {e1..e2} \<and>
   2.233 +      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   2.234 +      f (Suc 0) \<notin> newInt (Suc 0) f"
   2.235 +    by simp
   2.236 +  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   2.237 +      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   2.238      by simp
   2.239  next
   2.240    case (Suc n)
   2.241 -  hence "\<exists>a b.
   2.242 -   a < b \<and>
   2.243 -   newInt (Suc n) f = {a..b} \<and>
   2.244 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.245 -   f (Suc n) \<notin> newInt (Suc n) f" by simp
   2.246 +  then have "\<exists>a b.
   2.247 +      a < b \<and>
   2.248 +      newInt (Suc n) f = {a..b} \<and>
   2.249 +      newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.250 +      f (Suc n) \<notin> newInt (Suc n) f"
   2.251 +    by simp
   2.252    then obtain a and b where ab: "a < b \<and>
   2.253 -   newInt (Suc n) f = {a..b} \<and>
   2.254 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.255 -   f (Suc n) \<notin> newInt (Suc n) f" by auto
   2.256 -  hence cab: "{a..b} = newInt (Suc n) f" by simp
   2.257 +      newInt (Suc n) f = {a..b} \<and>
   2.258 +      newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.259 +      f (Suc n) \<notin> newInt (Suc n) f"
   2.260 +    by auto
   2.261 +  then have cab: "{a..b} = newInt (Suc n) f"
   2.262 +    by simp
   2.263  
   2.264    let ?e = "SOME e. \<exists>e1 e2.
   2.265 -    e1 < e2 \<and>
   2.266 -    e = {e1..e2} \<and>
   2.267 -    e \<subseteq> {a..b} \<and>
   2.268 -    f (Suc (Suc n)) \<notin> e"
   2.269 -  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   2.270 +      e1 < e2 \<and>
   2.271 +      e = {e1..e2} \<and>
   2.272 +      e \<subseteq> {a..b} \<and>
   2.273 +      f (Suc (Suc n)) \<notin> e"
   2.274 +  from cab have ni: "newInt (Suc (Suc n)) f = ?e"
   2.275 +    by auto
   2.276  
   2.277    from ab have "a < b" by simp
   2.278 -  with closed_subset_ex have
   2.279 -    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   2.280 -     f (Suc (Suc n)) \<notin> {ka..kb}" .
   2.281 -  hence
   2.282 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   2.283 -     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   2.284 +  with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   2.285 +    f (Suc (Suc n)) \<notin> {ka..kb}" .
   2.286 +  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   2.287 +      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   2.288 +    by simp
   2.289 +  then have "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
   2.290      by simp
   2.291 -  hence
   2.292 -    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   2.293 -     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
   2.294 -  hence
   2.295 -    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
   2.296 -     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   2.297 -  with ab ni show
   2.298 -    "\<exists>ka kb. ka < kb \<and>
   2.299 -     newInt (Suc (Suc n)) f = {ka..kb} \<and>
   2.300 -     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   2.301 -     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   2.302 +  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
   2.303 +    by (rule someI_ex)
   2.304 +  with ab ni show "\<exists>ka kb. ka < kb \<and>
   2.305 +      newInt (Suc (Suc n)) f = {ka..kb} \<and>
   2.306 +      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   2.307 +      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
   2.308 +    by auto
   2.309  qed
   2.310  
   2.311 -lemma newInt_subset:
   2.312 -  "newInt (Suc n) f \<subseteq> newInt n f"
   2.313 +lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
   2.314    using newInt_ex by auto
   2.315  
   2.316  
   2.317 @@ -232,34 +245,27 @@
   2.318  of f is in the intersection of all closed intervals generated by
   2.319  newInt. *}
   2.320  
   2.321 -lemma newInt_inter:
   2.322 -  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   2.323 +lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   2.324  proof
   2.325 -  fix n::nat
   2.326 -  {
   2.327 -    assume n0: "n = 0"
   2.328 -    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
   2.329 -    ultimately have "f n \<notin> newInt n f" by simp
   2.330 -  }
   2.331 -  moreover
   2.332 -  {
   2.333 -    assume "\<not> n = 0"
   2.334 -    hence "n > 0" by simp
   2.335 -    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   2.336 -
   2.337 -    from newInt_ex have
   2.338 -      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   2.339 -       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   2.340 -    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   2.341 -    with ndef have "f n \<notin> newInt n f" by simp
   2.342 -  }
   2.343 -  ultimately have "f n \<notin> newInt n f" by (rule case_split)
   2.344 -  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   2.345 +  fix n :: nat
   2.346 +  have "f n \<notin> newInt n f"
   2.347 +  proof (cases n)
   2.348 +    case 0
   2.349 +    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
   2.350 +      by simp
   2.351 +    ultimately show ?thesis by simp
   2.352 +  next
   2.353 +    case (Suc m)
   2.354 +    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   2.355 +      newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   2.356 +    then have "f (Suc m) \<notin> newInt (Suc m) f"
   2.357 +      by auto
   2.358 +    with Suc show ?thesis by simp
   2.359 +  qed
   2.360 +  then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
   2.361  qed
   2.362  
   2.363 -
   2.364 -lemma newInt_notempty:
   2.365 -  "(\<Inter>n. newInt n f) \<noteq> {}"
   2.366 +lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
   2.367  proof -
   2.368    let ?g = "\<lambda>n. newInt n f"
   2.369    have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   2.370 @@ -269,30 +275,26 @@
   2.371    qed
   2.372    moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   2.373    proof
   2.374 -    fix n::nat
   2.375 -    {
   2.376 -      assume "n = 0"
   2.377 -      then have
   2.378 -        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   2.379 +    fix n :: nat
   2.380 +    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   2.381 +    proof (cases n)
   2.382 +      case 0
   2.383 +      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   2.384          by simp
   2.385 -      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   2.386 -    }
   2.387 -    moreover
   2.388 -    {
   2.389 -      assume "\<not> n = 0"
   2.390 -      then have "n > 0" by simp
   2.391 -      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   2.392 -
   2.393 -      have
   2.394 -        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   2.395 +      then show ?thesis
   2.396 +        by blast
   2.397 +    next
   2.398 +      case (Suc m)
   2.399 +      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   2.400          (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   2.401          by (rule newInt_ex)
   2.402 -      then obtain a and b where
   2.403 -        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
   2.404 -      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
   2.405 -      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   2.406 -    }
   2.407 -    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
   2.408 +      then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
   2.409 +        by auto
   2.410 +      with Suc have "?g n = {a..b} \<and> a \<le> b"
   2.411 +        by auto
   2.412 +      then show ?thesis
   2.413 +        by blast
   2.414 +    qed
   2.415    qed
   2.416    ultimately show ?thesis by (rule NIP)
   2.417  qed
   2.418 @@ -300,17 +302,22 @@
   2.419  
   2.420  subsection {* Final Theorem *}
   2.421  
   2.422 -theorem real_non_denum:
   2.423 -  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   2.424 -proof -- "by contradiction"
   2.425 -  assume "\<exists>f::nat\<Rightarrow>real. surj f"
   2.426 -  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
   2.427 -  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   2.428 -  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   2.429 -  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   2.430 -  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   2.431 -  moreover from rangeF have "x \<in> range f" by simp
   2.432 -  ultimately show False by blast
   2.433 +theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
   2.434 +proof
   2.435 +  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
   2.436 +  then obtain f :: "nat \<Rightarrow> real" where "surj f"
   2.437 +    by auto
   2.438 +  txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
   2.439 +  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
   2.440 +    using newInt_notempty by blast
   2.441 +  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   2.442 +    by (rule newInt_inter)
   2.443 +  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
   2.444 +    by blast
   2.445 +  moreover from `surj f` have "x \<in> range f"
   2.446 +    by simp
   2.447 +  ultimately show False
   2.448 +    by blast
   2.449  qed
   2.450  
   2.451  end
     3.1 --- a/src/HOL/Library/Convex.thy	Tue Apr 29 21:54:26 2014 +0200
     3.2 +++ b/src/HOL/Library/Convex.thy	Tue Apr 29 22:50:55 2014 +0200
     3.3 @@ -29,11 +29,18 @@
     3.4    (is "_ \<longleftrightarrow> ?alt")
     3.5  proof
     3.6    assume alt[rule_format]: ?alt
     3.7 -  { fix x y and u v :: real assume mem: "x \<in> s" "y \<in> s"
     3.8 +  {
     3.9 +    fix x y and u v :: real
    3.10 +    assume mem: "x \<in> s" "y \<in> s"
    3.11      assume "0 \<le> u" "0 \<le> v"
    3.12 -    moreover assume "u + v = 1" then have "u = 1 - v" by auto
    3.13 -    ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s" using alt[OF mem] by auto }
    3.14 -  then show "convex s" unfolding convex_def by auto
    3.15 +    moreover
    3.16 +    assume "u + v = 1"
    3.17 +    then have "u = 1 - v" by auto
    3.18 +    ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s"
    3.19 +      using alt[OF mem] by auto
    3.20 +  }
    3.21 +  then show "convex s"
    3.22 +    unfolding convex_def by auto
    3.23  qed (auto simp: convex_def)
    3.24  
    3.25  lemma mem_convex:
    3.26 @@ -50,7 +57,7 @@
    3.27  lemma convex_UNIV[intro]: "convex UNIV"
    3.28    unfolding convex_def by auto
    3.29  
    3.30 -lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"
    3.31 +lemma convex_Inter: "(\<forall>s\<in>f. convex s) \<Longrightarrow> convex(\<Inter> f)"
    3.32    unfolding convex_def by auto
    3.33  
    3.34  lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
    3.35 @@ -68,13 +75,16 @@
    3.36  
    3.37  lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
    3.38  proof -
    3.39 -  have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto
    3.40 -  show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
    3.41 +  have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}"
    3.42 +    by auto
    3.43 +  show ?thesis
    3.44 +    unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
    3.45  qed
    3.46  
    3.47  lemma convex_hyperplane: "convex {x. inner a x = b}"
    3.48  proof -
    3.49 -  have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto
    3.50 +  have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}"
    3.51 +    by auto
    3.52    show ?thesis using convex_halfspace_le convex_halfspace_ge
    3.53      by (auto intro!: convex_Int simp: *)
    3.54  qed
    3.55 @@ -115,8 +125,11 @@
    3.56  
    3.57  lemma convex_setsum:
    3.58    fixes C :: "'a::real_vector set"
    3.59 -  assumes "finite s" and "convex C" and "(\<Sum> i \<in> s. a i) = 1"
    3.60 -  assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0" and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
    3.61 +  assumes "finite s"
    3.62 +    and "convex C"
    3.63 +    and "(\<Sum> i \<in> s. a i) = 1"
    3.64 +  assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0"
    3.65 +    and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
    3.66    shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C"
    3.67    using assms(1,3,4,5)
    3.68  proof (induct arbitrary: a set: finite)
    3.69 @@ -124,18 +137,27 @@
    3.70    then show ?case by simp
    3.71  next
    3.72    case (insert i s) note IH = this(3)
    3.73 -  have "a i + setsum a s = 1" and "0 \<le> a i" and "\<forall>j\<in>s. 0 \<le> a j" and "y i \<in> C" and "\<forall>j\<in>s. y j \<in> C"
    3.74 +  have "a i + setsum a s = 1"
    3.75 +    and "0 \<le> a i"
    3.76 +    and "\<forall>j\<in>s. 0 \<le> a j"
    3.77 +    and "y i \<in> C"
    3.78 +    and "\<forall>j\<in>s. y j \<in> C"
    3.79      using insert.hyps(1,2) insert.prems by simp_all
    3.80 -  then have "0 \<le> setsum a s" by (simp add: setsum_nonneg)
    3.81 +  then have "0 \<le> setsum a s"
    3.82 +    by (simp add: setsum_nonneg)
    3.83    have "a i *\<^sub>R y i + (\<Sum>j\<in>s. a j *\<^sub>R y j) \<in> C"
    3.84    proof (cases)
    3.85      assume z: "setsum a s = 0"
    3.86 -    with `a i + setsum a s = 1` have "a i = 1" by simp
    3.87 -    from setsum_nonneg_0 [OF `finite s` _ z] `\<forall>j\<in>s. 0 \<le> a j` have "\<forall>j\<in>s. a j = 0" by simp
    3.88 -    show ?thesis using `a i = 1` and `\<forall>j\<in>s. a j = 0` and `y i \<in> C` by simp
    3.89 +    with `a i + setsum a s = 1` have "a i = 1"
    3.90 +      by simp
    3.91 +    from setsum_nonneg_0 [OF `finite s` _ z] `\<forall>j\<in>s. 0 \<le> a j` have "\<forall>j\<in>s. a j = 0"
    3.92 +      by simp
    3.93 +    show ?thesis using `a i = 1` and `\<forall>j\<in>s. a j = 0` and `y i \<in> C`
    3.94 +      by simp
    3.95    next
    3.96      assume nz: "setsum a s \<noteq> 0"
    3.97 -    with `0 \<le> setsum a s` have "0 < setsum a s" by simp
    3.98 +    with `0 \<le> setsum a s` have "0 < setsum a s"
    3.99 +      by simp
   3.100      then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
   3.101        using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
   3.102        by (simp add: IH setsum_divide_distrib [symmetric])
   3.103 @@ -143,9 +165,11 @@
   3.104        and `0 \<le> setsum a s` and `a i + setsum a s = 1`
   3.105      have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
   3.106        by (rule convexD)
   3.107 -    then show ?thesis by (simp add: scaleR_setsum_right nz)
   3.108 +    then show ?thesis
   3.109 +      by (simp add: scaleR_setsum_right nz)
   3.110    qed
   3.111 -  then show ?case using `finite s` and `i \<notin> s` by simp
   3.112 +  then show ?case using `finite s` and `i \<notin> s`
   3.113 +    by simp
   3.114  qed
   3.115  
   3.116  lemma convex:
   3.117 @@ -159,18 +183,22 @@
   3.118      "\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s"
   3.119      "setsum u {1..k} = 1"
   3.120    from this convex_setsum[of "{1 .. k}" s]
   3.121 -  show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s" by auto
   3.122 +  show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s"
   3.123 +    by auto
   3.124  next
   3.125    assume asm: "\<forall>k u x. (\<forall> i :: nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1
   3.126      \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s"
   3.127 -  { fix \<mu> :: real
   3.128 +  {
   3.129 +    fix \<mu> :: real
   3.130      fix x y :: 'a
   3.131      assume xy: "x \<in> s" "y \<in> s"
   3.132      assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1"
   3.133      let ?u = "\<lambda>i. if (i :: nat) = 1 then \<mu> else 1 - \<mu>"
   3.134      let ?x = "\<lambda>i. if (i :: nat) = 1 then x else y"
   3.135 -    have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}" by auto
   3.136 -    then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1" by simp
   3.137 +    have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}"
   3.138 +      by auto
   3.139 +    then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1"
   3.140 +      by simp
   3.141      then have "setsum ?u {1 .. 2} = 1"
   3.142        using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
   3.143        by auto
   3.144 @@ -179,10 +207,13 @@
   3.145      have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
   3.146        using setsum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
   3.147      from setsum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
   3.148 -    have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y" by auto
   3.149 -    then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s" using s by (auto simp:add_commute)
   3.150 +    have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
   3.151 +      by auto
   3.152 +    then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"
   3.153 +      using s by (auto simp:add_commute)
   3.154    }
   3.155 -  then show "convex s" unfolding convex_alt by auto
   3.156 +  then show "convex s"
   3.157 +    unfolding convex_alt by auto
   3.158  qed
   3.159  
   3.160  
   3.161 @@ -193,42 +224,48 @@
   3.162  proof safe
   3.163    fix t
   3.164    fix u :: "'a \<Rightarrow> real"
   3.165 -  assume "convex s" "finite t"
   3.166 -    "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
   3.167 +  assume "convex s"
   3.168 +    and "finite t"
   3.169 +    and "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
   3.170    then show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
   3.171      using convex_setsum[of t s u "\<lambda> x. x"] by auto
   3.172  next
   3.173 -  assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x)
   3.174 -    \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
   3.175 +  assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and>
   3.176 +    setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
   3.177    show "convex s"
   3.178      unfolding convex_alt
   3.179    proof safe
   3.180      fix x y
   3.181      fix \<mu> :: real
   3.182      assume asm: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1"
   3.183 -    { assume "x \<noteq> y"
   3.184 +    {
   3.185 +      assume "x \<noteq> y"
   3.186        then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
   3.187          using asm0[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1 - \<mu> else \<mu>"]
   3.188 -          asm by auto }
   3.189 +          asm by auto
   3.190 +    }
   3.191      moreover
   3.192 -    { assume "x = y"
   3.193 +    {
   3.194 +      assume "x = y"
   3.195        then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
   3.196          using asm0[rule_format, of "{x, y}" "\<lambda> z. 1"]
   3.197 -          asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) }
   3.198 -    ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" by blast
   3.199 +          asm by (auto simp: field_simps real_vector.scale_left_diff_distrib)
   3.200 +    }
   3.201 +    ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
   3.202 +      by blast
   3.203    qed
   3.204  qed
   3.205  
   3.206  lemma convex_finite:
   3.207    assumes "finite s"
   3.208 -  shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
   3.209 -                      \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
   3.210 +  shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
   3.211    unfolding convex_explicit
   3.212  proof safe
   3.213    fix t u
   3.214    assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
   3.215      and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
   3.216 -  have *: "s \<inter> t = t" using as(2) by auto
   3.217 +  have *: "s \<inter> t = t"
   3.218 +    using as(2) by auto
   3.219    have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
   3.220      by simp
   3.221    show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
   3.222 @@ -236,6 +273,7 @@
   3.223     by (auto simp: assms setsum_cases if_distrib if_distrib_arg)
   3.224  qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
   3.225  
   3.226 +
   3.227  subsection {* Functions that are convex on a set *}
   3.228  
   3.229  definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
   3.230 @@ -246,11 +284,13 @@
   3.231    unfolding convex_on_def by auto
   3.232  
   3.233  lemma convex_on_add [intro]:
   3.234 -  assumes "convex_on s f" "convex_on s g"
   3.235 +  assumes "convex_on s f"
   3.236 +    and "convex_on s g"
   3.237    shows "convex_on s (\<lambda>x. f x + g x)"
   3.238  proof -
   3.239 -  { fix x y
   3.240 -    assume "x\<in>s" "y\<in>s"
   3.241 +  {
   3.242 +    fix x y
   3.243 +    assume "x \<in> s" "y \<in> s"
   3.244      moreover
   3.245      fix u v :: real
   3.246      assume "0 \<le> u" "0 \<le> v" "u + v = 1"
   3.247 @@ -260,13 +300,16 @@
   3.248      then have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)"
   3.249        by (simp add: field_simps)
   3.250    }
   3.251 -  then show ?thesis unfolding convex_on_def by auto
   3.252 +  then show ?thesis
   3.253 +    unfolding convex_on_def by auto
   3.254  qed
   3.255  
   3.256  lemma convex_on_cmul [intro]:
   3.257 -  assumes "0 \<le> (c::real)" "convex_on s f"
   3.258 +  fixes c :: real
   3.259 +  assumes "0 \<le> c"
   3.260 +    and "convex_on s f"
   3.261    shows "convex_on s (\<lambda>x. c * f x)"
   3.262 -proof-
   3.263 +proof -
   3.264    have *: "\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)"
   3.265      by (simp add: field_simps)
   3.266    show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)]
   3.267 @@ -274,13 +317,19 @@
   3.268  qed
   3.269  
   3.270  lemma convex_lower:
   3.271 -  assumes "convex_on s f"  "x\<in>s"  "y \<in> s"  "0 \<le> u"  "0 \<le> v"  "u + v = 1"
   3.272 +  assumes "convex_on s f"
   3.273 +    and "x \<in> s"
   3.274 +    and "y \<in> s"
   3.275 +    and "0 \<le> u"
   3.276 +    and "0 \<le> v"
   3.277 +    and "u + v = 1"
   3.278    shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"
   3.279 -proof-
   3.280 +proof -
   3.281    let ?m = "max (f x) (f y)"
   3.282    have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
   3.283      using assms(4,5) by (auto simp add: mult_left_mono add_mono)
   3.284 -  also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[symmetric] by auto
   3.285 +  also have "\<dots> = max (f x) (f y)"
   3.286 +    using assms(6) unfolding distrib[symmetric] by auto
   3.287    finally show ?thesis
   3.288      using assms unfolding convex_on_def by fastforce
   3.289  qed
   3.290 @@ -290,11 +339,13 @@
   3.291    shows "convex_on s (\<lambda>x. dist a x)"
   3.292  proof (auto simp add: convex_on_def dist_norm)
   3.293    fix x y
   3.294 -  assume "x\<in>s" "y\<in>s"
   3.295 +  assume "x \<in> s" "y \<in> s"
   3.296    fix u v :: real
   3.297 -  assume "0 \<le> u" "0 \<le> v" "u + v = 1"
   3.298 +  assume "0 \<le> u"
   3.299 +  assume "0 \<le> v"
   3.300 +  assume "u + v = 1"
   3.301    have "a = u *\<^sub>R a + v *\<^sub>R a"
   3.302 -    unfolding scaleR_left_distrib[symmetric] and `u+v=1` by simp
   3.303 +    unfolding scaleR_left_distrib[symmetric] and `u + v = 1` by simp
   3.304    then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
   3.305      by (auto simp add: algebra_simps)
   3.306    show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
   3.307 @@ -306,7 +357,9 @@
   3.308  subsection {* Arithmetic operations on sets preserve convexity. *}
   3.309  
   3.310  lemma convex_linear_image:
   3.311 -  assumes "linear f" and "convex s" shows "convex (f ` s)"
   3.312 +  assumes "linear f"
   3.313 +    and "convex s"
   3.314 +  shows "convex (f ` s)"
   3.315  proof -
   3.316    interpret f: linear f by fact
   3.317    from `convex s` show "convex (f ` s)"
   3.318 @@ -314,7 +367,9 @@
   3.319  qed
   3.320  
   3.321  lemma convex_linear_vimage:
   3.322 -  assumes "linear f" and "convex s" shows "convex (f -` s)"
   3.323 +  assumes "linear f"
   3.324 +    and "convex s"
   3.325 +  shows "convex (f -` s)"
   3.326  proof -
   3.327    interpret f: linear f by fact
   3.328    from `convex s` show "convex (f -` s)"
   3.329 @@ -322,21 +377,28 @@
   3.330  qed
   3.331  
   3.332  lemma convex_scaling:
   3.333 -  assumes "convex s" shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
   3.334 +  assumes "convex s"
   3.335 +  shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
   3.336  proof -
   3.337 -  have "linear (\<lambda>x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right)
   3.338 -  then show ?thesis using `convex s` by (rule convex_linear_image)
   3.339 +  have "linear (\<lambda>x. c *\<^sub>R x)"
   3.340 +    by (simp add: linearI scaleR_add_right)
   3.341 +  then show ?thesis
   3.342 +    using `convex s` by (rule convex_linear_image)
   3.343  qed
   3.344  
   3.345  lemma convex_negations:
   3.346 -  assumes "convex s" shows "convex ((\<lambda>x. - x) ` s)"
   3.347 +  assumes "convex s"
   3.348 +  shows "convex ((\<lambda>x. - x) ` s)"
   3.349  proof -
   3.350 -  have "linear (\<lambda>x. - x)" by (simp add: linearI)
   3.351 -  then show ?thesis using `convex s` by (rule convex_linear_image)
   3.352 +  have "linear (\<lambda>x. - x)"
   3.353 +    by (simp add: linearI)
   3.354 +  then show ?thesis
   3.355 +    using `convex s` by (rule convex_linear_image)
   3.356  qed
   3.357  
   3.358  lemma convex_sums:
   3.359 -  assumes "convex s" and "convex t"
   3.360 +  assumes "convex s"
   3.361 +    and "convex t"
   3.362    shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
   3.363  proof -
   3.364    have "linear (\<lambda>(x, y). x + y)"
   3.365 @@ -362,7 +424,8 @@
   3.366    assumes "convex s"
   3.367    shows "convex ((\<lambda>x. a + x) ` s)"
   3.368  proof -
   3.369 -  have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
   3.370 +  have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s"
   3.371 +    by auto
   3.372    then show ?thesis
   3.373      using convex_sums[OF convex_singleton[of a] assms] by auto
   3.374  qed
   3.375 @@ -371,7 +434,8 @@
   3.376    assumes "convex s"
   3.377    shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
   3.378  proof -
   3.379 -  have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
   3.380 +  have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s"
   3.381 +    by auto
   3.382    then show ?thesis
   3.383      using convex_translation[OF convex_scaling[OF assms], of a c] by auto
   3.384  qed
   3.385 @@ -381,18 +445,25 @@
   3.386  proof safe
   3.387    fix y x \<mu> :: real
   3.388    assume asms: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
   3.389 -  { assume "\<mu> = 0"
   3.390 +  {
   3.391 +    assume "\<mu> = 0"
   3.392      then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y" by simp
   3.393 -    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
   3.394 +    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp
   3.395 +  }
   3.396    moreover
   3.397 -  { assume "\<mu> = 1"
   3.398 -    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
   3.399 +  {
   3.400 +    assume "\<mu> = 1"
   3.401 +    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp
   3.402 +  }
   3.403    moreover
   3.404 -  { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
   3.405 +  {
   3.406 +    assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
   3.407      then have "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
   3.408      then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
   3.409 -      by (auto simp add: add_pos_pos) }
   3.410 -  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
   3.411 +      by (auto simp add: add_pos_pos)
   3.412 +  }
   3.413 +  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
   3.414 +    using assms by fastforce
   3.415  qed
   3.416  
   3.417  lemma convex_on_setsum:
   3.418 @@ -415,25 +486,32 @@
   3.419    case (insert i s) note asms = this
   3.420    then have "convex_on C f" by simp
   3.421    from this[unfolded convex_on_def, rule_format]
   3.422 -  have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1
   3.423 -      \<Longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   3.424 +  have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1 \<Longrightarrow>
   3.425 +      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   3.426      by simp
   3.427 -  { assume "a i = 1"
   3.428 +  {
   3.429 +    assume "a i = 1"
   3.430      then have "(\<Sum> j \<in> s. a j) = 0"
   3.431        using asms by auto
   3.432      then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
   3.433        using setsum_nonneg_0[where 'b=real] asms by fastforce
   3.434 -    then have ?case using asms by auto }
   3.435 +    then have ?case using asms by auto
   3.436 +  }
   3.437    moreover
   3.438 -  { assume asm: "a i \<noteq> 1"
   3.439 +  {
   3.440 +    assume asm: "a i \<noteq> 1"
   3.441      from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
   3.442      have fis: "finite (insert i s)" using asms by auto
   3.443      then have ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp
   3.444      then have "a i < 1" using asm by auto
   3.445      then have i0: "1 - a i > 0" by auto
   3.446      let ?a = "\<lambda>j. a j / (1 - a i)"
   3.447 -    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
   3.448 -        by fastforce }
   3.449 +    {
   3.450 +      fix j
   3.451 +      assume "j \<in> s"
   3.452 +      with i0 asms have "?a j \<ge> 0"
   3.453 +        by fastforce
   3.454 +    }
   3.455      note a_nonneg = this
   3.456      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
   3.457      then have "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
   3.458 @@ -466,51 +544,66 @@
   3.459      also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
   3.460      also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
   3.461      finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
   3.462 -      by simp }
   3.463 +      by simp
   3.464 +  }
   3.465    ultimately show ?case by auto
   3.466  qed
   3.467  
   3.468  lemma convex_on_alt:
   3.469    fixes C :: "'a::real_vector set"
   3.470    assumes "convex C"
   3.471 -  shows "convex_on C f =
   3.472 -  (\<forall> x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1
   3.473 -      \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
   3.474 +  shows "convex_on C f \<longleftrightarrow>
   3.475 +    (\<forall>x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
   3.476 +      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
   3.477  proof safe
   3.478    fix x y
   3.479    fix \<mu> :: real
   3.480    assume asms: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1"
   3.481    from this[unfolded convex_on_def, rule_format]
   3.482 -  have "\<And>u v. \<lbrakk>0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" by auto
   3.483 +  have "\<And>u v. 0 \<le> u \<Longrightarrow> 0 \<le> v \<Longrightarrow> u + v = 1 \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
   3.484 +    by auto
   3.485    from this[of "\<mu>" "1 - \<mu>", simplified] asms
   3.486 -  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y" by auto
   3.487 +  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   3.488 +    by auto
   3.489  next
   3.490 -  assume asm: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   3.491 -  { fix x y
   3.492 +  assume asm: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow>
   3.493 +    f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   3.494 +  {
   3.495 +    fix x y
   3.496      fix u v :: real
   3.497      assume lasm: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
   3.498      then have[simp]: "1 - u = v" by auto
   3.499      from asm[rule_format, of x y u]
   3.500 -    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using lasm by auto
   3.501 +    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
   3.502 +      using lasm by auto
   3.503    }
   3.504 -  then show "convex_on C f" unfolding convex_on_def by auto
   3.505 +  then show "convex_on C f"
   3.506 +    unfolding convex_on_def by auto
   3.507  qed
   3.508  
   3.509  lemma convex_on_diff:
   3.510    fixes f :: "real \<Rightarrow> real"
   3.511 -  assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y"
   3.512 +  assumes f: "convex_on I f"
   3.513 +    and I: "x \<in> I" "y \<in> I"
   3.514 +    and t: "x < t" "t < y"
   3.515    shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
   3.516 -    "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
   3.517 +    and "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
   3.518  proof -
   3.519    def a \<equiv> "(t - y) / (x - y)"
   3.520 -  with t have "0 \<le> a" "0 \<le> 1 - a" by (auto simp: field_simps)
   3.521 +  with t have "0 \<le> a" "0 \<le> 1 - a"
   3.522 +    by (auto simp: field_simps)
   3.523    with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
   3.524      by (auto simp: convex_on_def)
   3.525 -  have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps)
   3.526 -  also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp
   3.527 -  finally have "f t \<le> a * f x + (1 - a) * f y" using cvx by simp
   3.528 -  also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
   3.529 -  finally have "f t - f y \<le> a * (f x - f y)" by simp
   3.530 +  have "a * x + (1 - a) * y = a * (x - y) + y"
   3.531 +    by (simp add: field_simps)
   3.532 +  also have "\<dots> = t"
   3.533 +    unfolding a_def using `x < t` `t < y` by simp
   3.534 +  finally have "f t \<le> a * f x + (1 - a) * f y"
   3.535 +    using cvx by simp
   3.536 +  also have "\<dots> = a * (f x - f y) + f y"
   3.537 +    by (simp add: field_simps)
   3.538 +  finally have "f t - f y \<le> a * (f x - f y)"
   3.539 +    by simp
   3.540    with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
   3.541      by (simp add: le_divide_eq divide_le_eq field_simps a_def)
   3.542    with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
   3.543 @@ -520,7 +613,7 @@
   3.544  lemma pos_convex_function:
   3.545    fixes f :: "real \<Rightarrow> real"
   3.546    assumes "convex C"
   3.547 -    and leq: "\<And>x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
   3.548 +    and leq: "\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
   3.549    shows "convex_on C f"
   3.550    unfolding convex_on_alt[OF assms(1)]
   3.551    using assms
   3.552 @@ -529,11 +622,13 @@
   3.553    let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
   3.554    assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
   3.555    then have "1 - \<mu> \<ge> 0" by auto
   3.556 -  then have xpos: "?x \<in> C" using asm unfolding convex_alt by fastforce
   3.557 -  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
   3.558 -            \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
   3.559 +  then have xpos: "?x \<in> C"
   3.560 +    using asm unfolding convex_alt by fastforce
   3.561 +  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) \<ge>
   3.562 +      \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
   3.563      using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
   3.564 -      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
   3.565 +      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]]
   3.566 +    by auto
   3.567    then have "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
   3.568      by (auto simp add: field_simps)
   3.569    then show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   3.570 @@ -547,9 +642,11 @@
   3.571    shows "{x .. y} \<subseteq> C"
   3.572  proof safe
   3.573    fix z assume zasm: "z \<in> {x .. y}"
   3.574 -  { assume asm: "x < z" "z < y"
   3.575 +  {
   3.576 +    assume asm: "x < z" "z < y"
   3.577      let ?\<mu> = "(y - z) / (y - x)"
   3.578 -    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add: field_simps)
   3.579 +    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1"
   3.580 +      using assms asm by (auto simp add: field_simps)
   3.581      then have comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
   3.582        using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>]
   3.583        by (simp add: algebra_simps)
   3.584 @@ -560,7 +657,8 @@
   3.585      also have "\<dots> = z"
   3.586        using assms by (auto simp: field_simps)
   3.587      finally have "z \<in> C"
   3.588 -      using comb by auto }
   3.589 +      using comb by auto
   3.590 +  }
   3.591    note less = this
   3.592    show "z \<in> C" using zasm less assms
   3.593      unfolding atLeastAtMost_iff le_less by auto
   3.594 @@ -576,7 +674,8 @@
   3.595    shows "f' x * (y - x) \<le> f y - f x"
   3.596    using assms
   3.597  proof -
   3.598 -  { fix x y :: real
   3.599 +  {
   3.600 +    fix x y :: real
   3.601      assume asm: "x \<in> C" "y \<in> C" "y > x"
   3.602      then have ge: "y - x > 0" "y - x \<ge> 0" by auto
   3.603      from asm have le: "x - y < 0" "x - y \<le> 0" by auto
   3.604 @@ -627,14 +726,18 @@
   3.605      then have "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
   3.606      then have "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
   3.607        using res by auto } note less_imp = this
   3.608 -  { fix x y :: real
   3.609 +  {
   3.610 +    fix x y :: real
   3.611      assume "x \<in> C" "y \<in> C" "x \<noteq> y"
   3.612      then have"f y - f x \<ge> f' x * (y - x)"
   3.613 -    unfolding neq_iff using less_imp by auto } note neq_imp = this
   3.614 +    unfolding neq_iff using less_imp by auto
   3.615 +  }
   3.616    moreover
   3.617 -  { fix x y :: real
   3.618 +  {
   3.619 +    fix x y :: real
   3.620      assume asm: "x \<in> C" "y \<in> C" "x = y"
   3.621 -    then have "f y - f x \<ge> f' x * (y - x)" by auto }
   3.622 +    then have "f y - f x \<ge> f' x * (y - x)" by auto
   3.623 +  }
   3.624    ultimately show ?thesis using assms by blast
   3.625  qed
   3.626  
   3.627 @@ -645,14 +748,16 @@
   3.628      and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
   3.629      and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   3.630    shows "convex_on C f"
   3.631 -using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce
   3.632 +  using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
   3.633 +  by fastforce
   3.634  
   3.635  lemma minus_log_convex:
   3.636    fixes b :: real
   3.637    assumes "b > 1"
   3.638    shows "convex_on {0 <..} (\<lambda> x. - log b x)"
   3.639  proof -
   3.640 -  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
   3.641 +  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
   3.642 +    using DERIV_log by auto
   3.643    then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
   3.644      by (auto simp: DERIV_minus)
   3.645    have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
   3.646 @@ -661,9 +766,10 @@
   3.647    have "\<And>z :: real. z > 0 \<Longrightarrow>
   3.648      DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
   3.649      by auto
   3.650 -  then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
   3.651 +  then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
   3.652 +    DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
   3.653      unfolding inverse_eq_divide by (auto simp add: mult_assoc)
   3.654 -  have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
   3.655 +  have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
   3.656      using `b > 1` by (auto intro!:less_imp_le)
   3.657    from f''_ge0_imp_convex[OF pos_is_convex,
   3.658      unfolded greaterThan_iff, OF f' f''0 f''_ge0]
     4.1 --- a/src/HOL/Library/Finite_Lattice.thy	Tue Apr 29 21:54:26 2014 +0200
     4.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Tue Apr 29 22:50:55 2014 +0200
     4.3 @@ -1,4 +1,6 @@
     4.4 -(* Author: Alessandro Coglio *)
     4.5 +(*  Title:      HOL/Library/Finite_Lattice.thy
     4.6 +    Author:     Alessandro Coglio
     4.7 +*)
     4.8  
     4.9  theory Finite_Lattice
    4.10  imports Product_Order
    4.11 @@ -16,29 +18,27 @@
    4.12  The resulting class is a subclass of @{class complete_lattice}. *}
    4.13  
    4.14  class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
    4.15 -assumes bot_def: "bot = Inf_fin UNIV"
    4.16 -assumes top_def: "top = Sup_fin UNIV"
    4.17 -assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    4.18 -assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    4.19 +  assumes bot_def: "bot = Inf_fin UNIV"
    4.20 +  assumes top_def: "top = Sup_fin UNIV"
    4.21 +  assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    4.22 +  assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    4.23  
    4.24  text {* The definitional assumptions
    4.25  on the operators @{const bot} and @{const top}
    4.26  of class @{class finite_lattice_complete}
    4.27  ensure that they yield bottom and top. *}
    4.28  
    4.29 -lemma finite_lattice_complete_bot_least:
    4.30 -"(bot::'a::finite_lattice_complete) \<le> x"
    4.31 -by (auto simp: bot_def intro: Inf_fin.coboundedI)
    4.32 +lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \<le> x"
    4.33 +  by (auto simp: bot_def intro: Inf_fin.coboundedI)
    4.34  
    4.35  instance finite_lattice_complete \<subseteq> order_bot
    4.36 -proof qed (auto simp: finite_lattice_complete_bot_least)
    4.37 +  by default (auto simp: finite_lattice_complete_bot_least)
    4.38  
    4.39 -lemma finite_lattice_complete_top_greatest:
    4.40 -"(top::'a::finite_lattice_complete) \<ge> x"
    4.41 -by (auto simp: top_def Sup_fin.coboundedI)
    4.42 +lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
    4.43 +  by (auto simp: top_def Sup_fin.coboundedI)
    4.44  
    4.45  instance finite_lattice_complete \<subseteq> order_top
    4.46 -proof qed (auto simp: finite_lattice_complete_top_greatest)
    4.47 +  by default (auto simp: finite_lattice_complete_top_greatest)
    4.48  
    4.49  instance finite_lattice_complete \<subseteq> bounded_lattice ..
    4.50  
    4.51 @@ -47,19 +47,18 @@
    4.52  of class @{class finite_lattice_complete}
    4.53  ensure that they yield infimum and supremum. *}
    4.54  
    4.55 -lemma finite_lattice_complete_Inf_empty:
    4.56 -  "Inf {} = (top :: 'a::finite_lattice_complete)"
    4.57 +lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)"
    4.58    by (simp add: Inf_def)
    4.59  
    4.60 -lemma finite_lattice_complete_Sup_empty:
    4.61 -  "Sup {} = (bot :: 'a::finite_lattice_complete)"
    4.62 +lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)"
    4.63    by (simp add: Sup_def)
    4.64  
    4.65  lemma finite_lattice_complete_Inf_insert:
    4.66    fixes A :: "'a::finite_lattice_complete set"
    4.67    shows "Inf (insert x A) = inf x (Inf A)"
    4.68  proof -
    4.69 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
    4.70 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _"
    4.71 +    by (fact comp_fun_idem_inf)
    4.72    show ?thesis by (simp add: Inf_def)
    4.73  qed
    4.74  
    4.75 @@ -67,87 +66,87 @@
    4.76    fixes A :: "'a::finite_lattice_complete set"
    4.77    shows "Sup (insert x A) = sup x (Sup A)"
    4.78  proof -
    4.79 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
    4.80 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _"
    4.81 +    by (fact comp_fun_idem_sup)
    4.82    show ?thesis by (simp add: Sup_def)
    4.83  qed
    4.84  
    4.85  lemma finite_lattice_complete_Inf_lower:
    4.86    "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    4.87 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
    4.88 +  using finite [of A]
    4.89 +  by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
    4.90  
    4.91  lemma finite_lattice_complete_Inf_greatest:
    4.92    "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    4.93 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
    4.94 +  using finite [of A]
    4.95 +  by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
    4.96  
    4.97  lemma finite_lattice_complete_Sup_upper:
    4.98    "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    4.99 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
   4.100 +  using finite [of A]
   4.101 +  by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
   4.102  
   4.103  lemma finite_lattice_complete_Sup_least:
   4.104    "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
   4.105 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
   4.106 +  using finite [of A]
   4.107 +  by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
   4.108  
   4.109  instance finite_lattice_complete \<subseteq> complete_lattice
   4.110  proof
   4.111  qed (auto simp:
   4.112 - finite_lattice_complete_Inf_lower
   4.113 - finite_lattice_complete_Inf_greatest
   4.114 - finite_lattice_complete_Sup_upper
   4.115 - finite_lattice_complete_Sup_least
   4.116 - finite_lattice_complete_Inf_empty
   4.117 - finite_lattice_complete_Sup_empty)
   4.118 +  finite_lattice_complete_Inf_lower
   4.119 +  finite_lattice_complete_Inf_greatest
   4.120 +  finite_lattice_complete_Sup_upper
   4.121 +  finite_lattice_complete_Sup_least
   4.122 +  finite_lattice_complete_Inf_empty
   4.123 +  finite_lattice_complete_Sup_empty)
   4.124  
   4.125  text {* The product of two finite lattices is already a finite lattice. *}
   4.126  
   4.127  lemma finite_bot_prod:
   4.128    "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
   4.129 -   Inf_fin UNIV"
   4.130 -by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
   4.131 +    Inf_fin UNIV"
   4.132 +  by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
   4.133  
   4.134  lemma finite_top_prod:
   4.135    "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
   4.136 -   Sup_fin UNIV"
   4.137 -by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
   4.138 +    Sup_fin UNIV"
   4.139 +  by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
   4.140  
   4.141  lemma finite_Inf_prod:
   4.142    "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   4.143 -  Finite_Set.fold inf top A"
   4.144 -by (metis Inf_fold_inf finite_code)
   4.145 +    Finite_Set.fold inf top A"
   4.146 +  by (metis Inf_fold_inf finite_code)
   4.147  
   4.148  lemma finite_Sup_prod:
   4.149    "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   4.150 -  Finite_Set.fold sup bot A"
   4.151 -by (metis Sup_fold_sup finite_code)
   4.152 +    Finite_Set.fold sup bot A"
   4.153 +  by (metis Sup_fold_sup finite_code)
   4.154  
   4.155 -instance prod ::
   4.156 -  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   4.157 -proof
   4.158 -qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   4.159 +instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   4.160 +  by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   4.161  
   4.162  text {* Functions with a finite domain and with a finite lattice as codomain
   4.163  already form a finite lattice. *}
   4.164  
   4.165 -lemma finite_bot_fun:
   4.166 -  "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
   4.167 -by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
   4.168 +lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
   4.169 +  by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
   4.170  
   4.171 -lemma finite_top_fun:
   4.172 -  "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
   4.173 -by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
   4.174 +lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
   4.175 +  by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
   4.176  
   4.177  lemma finite_Inf_fun:
   4.178    "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   4.179 -  Finite_Set.fold inf top A"
   4.180 -by (metis Inf_fold_inf finite_code)
   4.181 +    Finite_Set.fold inf top A"
   4.182 +  by (metis Inf_fold_inf finite_code)
   4.183  
   4.184  lemma finite_Sup_fun:
   4.185    "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   4.186 -  Finite_Set.fold sup bot A"
   4.187 -by (metis Sup_fold_sup finite_code)
   4.188 +    Finite_Set.fold sup bot A"
   4.189 +  by (metis Sup_fold_sup finite_code)
   4.190  
   4.191  instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   4.192 -proof
   4.193 -qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   4.194 +  by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   4.195  
   4.196  
   4.197  subsection {* Finite Distributive Lattices *}
   4.198 @@ -161,22 +160,22 @@
   4.199  
   4.200  lemma finite_distrib_lattice_complete_sup_Inf:
   4.201    "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
   4.202 -  using finite by (induct A rule: finite_induct)
   4.203 -    (simp_all add: sup_inf_distrib1)
   4.204 +  using finite
   4.205 +  by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)
   4.206  
   4.207  lemma finite_distrib_lattice_complete_inf_Sup:
   4.208    "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   4.209 -apply (rule finite_induct)
   4.210 -apply (metis finite_code)
   4.211 -apply (metis SUP_empty Sup_empty inf_bot_right)
   4.212 -apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   4.213 -done
   4.214 +  apply (rule finite_induct)
   4.215 +  apply (metis finite_code)
   4.216 +  apply (metis SUP_empty Sup_empty inf_bot_right)
   4.217 +  apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   4.218 +  done
   4.219  
   4.220  instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   4.221  proof
   4.222  qed (auto simp:
   4.223 - finite_distrib_lattice_complete_sup_Inf
   4.224 - finite_distrib_lattice_complete_inf_Sup)
   4.225 +  finite_distrib_lattice_complete_sup_Inf
   4.226 +  finite_distrib_lattice_complete_inf_Sup)
   4.227  
   4.228  text {* The product of two finite distributive lattices
   4.229  is already a finite distributive lattice. *}
   4.230 @@ -184,7 +183,7 @@
   4.231  instance prod ::
   4.232    (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   4.233    finite_distrib_lattice_complete
   4.234 -..
   4.235 +  ..
   4.236  
   4.237  text {* Functions with a finite domain
   4.238  and with a finite distributive lattice as codomain
   4.239 @@ -192,7 +191,7 @@
   4.240  
   4.241  instance "fun" ::
   4.242    (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
   4.243 -..
   4.244 +  ..
   4.245  
   4.246  
   4.247  subsection {* Linear Orders *}
   4.248 @@ -206,8 +205,8 @@
   4.249  The resulting class is a subclass of @{class distrib_lattice}. *}
   4.250  
   4.251  class linorder_lattice = linorder + inf + sup +
   4.252 -assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   4.253 -assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   4.254 +  assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   4.255 +  assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   4.256  
   4.257  text {* The definitional assumptions
   4.258  on the operators @{const inf} and @{const sup}
   4.259 @@ -216,39 +215,39 @@
   4.260  and that they distribute over each other. *}
   4.261  
   4.262  lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
   4.263 -unfolding inf_def by (metis (full_types) linorder_linear)
   4.264 +  unfolding inf_def by (metis (full_types) linorder_linear)
   4.265  
   4.266  lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
   4.267 -unfolding inf_def by (metis (full_types) linorder_linear)
   4.268 +  unfolding inf_def by (metis (full_types) linorder_linear)
   4.269  
   4.270  lemma linorder_lattice_inf_greatest:
   4.271    "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
   4.272 -unfolding inf_def by (metis (full_types))
   4.273 +  unfolding inf_def by (metis (full_types))
   4.274  
   4.275  lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
   4.276 -unfolding sup_def by (metis (full_types) linorder_linear)
   4.277 +  unfolding sup_def by (metis (full_types) linorder_linear)
   4.278  
   4.279  lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
   4.280 -unfolding sup_def by (metis (full_types) linorder_linear)
   4.281 +  unfolding sup_def by (metis (full_types) linorder_linear)
   4.282  
   4.283  lemma linorder_lattice_sup_least:
   4.284    "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
   4.285 -by (auto simp: sup_def)
   4.286 +  by (auto simp: sup_def)
   4.287  
   4.288  lemma linorder_lattice_sup_inf_distrib1:
   4.289    "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
   4.290 -by (auto simp: inf_def sup_def)
   4.291 - 
   4.292 +  by (auto simp: inf_def sup_def)
   4.293 +
   4.294  instance linorder_lattice \<subseteq> distrib_lattice
   4.295 -proof                                                     
   4.296 +proof
   4.297  qed (auto simp:
   4.298 - linorder_lattice_inf_le1
   4.299 - linorder_lattice_inf_le2
   4.300 - linorder_lattice_inf_greatest
   4.301 - linorder_lattice_sup_ge1
   4.302 - linorder_lattice_sup_ge2
   4.303 - linorder_lattice_sup_least
   4.304 - linorder_lattice_sup_inf_distrib1)
   4.305 +  linorder_lattice_inf_le1
   4.306 +  linorder_lattice_inf_le2
   4.307 +  linorder_lattice_inf_greatest
   4.308 +  linorder_lattice_sup_ge1
   4.309 +  linorder_lattice_sup_ge2
   4.310 +  linorder_lattice_sup_least
   4.311 +  linorder_lattice_sup_inf_distrib1)
   4.312  
   4.313  
   4.314  subsection {* Finite Linear Orders *}
   4.315 @@ -265,6 +264,5 @@
   4.316  
   4.317  instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
   4.318  
   4.319 -
   4.320  end
   4.321  
     5.1 --- a/src/HOL/Library/Permutation.thy	Tue Apr 29 21:54:26 2014 +0200
     5.2 +++ b/src/HOL/Library/Permutation.thy	Tue Apr 29 22:50:55 2014 +0200
     5.3 @@ -22,12 +22,10 @@
     5.4  subsection {* Some examples of rule induction on permutations *}
     5.5  
     5.6  lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
     5.7 -  by (induct xs == "[]::'a list" ys pred: perm) simp_all
     5.8 +  by (induct xs == "[] :: 'a list" ys pred: perm) simp_all
     5.9  
    5.10  
    5.11 -text {*
    5.12 -  \medskip This more general theorem is easier to understand!
    5.13 -  *}
    5.14 +text {* \medskip This more general theorem is easier to understand! *}
    5.15  
    5.16  lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
    5.17    by (induct pred: perm) simp_all
    5.18 @@ -41,9 +39,7 @@
    5.19  
    5.20  subsection {* Ways of making new permutations *}
    5.21  
    5.22 -text {*
    5.23 -  We can insert the head anywhere in the list.
    5.24 -*}
    5.25 +text {* We can insert the head anywhere in the list. *}
    5.26  
    5.27  lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
    5.28    by (induct xs) auto
    5.29 @@ -72,10 +68,10 @@
    5.30  
    5.31  subsection {* Further results *}
    5.32  
    5.33 -lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
    5.34 +lemma perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
    5.35    by (blast intro: perm_empty_imp)
    5.36  
    5.37 -lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
    5.38 +lemma perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
    5.39    apply auto
    5.40    apply (erule perm_sym [THEN perm_empty_imp])
    5.41    done
    5.42 @@ -83,10 +79,10 @@
    5.43  lemma perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
    5.44    by (induct pred: perm) auto
    5.45  
    5.46 -lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    5.47 +lemma perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
    5.48    by (blast intro: perm_sing_imp)
    5.49  
    5.50 -lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
    5.51 +lemma perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
    5.52    by (blast dest: perm_sym)
    5.53  
    5.54  
    5.55 @@ -107,16 +103,16 @@
    5.56  lemma cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
    5.57    by (drule_tac z = z in perm_remove_perm) auto
    5.58  
    5.59 -lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
    5.60 +lemma cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
    5.61    by (blast intro: cons_perm_imp_perm)
    5.62  
    5.63  lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
    5.64    by (induct zs arbitrary: xs ys rule: rev_induct) auto
    5.65  
    5.66 -lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
    5.67 +lemma perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
    5.68    by (blast intro: append_perm_imp_perm perm_append1)
    5.69  
    5.70 -lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
    5.71 +lemma perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
    5.72    apply (safe intro!: perm_append2)
    5.73    apply (rule append_perm_imp_perm)
    5.74    apply (rule perm_append_swap [THEN perm.trans])
    5.75 @@ -124,21 +120,30 @@
    5.76    apply (blast intro: perm_append_swap)
    5.77    done
    5.78  
    5.79 -lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
    5.80 +lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys"
    5.81    apply (rule iffI)
    5.82 -  apply (erule_tac [2] perm.induct, simp_all add: union_ac)
    5.83 -  apply (erule rev_mp, rule_tac x=ys in spec)
    5.84 -  apply (induct_tac xs, auto)
    5.85 -  apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
    5.86 +  apply (erule_tac [2] perm.induct)
    5.87 +  apply (simp_all add: union_ac)
    5.88 +  apply (erule rev_mp)
    5.89 +  apply (rule_tac x=ys in spec)
    5.90 +  apply (induct_tac xs)
    5.91 +  apply auto
    5.92 +  apply (erule_tac x = "remove1 a x" in allE)
    5.93 +  apply (drule sym)
    5.94 +  apply simp
    5.95    apply (subgoal_tac "a \<in> set x")
    5.96    apply (drule_tac z = a in perm.Cons)
    5.97 -  apply (erule perm.trans, rule perm_sym, erule perm_remove)
    5.98 -  apply (drule_tac f=set_of in arg_cong, simp)
    5.99 +  apply (erule perm.trans)
   5.100 +  apply (rule perm_sym)
   5.101 +  apply (erule perm_remove)
   5.102 +  apply (drule_tac f=set_of in arg_cong)
   5.103 +  apply simp
   5.104    done
   5.105  
   5.106  lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
   5.107    apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   5.108 -  apply (insert surj_multiset_of, drule surjD)
   5.109 +  apply (insert surj_multiset_of)
   5.110 +  apply (drule surjD)
   5.111    apply (blast intro: sym)+
   5.112    done
   5.113  
   5.114 @@ -158,15 +163,16 @@
   5.115     apply simp_all
   5.116    apply (subgoal_tac "a \<in> set (remdups ys)")
   5.117     prefer 2 apply (metis set_simps(2) insert_iff set_remdups)
   5.118 -  apply (drule split_list) apply(elim exE conjE)
   5.119 -  apply (drule_tac x=list in spec) apply(erule impE) prefer 2
   5.120 -   apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   5.121 +  apply (drule split_list) apply (elim exE conjE)
   5.122 +  apply (drule_tac x = list in spec) apply (erule impE) prefer 2
   5.123 +   apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2
   5.124      apply simp
   5.125      apply (subgoal_tac "a # list <~~> a # ysa @ zs")
   5.126       apply (metis Cons_eq_appendI perm_append_Cons trans)
   5.127      apply (metis Cons Cons_eq_appendI distinct.simps(2)
   5.128        distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   5.129 -   apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   5.130 +   apply (subgoal_tac "set (a # list) =
   5.131 +      set (ysa @ a # zs) \<and> distinct (a # list) \<and> distinct (ysa @ a # zs)")
   5.132      apply (fastforce simp add: insert_ident)
   5.133     apply (metis distinct_remdups set_remdups)
   5.134     apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
   5.135 @@ -176,15 +182,17 @@
   5.136     apply (rule length_remdups_leq)
   5.137    done
   5.138  
   5.139 -lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> (set x = set y)"
   5.140 +lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
   5.141    by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   5.142  
   5.143  lemma permutation_Ex_bij:
   5.144    assumes "xs <~~> ys"
   5.145    shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
   5.146 -using assms proof induct
   5.147 +  using assms
   5.148 +proof induct
   5.149    case Nil
   5.150 -  then show ?case unfolding bij_betw_def by simp
   5.151 +  then show ?case
   5.152 +    unfolding bij_betw_def by simp
   5.153  next
   5.154    case (swap y x l)
   5.155    show ?case
   5.156 @@ -192,14 +200,15 @@
   5.157      show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
   5.158        by (auto simp: bij_betw_def)
   5.159      fix i
   5.160 -    assume "i < length(y#x#l)"
   5.161 +    assume "i < length (y # x # l)"
   5.162      show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
   5.163        by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
   5.164    qed
   5.165  next
   5.166    case (Cons xs ys z)
   5.167 -  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
   5.168 -    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
   5.169 +  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}"
   5.170 +    and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)"
   5.171 +    by blast
   5.172    let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
   5.173    show ?case
   5.174    proof (intro exI[of _ ?f] allI conjI impI)
   5.175 @@ -214,21 +223,24 @@
   5.176          by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
   5.177      qed (auto simp: bij_betw_def)
   5.178      fix i
   5.179 -    assume "i < length (z#xs)"
   5.180 +    assume "i < length (z # xs)"
   5.181      then show "(z # xs) ! i = (z # ys) ! (?f i)"
   5.182        using perm by (cases i) auto
   5.183    qed
   5.184  next
   5.185    case (trans xs ys zs)
   5.186 -  then obtain f g where
   5.187 -    bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
   5.188 -    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
   5.189 +  then obtain f g
   5.190 +    where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}"
   5.191 +    and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)"
   5.192 +    by blast
   5.193    show ?case
   5.194    proof (intro exI[of _ "g \<circ> f"] conjI allI impI)
   5.195      show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
   5.196        using bij by (rule bij_betw_trans)
   5.197 -    fix i assume "i < length xs"
   5.198 -    with bij have "f i < length ys" unfolding bij_betw_def by force
   5.199 +    fix i
   5.200 +    assume "i < length xs"
   5.201 +    with bij have "f i < length ys"
   5.202 +      unfolding bij_betw_def by force
   5.203      with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
   5.204        using trans(1,3)[THEN perm_length] perm by auto
   5.205    qed