# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464191228 -3600
# Node ID 427cf3baad1682afec454c8bc91b5faa14fc5aa3
# Parent  1aa23fe79b9761914f68bfb26da701f2ee29260a# Parent  6a767355d1a95009739df725ab9c53df1bb2fd59
Merge

diff -r 1aa23fe79b97 -r 427cf3baad16 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Wed May 25 16:39:07 2016 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Wed May 25 16:47:08 2016 +0100
@@ -161,7 +161,7 @@
   assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
   shows   "\<not>finite (UNION A f)"
 proof -
-  def g \<equiv> "\<lambda>x. SOME y. y \<in> f x"
+  define g where "g x = (SOME y. y \<in> f x)" for x
   have g: "g x \<in> f x" if "x \<in> A" for x
     unfolding g_def by (rule someI_ex, insert assms(2) that) blast
   have inj_on_g: "inj_on g A"
diff -r 1aa23fe79b97 -r 427cf3baad16 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Wed May 25 16:39:07 2016 +0100
+++ b/src/HOL/Library/Permutations.thy	Wed May 25 16:47:08 2016 +0100
@@ -943,7 +943,8 @@
 proof -
   from mset_eq have [simp]: "length xs = length ys"
     by (rule mset_eq_length)
-  def indices_of \<equiv> "\<lambda>(x::'a) xs. {i. i < length xs \<and> x = xs ! i}"
+  define indices_of :: "'a \<Rightarrow> 'a list \<Rightarrow> nat set"
+    where "indices_of x xs = {i. i < length xs \<and> x = xs ! i}" for x xs
   have indices_of_subset: "indices_of x xs \<subseteq> {..<length xs}" for x xs
     unfolding indices_of_def by blast
   have [simp]: "finite (indices_of x xs)" for x xs
@@ -961,7 +962,7 @@
   hence "\<exists>f. \<forall>x\<in>set xs. bij_betw (f x) (indices_of x xs) (indices_of x ys)"
     by (rule bchoice)
   then guess f .. note f = this
-  def g \<equiv> "\<lambda>i. if i < n then f (xs ! i) i else i"
+  define g where "g i = (if i < n then f (xs ! i) i else i)" for i
 
   have bij_f: "bij_betw (\<lambda>i. f (xs ! i) i) (indices_of x xs) (indices_of x ys)"
     if x: "x \<in> set xs" for x
diff -r 1aa23fe79b97 -r 427cf3baad16 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed May 25 16:39:07 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed May 25 16:47:08 2016 +0100
@@ -11457,7 +11457,7 @@
       using span_finite [OF \<open>finite B\<close>] by blast
     have "\<And>c v. \<lbrakk>(\<Sum>v\<in>C. c v *\<^sub>R v) = 0; v \<in> C\<rbrakk> \<Longrightarrow> c v = 0"
       using independent_explicit \<open>independent C\<close> by blast
-    def cc \<equiv> "(\<lambda>x. if x \<in> B then a x + e x else a x)"
+    define cc where "cc x = (if x \<in> B then a x + e x else a x)" for x
     have [simp]: "C \<inter> B = B" "D \<inter> B = B" "C \<inter> - B = C-D" "B \<inter> (D - C) = {}"
       using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> Beq by blast+
     have f2: "(\<Sum>v\<in>C \<inter> D. e v *\<^sub>R v) = (\<Sum>v\<in>D - C. a v *\<^sub>R v)"
@@ -11701,7 +11701,7 @@
   case (insert a T)
   have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     using insert by (simp add: pairwise_def orthogonal_def)
-  def a' \<equiv> "a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
+  define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
   obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
              and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
     apply (rule exE [OF insert.IH [of "insert a' S"]])
@@ -11875,7 +11875,7 @@
   case True
   then obtain u v where "u \<in> S" "v \<in> S" "a \<bullet> u \<le> b" "a \<bullet> v > b"
     using assms by (auto simp: not_le)
