# HG changeset patch
# User wenzelm
# Date 1398804655 -7200
# Node ID 9f84219715a7341788c788198c4d6570ac82ea8b
# Parent  e8cce2bd23e57e93ac80c19f18145dafc5f2320c
tuned proofs;

diff -r e8cce2bd23e5 -r 9f84219715a7 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/BigO.thy	Tue Apr 29 22:50:55 2014 +0200
@@ -390,7 +390,7 @@
     also have "\<dots> \<subseteq> O(g) + O(g)"
     proof -
       from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
-      thus ?thesis by (auto del: subsetI)
+      then show ?thesis by (auto del: subsetI)
     qed
     also have "\<dots> \<subseteq> O(g)" by simp
     finally show ?thesis .
diff -r e8cce2bd23e5 -r 9f84219715a7 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/ContNotDenum.thy	Tue Apr 29 22:50:55 2014 +0200
@@ -1,5 +1,5 @@
-(*  Title       : HOL/ContNonDenum
-    Author      : Benjamin Porter, Monash University, NICTA, 2005
+(*  Title:      HOL/Library/ContNonDenum.thy
+    Author:     Benjamin Porter, Monash University, NICTA, 2005
 *)
 
 header {* Non-denumerability of the Continuum. *}
@@ -15,7 +15,7 @@
 system.
 
 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
-words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
+words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
 surjective.
 
 {\em Outline:} An elegant informal proof of this result uses Cantor's
@@ -25,41 +25,50 @@
 completeness of the Real numbers and is the foundation for our
 argument. Informally it states that an intersection of countable
 closed intervals (where each successive interval is a subset of the
-last) is non-empty. We then assume a surjective function f:@{text
-"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
+last) is non-empty. We then assume a surjective function @{text
+"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
 by generating a sequence of closed intervals then using the NIP. *}
 
+
 subsection {* Closed Intervals *}
 
 subsection {* Nested Interval Property *}
 
 theorem NIP:
-  fixes f::"nat \<Rightarrow> real set"
+  fixes f :: "nat \<Rightarrow> real set"
   assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
-  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
+    and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
   shows "(\<Inter>n. f n) \<noteq> {}"
 proof -
   let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
-  { fix n 
+  {
+    fix n
     from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
       by auto
     then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
-      by auto }
+      by auto
+  }
   note f_eq = this
-  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
-      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
+  {
+    fix n m :: nat
+    assume "n \<le> m"
+    then have "f m \<subseteq> f n"
+      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
+  }
   note subset' = this
 
   have "compact (f 0)"
     by (subst f_eq) (rule compact_Icc)
   then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
   proof (rule compact_imp_fip_image)
-    fix I :: "nat set" assume I: "finite I"
+    fix I :: "nat set"
+    assume I: "finite I"
     have "{} \<subset> f (Max (insert 0 I))"
       using f_eq[of "Max (insert 0 I)"] by auto
     also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
     proof (rule INF_greatest)
-      fix i assume "i \<in> insert 0 I"
+      fix i
+      assume "i \<in> insert 0 I"
       with I show "f (Max (insert 0 I)) \<subseteq> f i"
         by (intro subset') auto
     qed
@@ -70,6 +79,7 @@
     by auto
 qed
 
+
 subsection {* Generating the intervals *}
 
 subsubsection {* Existence of non-singleton closed intervals *}
@@ -80,7 +90,7 @@
 non-singleton itself. *}
 
 lemma closed_subset_ex:
-  fixes c::real
+  fixes c :: real
   assumes "a < b"
   shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
 proof (cases "c < b")
@@ -90,39 +100,45 @@
     case True
     with `a < b` `c < b` have "c \<notin> {a..b}"
       by auto
-    with `a < b` show ?thesis by auto
+    with `a < b` show ?thesis
+      by auto
   next
     case False
     then have "a \<le> c" by simp
     def ka \<equiv> "(c + b)/2"
-
-    from ka_def `c < b` have kalb: "ka < b" by auto
-    moreover from ka_def `c < b` have kagc: "ka > c" by simp
-    ultimately have "c\<notin>{ka..b}" by auto
-    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
-    hence "{ka..b} \<subseteq> {a..b}" by auto
-    ultimately have
-      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
-      using kalb by auto
+    from ka_def `c < b` have "ka < b"
+      by auto
+    moreover from ka_def `c < b` have "ka > c"
+      by simp
+    ultimately have "c \<notin> {ka..b}"
+      by auto
+    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
+      by simp
+    then have "{ka..b} \<subseteq> {a..b}"
+      by auto
+    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
+      using `ka < b` by auto
     then show ?thesis
       by auto
   qed
 next
   case False
   then have "c \<ge> b" by simp
-
   def kb \<equiv> "(a + b)/2"
   with `a < b` have "kb < b" by auto
-  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
+  with kb_def `c \<ge> b` have "a < kb" "kb < c"
+    by auto
   from `kb < c` have c: "c \<notin> {a..kb}"
     by auto
   with `kb < b` have "{a..kb} \<subseteq> {a..b}"
     by auto
   with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
     by simp
-  then show ?thesis by auto
+  then show ?thesis
+    by auto
 qed
 
+
 subsection {* newInt: Interval generation *}
 
 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
@@ -130,17 +146,19 @@
 does not contain @{text "f (Suc n)"}. With the base case defined such
 that @{text "(f 0)\<notin>newInt 0 f"}. *}
 
+
 subsubsection {* Definition *}
 
-primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
+primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
+where
   "newInt 0 f = {f 0 + 1..f 0 + 2}"
-  | "newInt (Suc n) f =
-      (SOME e. (\<exists>e1 e2.
-       e1 < e2 \<and>
-       e = {e1..e2} \<and>
-       e \<subseteq> newInt n f \<and>
-       f (Suc n) \<notin> e)
-      )"
+| "newInt (Suc n) f =
+    (SOME e.
+      (\<exists>e1 e2.
+         e1 < e2 \<and>
+         e = {e1..e2} \<and>
+         e \<subseteq> newInt n f \<and>
+         f (Suc n) \<notin> e))"
 
 
 subsubsection {* Properties *}
@@ -150,81 +168,76 @@
 
 lemma newInt_ex:
   "\<exists>a b. a < b \<and>
