# HG changeset patch # User paulson # Date 1462806143 -3600 # Node ID eb5d493a9e03ed4e048f3bc3c6b667046335ba12 # Parent 3ca3bc795908ff9847380afcca1e4692febeea18 renamings and refinements diff -r 3ca3bc795908 -r eb5d493a9e03 src/HOL/Fun.thy --- 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\'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 \ inj_on g (f ` A)" - by (simp add: inj_on_def) blast + by (auto simp add: inj_on_def) lemma inj_on_image_iff: "\ ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y); inj_on f A \ \ 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 (\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) = diff -r 3ca3bc795908 -r eb5d493a9e03 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \ 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) \ 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 \ 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) \ 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 \ 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 \ 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 \ x \ r}) = DIM('a)" if "(a = 0 \ r \ 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 \ S" and xno: "x \ rel_interior S" obtains a where "a \ 0" @@ -11374,7 +11374,7 @@ obtains a where "a \ 0" and "\y. y \ closure S \ a \ x \ a \ y" and "\y. y \ rel_interior S \ a \ x < a \ 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\ Some results on decomposing convex hulls, e.g. simplicial subdivision\ @@ -11501,7 +11501,7 @@ by (simp add: aff_dim_affine_independent indb) then show ?thesis using fbc aff - by (simp add: \\ affine_dependent c\ \b \ c\ aff_dim_affine_independent aff_dim_univ card_Diff_subset of_nat_diff) + by (simp add: \\ affine_dependent c\ \b \ c\ 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: "\ affine_dependent (\a\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 = "(\x. affine hull x) ` ((\a. c - {a}) ` (c - b))" in that) diff -r 3ca3bc795908 -r eb5d493a9e03 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- 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 (\x. 0)" by (simp add: linear_iff) +lemma linear_uminus: "linear uminus" +by (simp add: linear_iff) + lemma linear_compose_setsum: assumes lS: "\a \ S. linear (f a)" shows "linear (\x. setsum (\a. f a x) S)" @@ -1474,6 +1477,9 @@ definition "orthogonal x y \ x \ y = 0" +lemma orthogonal_self: "orthogonal x x \ x = 0" + by (simp add: orthogonal_def) + lemma orthogonal_clauses: "orthogonal a 0" "orthogonal a x \ orthogonal a (c *\<^sub>R x)" diff -r 3ca3bc795908 -r eb5d493a9e03 src/HOL/Set.thy --- 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 \ (\x \ S. \y\ S. x\y \ R x y)" +lemma pairwise_subset: "\pairwise P S; T \ S\ \ pairwise P T" + by (force simp: pairwise_def) + definition disjnt where "disjnt A B \ A \ 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