legacy/oldleg/collect_geom_error.ml

   1 (* Moved by Thales from collect_geom.ml on Nov 11, 2008 because of
   2    syntax and proof errors. *)
   3
   4 (* VUONG ANH QUYEN *)
   5 let line_exists = prove
   6 ( ` ? l:real^N ->real^N ->(real^N->bool). ! (u:real^N) v. ~(u = v)
   7   ==> (line (l u v))/\(u IN (l u v))/\(v IN (l u v))/\
   8  (! d:real^N->bool. (line d)/\ (u IN d)/\ (v IN d) ==> d = l u v)`
   9
  10 let pr1 = prove
  11 ( ` ! (t:real) t'. ~(t = t') ==>
  12 ( (&1 - t') / (t - t') * t + (&1 - (&1 - t') / (t - t')) * t' = &1) /\
  13  ((&1 - t') / (t - t') * (&1 - t) + (&1 - (&1 - t') / (t - t')) * (&1 - t') = &0)`,
  14 REPEAT GEN_TAC THEN ABBREV_TAC ` m:real = (&1 - t') / (t - t')` THEN
  15 FIRST_X_ASSUM(LABEL_TAC "m" o GSYM) THEN
  16 ONCE_REWRITE_TAC[REAL_ARITH ` ~(t:real = t') <=> ~(t - t' = &0)`] THEN
  17 DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o (MATCH_MP REAL_DIV_RMUL)) THEN
  18 DISCH_TAC THEN CONJ_TAC THENL
  19 [REWRITE_TAC[ARITH_RULE `m * t + (&1 - m) * t' = m * (t - t') + t'`];
  20  REWRITE_TAC[ARITH_RULE `m * (&1 - t) + (&1 - m) * (&1 - t') = &1 - t' - m * (t - t')`]] THEN
  21 ASM_REWRITE_TAC[] THEN ARITH_TAC) in
  22
  23 let pr2 = prove
  24 (`! (a:real^N) b u v. (a IN aff {u,v})/\(b IN aff {u,v}) ==>(aff {a,b} SUBSET aff {u,v})`,
  25 REPEAT GEN_TAC THEN
  26 DISCH_THEN (MP_TAC o (MATCH_MP (SET_RULE `! (a:A) b (M:A->bool). a IN M /\ b IN M ==> {a,b} SUBSET M`))) THEN
  27 DISCH_THEN (MP_TAC o (MATCH_MP aff_SUBSET)) THEN
  28 REWRITE_TAC[MATCH_MP aff_affine (SPEC_ALL affine_aff)] ) in
  29
  30 let pr3 = prove
  31 (` ! (u:real^N) v a b. ~(u = v)/\ (u IN aff {a,b}) /\ (v IN aff {a,b}) ==> (a IN aff {u,v})`,
  32 REPEAT GEN_TAC THEN REWRITE_TAC[aff_2;IN_ELIM_THM] THEN STRIP_TAC THEN
  33 ASM_CASES_TAC ` t:real = t'` THENL
  34 [ ASM_MESON_TAC[]; EXISTS_TAC ` (&1 - t') / (t - t')` THEN
  35   ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC ] THEN
  36   ONCE_REWRITE_TAC[ VECTOR_ARITH ` ( (m:real^N) + n) + ( p + q) = ( m + p) +( n + q)`] THEN
  37   ONCE_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB ] THEN FIRST_X_ASSUM(MP_TAC o (MATCH_MP pr1)) THEN
  38   MESON_TAC[ VECTOR_ARITH ` a:real^N = &1 % a + &0 % b`] ]) in
  39
  40 let pr4 = prove
  41 ( `! (a:real^N) b u v. ~( u = v )/\ ( u IN aff {a,b})/\ (v IN aff {a,b}) ==> (aff {u,v} = aff {a,b})`,
  42 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN DISCH_TAC THEN CONJ_TAC THENL
  43 [ ASM_MESON_TAC[pr2];MATCH_MP_TAC(pr2)] THEN CONJ_TAC THENL
  44 [ ASM_MESON_TAC[pr3];UNDISCH_TAC `~(u:real^N = v) /\ u IN aff {a, b} /\ v IN aff {a, b}` THEN
  45 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN MESON_TAC[pr3] ] ) in
  46
  47 ABBREV_TAC ` l = (\ (u:real^N) v. aff {u,v})` THEN FIRST_X_ASSUM(LABEL_TAC "l" o GSYM) THEN
  48 EXISTS_TAC `l:real^N ->real^N->(real^N->bool)`  THEN
  49 REPEAT GEN_TAC THEN STRIP_TAC THEN
  50 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
  51 [ ASM_MESON_TAC[line]; MP_TAC(SPEC ` ({u,v} :real^N->bool)` SUBSET_aff) THEN SET_TAC[];
  52   MP_TAC(SPEC ` ({u,v} :real^N->bool)` SUBSET_aff) THEN SET_TAC[];GEN_TAC THEN REWRITE_TAC[line] THEN
  53  STRIP_TAC THEN ASM_MESON_TAC[pr4]]);;
  54
  55 let line_match_def = new_specification ["line_match"] line_exists;;
  56
  57 let line_unique = prove
  58 (`! u:real^N v. ~(u = v) ==> (?! (d:real^N->bool). (line d)/\(u IN d)/\(v IN d))`,
  59 MESON_TAC[line_match_def]);;
  60
  61 let lemma4 = prove
  62 (`! u:real^N v. ~(u=v) ==> aff {u,v} = line_match u v`,
  63 REPEAT GEN_TAC THEN DISCH_TAC THEN
  64 FIRST_ASSUM(MP_TAC o (MATCH_MP line_match_def)) THEN STRIP_TAC THEN
  65 FIRST_ASSUM(MATCH_MP_TAC o (SPEC ` (aff {u, v}):real^N->bool`)) THEN
  66 REPEAT CONJ_TAC THENL
  67   [ ASM_MESON_TAC[line]; MP_TAC(SPEC ` ({u,v} :real^N->bool)` SUBSET_aff) THEN SET_TAC[];
  68   MP_TAC(SPEC ` ({u,v} :real^N->bool)` SUBSET_aff) THEN SET_TAC[]]);;
  69
  70