renamings and refinements
authorpaulson <lp15@cam.ac.uk>
Mon May 09 16:02:23 2016 +0100 (2016-05-09 ago)
changeset 63072eb5d493a9e03
parent 63071 3ca3bc795908
child 63074 c60730295599
child 63075 60a42a4166af
renamings and refinements
src/HOL/Fun.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Fun.thy	Wed May 04 10:19:01 2016 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon May 09 16:02:23 2016 +0100
     1.3 @@ -213,6 +213,12 @@
     1.4  lemma bij_id[simp]: "bij id"
     1.5  by (simp add: bij_betw_def)
     1.6  
     1.7 +lemma bij_uminus:
     1.8 +  fixes x :: "'a :: ab_group_add"
     1.9 +  shows "bij (uminus :: 'a\<Rightarrow>'a)"
    1.10 +unfolding bij_betw_def inj_on_def
    1.11 +by (force intro: minus_minus [symmetric])
    1.12 +
    1.13  lemma inj_onI [intro?]:
    1.14      "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
    1.15  by (simp add: inj_on_def)
    1.16 @@ -228,25 +234,23 @@
    1.17  by (simp add: comp_def inj_on_def)
    1.18  
    1.19  lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
    1.20 -  by (simp add: inj_on_def) blast
    1.21 +  by (auto simp add: inj_on_def)
    1.22  
    1.23  lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
    1.24    inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
    1.25 -apply(unfold inj_on_def)
    1.26 -apply blast
    1.27 -done
    1.28 +unfolding inj_on_def by blast
    1.29  
    1.30  lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
    1.31 -by (unfold inj_on_def, blast)
    1.32 +unfolding inj_on_def by blast
    1.33  
    1.34 -lemma inj_singleton: "inj (%s. {s})"
    1.35 -by (simp add: inj_on_def)
    1.36 +lemma inj_singleton [simp]: "inj_on (\<lambda>x. {x}) A"
    1.37 +  by (simp add: inj_on_def)
    1.38  
    1.39  lemma inj_on_empty[iff]: "inj_on f {}"
    1.40  by(simp add: inj_on_def)
    1.41  
    1.42  lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A"
    1.43 -by (unfold inj_on_def, blast)
    1.44 +unfolding inj_on_def by blast
    1.45  
    1.46  lemma inj_on_Un:
    1.47   "inj_on f (A Un B) =
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed May 04 10:19:01 2016 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
     2.3 @@ -2942,7 +2942,7 @@
     2.4      by (metis aff_dim_translation_eq)
     2.5  qed
     2.6  
     2.7 -lemma aff_dim_univ: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
     2.8 +lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
     2.9    using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
    2.10      dim_UNIV[where 'a="'n::euclidean_space"]
    2.11    by auto
    2.12 @@ -2990,7 +2990,7 @@
    2.13    shows "aff_dim S \<le> int (DIM('n))"
    2.14  proof -
    2.15    have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
    2.16 -    using aff_dim_univ by auto
    2.17 +    using aff_dim_UNIV by auto
    2.18    then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
    2.19      using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
    2.20  qed
    2.21 @@ -3036,7 +3036,7 @@
    2.22    have h0: "S \<subseteq> affine hull S"
    2.23      using hull_subset[of S _] by auto
    2.24    have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
    2.25 -    using aff_dim_univ assms by auto
    2.26 +    using aff_dim_UNIV assms by auto
    2.27    then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
    2.28      using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
    2.29    have h3: "aff_dim S \<le> aff_dim (affine hull S)"
    2.30 @@ -3615,7 +3615,7 @@
    2.31    apply auto
    2.32    done
    2.33  
    2.34 -lemma opein_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
    2.35 +lemma openin_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
    2.36    apply (simp add: rel_interior_def)
    2.37    apply (subst openin_subopen)
    2.38    apply blast
    2.39 @@ -7957,7 +7957,7 @@
    2.40    shows "rel_interior (rel_interior S) = rel_interior S"
    2.41  proof -
    2.42    have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)"
    2.43 -    using opein_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
    2.44 +    using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
    2.45    then show ?thesis
    2.46      using rel_interior_def by auto
    2.47  qed
    2.48 @@ -8164,7 +8164,7 @@
    2.49    have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
    2.50      apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"])
    2.51      using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
    2.52 -      closure_affine_hull[of S] opein_rel_interior[of S]
    2.53 +      closure_affine_hull[of S] openin_rel_interior[of S]
    2.54      apply auto
    2.55      done
    2.56    show ?thesis
    2.57 @@ -8392,7 +8392,7 @@
    2.58      then have "affine hull S = UNIV"
    2.59        by auto
    2.60      then have "aff_dim S = int DIM('n)"
    2.61 -      using aff_dim_affine_hull[of S] by (simp add: aff_dim_univ)
    2.62 +      using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV)
    2.63      then have False
    2.64        using False by auto
    2.65    }
    2.66 @@ -10889,7 +10889,7 @@
    2.67          (if a = 0 \<and> r < 0 then -1 else DIM('a))"
    2.68  proof -
    2.69    have "int (DIM('a)) = aff_dim (UNIV::'a set)"
    2.70 -    by (simp add: aff_dim_univ)
    2.71 +    by (simp add: aff_dim_UNIV)
    2.72    then have "aff_dim (affine hull {x. a \<bullet> x \<le> r}) = DIM('a)" if "(a = 0 \<longrightarrow> r \<ge> 0)"
    2.73      using that by (simp add: affine_hull_halfspace_le not_less)
    2.74    then show ?thesis
    2.75 @@ -11320,7 +11320,7 @@
    2.76      done
    2.77  qed
    2.78  
    2.79 -proposition supporting_hyperplane_relative_boundary:
    2.80 +proposition supporting_hyperplane_rel_boundary:
    2.81    fixes S :: "'a::euclidean_space set"
    2.82    assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S"
    2.83    obtains a where "a \<noteq> 0"
    2.84 @@ -11374,7 +11374,7 @@
    2.85    obtains a where "a \<noteq> 0"
    2.86                and "\<And>y. y \<in> closure S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y"
    2.87                and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"
    2.88 -using supporting_hyperplane_relative_boundary [of "closure S" x]
    2.89 +using supporting_hyperplane_rel_boundary [of "closure S" x]
    2.90  by (metis assms convex_closure convex_rel_interior_closure)
    2.91  
    2.92  subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
    2.93 @@ -11501,7 +11501,7 @@
    2.94        by (simp add: aff_dim_affine_independent indb)
    2.95      then show ?thesis
    2.96        using fbc aff
    2.97 -      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)
    2.98 +      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)
    2.99    qed
   2.100    show ?thesis
   2.101    proof (cases "c = b")
   2.102 @@ -11509,7 +11509,7 @@
   2.103        apply (rule_tac f="{}" in that)
   2.104        using True affc
   2.105        apply (simp_all add: eq [symmetric])
   2.106 -      by (metis aff_dim_univ aff_dim_affine_hull)
   2.107 +      by (metis aff_dim_UNIV aff_dim_affine_hull)
   2.108    next
   2.109      case False
   2.110      have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})"
   2.111 @@ -11525,7 +11525,7 @@
   2.112        have "insert t c = c"
   2.113          using t by blast
   2.114        then show ?thesis
   2.115 -        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)
   2.116 +        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)
   2.117      qed
   2.118      show ?thesis
   2.119        apply (rule_tac f = "(\<lambda>x. affine hull x) ` ((\<lambda>a. c - {a}) ` (c - b))" in that)
     3.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed May 04 10:19:01 2016 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon May 09 16:02:23 2016 +0100
     3.3 @@ -114,6 +114,9 @@
     3.4  lemma linear_zero: "linear (\<lambda>x. 0)"
     3.5    by (simp add: linear_iff)
     3.6  
     3.7 +lemma linear_uminus: "linear uminus"
     3.8 +by (simp add: linear_iff)
     3.9 +
    3.10  lemma linear_compose_setsum:
    3.11    assumes lS: "\<forall>a \<in> S. linear (f a)"
    3.12    shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
    3.13 @@ -1474,6 +1477,9 @@
    3.14  
    3.15  definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
    3.16  
    3.17 +lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
    3.18 +  by (simp add: orthogonal_def)
    3.19 +
    3.20  lemma orthogonal_clauses:
    3.21    "orthogonal a 0"
    3.22    "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
     4.1 --- a/src/HOL/Set.thy	Wed May 04 10:19:01 2016 +0200
     4.2 +++ b/src/HOL/Set.thy	Mon May 09 16:02:23 2016 +0100
     4.3 @@ -1905,13 +1905,16 @@
     4.4  
     4.5  definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
     4.6  
     4.7 +lemma pairwise_subset: "\<lbrakk>pairwise P S; T \<subseteq> S\<rbrakk> \<Longrightarrow> pairwise P T"
     4.8 +  by (force simp: pairwise_def)
     4.9 +
    4.10  definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}"
    4.11  
    4.12 -lemma pairwise_disjoint_empty [simp]: "pairwise disjnt {}"
    4.13 -  by (simp add: pairwise_def disjnt_def)
    4.14 -
    4.15 -lemma pairwise_disjoint_singleton [simp]: "pairwise disjnt {A}"
    4.16 -  by (simp add: pairwise_def disjnt_def)
    4.17 +lemma pairwise_empty [simp]: "pairwise P {}"
    4.18 +  by (simp add: pairwise_def)
    4.19 +
    4.20 +lemma pairwise_singleton [simp]: "pairwise P {A}"
    4.21 +  by (simp add: pairwise_def)
    4.22  
    4.23  hide_const (open) member not_member
    4.24