-   newInt (Suc n) f = {a..b} \<and>
-   newInt (Suc n) f \<subseteq> newInt n f \<and>
-   f (Suc n) \<notin> newInt (Suc n) f"
+    newInt (Suc n) f = {a..b} \<and>
+    newInt (Suc n) f \<subseteq> newInt n f \<and>
+    f (Suc n) \<notin> newInt (Suc n) f"
 proof (induct n)
   case 0
-
   let ?e = "SOME e. \<exists>e1 e2.
-   e1 < e2 \<and>
-   e = {e1..e2} \<and>
-   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
-   f (Suc 0) \<notin> e"
+    e1 < e2 \<and>
+    e = {e1..e2} \<and>
+    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+    f (Suc 0) \<notin> e"
 
   have "newInt (Suc 0) f = ?e" by auto
   moreover
   have "f 0 + 1 < f 0 + 2" by simp
-  with closed_subset_ex have
-    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
-     f (Suc 0) \<notin> {ka..kb}" .
-  hence
-    "\<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" by simp
-  hence
-    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
+  with closed_subset_ex
+  have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
+  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"
+    by simp
+  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"
     by (rule someI_ex)
   ultimately have "\<exists>e1 e2. e1 < e2 \<and>
-   newInt (Suc 0) f = {e1..e2} \<and>
-   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
-   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
-  thus
-    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
-     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
+      newInt (Suc 0) f = {e1..e2} \<and>
+      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+      f (Suc 0) \<notin> newInt (Suc 0) f"
+    by simp
+  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
+      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
     by simp
 next
   case (Suc n)
-  hence "\<exists>a b.
-   a < b \<and>
-   newInt (Suc n) f = {a..b} \<and>
-   newInt (Suc n) f \<subseteq> newInt n f \<and>
-   f (Suc n) \<notin> newInt (Suc n) f" by simp
+  then have "\<exists>a b.
+      a < b \<and>
+      newInt (Suc n) f = {a..b} \<and>
+      newInt (Suc n) f \<subseteq> newInt n f \<and>
+      f (Suc n) \<notin> newInt (Suc n) f"
+    by simp
   then obtain a and b where ab: "a < b \<and>
-   newInt (Suc n) f = {a..b} \<and>
-   newInt (Suc n) f \<subseteq> newInt n f \<and>
-   f (Suc n) \<notin> newInt (Suc n) f" by auto
-  hence cab: "{a..b} = newInt (Suc n) f" by simp
+      newInt (Suc n) f = {a..b} \<and>
+      newInt (Suc n) f \<subseteq> newInt n f \<and>
+      f (Suc n) \<notin> newInt (Suc n) f"
+    by auto
+  then have cab: "{a..b} = newInt (Suc n) f"
+    by simp
 
   let ?e = "SOME e. \<exists>e1 e2.
-    e1 < e2 \<and>
-    e = {e1..e2} \<and>
-    e \<subseteq> {a..b} \<and>
-    f (Suc (Suc n)) \<notin> e"
-  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
+      e1 < e2 \<and>
+      e = {e1..e2} \<and>
+      e \<subseteq> {a..b} \<and>
+      f (Suc (Suc n)) \<notin> e"
+  from cab have ni: "newInt (Suc (Suc n)) f = ?e"
+    by auto
 
   from ab have "a < b" by simp
-  with closed_subset_ex have
-    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
-     f (Suc (Suc n)) \<notin> {ka..kb}" .
-  hence
-    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
-     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
+  with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
+    f (Suc (Suc n)) \<notin> {ka..kb}" .
+  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
+      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
+    by simp
+  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"
     by simp
-  hence
-    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
-     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
-  hence
-    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
-     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
-  with ab ni show
-    "\<exists>ka kb. ka < kb \<and>
-     newInt (Suc (Suc n)) f = {ka..kb} \<and>
-     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
-     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
+  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
+    by (rule someI_ex)
+  with ab ni show "\<exists>ka kb. ka < kb \<and>
+      newInt (Suc (Suc n)) f = {ka..kb} \<and>
+      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
+      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
+    by auto
 qed
 
-lemma newInt_subset:
-  "newInt (Suc n) f \<subseteq> newInt n f"
+lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
   using newInt_ex by auto
 
 
@@ -232,34 +245,27 @@
 of f is in the intersection of all closed intervals generated by
 newInt. *}
 
-lemma newInt_inter:
-  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
 proof
-  fix n::nat
-  {
-    assume n0: "n = 0"
-    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
-    ultimately have "f n \<notin> newInt n f" by simp
-  }
-  moreover
-  {
-    assume "\<not> n = 0"
-    hence "n > 0" by simp
-    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
-    from newInt_ex have
-      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
-       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
-    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
-    with ndef have "f n \<notin> newInt n f" by simp
-  }
-  ultimately have "f n \<notin> newInt n f" by (rule case_split)
-  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
+  fix n :: nat
+  have "f n \<notin> newInt n f"
+  proof (cases n)
+    case 0
+    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
+      by simp
+    ultimately show ?thesis by simp
+  next
+    case (Suc m)
+    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
+      newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
+    then have "f (Suc m) \<notin> newInt (Suc m) f"
+      by auto
+    with Suc show ?thesis by simp
+  qed
+  then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
 qed
 
-
-lemma newInt_notempty:
-  "(\<Inter>n. newInt n f) \<noteq> {}"
+lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
 proof -
   let ?g = "\<lambda>n. newInt n f"
   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
@@ -269,30 +275,26 @@
   qed
   moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   proof