-  def \<eta> \<equiv> "u + ((b - a \<bullet> u) / (a \<bullet> v - a \<bullet> u)) *\<^sub>R (v - u)"
+  define \<eta> where "\<eta> = u + ((b - a \<bullet> u) / (a \<bullet> v - a \<bullet> u)) *\<^sub>R (v - u)"
   have "\<eta> \<in> S"
     by (simp add: \<eta>_def \<open>u \<in> S\<close> \<open>v \<in> S\<close> \<open>affine S\<close> mem_affine_3_minus)
   moreover have "a \<bullet> \<eta> = b"
diff -r 1aa23fe79b97 -r 427cf3baad16 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed May 25 16:39:07 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed May 25 16:47:08 2016 +0100
@@ -978,8 +978,8 @@
     using \<open>independent B'\<close>
     by (rule independentD_unique[OF _ X(2) X(1)]) (auto intro: X simp: X(3)[symmetric])
 
-  def f' \<equiv> "\<lambda>y. if y \<in> B then f y else 0"
-  def g \<equiv> "\<lambda>y. \<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R f' x"
+  define f' where "f' y = (if y \<in> B then f y else 0)" for y
+  define g where "g y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R f' x)" for y
 
   have g_f': "x \<in> B' \<Longrightarrow> g x = f' x" for x
     by (auto simp: g_def X_B')
diff -r 1aa23fe79b97 -r 427cf3baad16 src/HOL/Multivariate_Analysis/Polytope.thy
--- a/src/HOL/Multivariate_Analysis/Polytope.thy	Wed May 25 16:39:07 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy	Wed May 25 16:47:08 2016 +0100
@@ -186,7 +186,7 @@
     case True with \<open>b \<in> T\<close> show ?thesis by blast
   next
     case False
-    def d \<equiv> "b + (e / norm(b - c)) *\<^sub>R (b - c)"
+    define d where "d = b + (e / norm(b - c)) *\<^sub>R (b - c)"
     have "d \<in> cball b e \<inter> affine hull u"
       using \<open>e > 0\<close> \<open>b \<in> u\<close> \<open>c \<in> u\<close>
       by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False)
@@ -299,7 +299,7 @@
     obtain u where "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> convex hull T" "x \<noteq> y" and weq: "w = (1 - u) *\<^sub>R x + u *\<^sub>R y"
                and u01: "0 < u" "u < 1"
       using w by (auto simp: open_segment_image_interval split: if_split_asm)
-    def c \<equiv> "\<lambda>i. (1 - u) * a i + u * b i"
+    define c where "c i = (1 - u) * a i + u * b i" for i
     have cge0: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> c i"
       using a b u01 by (simp add: c_def)
     have sumc1: "setsum c S = 1"
@@ -325,7 +325,7 @@
         done
     next
       case False
-      def k \<equiv> "setsum c (S - T)"
+      define k where "k = setsum c (S - T)"
       have "k > 0" using False
         unfolding k_def by (metis DiffD1 antisym_conv cge0 setsum_nonneg not_less)
       have weq_sumsum: "w = setsum (\<lambda>x. c x *\<^sub>R x) T + setsum (\<lambda>x. c x *\<^sub>R x) (S - T)"
@@ -431,7 +431,7 @@
   then obtain c where c:
        "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
     by metis
-  def d \<equiv> "rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
+  define d where "d = rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
   have [simp]: "d 0 = {c {}}"
     by (simp add: d_def)
   have dSuc [simp]: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
@@ -1047,7 +1047,7 @@
     then obtain m where "m \<in> S" and m: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> m \<le> a \<bullet> y"
       using continuous_attains_inf [of S "\<lambda>x. a \<bullet> x"] \<open>compact S\<close> \<open>u \<in> S\<close>
       by auto
-    def T \<equiv> "S \<inter> {x. a \<bullet> x = a \<bullet> m}"
+    define T where "T = S \<inter> {x. a \<bullet> x = a \<bullet> m}"
     have "m \<in> T"
       by (simp add: T_def \<open>m \<in> S\<close>)
     moreover have "compact T"
