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"
```