# HG changeset patch # User paulson # 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 \ + T face_of S \ + (\a b. S \ {x. a \ x \ b} \ T = S \ {x. a \ x = b} \ + (T \ {} \ T \ S \ a \ 0) \ + (T \ S \ (\w \ affine hull S. (w + a) \ 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 \ {x. a \ x = b} face_of S" and Ssub: "S \ {x. a \ x \ b}" + show "\c d. S \ {x. c \ x \ d} \ + S \ {x. a \ x = b} = S \ {x. c \ x = d} \ + (S \ {x. a \ x = b} \ {} \ S \ {x. a \ x = b} \ S \ c \ 0) \ + (S \ {x. a \ x = b} \ S \ (\w \ affine hull S. w + c \ affine hull S))" + proof (cases "affine hull S \ {x. -a \ x \ -b} = {} \ affine hull S \ {x. - a \ x \ - b}") + case True + then show ?thesis + proof + assume "affine hull S \ {x. - a \ x \ - 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 \ {x. - a \ x \ - 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' \ 0" + and le: "affine hull S \ {x. a' \ x \ b'} = affine hull S \ {x. - a \ x \ - b}" + and eq: "affine hull S \ {x. a' \ x = b'} = affine hull S \ {x. - a \ x = - b}" + and mem: "\w. w \ affine hull S \ w + a' \ affine hull S" + using affine_parallel_slice affine_affine_hull by metis + show ?thesis + proof (intro conjI impI allI ballI exI) + have *: "S \ - (affine hull S \ {x. P x}) \ affine hull S \ {x. Q x} \ S \ {x. ~P x \ Q x}" + for P Q + using hull_subset by fastforce + have "S \ {x. ~ (a' \ x \ b') \ a' \ x = b'}" + apply (rule *) + apply (simp only: le eq) + using Ssub by auto + then show "S \ {x. - a' \ x \ - b'}" + by auto + show "S \ {x. a \ x = b} = S \ {x. - a' \ x = - b'}" + using eq hull_subset [of S affine] by force + show "\S \ {x. a \ x = b} \ {}; S \ {x. a \ x = b} \ S\ \ - a' \ 0" + using \a' \ 0\ by auto + show "w + - a' \ affine hull S" + if "S \ {x. a \ x = b} \ S" "w \ affine hull S" for w + proof - + have "w + 1 *\<^sub>R (w - (w + a')) \ 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\Extreme points of a set: its singleton faces\ definition extreme_point_of :: "['a::real_vector, 'a set] \ bool"