new theorem about exposed faces
authorpaulson <lp15@cam.ac.uk>
Mon Sep 11 17:07:38 2017 +0100 (21 months ago)
changeset 6665293edcbc88536
parent 66651 435cb8d69e27
child 66653 52bf9f67a3c9
new theorem about exposed faces
src/HOL/Analysis/Polytope.thy
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Fri Sep 08 19:37:46 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Mon Sep 11 17:07:38 2017 +0100
     1.3 @@ -806,6 +806,75 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma exposed_face_of_parallel:
     1.8 +   "T exposed_face_of S \<longleftrightarrow>
     1.9 +         T face_of S \<and>
    1.10 +         (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
    1.11 +                (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
    1.12 +                (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
    1.13 +  (is "?lhs = ?rhs")
    1.14 +proof
    1.15 +  assume ?lhs then show ?rhs
    1.16 +  proof (clarsimp simp: exposed_face_of_def)
    1.17 +    fix a b
    1.18 +    assume faceS: "S \<inter> {x. a \<bullet> x = b} face_of S" and Ssub: "S \<subseteq> {x. a \<bullet> x \<le> b}" 
    1.19 +    show "\<exists>c d. S \<subseteq> {x. c \<bullet> x \<le> d} \<and>
    1.20 +                S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. c \<bullet> x = d} \<and>
    1.21 +                (S \<inter> {x. a \<bullet> x = b} \<noteq> {} \<longrightarrow> S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> c \<noteq> 0) \<and>
    1.22 +                (S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. w + c \<in> affine hull S))"
    1.23 +    proof (cases "affine hull S \<inter> {x. -a \<bullet> x \<le> -b} = {} \<or> affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}")
    1.24 +      case True
    1.25 +      then show ?thesis
    1.26 +      proof
    1.27 +        assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
    1.28 +       then show ?thesis
    1.29 +         apply (rule_tac x="0" in exI)
    1.30 +         apply (rule_tac x="1" in exI)
    1.31 +         using hull_subset by fastforce
    1.32 +    next
    1.33 +      assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
    1.34 +      then show ?thesis
    1.35 +         apply (rule_tac x="0" in exI)
    1.36 +         apply (rule_tac x="0" in exI)
    1.37 +        using Ssub hull_subset by fastforce
    1.38 +    qed
    1.39 +  next
    1.40 +    case False
    1.41 +    then obtain a' b' where "a' \<noteq> 0" 
    1.42 +      and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
    1.43 +      and eq: "affine hull S \<inter> {x. a' \<bullet> x = b'} = affine hull S \<inter> {x. - a \<bullet> x = - b}" 
    1.44 +      and mem: "\<And>w. w \<in> affine hull S \<Longrightarrow> w + a' \<in> affine hull S"
    1.45 +      using affine_parallel_slice affine_affine_hull by metis 
    1.46 +    show ?thesis
    1.47 +    proof (intro conjI impI allI ballI exI)
    1.48 +      have *: "S \<subseteq> - (affine hull S \<inter> {x. P x}) \<union> affine hull S \<inter> {x. Q x} \<Longrightarrow> S \<subseteq> {x. ~P x \<or> Q x}" 
    1.49 +        for P Q 
    1.50 +        using hull_subset by fastforce  
    1.51 +      have "S \<subseteq> {x. ~ (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
    1.52 +        apply (rule *)
    1.53 +        apply (simp only: le eq)
    1.54 +        using Ssub by auto
    1.55 +      then show "S \<subseteq> {x. - a' \<bullet> x \<le> - b'}"
    1.56 +        by auto 
    1.57 +      show "S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. - a' \<bullet> x = - b'}"
    1.58 +        using eq hull_subset [of S affine] by force
    1.59 +      show "\<lbrakk>S \<inter> {x. a \<bullet> x = b} \<noteq> {}; S \<inter> {x. a \<bullet> x = b} \<noteq> S\<rbrakk> \<Longrightarrow> - a' \<noteq> 0"
    1.60 +        using \<open>a' \<noteq> 0\<close> by auto
    1.61 +      show "w + - a' \<in> affine hull S"
    1.62 +        if "S \<inter> {x. a \<bullet> x = b} \<noteq> S" "w \<in> affine hull S" for w
    1.63 +      proof -
    1.64 +        have "w + 1 *\<^sub>R (w - (w + a')) \<in> affine hull S"
    1.65 +          using affine_affine_hull mem mem_affine_3_minus that(2) by blast
    1.66 +        then show ?thesis  by simp
    1.67 +      qed
    1.68 +    qed
    1.69 +  qed
    1.70 +qed
    1.71 +next
    1.72 +  assume ?rhs then show ?lhs
    1.73 +    unfolding exposed_face_of_def by blast
    1.74 +qed
    1.75 +
    1.76  subsection\<open>Extreme points of a set: its singleton faces\<close>
    1.77  
    1.78  definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"