--- a/src/HOL/Library/Disjoint_Sets.thy Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Wed May 25 16:01:42 2016 +0200
@@ -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"
--- a/src/HOL/Library/Permutations.thy Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Library/Permutations.thy Wed May 25 16:01:42 2016 +0200
@@ -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
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 25 16:01:42 2016 +0200
@@ -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"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed May 25 16:01:42 2016 +0200
@@ -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')
--- a/src/HOL/Multivariate_Analysis/Polytope.thy Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy Wed May 25 16:01:42 2016 +0200
@@ -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)