1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 module State_manager:sig
11 val neutralize_state:unit->unit
19 binders, infixes, and prefixes add on July 18, 2010.
23 Bring conversions back to the following state of hol_version 2.20+ 100110:
26 val it : (string * (term * conv)) list =
27 [("FUN_ONEPATTERN_CONV", (`_FUNCTION (\y z. P y z) x`, <fun>));
28 ("MATCH_ONEPATTERN_CONV", (`_MATCH x (\y z. P y z)`, <fun>));
29 ("FUN_SEQPATTERN_CONV", (`_FUNCTION (_SEQPATTERN r s) x`, <fun>));
30 ("MATCH_SEQPATTERN_CONV", (`_MATCH x (_SEQPATTERN r s)`, <fun>));
31 ("GEN_BETA_CONV", (`GABS (\a. b) c`, <fun>))]
33 We cannot restore the list above if someone changes it before this file is read.
34 The following checking can easily be defeated. An honor system is in place. *)
37 let neutralize_basic_convs =
38 let bc = basic_convs() in
39 let msg = "conversions beyond hol_version 2.20+ 100110. Cannot neutralize state" in
40 let original=["FUN_ONEPATTERN_CONV"; "MATCH_ONEPATTERN_CONV";
41 "FUN_SEQPATTERN_CONV";
42 "MATCH_SEQPATTERN_CONV"; "GEN_BETA_CONV"] in
43 let _ = if not(List.length(bc)=5) then failwith ("Added "^msg) in
44 let _ = if not(map fst bc=original) then failwith ("Changed "^msg) in
45 fun () -> set_basic_convs(bc);;
50 val rewrites : thm list =
51 [|- FST (x,y) = x; |- SND (x,y) = y; |- FST x,SND x = x;
52 |- (if x = x then y else z) = y; |- (if T then t1 else t2) = t1;
53 |- (if F then t1 else t2) = t2; |- ~ ~t <=> t; |- (@y. y = x) = x;
54 |- x = x <=> T; |- (T <=> t) <=> t; |- (t <=> T) <=> t;
55 |- (F <=> t) <=> ~t; |- (t <=> F) <=> ~t; |- ~T <=> F; |- ~F <=> T;
56 |- T /\ t <=> t; |- t /\ T <=> t; |- F /\ t <=> F; |- t /\ F <=> F;
57 |- t /\ t <=> t; |- T \/ t <=> T; |- t \/ T <=> T; |- F \/ t <=> t;
58 |- t \/ F <=> t; |- t \/ t <=> t; |- T ==> t <=> t; |- t ==> T <=> T;
59 |- F ==> t <=> T; |- t ==> t <=> T; |- t ==> F <=> ~t; |- (!x. t) <=> t;
60 |- (?x. t) <=> t; |- (\x. f x) y = f y; |- x = x ==> p <=> p]
62 Again, we do not really check that this list is the one above.
65 let neutralize_basic_rewrites=
66 let bw = basic_rewrites() in
67 let msg = "Added rewrites beyond hol_version 2.20+ 100110. Cannot neutralize" in
68 let _ = if not(List.length(bw)=34) then failwith msg in
69 fun () -> set_basic_rewrites(bw);;
74 [|- (!x. ~(x = a) ==> f x = g x)
75 ==> (((\x. f x) --> l) (at a within s) <=> (g --> l) (at a within s));
76 |- (!x. ~(x = a) ==> f x = g x)
77 ==> (((\x. f x) --> l) (at a) <=> (g --> l) (at a));
78 |- (!x. x IN s ==> f x = g x) ==> product s (\i. f i) = product s g;
79 |- (!i. a <= i /\ i <= b ==> f i = g i)
80 ==> product (a..b) (\i. f i) = product (a..b) g;
81 |- (!x. p x ==> f x = g x)
82 ==> product {y | p y} (\i. f i) = product {y | p y} g;
83 |- (!x. x IN s ==> f x = g x) ==> vsum s (\i. f i) = vsum s g;
84 |- (!i. a <= i /\ i <= b ==> f i = g i)
85 ==> vsum (a..b) (\i. f i) = vsum (a..b) g;
86 |- (!x. p x ==> f x = g x) ==> vsum {y | p y} (\i. f i) = vsum {y | p y} g;
87 |- (!x. x IN s ==> f x = g x) ==> sum s (\i. f i) = sum s g;
88 |- (!i. a <= i /\ i <= b ==> f i = g i)
89 ==> sum (a..b) (\i. f i) = sum (a..b) g;
90 |- (!x. p x ==> f x = g x) ==> sum {y | p y} (\i. f i) = sum {y | p y} g;
91 |- (!x. x IN s ==> f x = g x) ==> nsum s (\i. f i) = nsum s g;
92 |- (!i. a <= i /\ i <= b ==> f i = g i)
93 ==> nsum (a..b) (\i. f i) = nsum (a..b) g;
94 |- (!x. p x ==> f x = g x) ==> nsum {y | p y} (\i. f i) = nsum {y | p y} g;
98 ==> (if g then t else e) = (if g' then t' else e');
99 |- (p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')]
104 let neutralize_basic_congs=
105 let bc = basic_congs() in
106 let msg = "Added "^string_of_int(List.length bc)^
107 " congruences. Cannot neutralize. " in
108 let _ = if not(List.length(bc)=16) then
109 (let _ = map print_thm bc in failwith msg) in
110 fun () -> set_basic_congs(bc);;
112 let default_overload_skeletons = (* unchanged since July 31 2009 *)
113 [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
114 ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
115 ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
116 ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
117 ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
118 ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
119 (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
120 ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
123 let neutralize_overload_skeletons()=
124 the_overload_skeletons:= default_overload_skeletons;;
127 let the_default_interface = (* set on Feb 12 2010 *)
128 [("+", ("real_add", `:real->real->real`));
129 ("-", ("real_sub", `:real->real->real`));
130 ("*", ("real_mul", `:real->real->real`));
131 ("/", ("real_div", `:real->real->real`));
132 ("<", ("real_lt", `:real->real->bool`));
133 ("<=", ("real_le", `:real->real->bool`));
134 (">", ("real_gt", `:real->real->bool`));
135 (">=", ("real_ge", `:real->real->bool`));
136 ("--", ("real_neg", `:real->real`));
137 ("pow", ("real_pow", `:real->num->real`));
138 ("inv", ("real_inv", `:real->real`));
139 ("abs", ("real_abs", `:real->real`));
140 ("max", ("real_max", `:real->real->real`));
141 ("min", ("real_min", `:real->real->real`));
142 ("&", ("real_of_num", `:num->real`));
143 ("mod", ("real_mod", `:real->real->real->bool`));
144 ("+", ("vector_add", `:real^N->real^N->real^N`));
145 ("-", ("vector_sub", `:real^N->real^N->real^N`));
146 ("--", ("vector_neg", `:real^N->real^N`));
147 ("norm", ("vector_norm", `:real^N->real`));
148 ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
149 ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
150 ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
151 ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
152 (">=", (">=", `:num->num->bool`));
153 ("divides", ("num_divides", `:num->num->bool`));
154 ("mod", ("num_mod", `:num->num->num->bool`));
155 ("coprime", ("num_coprime", `:num#num->bool`));
156 ("gcd", ("num_gcd", `:num#num->num`));
157 ("+", ("int_add", `:int->int->int`));
158 ("-", ("int_sub", `:int->int->int`));
159 ("*", ("int_mul", `:int->int->int`));
160 ("<", ("int_lt", `:int->int->bool`));
161 ("<=", ("int_le", `:int->int->bool`));
162 (">", ("int_gt", `:int->int->bool`));
163 (">=", ("int_ge", `:int->int->bool`)); ("--", ("int_neg", `:int->int`));
164 ("pow", ("int_pow", `:int->num->int`)); ("abs", ("int_abs", `:int->int`));
165 ("max", ("int_max", `:int->int->int`));
166 ("min", ("int_min", `:int->int->int`));
167 ("&", ("int_of_num", `:num->int`));
168 ("divides", ("int_divides", `:int->int->bool`));
169 ("mod", ("int_mod", `:int->int->int->bool`));
170 ("coprime", ("int_coprime", `:int#int->bool`));
171 ("gcd", ("int_gcd", `:int#int->int`));
172 ("inv", ("complex_inv", `:real^2->real^2`));
173 ("pow", ("complex_pow", `:real^2->num->real^2`));
174 ("/", ("complex_div", `:real^2->real^2->real^2`));
175 ("*", ("complex_mul", `:real^2->real^2->real^2`));
176 ("-", ("vector_sub", `:real^2->real^2->real^2`));
177 ("+", ("vector_add", `:real^2->real^2->real^2`));
178 ("--", ("vector_neg", `:real^2->real^2`));
179 ("vol", ("measure", `:(real^3->bool)->real`));
180 ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
182 ("closed_real_interval", `:(real#real)list->real->bool`));
183 ("real_interval", ("open_real_interval", `:real#real->real->bool`));
184 ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
185 ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
186 ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
187 ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
188 ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
189 ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
190 ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
191 ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
192 ("--", ("matrix_neg", `:real^N^M->real^N^M`));
193 ("dist", ("distance", `:real^N#real^N->real`));
194 ("&", ("hreal_of_num", `:num->hreal`));
195 ("<=>", ("=", `:bool->bool->bool`))];;
197 let neutralize_interface()=
198 the_interface:= the_default_interface;;
200 let set_parsel f g h xl =
201 (let _ = map f (h()) in let _ = map g xl in ());;
203 let neutralize_binders() =
204 let bind = ["\\"; "!"; "?"; "?!"; "@"; "minimal"; "lambda"] in
205 set_parsel unparse_as_binder parse_as_binder binders bind;;
207 let neutralize_prefixes() =
208 let pre = ["~"; "--"; "mod"] in
209 set_parsel unparse_as_prefix parse_as_prefix prefixes pre;;
211 let neutralize_infixes() =
212 let inf = [("<=>", (2, "right")); ("==>", (4, "right")); ("\\/", (6, "right"));
213 ("/\\", (8, "right")); ("==", (10, "right")); ("===", (10, "right"));
214 ("treal_eq", (10, "right")); ("IN", (11, "right"));
215 ("--->", (12, "right")); ("-->", (12, "right")); ("<", (12, "right"));
216 ("<<", (12, "right"));
217 ("<<<", (12, "right")); ("<<=", (12, "right")); ("<=", (12, "right"));
218 ("<=_c", (12, "right"));
219 ("<_c", (12, "right"));
220 ("=", (12, "right")); ("=_c", (12, "right")); (">", (12, "right"));
221 (">=", (12, "right"));
222 (">=_c", (12, "right"));
223 (">_c", (12, "right"));
224 ("HAS_SIZE", (12, "right")); ("PSUBSET", (12, "right"));
225 ("SUBSET", (12, "right")); ("absolutely_integrable_on", (12, "right"));
226 ("absolutely_real_integrable_on", (12, "right"));
227 ("analytic_on", (12, "right")); ("complex_differentiable", (12, "right"));
228 ("continuous", (12, "right")); ("continuous_on", (12, "right"));
229 ("convex_on", (12, "right")); ("differentiable", (12, "right"));
230 ("differentiable_on", (12, "right")); ("divides", (12, "right"));
231 ("division_of", (12, "right")); ("edge_of", (12, "right"));
232 ("exposed_face_of", (12, "right")); ("extreme_point_of", (12, "right"));
233 ("face_of", (12, "right")); ("facet_of", (12, "right"));
234 ("fine", (12, "right")); ("has_complex_derivative", (12, "right"));
235 ("has_derivative", (12, "right")); ("has_integral", (12, "right"));
236 ("has_integral_compact_interval", (12, "right"));
237 ("has_measure", (12, "right")); ("has_real_derivative", (12, "right"));
238 ("has_real_integral", (12, "right")); ("has_real_measure", (12, "right"));
239 ("has_vector_derivative", (12, "right"));
240 ("holomorphic_on", (12, "right")); ("homeomorphic", (12, "right"));
241 ("inseg", (12, "right")); ("integrable_on", (12, "right"));
242 ("limit_point_of", (12, "right")); ("permutes", (12, "right"));
243 ("real_continuous", (12, "right")); ("real_continuous_on", (12, "right"));
244 ("real_convex_on", (12, "right")); ("real_differentiable", (12, "right"));
245 ("real_differentiable_on", (12, "right"));
246 ("real_integrable_on", (12, "right")); ("real_sums", (12, "right"));
247 ("real_uniformly_continuous_on", (12, "right"));
248 ("retract_of", (12, "right")); ("simplex", (12, "right"));
249 ("sums", (12, "right")); ("tagged_division_of", (12, "right"));
250 ("tagged_partial_division_of", (12, "right"));
251 ("treal_le", (12, "right")); ("uniformly_continuous_on", (12, "right"));
252 (",", (14, "right")); ("in_direction", (14, "right"));
253 ("within", (14, "right")); ("..", (15, "right")); ("+", (16, "right"));
254 ("++", (16, "right"));
255 ("+_c", (16, "right")); ("UNION", (16, "right"));
256 ("treal_add", (16, "right")); ("-", (18, "left"));
257 ("DIFF", (18, "left")); ("*", (20, "right"));
258 ("**", (20, "right"));
259 ("*_c", (20, "right")); ("INTER", (20, "right"));
260 ("cross", (20, "right")); ("dot", (20, "right"));
261 ("treal_mul", (20, "right")); ("%", (21, "right"));
262 ("INSERT", (21, "right")); ("DELETE", (21, "left"));
263 ("hull", (21, "left")); ("CROSS", (22, "right"));
264 ("/", (22, "left")); ("DIV", (22, "left"));
265 ("MOD", (22, "left")); ("div", (22, "left")); ("rem", (22, "left"));
266 ("POWER",(24,"right"));
267 ("EXP", (24, "left")); ("cpow", (24, "left")); ("pow", (24, "left"));
268 ("$", (25, "left")); ("o", (26, "right"))]
270 set_parsel (fun (a,_) -> unparse_as_infix a) parse_as_infix infixes inf ;;
274 (* What we cannot neutralize we destroy *)
276 let neutralize_axioms() =
277 if not(List.length(axioms()) =3) then failwith ("Further axioms are not allowed");;
280 let neutralize_state()=
282 current_goalstack := ([]:goalstack);
283 neutralize_overload_skeletons();
284 neutralize_interface();
285 neutralize_basic_congs();
286 neutralize_basic_convs();
287 neutralize_basic_rewrites();
288 neutralize_binders();
289 neutralize_prefixes();
290 neutralize_infixes();