--- a/src/HOL/Fun.thy Wed May 04 10:19:01 2016 +0200
+++ b/src/HOL/Fun.thy Mon May 09 16:02:23 2016 +0100
@@ -213,6 +213,12 @@
lemma bij_id[simp]: "bij id"
by (simp add: bij_betw_def)
+lemma bij_uminus:
+ fixes x :: "'a :: ab_group_add"
+ shows "bij (uminus :: 'a\<Rightarrow>'a)"
+unfolding bij_betw_def inj_on_def
+by (force intro: minus_minus [symmetric])
+
lemma inj_onI [intro?]:
"(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A"
by (simp add: inj_on_def)
@@ -228,25 +234,23 @@
by (simp add: comp_def inj_on_def)
lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
- by (simp add: inj_on_def) blast
+ by (auto simp add: inj_on_def)
lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
-apply(unfold inj_on_def)
-apply blast
-done
+unfolding inj_on_def by blast
lemma inj_on_contraD: "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"
-by (unfold inj_on_def, blast)
+unfolding inj_on_def by blast
-lemma inj_singleton: "inj (%s. {s})"
-by (simp add: inj_on_def)
+lemma inj_singleton [simp]: "inj_on (\<lambda>x. {x}) A"
+ by (simp add: inj_on_def)
lemma inj_on_empty[iff]: "inj_on f {}"
by(simp add: inj_on_def)
lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A"
-by (unfold inj_on_def, blast)
+unfolding inj_on_def by blast
lemma inj_on_Un:
"inj_on f (A Un B) =
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 04 10:19:01 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon May 09 16:02:23 2016 +0100
@@ -2942,7 +2942,7 @@
by (metis aff_dim_translation_eq)
qed
-lemma aff_dim_univ: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
+lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
dim_UNIV[where 'a="'n::euclidean_space"]
by auto
@@ -2990,7 +2990,7 @@
shows "aff_dim S \<le> int (DIM('n))"
proof -
have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
- using aff_dim_univ by auto
+ using aff_dim_UNIV by auto
then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
qed
@@ -3036,7 +3036,7 @@
have h0: "S \<subseteq> affine hull S"
using hull_subset[of S _] by auto
have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
- using aff_dim_univ assms by auto
+ using aff_dim_UNIV assms by auto
then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
have h3: "aff_dim S \<le> aff_dim (affine hull S)"
@@ -3615,7 +3615,7 @@
apply auto
done
-lemma opein_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
+lemma openin_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
apply (simp add: rel_interior_def)
apply (subst openin_subopen)
apply blast
@@ -7957,7 +7957,7 @@
shows "rel_interior (rel_interior S) = rel_interior S"
proof -
have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)"
- using opein_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
+ using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
then show ?thesis
using rel_interior_def by auto
qed
@@ -8164,7 +8164,7 @@
have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"])
using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
- closure_affine_hull[of S] opein_rel_interior[of S]
+ closure_affine_hull[of S] openin_rel_interior[of S]
apply auto
done
show ?thesis
@@ -8392,7 +8392,7 @@
then have "affine hull S = UNIV"
by auto
then have "aff_dim S = int DIM('n)"
- using aff_dim_affine_hull[of S] by (simp add: aff_dim_univ)
+ using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV)
then have False
using False by auto
}
@@ -10889,7 +10889,7 @@
(if a = 0 \<and> r < 0 then -1 else DIM('a))"
proof -
have "int (DIM('a)) = aff_dim (UNIV::'a set)"
- by (simp add: aff_dim_univ)
+ by (simp add: aff_dim_UNIV)
then have "aff_dim (affine hull {x. a \<bullet> x \<le> r}) = DIM('a)" if "(a = 0 \<longrightarrow> r \<ge> 0)"
using that by (simp add: affine_hull_halfspace_le not_less)
then show ?thesis
@@ -11320,7 +11320,7 @@
done
qed
-proposition supporting_hyperplane_relative_boundary:
+proposition supporting_hyperplane_rel_boundary:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S"
obtains a where "a \<noteq> 0"
@@ -11374,7 +11374,7 @@
obtains a where "a \<noteq> 0"
and "\<And>y. y \<in> closure S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y"
and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"
-using supporting_hyperplane_relative_boundary [of "closure S" x]
+using supporting_hyperplane_rel_boundary [of "closure S" x]
by (metis assms convex_closure convex_rel_interior_closure)
subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
@@ -11501,7 +11501,7 @@
by (simp add: aff_dim_affine_independent indb)
then show ?thesis
using fbc aff
- by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent aff_dim_univ card_Diff_subset of_nat_diff)
+ by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent aff_dim_UNIV card_Diff_subset of_nat_diff)
qed
show ?thesis
proof (cases "c = b")
@@ -11509,7 +11509,7 @@
apply (rule_tac f="{}" in that)
using True affc
apply (simp_all add: eq [symmetric])
- by (metis aff_dim_univ aff_dim_affine_hull)
+ by (metis aff_dim_UNIV aff_dim_affine_hull)
next
case False
have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})"
@@ -11525,7 +11525,7 @@
have "insert t c = c"
using t by blast
then show ?thesis
- by (metis (full_types) add.commute aff_dim_affine_hull aff_dim_insert aff_dim_univ affc affine_dependent_def indc insert_Diff_single t)
+ by (metis (full_types) add.commute aff_dim_affine_hull aff_dim_insert aff_dim_UNIV affc affine_dependent_def indc insert_Diff_single t)
qed
show ?thesis
apply (rule_tac f = "(\<lambda>x. affine hull x) ` ((\<lambda>a. c - {a}) ` (c - b))" in that)
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed May 04 10:19:01 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon May 09 16:02:23 2016 +0100
@@ -114,6 +114,9 @@
lemma linear_zero: "linear (\<lambda>x. 0)"
by (simp add: linear_iff)
+lemma linear_uminus: "linear uminus"
+by (simp add: linear_iff)
+
lemma linear_compose_setsum:
assumes lS: "\<forall>a \<in> S. linear (f a)"
shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
@@ -1474,6 +1477,9 @@
definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
+lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
+ by (simp add: orthogonal_def)
+
lemma orthogonal_clauses:
"orthogonal a 0"
"orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
--- a/src/HOL/Set.thy Wed May 04 10:19:01 2016 +0200
+++ b/src/HOL/Set.thy Mon May 09 16:02:23 2016 +0100
@@ -1905,13 +1905,16 @@
definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
+lemma pairwise_subset: "\<lbrakk>pairwise P S; T \<subseteq> S\<rbrakk> \<Longrightarrow> pairwise P T"
+ by (force simp: pairwise_def)
+
definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}"
-lemma pairwise_disjoint_empty [simp]: "pairwise disjnt {}"
- by (simp add: pairwise_def disjnt_def)
-
-lemma pairwise_disjoint_singleton [simp]: "pairwise disjnt {A}"
- by (simp add: pairwise_def disjnt_def)
+lemma pairwise_empty [simp]: "pairwise P {}"
+ by (simp add: pairwise_def)
+
+lemma pairwise_singleton [simp]: "pairwise P {A}"
+ by (simp add: pairwise_def)
hide_const (open) member not_member