-    fix n::nat
-    {
-      assume "n = 0"
-      then have
-        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
+    fix n :: nat
+    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
+    proof (cases n)
+      case 0
+      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
         by simp
-      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
-    }
-    moreover
-    {
-      assume "\<not> n = 0"
-      then have "n > 0" by simp
-      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
-      have
-        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
+      then show ?thesis
+        by blast
+    next
+      case (Suc m)
+      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
         (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
         by (rule newInt_ex)
-      then obtain a and b where
-        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
-      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
-      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
-    }
-    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
+      then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
+        by auto
+      with Suc have "?g n = {a..b} \<and> a \<le> b"
+        by auto
+      then show ?thesis
+        by blast
+    qed
   qed
   ultimately show ?thesis by (rule NIP)
 qed
@@ -300,17 +302,22 @@
 
 subsection {* Final Theorem *}
 
-theorem real_non_denum:
-  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
-proof -- "by contradiction"
-  assume "\<exists>f::nat\<Rightarrow>real. surj f"
-  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
-  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
-  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
-  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
-  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
-  moreover from rangeF have "x \<in> range f" by simp
-  ultimately show False by blast
+theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
+proof
+  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
+  then obtain f :: "nat \<Rightarrow> real" where "surj f"
+    by auto
+  txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
+  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
+    using newInt_notempty by blast
+  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+    by (rule newInt_inter)
+  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
+    by blast
+  moreover from `surj f` have "x \<in> range f"
+    by simp
+  ultimately show False
+    by blast
 qed
 
 end
diff -r e8cce2bd23e5 -r 9f84219715a7 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/Convex.thy	Tue Apr 29 22:50:55 2014 +0200
@@ -29,11 +29,18 @@
   (is "_ \<longleftrightarrow> ?alt")
 proof
   assume alt[rule_format]: ?alt
-  { fix x y and u v :: real assume mem: "x \<in> s" "y \<in> s"
+  {
+    fix x y and u v :: real
+    assume mem: "x \<in> s" "y \<in> s"
     assume "0 \<le> u" "0 \<le> v"
-    moreover assume "u + v = 1" then have "u = 1 - v" by auto
-    ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s" using alt[OF mem] by auto }
-  then show "convex s" unfolding convex_def by auto
+    moreover
+    assume "u + v = 1"
+    then have "u = 1 - v" by auto
+    ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s"
+      using alt[OF mem] by auto
+  }
+  then show "convex s"
+    unfolding convex_def by auto
 qed (auto simp: convex_def)
 
 lemma mem_convex:
@@ -50,7 +57,7 @@
 lemma convex_UNIV[intro]: "convex UNIV"
   unfolding convex_def by auto
 
-lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"
+lemma convex_Inter: "(\<forall>s\<in>f. convex s) \<Longrightarrow> convex(\<Inter> f)"
   unfolding convex_def by auto
 
 lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
@@ -68,13 +75,16 @@
 
 lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
 proof -
-  have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto
-  show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
+  have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}"
+    by auto
+  show ?thesis
+    unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
 qed
 
 lemma convex_hyperplane: "convex {x. inner a x = b}"
 proof -
-  have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto
+  have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}"
+    by auto
   show ?thesis using convex_halfspace_le convex_halfspace_ge
     by (auto intro!: convex_Int simp: *)
 qed
@@ -115,8 +125,11 @@
 
 lemma convex_setsum:
   fixes C :: "'a::real_vector set"
-  assumes "finite s" and "convex C" and "(\<Sum> i \<in> s. a i) = 1"
-  assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0" and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
+  assumes "finite s"
+    and "convex C"
+    and "(\<Sum> i \<in> s. a i) = 1"
+  assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0"
+    and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
   shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C"
   using assms(1,3,4,5)
 proof (induct arbitrary: a set: finite)
@@ -124,18 +137,27 @@
   then show ?case by simp
 next
   case (insert i s) note IH = this(3)
-  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"
+  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"
     using insert.hyps(1,2) insert.prems by simp_all
-  then have "0 \<le> setsum a s" by (simp add: setsum_nonneg)
+  then have "0 \<le> setsum a s"
+    by (simp add: setsum_nonneg)
   have "a i *\<^sub>R y i + (\<Sum>j\<in>s. a j *\<^sub>R y j) \<in> C"
   proof (cases)
     assume z: "setsum a s = 0"
-    with `a i + setsum a s = 1` have "a i = 1" by simp
-    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
-    show ?thesis using `a i = 1` and `\<forall>j\<in>s. a j = 0` and `y i \<in> C` by simp
+    with `a i + setsum a s = 1` have "a i = 1"
+      by simp
+    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
+    show ?thesis using `a i = 1` and `\<forall>j\<in>s. a j = 0` and `y i \<in> C`
+      by simp
   next
     assume nz: "setsum a s \<noteq> 0"
-    with `0 \<le> setsum a s` have "0 < setsum a s" by simp
+    with `0 \<le> setsum a s` have "0 < setsum a s"
+      by simp
     then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
       using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
       by (simp add: IH setsum_divide_distrib [symmetric])
@@ -143,9 +165,11 @@
       and `0 \<le> setsum a s` and `a i + setsum a s = 1`
     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"
       by (rule convexD)
-    then show ?thesis by (simp add: scaleR_setsum_right nz)
+    then show ?thesis
+      by (simp add: scaleR_setsum_right nz)
   qed
-  then show ?case using `finite s` and `i \<notin> s` by simp
+  then show ?case using `finite s` and `i \<notin> s`
+    by simp
 qed
 
 lemma convex:
@@ -159,18 +183,22 @@
     "\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s"
     "setsum u {1..k} = 1"
   from this convex_setsum[of "{1 .. k}" s]
-  show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s" by auto
+  show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s"
+    by auto
 next
   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
     \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s"
-  { fix \<mu> :: real
+  {
+    fix \<mu> :: real
     fix x y :: 'a
     assume xy: "x \<in> s" "y \<in> s"
     assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1"
     let ?u = "\<lambda>i. if (i :: nat) = 1 then \<mu> else 1 - \<mu>"
     let ?x = "\<lambda>i. if (i :: nat) = 1 then x else y"
-    have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}" by auto
-    then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1" by simp
+    have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}"
+      by auto
+    then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1"
+      by simp
     then have "setsum ?u {1 .. 2} = 1"
       using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
       by auto
@@ -179,10 +207,13 @@
     have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
       using setsum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
     from setsum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
-    have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y" by auto
-    then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s" using s by (auto simp:add_commute)
+    have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
+      by auto
+    then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"
+      using s by (auto simp:add_commute)
   }
-  then show "convex s" unfolding convex_alt by auto
+  then show "convex s"
+    unfolding convex_alt by auto
 qed
 
 
