Lines Matching defs:frontier
5182 val frontier = new_definition ("frontier",
5183 ``frontier s = (closure s) DIFF (interior s)``);
5186 ``!s. closed(frontier s)``,
5187 SIMP_TAC std_ss [frontier, CLOSED_DIFF, CLOSED_CLOSURE, OPEN_INTERIOR]);
5190 ``!s:real->bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))``,
5191 REWRITE_TAC[frontier, INTERIOR_CLOSURE,
5196 a IN frontier s <=> !e. &0 < e ==> (?x. x IN s /\ dist(a,x) < e) /\
5205 ``!s. closed s ==> (frontier s) SUBSET s``,
5206 METIS_TAC[frontier, CLOSURE_CLOSED, DIFF_SUBSET]);
5209 ``frontier {} = {}``,
5210 REWRITE_TAC[frontier, CLOSURE_EMPTY, EMPTY_DIFF]);
5213 ``frontier univ(:real) = {}``,
5214 REWRITE_TAC[frontier, CLOSURE_UNIV, INTERIOR_UNIV] THEN SET_TAC[]);
5217 ``!s:real->bool. (frontier s) SUBSET s <=> closed s``,
5219 REWRITE_TAC[frontier] THEN
5225 ``!s:real->bool. frontier(UNIV DIFF s) = frontier s``,
5226 REWRITE_TAC[frontier, CLOSURE_COMPLEMENT, INTERIOR_COMPLEMENT] THEN
5230 ``!s. ((frontier s) INTER s = {}) <=> open s``,
5235 ``!s t. frontier(s INTER t) SUBSET frontier(s) UNION frontier(t)``,
5236 REPEAT GEN_TAC THEN REWRITE_TAC[frontier, INTERIOR_INTER] THEN
5242 ``!s t:real->bool. frontier(s UNION t) SUBSET frontier s UNION frontier t``,
5248 ``!s. frontier s = univ(:real) DIFF interior(s) DIFF interior(univ(:real) DIFF s)``,
5249 REWRITE_TAC[frontier, CLOSURE_INTERIOR] THEN SET_TAC[]);
5252 ``!s:real->bool. frontier(frontier s) SUBSET frontier s``,
5253 GEN_TAC THEN GEN_REWR_TAC LAND_CONV [frontier] THEN
5258 interior(frontier s) = interior(closure s) DIFF closure(interior s)``,
5260 REWRITE_TAC[GSYM INTERIOR_COMPLEMENT, GSYM INTERIOR_INTER, frontier] THEN
5264 ``!s:real->bool. open s \/ closed s ==> (interior(frontier s) = {})``,
5271 ``!s:real->bool. open s \/ closed s ==> (frontier(frontier s) = frontier s)``,
5272 GEN_TAC THEN GEN_REWR_TAC (RAND_CONV o LAND_CONV) [frontier] THEN STRIP_TAC THEN
5277 ``!s:real->bool. frontier(frontier(frontier s)) = frontier(frontier s)``,
5281 ``!s t x. x IN frontier s /\ x IN interior t ==> x IN frontier(s INTER t)``,
5290 ``!s t:real->bool. frontier(s) UNION frontier(t) =
5291 frontier(s UNION t) UNION frontier(s INTER t) UNION
5292 frontier(s) INTER frontier(t)``,
5297 KNOW_TAC ``((!s t x. x IN frontier s
5298 ==> x IN frontier (s UNION t) \/
5299 x IN frontier (s INTER t) \/
5300 x IN frontier s INTER frontier t) /\
5302 x IN frontier (s UNION t) \/
5303 x IN frontier (s INTER t) \/
5304 x IN frontier s INTER frontier t <=>
5305 x IN frontier (t UNION s) \/
5306 x IN frontier (t INTER s) \/
5307 x IN frontier t INTER frontier s))`` THENL
5310 ASM_CASES_TAC ``(x:real) IN frontier t`` THEN ASM_REWRITE_TAC[IN_INTER] THEN
5323 ==> ~(s INTER frontier t = {})``,
5336 ?t. open t /\ (s = frontier t)``,
5340 ASM_SIMP_TAC std_ss [frontier, CLOSURE_CLOSED, DIFF_EMPTY],
5345 ==> (frontier(s UNION t) = frontier(s) UNION frontier(t))``,
5348 GEN_REWR_TAC RAND_CONV [frontier] THEN
5352 CONJ_TAC THENL [REWRITE_TAC[frontier] THEN SET_TAC[], ALL_TAC] THEN
5359 REWRITE_TAC[frontier, DIFF_SUBSET, GSYM INTERIOR_COMPLEMENT] THENL
5378 ``!s:real->bool. closure s = s UNION frontier s``,
5379 GEN_TAC THEN REWRITE_TAC[frontier] THEN
5385 ``!s:real->bool. frontier(interior s) SUBSET frontier s``,
5386 GEN_TAC THEN REWRITE_TAC[frontier, INTERIOR_INTERIOR] THEN
5391 ``!s:real->bool. frontier(closure s) SUBSET frontier s``,
5392 GEN_TAC THEN REWRITE_TAC[frontier, CLOSURE_CLOSURE] THEN
5397 ``!s:real->bool. s DIFF frontier s = interior s``,
5398 GEN_TAC THEN REWRITE_TAC[frontier] THEN
5405 frontier(s INTER t) SUBSET closure s INTER frontier t UNION
5406 frontier s INTER closure t``,
5407 REPEAT GEN_TAC THEN REWRITE_TAC[frontier, INTERIOR_INTER] THEN
7139 ``!a e. &0 < e ==> (frontier(ball(a,e)) = sphere(a,e))``,
7140 SIMP_TAC std_ss [frontier, sphere, CLOSURE_BALL, INTERIOR_OPEN, OPEN_BALL,
7146 ``!a e. (frontier(cball(a,e)) = sphere(a,e))``,
7147 SIMP_TAC std_ss [frontier, sphere, INTERIOR_CBALL, CLOSED_CBALL, CLOSURE_CLOSED,
8692 ``!s. bounded s ==> compact(frontier s)``,
8693 SIMP_TAC std_ss [frontier, COMPACT_EQ_BOUNDED_CLOSED,
8698 ``!s. compact s ==> compact (frontier s)``,
8702 ``!s:real->bool. bounded s ==> bounded(frontier s)``,
8706 ``!s. compact s ==> frontier s SUBSET s``,
8775 ``!a:real. frontier {a} = {a}``,
8776 REWRITE_TAC[frontier, CLOSURE_SING, INTERIOR_SING, DIFF_EMPTY]);
11525 ==> (frontier {x | a * x <= b} = {x | a * x = b})``,
11530 ASM_SIMP_TAC std_ss [frontier, INTERIOR_HALFSPACE_LE, CLOSURE_CLOSED,
11536 ==> (frontier {x | a * x >= b} = {x | a * x = b})``,
11545 ==> (frontier {x | a * x < b} = {x | a * x = b})``,
11550 ASM_SIMP_TAC std_ss [frontier, CLOSURE_HALFSPACE_LT, INTERIOR_OPEN,
11556 ==> (frontier {x | a * x > b} = {x | a * x = b})``,
14782 ``!a b. frontier(interval[a,b]) = interval[a,b] DIFF interval(a,b)``,
14783 SIMP_TAC std_ss [frontier, INTERIOR_CLOSED_INTERVAL, CLOSURE_CLOSED,
14787 ``!a b. frontier(interval(a,b)) =
14791 ASM_SIMP_TAC std_ss [frontier, CLOSURE_OPEN_INTERVAL, INTERIOR_OPEN,
15625 is_interval s ==> FINITE(frontier s) /\ CARD(frontier s) <= 2``,
17611 ``{x:real | abs x = abs(a:real)} = frontier(cball(0,abs a))``
19595 ==> (closest_point s x) IN frontier s``,
19596 SIMP_TAC std_ss [frontier, IN_DIFF, CLOSEST_POINT_IN_INTERIOR] THEN
19815 DISJOINT s t ==> (setdist(frontier s,t) = setdist(s,t))) /\
19817 DISJOINT s t ==> (setdist(s,frontier t) = setdist(s,t)))``,
19823 SIMP_TAC std_ss [frontier, IN_DIFF, DIFF_SUBSET, SUBSET_REFL] THEN
19841 POP_ASSUM MP_TAC THEN SIMP_TAC std_ss [IN_INTER, frontier, IN_DIFF] THEN
19984 if DISJOINT s t then setdist(frontier s,frontier t) else &0``,
19990 ASM_CASES_TAC ``DISJOINT s (frontier t:real->bool)`` THENL
19994 SIMP_TAC std_ss [frontier, DIFF_SUBSET, SUBSET_REFL, IN_DIFF] THEN
20018 SIMP_TAC std_ss [IN_INTER, GSYM frontier, GSYM IN_DIFF] THEN
20022 ``!s x:real. ~(x IN s) ==> (setdist({x},frontier s) = setdist({x},s))``,
20053 setdist({x},s) = if x IN s then &0 else setdist({x},frontier s)``,