# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1505146058 -3600
# Node ID 93edcbc88536d8254f74e8bc0c633c338eb9d98e
# Parent  435cb8d69e272e83423ee360db6ac316762290fd
new theorem about exposed faces

diff -r 435cb8d69e27 -r 93edcbc88536 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Fri Sep 08 19:37:46 2017 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Mon Sep 11 17:07:38 2017 +0100
@@ -806,6 +806,75 @@
   qed
 qed
 
+lemma exposed_face_of_parallel:
+   "T exposed_face_of S \<longleftrightarrow>
+         T face_of S \<and>
+         (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
+                (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
+                (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+  proof (clarsimp simp: exposed_face_of_def)
+    fix a b
+    assume faceS: "S \<inter> {x. a \<bullet> x = b} face_of S" and Ssub: "S \<subseteq> {x. a \<bullet> x \<le> b}" 
+    show "\<exists>c d. S \<subseteq> {x. c \<bullet> x \<le> d} \<and>
+                S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. c \<bullet> x = d} \<and>
+                (S \<inter> {x. a \<bullet> x = b} \<noteq> {} \<longrightarrow> S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> c \<noteq> 0) \<and>
+                (S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. w + c \<in> affine hull S))"
+    proof (cases "affine hull S \<inter> {x. -a \<bullet> x \<le> -b} = {} \<or> affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}")
+      case True
+      then show ?thesis
+      proof
+        assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
+       then show ?thesis
+         apply (rule_tac x="0" in exI)
+         apply (rule_tac x="1" in exI)
+         using hull_subset by fastforce
+    next
+      assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
+      then show ?thesis
+         apply (rule_tac x="0" in exI)
+         apply (rule_tac x="0" in exI)
+        using Ssub hull_subset by fastforce
+    qed
+  next
+    case False
+    then obtain a' b' where "a' \<noteq> 0" 
+      and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
+      and eq: "affine hull S \<inter> {x. a' \<bullet> x = b'} = affine hull S \<inter> {x. - a \<bullet> x = - b}" 
+      and mem: "\<And>w. w \<in> affine hull S \<Longrightarrow> w + a' \<in> affine hull S"
+      using affine_parallel_slice affine_affine_hull by metis 
+    show ?thesis
+    proof (intro conjI impI allI ballI exI)
+      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}" 
+        for P Q 
+        using hull_subset by fastforce  
+      have "S \<subseteq> {x. ~ (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
+        apply (rule *)
+        apply (simp only: le eq)
+        using Ssub by auto
+      then show "S \<subseteq> {x. - a' \<bullet> x \<le> - b'}"
+        by auto 
+      show "S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. - a' \<bullet> x = - b'}"
+        using eq hull_subset [of S affine] by force
+      show "\<lbrakk>S \<inter> {x. a \<bullet> x = b} \<noteq> {}; S \<inter> {x. a \<bullet> x = b} \<noteq> S\<rbrakk> \<Longrightarrow> - a' \<noteq> 0"
+        using \<open>a' \<noteq> 0\<close> by auto
+      show "w + - a' \<in> affine hull S"
+        if "S \<inter> {x. a \<bullet> x = b} \<noteq> S" "w \<in> affine hull S" for w
+      proof -
+        have "w + 1 *\<^sub>R (w - (w + a')) \<in> affine hull S"
+          using affine_affine_hull mem mem_affine_3_minus that(2) by blast
+        then show ?thesis  by simp
+      qed
+    qed
+  qed
+qed
+next
+  assume ?rhs then show ?lhs
+    unfolding exposed_face_of_def by blast
+qed
+
 subsection\<open>Extreme points of a set: its singleton faces\<close>
 
 definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"