@@ -193,42 +224,48 @@
 proof safe
   fix t
   fix u :: "'a \<Rightarrow> real"
-  assume "convex s" "finite t"
-    "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
+  assume "convex s"
+    and "finite t"
+    and "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
   then show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
     using convex_setsum[of t s u "\<lambda> x. x"] by auto
 next
-  assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x)
-    \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
+  assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and>
+    setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
   show "convex s"
     unfolding convex_alt
   proof safe
     fix x y
     fix \<mu> :: real
     assume asm: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1"
-    { assume "x \<noteq> y"
+    {
+      assume "x \<noteq> y"
       then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
         using asm0[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1 - \<mu> else \<mu>"]
-          asm by auto }
+          asm by auto
+    }
     moreover
-    { assume "x = y"
+    {
+      assume "x = y"
       then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
         using asm0[rule_format, of "{x, y}" "\<lambda> z. 1"]
-          asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) }
-    ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" by blast
+          asm by (auto simp: field_simps real_vector.scale_left_diff_distrib)
+    }
+    ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
+      by blast
   qed
 qed
 
 lemma convex_finite:
   assumes "finite s"
-  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)"
+  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)"
   unfolding convex_explicit
 proof safe
   fix t u
   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"
     and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
-  have *: "s \<inter> t = t" using as(2) by auto
+  have *: "s \<inter> t = t"
+    using as(2) by auto
   have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
     by simp
   show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
@@ -236,6 +273,7 @@
    by (auto simp: assms setsum_cases if_distrib if_distrib_arg)
 qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
 
+
 subsection {* Functions that are convex on a set *}
 
 definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
@@ -246,11 +284,13 @@
   unfolding convex_on_def by auto
 
 lemma convex_on_add [intro]:
-  assumes "convex_on s f" "convex_on s g"
+  assumes "convex_on s f"
+    and "convex_on s g"
   shows "convex_on s (\<lambda>x. f x + g x)"
 proof -
-  { fix x y
-    assume "x\<in>s" "y\<in>s"
+  {
+    fix x y
+    assume "x \<in> s" "y \<in> s"
     moreover
     fix u v :: real
     assume "0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -260,13 +300,16 @@
     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)"
       by (simp add: field_simps)
   }
-  then show ?thesis unfolding convex_on_def by auto
+  then show ?thesis
+    unfolding convex_on_def by auto
 qed
 
 lemma convex_on_cmul [intro]:
-  assumes "0 \<le> (c::real)" "convex_on s f"
+  fixes c :: real
+  assumes "0 \<le> c"
+    and "convex_on s f"
   shows "convex_on s (\<lambda>x. c * f x)"
-proof-
+proof -
   have *: "\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)"
     by (simp add: field_simps)
   show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)]
@@ -274,13 +317,19 @@
 qed
 
 lemma convex_lower:
-  assumes "convex_on s f"  "x\<in>s"  "y \<in> s"  "0 \<le> u"  "0 \<le> v"  "u + v = 1"
+  assumes "convex_on s f"
+    and "x \<in> s"
+    and "y \<in> s"
+    and "0 \<le> u"
+    and "0 \<le> v"
+    and "u + v = 1"
   shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"
-proof-
+proof -
   let ?m = "max (f x) (f y)"
   have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
     using assms(4,5) by (auto simp add: mult_left_mono add_mono)
-  also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[symmetric] by auto
+  also have "\<dots> = max (f x) (f y)"
+    using assms(6) unfolding distrib[symmetric] by auto
   finally show ?thesis
     using assms unfolding convex_on_def by fastforce
 qed
@@ -290,11 +339,13 @@
   shows "convex_on s (\<lambda>x. dist a x)"
 proof (auto simp add: convex_on_def dist_norm)
   fix x y
-  assume "x\<in>s" "y\<in>s"
+  assume "x \<in> s" "y \<in> s"
   fix u v :: real
-  assume "0 \<le> u" "0 \<le> v" "u + v = 1"
+  assume "0 \<le> u"
+  assume "0 \<le> v"
+  assume "u + v = 1"
   have "a = u *\<^sub>R a + v *\<^sub>R a"
-    unfolding scaleR_left_distrib[symmetric] and `u+v=1` by simp
+    unfolding scaleR_left_distrib[symmetric] and `u + v = 1` by simp
   then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
     by (auto simp add: algebra_simps)
   show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
@@ -306,7 +357,9 @@
 subsection {* Arithmetic operations on sets preserve convexity. *}
 
 lemma convex_linear_image:
-  assumes "linear f" and "convex s" shows "convex (f ` s)"
+  assumes "linear f"
+    and "convex s"
+  shows "convex (f ` s)"
 proof -
   interpret f: linear f by fact
   from `convex s` show "convex (f ` s)"
@@ -314,7 +367,9 @@
 qed
 
 lemma convex_linear_vimage:
-  assumes "linear f" and "convex s" shows "convex (f -` s)"
+  assumes "linear f"
+    and "convex s"
+  shows "convex (f -` s)"
 proof -
   interpret f: linear f by fact
   from `convex s` show "convex (f -` s)"
@@ -322,21 +377,28 @@
 qed
 
 lemma convex_scaling:
-  assumes "convex s" shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
+  assumes "convex s"
+  shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
 proof -
-  have "linear (\<lambda>x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right)
-  then show ?thesis using `convex s` by (rule convex_linear_image)
+  have "linear (\<lambda>x. c *\<^sub>R x)"
+    by (simp add: linearI scaleR_add_right)
+  then show ?thesis
+    using `convex s` by (rule convex_linear_image)
 qed
 
 lemma convex_negations:
-  assumes "convex s" shows "convex ((\<lambda>x. - x) ` s)"
+  assumes "convex s"
+  shows "convex ((\<lambda>x. - x) ` s)"
 proof -
-  have "linear (\<lambda>x. - x)" by (simp add: linearI)
-  then show ?thesis using `convex s` by (rule convex_linear_image)
+  have "linear (\<lambda>x. - x)"
+    by (simp add: linearI)
+  then show ?thesis
+    using `convex s` by (rule convex_linear_image)
 qed
 
 lemma convex_sums:
-  assumes "convex s" and "convex t"
+  assumes "convex s"
+    and "convex t"
   shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
 proof -
   have "linear (\<lambda>(x, y). x + y)"
