Tutorial/Defining_new_types.ml

   1 needs "Tutorial/Vectors.ml";;
   2
   3 let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir")
   4  (MESON[LEMMA_0] `?x:real^3. ~(x = vec 0)`);;
   5
   6 parse_as_infix("||",(11,"right"));;
   7 parse_as_infix("_|_",(11,"right"));;
   8
   9 let perpdir = new_definition
  10  `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
  11
  12 let pardir = new_definition
  13  `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
  14
  15 let DIRECTION_CLAUSES = prove
  16  (`((!x. P(dest_dir x)) <=> (!x. ~(x = vec 0) ==> P x)) /\
  17    ((?x. P(dest_dir x)) <=> (?x. ~(x = vec 0) /\ P x))`,
  18   MESON_TAC[direction_tybij]);;
  19
  20 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
  21  (`(!x. x || x) /\
  22    (!x y. x || y <=> y || x) /\
  23    (!x y z. x || y /\ y || z ==> x || z)`,
  24   REWRITE_TAC[pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
  25
  26 let DIRECTION_AXIOM_1 = prove
  27  (`!p p'. ~(p || p') ==> ?l. p _|_ l /\ p' _|_ l /\
  28                              !l'. p _|_ l' /\ p' _|_ l' ==> l' || l`,
  29   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN REPEAT STRIP_TAC THEN
  30   MP_TAC(SPECL [`p:real^3`; `p':real^3`] NORMAL_EXISTS) THEN
  31   MATCH_MP_TAC MONO_EXISTS THEN
  32   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
  33
  34 let DIRECTION_AXIOM_2 = prove
  35  (`!l l'. ?p. p _|_ l /\ p _|_ l'`,
  36   REWRITE_TAC[perpdir; DIRECTION_CLAUSES] THEN
  37   MESON_TAC[NORMAL_EXISTS; ORTHOGONAL_SYM]);;
  38
  39 let DIRECTION_AXIOM_3 = prove
  40  (`?p p' p''.
  41         ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
  42         ~(?l. p _|_ l /\ p' _|_ l /\ p'' _|_ l)`,
  43   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN
  44   MAP_EVERY (fun t -> EXISTS_TAC t THEN REWRITE_TAC[LEMMA_0])
  45    [`basis 1 :real^3`; `basis 2 : real^3`; `basis 3 :real^3`] THEN
  46   VEC3_TAC);;
  47
  48 let CROSS_0 = VEC3_RULE `x cross vec 0 = vec 0 /\ vec 0 cross x = vec 0`;;
  49
  50 let DIRECTION_AXIOM_4_WEAK = prove
  51  (`!l. ?p p'. ~(p || p') /\ p _|_ l /\ p' _|_ l`,
  52   REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN REPEAT STRIP_TAC THEN
  53   SUBGOAL_THEN
  54    `orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 2) l /\
  55     ~((l cross basis 1) cross (l cross basis 2) = vec 0) \/
  56     orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 3) l /\
  57     ~((l cross basis 1) cross (l cross basis 3) = vec 0) \/
  58     orthogonal (l cross basis 2) l /\ orthogonal (l cross basis 3) l /\
  59     ~((l cross basis 2) cross (l cross basis 3) = vec 0)`
  60   MP_TAC THENL [POP_ASSUM MP_TAC THEN VEC3_TAC; MESON_TAC[CROSS_0]]);;
  61
  62 let ORTHOGONAL_COMBINE = prove
  63  (`!x a b. a _|_ x /\ b _|_ x /\ ~(a || b)
  64            ==> ?c. c _|_ x /\ ~(a || c) /\ ~(b || c)`,
  65   REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN
  66   REPEAT STRIP_TAC THEN EXISTS_TAC `a + b:real^3` THEN
  67   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
  68
  69 let DIRECTION_AXIOM_4 = prove
  70  (`!l. ?p p' p''. ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
  71                   p _|_ l /\ p' _|_ l /\ p'' _|_ l`,
  72   MESON_TAC[DIRECTION_AXIOM_4_WEAK; ORTHOGONAL_COMBINE]);;
  73
  74 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
  75
  76 let PERPDIR_WELLDEF = prove
  77  (`!x y x' y'. x || x' /\ y || y' ==> (x _|_ y <=> x' _|_ y')`,
  78   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
  79
  80 let perpl,perpl_th =
  81   lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
  82                 "perpl" PERPDIR_WELLDEF;;
  83
  84 let line_lift_thm = lift_theorem line_tybij
  85  (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
  86
  87 let LINE_AXIOM_1 = line_lift_thm DIRECTION_AXIOM_1;;
  88 let LINE_AXIOM_2 = line_lift_thm DIRECTION_AXIOM_2;;
  89 let LINE_AXIOM_3 = line_lift_thm DIRECTION_AXIOM_3;;
  90 let LINE_AXIOM_4 = line_lift_thm DIRECTION_AXIOM_4;;
  91
  92 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
  93  (prove(`?x:line. T`,REWRITE_TAC[]));;
  94
  95 parse_as_infix("on",(11,"right"));;
  96
  97 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
  98
  99 let POINT_CLAUSES = prove
 100  (`((p = p') <=> (dest_point p = dest_point p')) /\
 101    ((!p. P (dest_point p)) <=> (!l. P l)) /\
 102    ((?p. P (dest_point p)) <=> (?l. P l))`,
 103   MESON_TAC[point_tybij]);;
 104
 105 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
 106
 107 let AXIOM_1 = prove
 108  (`!p p'. ~(p = p') ==> ?l. p on l /\ p' on l /\
 109           !l'. p on l' /\ p' on l' ==> (l' = l)`,
 110   POINT_TAC LINE_AXIOM_1);;
 111
 112 let AXIOM_2 = prove
 113  (`!l l'. ?p. p on l /\ p on l'`,
 114   POINT_TAC LINE_AXIOM_2);;
 115
 116 let AXIOM_3 = prove
 117  (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 118     ~(?l. p on l /\ p' on l /\ p'' on l)`,
 119   POINT_TAC LINE_AXIOM_3);;
 120
 121 let AXIOM_4 = prove
 122  (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 123     p on l /\ p' on l /\ p'' on l`,
 124   POINT_TAC LINE_AXIOM_4);;