1 (* The first change for toplevel.ml *)
2 needs "Multivariate/vectors.ml";;
3 needs "Examples/floor.ml";;
8 let open_ball = new_definition `open_ball (x:real^3) (r:real)= { y | norm(y-x)< r }`;;
11 (* packing already defined in sphere.hl
12 let packing = new_definition `packing (Lambda:real^3 -> bool) = (!x y. ( x IN Lambda) /\ ( y IN Lambda) /\ ~(x = y) ==> norm(x - y) >= &2 )`;;
15 (* B( x , r , Lambda) *)
16 let ball3_lambda = new_definition ` ball3_lambda (x:real^3) (r:real) (Lambda:real^3 -> bool) = ((open_ball x r ) INTER ( UNIONS ( IMAGE (\v. open_ball v (&1)
18 (* Delta ( Lambda x r) This definition is not good because I don't know where to load the definition of Vol 3 *)
20 let delta_finite = new_definition `delta_finite (x:real^3) (r:real) (Lambda:real^3 -> bool) = (( vol 3 ( ball3_lambda x r Lambda) ) / ( vol 3 (open_ball x r )))`;;
23 let truncated_packing = new_definition ` truncated_packing x r Lambda = Lambda INTER (ball3_lambda x r Lambda) `;;
26 (* Beginning of Proving Lemma 7.1 (lemmaseo) that needs Examples/floor.ml; FLOOR_EQ , VECTOR_SUB_COMPONENT_3 theorem and lemmaseoo proved in following *)
28 g ` packing Lambda ==> FINITE (truncated_packing x r Lambda )`;;
33 (`!(x:real) y. floor x = floor y ==> abs(x - y) < &1`,
34 REPEAT GEN_TAC THEN STRIP_TAC THEN SIMP_TAC[ GSYM REAL_BOUNDS_LT]
35 THEN MP_TAC(SPEC `x:real` FLOOR_FRAC) THEN STRIP_TAC THEN FIRST_X_ASSUM(SUBST1_TAC)
36 THEN MP_TAC(SPEC `y:real` FLOOR_FRAC) THEN STRIP_TAC THEN FIRST_X_ASSUM(SUBST1_TAC)
37 THEN FIRST_X_ASSUM(SUBST1_TAC) THEN REWRITE_TAC[REAL_ARITH `(floor y + frac x) - (floor y + frac y) = frac x - frac y`]
38 THEN UNDISCH_TAC `&0 <= frac x` THEN UNDISCH_TAC `&0 <= frac y` THEN UNDISCH_TAC `frac x < &1` THEN UNDISCH_TAC `frac y < &1`
39 THEN REAL_ARITH_TAC );;
41 let VECTOR_SUB_COMPONENT_3 = prove
42 (`!(x:real^3) (y:real^3). x$1 - y$1 = (x - y)$1 /\ x$2 - y$2 = (x - y)$2 /\ x$3 - y$3 = (x - y)$3`,
43 REPEAT GEN_TAC THEN MP_TAC (ISPECL [`x:real^3`; `y:real^3`; `1`] VECTOR_SUB_COMPONENT) THEN
44 MP_TAC (ISPECL [`x:real^3`; `y:real^3`; `2`] VECTOR_SUB_COMPONENT) THEN
45 MP_TAC (ISPECL [`x:real^3`; `y:real^3`; `3`] VECTOR_SUB_COMPONENT) THEN REWRITE_TAC[DIMINDEX_3] THEN ARITH_TAC);;
47 (`!(p:real^3) x y. (!(v:real^3). f v = ( floor (&2 * (v$1 - p$1)),floor (&2 * (v$2 - p$2)),floor (&2 * (v$3 - p$3)))) /\ norm (x - y) >= &2 ==> ~(f x = f y) `,
48 REPEAT GEN_TAC THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC
49 THEN REPEAT (FIRST_X_ASSUM(MP_TAC o (MATCH_MP FLOOR_EQ)))
50 THEN REWRITE_TAC[REAL_ARITH `(abs (&2 * (x$1 - p$1) - &2 * (y$1 - p$1)) < &1) <=> abs(x$1 - y$1) < &1/ &2` ]
51 THEN REWRITE_TAC[REAL_ARITH `(abs (&2 * (x$2 - p$2) - &2 * (y$2 - p$2)) < &1) <=> abs(x$2 - y$2) < &1/ &2` ]
52 THEN REWRITE_TAC[REAL_ARITH `(abs (&2 * (x$3 - p$3) - &2 * (y$3 - p$3)) < &1) <=> abs(x$3 - y$3) < &1/ &2` ]
53 THEN REWRITE_TAC[VECTOR_SUB_COMPONENT_3] THEN REPEAT STRIP_TAC THEN MP_TAC (ISPEC `x:real^3 - y` NORM_LE_L1)
54 THEN REWRITE_TAC[SUM_3;DIMINDEX_3]
55 THEN UNDISCH_TAC`norm (x:real^3 - y) >= &2`
56 THEN UNDISCH_TAC`abs ((x:real^3 - y)$1) < &1 / &2`
57 THEN UNDISCH_TAC`abs ((x:real^3 - y)$2) < &1 / &2`
58 THEN UNDISCH_TAC`abs ((x:real^3 - y)$3) < &1 / &2`
59 THEN REAL_ARITH_TAC );;
61 g ` !p. (!v. f v = (floor(&2 * ( v$1 - p$1)), floor(&2 * (v$2 - p$2)), floor(&2 * (v$3 - p$3)))) /\ packing Lambda
62 ==> INJ f Lambda (int^3) `;;