@@ -362,7 +424,8 @@
   assumes "convex s"
   shows "convex ((\<lambda>x. a + x) ` s)"
 proof -
-  have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
+  have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s"
+    by auto
   then show ?thesis
     using convex_sums[OF convex_singleton[of a] assms] by auto
 qed
@@ -371,7 +434,8 @@
   assumes "convex s"
   shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof -
-  have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
+  have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s"
+    by auto
   then show ?thesis
     using convex_translation[OF convex_scaling[OF assms], of a c] by auto
 qed
@@ -381,18 +445,25 @@
 proof safe
   fix y x \<mu> :: real
   assume asms: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
-  { assume "\<mu> = 0"
+  {
+    assume "\<mu> = 0"
     then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y" by simp
-    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
+    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp
+  }
   moreover
-  { assume "\<mu> = 1"
-    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
+  {
+    assume "\<mu> = 1"
+    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp
+  }
   moreover
-  { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
+  {
+    assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     then have "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
-      by (auto simp add: add_pos_pos) }
-  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
+      by (auto simp add: add_pos_pos)
+  }
+  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
+    using assms by fastforce
 qed
 
 lemma convex_on_setsum:
@@ -415,25 +486,32 @@
   case (insert i s) note asms = this
   then have "convex_on C f" by simp
   from this[unfolded convex_on_def, rule_format]
-  have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1
-      \<Longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+  have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1 \<Longrightarrow>
+      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
     by simp
-  { assume "a i = 1"
+  {
+    assume "a i = 1"
     then have "(\<Sum> j \<in> s. a j) = 0"
       using asms by auto
     then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
       using setsum_nonneg_0[where 'b=real] asms by fastforce
-    then have ?case using asms by auto }
+    then have ?case using asms by auto
+  }
   moreover
-  { assume asm: "a i \<noteq> 1"
+  {
+    assume asm: "a i \<noteq> 1"
     from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
     have fis: "finite (insert i s)" using asms by auto
     then have ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp
     then have "a i < 1" using asm by auto
     then have i0: "1 - a i > 0" by auto
     let ?a = "\<lambda>j. a j / (1 - a i)"
-    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
-        by fastforce }
+    {
+      fix j
+      assume "j \<in> s"
+      with i0 asms have "?a j \<ge> 0"
+        by fastforce
+    }
     note a_nonneg = this
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     then have "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
@@ -466,51 +544,66 @@
     also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
     also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
     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))"
-      by simp }
+      by simp
+  }
   ultimately show ?case by auto
 qed
 
 lemma convex_on_alt:
   fixes C :: "'a::real_vector set"
   assumes "convex C"
-  shows "convex_on C f =
-  (\<forall> x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1
-      \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
+  shows "convex_on C f \<longleftrightarrow>
+    (\<forall>x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
+      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
 proof safe
   fix x y
   fix \<mu> :: real
   assume asms: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1"
   from this[unfolded convex_on_def, rule_format]
-  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
+  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"
+    by auto
   from this[of "\<mu>" "1 - \<mu>", simplified] asms
-  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y" by auto
+  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+    by auto
 next
-  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"
-  { fix x y
+  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"
+  {
+    fix x y
     fix u v :: real
     assume lasm: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
     then have[simp]: "1 - u = v" by auto
     from asm[rule_format, of x y u]
-    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using lasm by auto
+    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
+      using lasm by auto
   }
-  then show "convex_on C f" unfolding convex_on_def by auto
+  then show "convex_on C f"
+    unfolding convex_on_def by auto
 qed
 
 lemma convex_on_diff:
   fixes f :: "real \<Rightarrow> real"
-  assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y"
+  assumes f: "convex_on I f"
+    and I: "x \<in> I" "y \<in> I"
+    and t: "x < t" "t < y"
   shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
-    "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
+    and "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
 proof -
   def a \<equiv> "(t - y) / (x - y)"
-  with t have "0 \<le> a" "0 \<le> 1 - a" by (auto simp: field_simps)
+  with t have "0 \<le> a" "0 \<le> 1 - a"
+    by (auto simp: field_simps)
   with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
     by (auto simp: convex_on_def)
-  have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps)
-  also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp
-  finally have "f t \<le> a * f x + (1 - a) * f y" using cvx by simp
-  also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
-  finally have "f t - f y \<le> a * (f x - f y)" by simp
+  have "a * x + (1 - a) * y = a * (x - y) + y"
+    by (simp add: field_simps)
+  also have "\<dots> = t"
+    unfolding a_def using `x < t` `t < y` by simp
+  finally have "f t \<le> a * f x + (1 - a) * f y"
+    using cvx by simp
+  also have "\<dots> = a * (f x - f y) + f y"
+    by (simp add: field_simps)
+  finally have "f t - f y \<le> a * (f x - f y)"
+    by simp
   with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
     by (simp add: le_divide_eq divide_le_eq field_simps a_def)
   with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
@@ -520,7 +613,7 @@
 lemma pos_convex_function:
   fixes f :: "real \<Rightarrow> real"
   assumes "convex C"
-    and leq: "\<And>x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
+    and leq: "\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
   shows "convex_on C f"
   unfolding convex_on_alt[OF assms(1)]
   using assms
@@ -529,11 +622,13 @@
   let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
   assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
   then have "1 - \<mu> \<ge> 0" by auto
-  then have xpos: "?x \<in> C" using asm unfolding convex_alt by fastforce
-  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
-            \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
+  then have xpos: "?x \<in> C"
+    using asm unfolding convex_alt by fastforce
+  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) \<ge>
+      \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
     using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
-      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]]
+    by auto
   then have "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
     by (auto simp add: field_simps)
   then show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
@@ -547,9 +642,11 @@
   shows "{x .. y} \<subseteq> C"
 proof safe
   fix z assume zasm: "z \<in> {x .. y}"
-  { assume asm: "x < z" "z < y"
+  {
+    assume asm: "x < z" "z < y"
     let ?\<mu> = "(y - z) / (y - x)"
-    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add: field_simps)
+    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1"
+      using assms asm by (auto simp add: field_simps)
     then have comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
       using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>]
       by (simp add: algebra_simps)
