1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definition: affprops *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
11 module type Affprops_def_type = sig
12 val affprops_goal : term
17 simp_def2 was assumed as an axiom in collect_geom.ml.
19 The first and last clauses were corrected by inserting DISJOINT.
22 flyspeck_needs "leg/AFF_SGN_TAC.hl";;
25 module Affprops : Affprops_def_type = struct
28 let AFF_SGN_TAC = Aff_sgn_tac.AFF_SGN_TAC;;
30 let affprops_goal = `(!a b v0.
31 DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
33 ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
38 x = ta % a + tb % b + t % v0}) /\
46 t = a % x + b % y + c % z}) /\
48 affine hull {x, y, z} =
49 {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z})/\
51 DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
55 x = t2 % v2 + t3 % v3 + t1 % v1}) `;;
57 let affprops_2_1_goal = `!a b v0.
58 DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
60 ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} `;;
62 let affprops_2_1 = prove(affprops_2_1_goal,AFF_SGN_TAC);;
65 let affprops_ge_2_1_goal = `(!a b v0.
66 DISJOINT {a,b} {v0} ==>
71 x = ta % a + tb % b + t % v0})`;;
73 let affprops_ge_2_1 = prove(affprops_ge_2_1_goal,AFF_SGN_TAC);;
75 let affprops_0_3_goal = ` (!x y z.
82 t = a % x + b % y + c % z})`;;
84 let affprops_0_3 = prove(affprops_0_3_goal,REWRITE_TAC[conv0] THEN AFF_SGN_TAC);;
86 let affprops_3_0_goal = ` (!x y z.
87 affine hull {x, y, z} =
88 {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z}) `;;
90 let affprops_3_0 = prove(affprops_3_0_goal,
91 REWRITE_TAC[AFFINE_HULL_3] THEN SET_TAC[]);;
93 let affprops_lt_2_1_goal = ` (!v1 v2 v3.
94 DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
98 x = t2 % v2 + t3 % v3 + t1 % v1}) `;;
100 let affpropos_lt_2_1 = prove(affprops_lt_2_1_goal,AFF_SGN_TAC);;
103 let affprops_goal = `(!a b v0.
104 DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
106 ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
111 x = ta % a + tb % b + t % v0}) /\
119 t = a % x + b % y + c % z}) /\
121 affine hull {x, y, z} =
122 {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z})/\
124 DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
128 x = t2 % v2 + t3 % v3 + t1 % v1}) `;;
130 let affprops = prove(affprops_goal,
131 REWRITE_TAC[affprops_0_3;affprops_3_0 ;affpropos_lt_2_1] THEN
132 REPEAT STRIP_TAC THEN
133 ASM_SIMP_TAC[affprops_2_1;affprops_ge_2_1]);;