src/HOL/Analysis/Polytope.thy
changeset 67613 ce654b0e6d69
parent 67399 eab6ce8368fa
child 67829 2a6ef5ba4822
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -3201,7 +3201,7 @@
     1.4          finite \<C> \<and>
     1.5          (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
     1.6          (\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
     1.7 -        (!S S'. S \<in> \<C> \<and> S' \<in> \<C>
     1.8 +        (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
     1.9                  \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
    1.10  
    1.11  definition triangulation where
    1.12 @@ -3350,7 +3350,7 @@
    1.13        and convex\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> convex C"
    1.14        and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
    1.15        by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
    1.16 -    have in_rel_interior: "(@z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
    1.17 +    have in_rel_interior: "(SOME z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
    1.18          using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
    1.19      have *: "\<exists>T. ~affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
    1.20        if "K \<in> \<U>" for K
    1.21 @@ -3396,7 +3396,7 @@
    1.22          by fastforce
    1.23      qed
    1.24      let ?\<T> = "(\<Union>C \<in> \<N>. \<Union>K \<in> \<U> \<inter> Pow (rel_frontier C).
    1.25 -                     {convex hull (insert (@z. z \<in> rel_interior C) K)})"
    1.26 +                     {convex hull (insert (SOME z. z \<in> rel_interior C) K)})"
    1.27      have "\<exists>\<T>. simplicial_complex \<T> \<and>
    1.28                (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
    1.29                (\<forall>C \<in> \<M>. \<exists>F. F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
    1.30 @@ -3415,9 +3415,9 @@
    1.31              using S face\<U> that by blast
    1.32            moreover have "F \<in> \<U> \<union> ?\<T>"
    1.33              if "F face_of S" "C \<in> \<N>" "K \<in> \<U>" and "K \<subseteq> rel_frontier C"
    1.34 -              and S: "S = convex hull insert (@z. z \<in> rel_interior C) K" for C K
    1.35 +              and S: "S = convex hull insert (SOME z. z \<in> rel_interior C) K" for C K
    1.36            proof -
    1.37 -            let ?z = "@z. z \<in> rel_interior C"
    1.38 +            let ?z = "SOME z. z \<in> rel_interior C"
    1.39              have "?z \<in> rel_interior C"
    1.40                by (simp add: in_rel_interior \<open>C \<in> \<N>\<close>)
    1.41              moreover
    1.42 @@ -3490,13 +3490,13 @@
    1.43              proof -
    1.44                obtain C K
    1.45                  where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
    1.46 -                and Y: "Y = convex hull insert (@z. z \<in> rel_interior C) K"
    1.47 +                and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
    1.48                  using XY by blast
    1.49                have "convex C"
    1.50                  by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
    1.51                have "K \<subseteq> C"
    1.52                  by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
    1.53 -              let ?z = "(@z. z \<in> rel_interior C)"
    1.54 +              let ?z = "(SOME z. z \<in> rel_interior C)"
    1.55                have z: "?z \<in> rel_interior C"
    1.56                  using \<open>C \<in> \<N>\<close> in_rel_interior by blast
    1.57                obtain D where "D \<in> \<S>" "X \<subseteq> D"
    1.58 @@ -3533,11 +3533,11 @@
    1.59              proof -
    1.60                obtain C K D L
    1.61                  where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
    1.62 -                and X: "X = convex hull insert (@z. z \<in> rel_interior C) K"
    1.63 +                and X: "X = convex hull insert (SOME z. z \<in> rel_interior C) K"
    1.64                  and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
    1.65 -                and Y: "Y = convex hull insert (@z. z \<in> rel_interior D) L"
    1.66 +                and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior D) L"
    1.67                  using XY by blast
    1.68 -              let ?z = "(@z. z \<in> rel_interior C)"
    1.69 +              let ?z = "(SOME z. z \<in> rel_interior C)"
    1.70                have z: "?z \<in> rel_interior C"
    1.71                  using \<open>C \<in> \<N>\<close> in_rel_interior by blast
    1.72                have "convex C"
    1.73 @@ -3564,7 +3564,7 @@
    1.74                    by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
    1.75                  have "L \<subseteq> D"
    1.76                    by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
    1.77 -                let ?w = "(@w. w \<in> rel_interior D)"
    1.78 +                let ?w = "(SOME w. w \<in> rel_interior D)"
    1.79                  have w: "?w \<in> rel_interior D"
    1.80                    using \<open>D \<in> \<N>\<close> in_rel_interior by blast
    1.81                  have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
    1.82 @@ -3663,7 +3663,7 @@
    1.83          case False
    1.84          then have "C \<in> \<N>"
    1.85            by (simp add: \<N>_def \<S>_def aff\<M> less_le that)
    1.86 -        let ?z = "@z. z \<in> rel_interior C"
    1.87 +        let ?z = "SOME z. z \<in> rel_interior C"
    1.88          have z: "?z \<in> rel_interior C"
    1.89            using \<open>C \<in> \<N>\<close> in_rel_interior by blast
    1.90          let ?F = "\<Union>K \<in> \<U> \<inter> Pow (rel_frontier C). {convex hull (insert ?z K)}"
    1.91 @@ -3726,7 +3726,7 @@
    1.92        next
    1.93          assume "L \<in> ?\<T>"
    1.94          then obtain C K where "C \<in> \<N>"
    1.95 -          and L: "L = convex hull insert (@z. z \<in> rel_interior C) K"
    1.96 +          and L: "L = convex hull insert (SOME z. z \<in> rel_interior C) K"
    1.97            and K: "K \<in> \<U>" "K \<subseteq> rel_frontier C"
    1.98            by auto
    1.99          then have "convex hull C = C"