@@ -560,7 +657,8 @@
     also have "\<dots> = z"
       using assms by (auto simp: field_simps)
     finally have "z \<in> C"
-      using comb by auto }
+      using comb by auto
+  }
   note less = this
   show "z \<in> C" using zasm less assms
     unfolding atLeastAtMost_iff le_less by auto
@@ -576,7 +674,8 @@
   shows "f' x * (y - x) \<le> f y - f x"
   using assms
 proof -
-  { fix x y :: real
+  {
+    fix x y :: real
     assume asm: "x \<in> C" "y \<in> C" "y > x"
     then have ge: "y - x > 0" "y - x \<ge> 0" by auto
     from asm have le: "x - y < 0" "x - y \<le> 0" by auto
@@ -627,14 +726,18 @@
     then have "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
     then have "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
       using res by auto } note less_imp = this
-  { fix x y :: real
+  {
+    fix x y :: real
     assume "x \<in> C" "y \<in> C" "x \<noteq> y"
     then have"f y - f x \<ge> f' x * (y - x)"
-    unfolding neq_iff using less_imp by auto } note neq_imp = this
+    unfolding neq_iff using less_imp by auto
+  }
   moreover
-  { fix x y :: real
+  {
+    fix x y :: real
     assume asm: "x \<in> C" "y \<in> C" "x = y"
-    then have "f y - f x \<ge> f' x * (y - x)" by auto }
+    then have "f y - f x \<ge> f' x * (y - x)" by auto
+  }
   ultimately show ?thesis using assms by blast
 qed
 
@@ -645,14 +748,16 @@
     and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
     and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   shows "convex_on C f"
-using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce
+  using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
+  by fastforce
 
 lemma minus_log_convex:
   fixes b :: real
   assumes "b > 1"
   shows "convex_on {0 <..} (\<lambda> x. - log b x)"
 proof -
-  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
+  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
+    using DERIV_log by auto
   then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
     by (auto simp: DERIV_minus)
   have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
@@ -661,9 +766,10 @@
   have "\<And>z :: real. z > 0 \<Longrightarrow>
     DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
     by auto
-  then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
+  then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
+    DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
     unfolding inverse_eq_divide by (auto simp add: mult_assoc)
-  have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
+  have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
     using `b > 1` by (auto intro!:less_imp_le)
   from f''_ge0_imp_convex[OF pos_is_convex,
     unfolded greaterThan_iff, OF f' f''0 f''_ge0]
diff -r e8cce2bd23e5 -r 9f84219715a7 src/HOL/Library/Finite_Lattice.thy
--- a/src/HOL/Library/Finite_Lattice.thy	Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy	Tue Apr 29 22:50:55 2014 +0200
@@ -1,4 +1,6 @@
-(* Author: Alessandro Coglio *)
+(*  Title:      HOL/Library/Finite_Lattice.thy
+    Author:     Alessandro Coglio
+*)
 
 theory Finite_Lattice
 imports Product_Order
@@ -16,29 +18,27 @@
 The resulting class is a subclass of @{class complete_lattice}. *}
 
 class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
-assumes bot_def: "bot = Inf_fin UNIV"
-assumes top_def: "top = Sup_fin UNIV"
-assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
-assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
+  assumes bot_def: "bot = Inf_fin UNIV"
+  assumes top_def: "top = Sup_fin UNIV"
+  assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
+  assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
 
 text {* The definitional assumptions
 on the operators @{const bot} and @{const top}
 of class @{class finite_lattice_complete}
 ensure that they yield bottom and top. *}
 
-lemma finite_lattice_complete_bot_least:
-"(bot::'a::finite_lattice_complete) \<le> x"
-by (auto simp: bot_def intro: Inf_fin.coboundedI)
+lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \<le> x"
+  by (auto simp: bot_def intro: Inf_fin.coboundedI)
 
 instance finite_lattice_complete \<subseteq> order_bot
-proof qed (auto simp: finite_lattice_complete_bot_least)
+  by default (auto simp: finite_lattice_complete_bot_least)
 
-lemma finite_lattice_complete_top_greatest:
-"(top::'a::finite_lattice_complete) \<ge> x"
-by (auto simp: top_def Sup_fin.coboundedI)
+lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
+  by (auto simp: top_def Sup_fin.coboundedI)
 
 instance finite_lattice_complete \<subseteq> order_top
-proof qed (auto simp: finite_lattice_complete_top_greatest)
+  by default (auto simp: finite_lattice_complete_top_greatest)
 
 instance finite_lattice_complete \<subseteq> bounded_lattice ..
 
@@ -47,19 +47,18 @@
 of class @{class finite_lattice_complete}
 ensure that they yield infimum and supremum. *}
 
-lemma finite_lattice_complete_Inf_empty:
-  "Inf {} = (top :: 'a::finite_lattice_complete)"
+lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)"
   by (simp add: Inf_def)
 
-lemma finite_lattice_complete_Sup_empty:
-  "Sup {} = (bot :: 'a::finite_lattice_complete)"
+lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)"
   by (simp add: Sup_def)
 
 lemma finite_lattice_complete_Inf_insert:
   fixes A :: "'a::finite_lattice_complete set"
   shows "Inf (insert x A) = inf x (Inf A)"
 proof -
-  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
+  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _"
+    by (fact comp_fun_idem_inf)
   show ?thesis by (simp add: Inf_def)
 qed
 
@@ -67,87 +66,87 @@
   fixes A :: "'a::finite_lattice_complete set"
   shows "Sup (insert x A) = sup x (Sup A)"
 proof -
-  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
+  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _"
+    by (fact comp_fun_idem_sup)
   show ?thesis by (simp add: Sup_def)
 qed
 
 lemma finite_lattice_complete_Inf_lower:
   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
-  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
+  using finite [of A]
+  by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
 
 lemma finite_lattice_complete_Inf_greatest:
   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
-  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
+  using finite [of A]
+  by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
 
 lemma finite_lattice_complete_Sup_upper:
   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
-  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
+  using finite [of A]
+  by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
 
 lemma finite_lattice_complete_Sup_least:
   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