@@ -1560,7 +1560,7 @@
       using x by (auto simp: mem_rel_interior_ball)
     then have ins: "\<And>y. \<lbrakk>norm (x - y) < e; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
       by (metis IntI subsetD dist_norm mem_ball)
-    def \<xi> \<equiv> "min (1/2) (e / 2 / norm(z - x))"
+    define \<xi> where "\<xi> = min (1/2) (e / 2 / norm(z - x))"
     have "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) = norm (\<xi> *\<^sub>R (x - z))"
       by (simp add: \<xi>_def algebra_simps norm_mult)
     also have "... = \<xi> * norm (x - z)"
@@ -1679,7 +1679,7 @@
                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)"
                    (is "?Q f0")
     by (force simp: polyhedron_Int_affine_parallel)
-  def n \<equiv> "LEAST n. \<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
+  define n where "n = (LEAST n. \<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F)"
   have nf: "\<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
     apply (simp add: n_def)
     apply (rule LeastI [where k = "card f0"])
@@ -1755,8 +1755,8 @@
       using faceq that by blast
     also have "... < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
     finally have xltz: "a h \<bullet> x < a h \<bullet> z" .
-    def l \<equiv> "(b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
-    def w \<equiv> "(1 - l) *\<^sub>R x + l *\<^sub>R z"
+    define l where "l = (b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
+    define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z"
     have "0 < l" "l < 1"
       using able xltz \<open>b h < a h \<bullet> z\<close> \<open>h \<in> F\<close>
       by (auto simp: l_def divide_simps)
@@ -1808,9 +1808,11 @@
         next
           case False
           then obtain h' where h': "h' \<in> F - {h}" by auto
-          def inff \<equiv> "INF j:F - {h}. if 0 < a j \<bullet> y - a j \<bullet> w
-                                      then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
-                                      else 1"
+          define inff where "inff =
+            (INF j:F - {h}.
+              if 0 < a j \<bullet> y - a j \<bullet> w
+              then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
+              else 1)"
           have "0 < inff"
             apply (simp add: inff_def)
             apply (rule finite_imp_less_Inf)
@@ -1843,7 +1845,7 @@
           ultimately show ?thesis
             by (blast intro: that)
         qed
-        def c \<equiv> "(1 - T) *\<^sub>R w + T *\<^sub>R y"
+        define c where "c = (1 - T) *\<^sub>R w + T *\<^sub>R y"
         have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> j" if "j \<in> F" for j
         proof (cases "j = h")
           case True
@@ -2313,18 +2315,18 @@
     case True then show ?thesis by auto
   next
     case False
-    def F \<equiv> "{h. h exposed_face_of S \<and> h \<noteq> {} \<and> h \<noteq> S}"
+    define F where "F = {h. h exposed_face_of S \<and> h \<noteq> {} \<and> h \<noteq> S}"
     have "finite F" by (simp add: fin F_def)
     have hface: "h face_of S"
-                and "\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> h = S \<inter> {x. a \<bullet> x = b}"
-         if "h \<in> F" for h
+      and "\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> h = S \<inter> {x. a \<bullet> x = b}"
+      if "h \<in> F" for h
       using exposed_face_of F_def that by simp_all auto
     then obtain a b where ab:
       "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> S \<subseteq> {x. a h \<bullet> x \<le> b h} \<and> h = S \<inter> {x. a h \<bullet> x = b h}"
       by metis
     have *: "False"
-      if paff: "p \<in> affine hull S" and "p \<notin> S" and
-         pint: "p \<in> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" for p
+      if paff: "p \<in> affine hull S" and "p \<notin> S"
+      and pint: "p \<in> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" for p
     proof -
       have "rel_interior S \<noteq> {}"
         by (simp add: \<open>S \<noteq> {}\<close> \<open>convex S\<close> rel_interior_eq_empty)