-  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
+  using finite [of A]
+  by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
 
 instance finite_lattice_complete \<subseteq> complete_lattice
 proof
 qed (auto simp:
- finite_lattice_complete_Inf_lower
- finite_lattice_complete_Inf_greatest
- finite_lattice_complete_Sup_upper
- finite_lattice_complete_Sup_least
- finite_lattice_complete_Inf_empty
- finite_lattice_complete_Sup_empty)
+  finite_lattice_complete_Inf_lower
+  finite_lattice_complete_Inf_greatest
+  finite_lattice_complete_Sup_upper
+  finite_lattice_complete_Sup_least
+  finite_lattice_complete_Inf_empty
+  finite_lattice_complete_Sup_empty)
 
 text {* The product of two finite lattices is already a finite lattice. *}
 
 lemma finite_bot_prod:
   "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
-   Inf_fin UNIV"
-by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
+    Inf_fin UNIV"
+  by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
 
 lemma finite_top_prod:
   "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
-   Sup_fin UNIV"
-by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
+    Sup_fin UNIV"
+  by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
 
 lemma finite_Inf_prod:
   "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
-  Finite_Set.fold inf top A"
-by (metis Inf_fold_inf finite_code)
+    Finite_Set.fold inf top A"
+  by (metis Inf_fold_inf finite_code)
 
 lemma finite_Sup_prod:
   "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
-  Finite_Set.fold sup bot A"
-by (metis Sup_fold_sup finite_code)
+    Finite_Set.fold sup bot A"
+  by (metis Sup_fold_sup finite_code)
 
-instance prod ::
-  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
-proof
-qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
+instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
+  by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
 
 text {* Functions with a finite domain and with a finite lattice as codomain
 already form a finite lattice. *}
 
-lemma finite_bot_fun:
-  "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
-by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
+lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
+  by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
 
-lemma finite_top_fun:
-  "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
-by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
+lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
+  by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
 
 lemma finite_Inf_fun:
   "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
-  Finite_Set.fold inf top A"
-by (metis Inf_fold_inf finite_code)
+    Finite_Set.fold inf top A"
+  by (metis Inf_fold_inf finite_code)
 
 lemma finite_Sup_fun:
   "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
-  Finite_Set.fold sup bot A"
-by (metis Sup_fold_sup finite_code)
+    Finite_Set.fold sup bot A"
+  by (metis Sup_fold_sup finite_code)
 
 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
-proof
-qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
+  by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
 
 
 subsection {* Finite Distributive Lattices *}
@@ -161,22 +160,22 @@
 
 lemma finite_distrib_lattice_complete_sup_Inf:
   "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
-  using finite by (induct A rule: finite_induct)
-    (simp_all add: sup_inf_distrib1)
+  using finite
+  by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)
 
 lemma finite_distrib_lattice_complete_inf_Sup:
   "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
-apply (rule finite_induct)
-apply (metis finite_code)
-apply (metis SUP_empty Sup_empty inf_bot_right)
-apply (metis SUP_insert Sup_insert inf_sup_distrib1)
-done
+  apply (rule finite_induct)
+  apply (metis finite_code)
+  apply (metis SUP_empty Sup_empty inf_bot_right)
+  apply (metis SUP_insert Sup_insert inf_sup_distrib1)
+  done
 
 instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
 proof
 qed (auto simp:
- finite_distrib_lattice_complete_sup_Inf
- finite_distrib_lattice_complete_inf_Sup)
+  finite_distrib_lattice_complete_sup_Inf
+  finite_distrib_lattice_complete_inf_Sup)
 
 text {* The product of two finite distributive lattices
 is already a finite distributive lattice. *}
@@ -184,7 +183,7 @@
 instance prod ::
   (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   finite_distrib_lattice_complete
-..
+  ..
 
 text {* Functions with a finite domain
 and with a finite distributive lattice as codomain
@@ -192,7 +191,7 @@
 
 instance "fun" ::
   (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
-..
+  ..
 
 
 subsection {* Linear Orders *}
@@ -206,8 +205,8 @@
 The resulting class is a subclass of @{class distrib_lattice}. *}
 
 class linorder_lattice = linorder + inf + sup +
-assumes inf_def: "inf x y = (if x \<le> y then x else y)"
-assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
+  assumes inf_def: "inf x y = (if x \<le> y then x else y)"
+  assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
 
 text {* The definitional assumptions
 on the operators @{const inf} and @{const sup}
@@ -216,39 +215,39 @@
 and that they distribute over each other. *}
 
 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
-unfolding inf_def by (metis (full_types) linorder_linear)
+  unfolding inf_def by (metis (full_types) linorder_linear)
 
 lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
-unfolding inf_def by (metis (full_types) linorder_linear)
+  unfolding inf_def by (metis (full_types) linorder_linear)
 
 lemma linorder_lattice_inf_greatest:
   "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
-unfolding inf_def by (metis (full_types))
+  unfolding inf_def by (metis (full_types))
 
 lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
-unfolding sup_def by (metis (full_types) linorder_linear)
+  unfolding sup_def by (metis (full_types) linorder_linear)
 
 lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
-unfolding sup_def by (metis (full_types) linorder_linear)
+  unfolding sup_def by (metis (full_types) linorder_linear)
 
 lemma linorder_lattice_sup_least:
   "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
-by (auto simp: sup_def)
+  by (auto simp: sup_def)
 
 lemma linorder_lattice_sup_inf_distrib1:
   "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
-by (auto simp: inf_def sup_def)
- 
+  by (auto simp: inf_def sup_def)
+
 instance linorder_lattice \<subseteq> distrib_lattice
-proof                                                     
+proof
 qed (auto simp:
- linorder_lattice_inf_le1
- linorder_lattice_inf_le2
- linorder_lattice_inf_greatest
- linorder_lattice_sup_ge1
- linorder_lattice_sup_ge2
- linorder_lattice_sup_least
- linorder_lattice_sup_inf_distrib1)
+  linorder_lattice_inf_le1
+  linorder_lattice_inf_le2
+  linorder_lattice_inf_greatest
+  linorder_lattice_sup_ge1
+  linorder_lattice_sup_ge2
+  linorder_lattice_sup_least
+  linorder_lattice_sup_inf_distrib1)
 
 
 subsection {* Finite Linear Orders *}
@@ -265,6 +264,5 @@
 
 instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
 
-
 end
 
diff -r e8cce2bd23e5 -r 9f84219715a7 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/Permutation.thy	Tue Apr 29 22:50:55 2014 +0200
@@ -22,12 +22,10 @@
 subsection {* Some examples of rule induction on permutations *}
 
 lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
-  by (induct xs == "[]::'a list" ys pred: perm) simp_all
+  by (induct xs == "[] :: 'a list" ys pred: perm) simp_all
 
 
-text {*
-  \medskip This more general theorem is easier to understand!
-  *}
+text {* \medskip This more general theorem is easier to understand! *}
 
 lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
   by (induct pred: perm) simp_all
@@ -41,9 +39,7 @@
 
 subsection {* Ways of making new permutations *}
 
-text {*
-  We can insert the head anywhere in the list.
-*}
+text {* We can insert the head anywhere in the list. *}
 
 lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
   by (induct xs) auto
@@ -72,10 +68,10 @@
 
 subsection {* Further results *}
 
-lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
+lemma perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
   by (blast intro: perm_empty_imp)
 
-lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
+lemma perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
   apply auto
   apply (erule perm_sym [THEN perm_empty_imp])
   done
@@ -83,10 +79,10 @@
 lemma perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
   by (induct pred: perm) auto
 
-lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
+lemma perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
   by (blast intro: perm_sing_imp)
 
-lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
+lemma perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
   by (blast dest: perm_sym)
 
 
@@ -107,16 +103,16 @@
 lemma cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
   by (drule_tac z = z in perm_remove_perm) auto
 
-lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
+lemma cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
   by (blast intro: cons_perm_imp_perm)
 
 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
   by (induct zs arbitrary: xs ys rule: rev_induct) auto
 
-lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
+lemma perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
   by (blast intro: append_perm_imp_perm perm_append1)
 
-lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
+lemma perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
   apply (safe intro!: perm_append2)
   apply (rule append_perm_imp_perm)
   apply (rule perm_append_swap [THEN perm.trans])
@@ -124,21 +120,30 @@
   apply (blast intro: perm_append_swap)
   done
 
-lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
+lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys"
   apply (rule iffI)
-  apply (erule_tac [2] perm.induct, simp_all add: union_ac)
-  apply (erule rev_mp, rule_tac x=ys in spec)
-  apply (induct_tac xs, auto)
-  apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
+  apply (erule_tac [2] perm.induct)
+  apply (simp_all add: union_ac)
+  apply (erule rev_mp)
+  apply (rule_tac x=ys in spec)
+  apply (induct_tac xs)
+  apply auto
+  apply (erule_tac x = "remove1 a x" in allE)
+  apply (drule sym)
+  apply simp
   apply (subgoal_tac "a \<in> set x")
   apply (drule_tac z = a in perm.Cons)
-  apply (erule perm.trans, rule perm_sym, erule perm_remove)
-  apply (drule_tac f=set_of in arg_cong, simp)
+  apply (erule perm.trans)
+  apply (rule perm_sym)
+  apply (erule perm_remove)
+  apply (drule_tac f=set_of in arg_cong)
+  apply simp
   done
 
 lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
-  apply (insert surj_multiset_of, drule surjD)
+  apply (insert surj_multiset_of)
+  apply (drule surjD)
   apply (blast intro: sym)+
   done
 
@@ -158,15 +163,16 @@
    apply simp_all
   apply (subgoal_tac "a \<in> set (remdups ys)")
    prefer 2 apply (metis set_simps(2) insert_iff set_remdups)
-  apply (drule split_list) apply(elim exE conjE)
-  apply (drule_tac x=list in spec) apply(erule impE) prefer 2
-   apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
+  apply (drule split_list) apply (elim exE conjE)
+  apply (drule_tac x = list in spec) apply (erule impE) prefer 2
+   apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2
     apply simp
     apply (subgoal_tac "a # list <~~> a # ysa @ zs")
      apply (metis Cons_eq_appendI perm_append_Cons trans)
     apply (metis Cons Cons_eq_appendI distinct.simps(2)
       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
-   apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
+   apply (subgoal_tac "set (a # list) =
+      set (ysa @ a # zs) \<and> distinct (a # list) \<and> distinct (ysa @ a # zs)")
     apply (fastforce simp add: insert_ident)
    apply (metis distinct_remdups set_remdups)
    apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
@@ -176,15 +182,17 @@
    apply (rule length_remdups_leq)
   done
 
-lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> (set x = set y)"
+lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
 
 lemma permutation_Ex_bij:
   assumes "xs <~~> ys"
   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
-using assms proof induct
+  using assms
+proof induct
   case Nil
-  then show ?case unfolding bij_betw_def by simp
+  then show ?case
+    unfolding bij_betw_def by simp
 next
   case (swap y x l)
   show ?case
@@ -192,14 +200,15 @@
     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
       by (auto simp: bij_betw_def)
     fix i
-    assume "i < length(y#x#l)"
+    assume "i < length (y # x # l)"
     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
   qed
 next
   case (Cons xs ys z)
-  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
-    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
+  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}"
+    and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)"
+    by blast
   let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
   show ?case
   proof (intro exI[of _ ?f] allI conjI impI)
@@ -214,21 +223,24 @@
         by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
     qed (auto simp: bij_betw_def)
     fix i
-    assume "i < length (z#xs)"
+    assume "i < length (z # xs)"
     then show "(z # xs) ! i = (z # ys) ! (?f i)"
       using perm by (cases i) auto
   qed
 next
   case (trans xs ys zs)
-  then obtain f g where
-    bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
-    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
+  then obtain f g
+    where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}"
+    and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)"
+    by blast
   show ?case
   proof (intro exI[of _ "g \<circ> f"] conjI allI impI)
     show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
       using bij by (rule bij_betw_trans)
-    fix i assume "i < length xs"
-    with bij have "f i < length ys" unfolding bij_betw_def by force
+    fix i
+    assume "i < length xs"
+    with bij have "f i < length ys"
+      unfolding bij_betw_def by force
     with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
       using trans(1,3)[THEN perm_length] perm by auto
   qed