5 The main thing that works well is the expanded SIMP_TAC, with custom local constants.
7 rehash local simp tac when new theorems are added, rather than have it rebuild with each call.
14 (* experiments in revising proof style *)
18 let section_stack = ref [];;
20 let context = ref [];;
22 let assumption_list = ref [];;
24 let begin_section (s:string) =
25 section_stack := s:: !section_stack;;
27 let get_section() = hd (!section_stack);;
29 let end_section (s:string) =
30 let s1 = hd(!section_stack) in
31 let _ = (s1 = s) or failwith "section" in
32 let _ = section_stack := tl !section_stack in
33 let _ = context := filter (fun (s1,_) -> not(s1 = s)) !context in
37 let _ = context := setify ((get_section(),t) :: !context) in
41 (* from Hales_tactic *)
44 let varl = filter has_stv (setify(frees tm)) in
45 let svarl = map (fun t-> (fst(dest_var t),t)) varl in
46 let fn = fun buff (s,t) -> try (let (_,_,m)= term_match [] t (assoc s gls) in m @ buff)
47 with _ -> failwith ("not found: "^s) in
48 let tyassoc = List.fold_left fn [] svarl in
49 (instantiate ([],[],tyassoc)) tm ;;
52 map (fun (_,t) -> (fst (dest_var t),t)) !context;;
54 let declare_as (v,t) =
55 let v1 = mk_var(v,mk_vartype("?1")) in
56 let t1 = map (fun t -> (fst (dest_var t),t)) (frees t) in
57 declare (retype (t1 @ (get_env())) v1);;
59 let mk_assumption (s,t) = assumption_list := (get_section(),s,retype (get_env()) t) :: !assumption_list;;
61 begin_section "stuff";;
63 declare_as ("V",`packing V`);;
70 mk_assumption ("pV",`packing V`);;
71 mk_assumption ("sV",`saturated V`);;
73 (* Augment simplification theorems. *)
76 let simp_thm_list = ref [];;
77 let add_simp_thm q = simp_thm_list := q::!simp_thm_list;;
78 let get_simp_thms () = (!simp_thm_list);;
81 let local_net_of_thm locals rep th =
83 let lconsts = setify (union locals (freesl (hyp th))) in
84 let matchable = can o term_match lconsts in
86 Comb(Comb(Const("=",_),(Abs(x,Comb(Var(s,ty) as v,x')) as l)),v')
87 when x' = x & v' = v & not(x = v) ->
90 Abs(y,Comb(t,y')) when y = y' & not(free_in y t) ->
91 INSTANTIATE(term_match [] v t) th
92 | _ -> failwith "REWR_CONV (ETA_AX special case)" in
93 enter lconsts (l,(1,conv))
94 | Comb(Comb(Const("=",_),l),r) ->
95 if rep & free_in l r then
96 let th' = EQT_INTRO th in
97 enter lconsts (l,(1,REWR_CONV th'))
98 else if rep & matchable l r & matchable r l then
99 enter lconsts (l,(1,ORDERED_REWR_CONV term_order th))
100 else enter lconsts (l,(1,REWR_CONV th))
101 | Comb(Comb(_,t),Comb(Comb(Const("=",_),l),r)) ->
102 if rep & free_in l r then
103 let th' = DISCH t (EQT_INTRO(UNDISCH th)) in
104 enter lconsts (l,(3,IMP_REWR_CONV th'))
105 else if rep & matchable l r & matchable r l then
106 enter lconsts (l,(3,ORDERED_IMP_REWR_CONV term_order th))
107 else enter lconsts(l,(3,IMP_REWR_CONV th));;
115 EXISTS (mk_exists(v, (concl thm)),v) thm in
116 let ex_shared v thm =
117 let a4 = ASSUME (mk_exists (v,hd(hyp thm))) in
118 let a5 = EXISTS (concl a4,v) thm in
120 let ex_comb local v thm = if (mem v local) then ex_local v thm else ex_shared v thm in
122 if (not (is_imp (concl th))) then th else
123 let (p,q) = dest_imp (concl th) in
124 let (evs,p') = strip_exists p in
125 let a1 = ASSUME p' in
126 let a2 = List.fold_right (ex_comb locals) evs a1 in
127 let a3 = DISCH_ALL a2 in
132 EXISTS (mk_exists(v, (concl thm)),v) thm;;
133 let ex_shared v thm =
134 let a4 = ASSUME (mk_exists (v,hd(hyp thm))) in
135 let a5 = EXISTS (concl a4,v) thm in
137 let ex_comb local v thm = if (mem v local) then ex_local v thm else ex_shared v thm;;
139 let a0 = hd(mk_rewrites true LEAF_SQRT2 []);;
140 post_rewrite [x] a0;;
144 ex_local v (ex_shared x a2);;
146 let a0 = snd(post_rewrite [`V:real^3->bool`] (hd(mk_rewrites true LEAF_SQRT2 [])));;
147 let v = `V:real^3->bool`;;
148 let a1 = fst (EQ_IMP_RULE (REFL a0));;
149 let a2 = UNDISCH a1;;
150 let a3 = EXISTS (mk_exists(v, (concl a2)),v) a2;;
152 let x = `ul:(real^3)list`;;
153 let a4 = ASSUME (mk_exists(x, a0));;
154 let a5 = EXISTS (concl a4,x) a2;;
155 let a6 = CHOOSE(x,a4) a5;;
157 add_simp_thm LEAF_SQRT2;;
158 mk_rewrites true LEAF_SQRT2 [];;
159 add_simp_thm (hd(mk_rewrites true (UNDISCH (SPEC_ALL LEAF_SQRT2)) []));;
164 let evs'= subtract evs locals in
165 let p'' = list_mk_exists (evs',p') in
166 let p''p = (p''-> p) in
167 IMP_TRANS p''p th;; *)
170 let mk_local_rewrites locals thm sofar =
171 let rw = mk_rewrites true thm [] in
172 (map (post_rewrite locals) rw @ sofar);;
176 let local = map snd !context in
177 let rewmaker = mk_local_rewrites local in
178 let cthms = itlist rewmaker thl [] in
179 let net' = itlist (local_net_of_thm local true) cthms (basic_net()) in
180 let net'' = itlist net_of_cong (basic_congs()) net' in
181 Simpset(net'',basic_prover,[],rewmaker);;
185 let LOCAL_SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 8;;
186 let LOCAL_SIMP_CONV thl = LOCAL_SIMPLIFY_CONV (local_basic_ss []) ((get_simp_thms()) @ thl);;
187 let LOCAL_SIMP_RULE thl = CONV_RULE(LOCAL_SIMP_CONV thl);;
188 let LOCAL_SIMP_TAC thl = CONV_TAC(LOCAL_SIMP_CONV thl);;
189 let LOCAL_ASM_SIMP_TAC = ASM LOCAL_SIMP_TAC;;
190 let LOCAL_STEP_TAC () = RULE_ASSUM_TAC (LOCAL_SIMP_RULE (get_simp_thms())) THEN LOCAL_ASM_SIMP_TAC (get_simp_thms());;
193 (* GENERAL TACTIC KEYED TO TERMS *)
196 let act_list = ref [];;
197 let add_actionl p q = act_list := (p,q):: !act_list;;
198 let add_action = unlist add_actionl;;
201 let matchable s t = can(term_match[] s) t;;
202 let some_matchable s tl = exists (matchable s) tl;;
203 let all_matchable sl tl = forall (fun s -> some_matchable s tl) sl;;
206 let pl = map (retype (get_env())) pl in
207 let r = filter (fun (tl,_) -> all_matchable pl tl) !act_list in
208 let _ = (List.length r > 0) or failwith "act -- no match" in
211 let act = unlist actl;;
214 let patl = map (retype (get_env())) patl in
215 let matcher u pat = can (find_term (can (term_match[] pat))) (concl u) in
216 let matches = filter (fun (_,u) -> forall (matcher u) patl) (!thm_list) in
220 let w = whatl patl in
221 let _ = List.length w > 0 or failwith "no patterns" in
224 let get = unlist getl;;
226 add_action `&0 < sqrt x` (GMATCH_SIMP_TAC SQRT_POS_LT);;
227 add_action `&0 <= sqrt x` (GMATCH_SIMP_TAC SQRT_POS_LE);;
228 add_action `sqrt x <= sqrt y` (GMATCH_SIMP_TAC SQRT_MONO_LE_EQ);;
229 add_action `sqrt x < sqrt y` (GMATCH_SIMP_TAC SQRT_MONO_LT_EQ);;
230 add_action `&0 < x * y` (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);;
231 add_action `x * x <= y * y` (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE);;
232 add_action `&0 <= x/y` (GMATCH_SIMP_TAC REAL_LE_DIV);;
233 add_action `&0 <= x * y` (GMATCH_SIMP_TAC REAL_LE_MUL);;
234 add_action `&0 <= x * x` (REWRITE_TAC[ REAL_LE_SQUARE]);;
235 add_action `&0 <= x pow 2` (REWRITE_TAC[ REAL_LE_POW_2]);;
236 add_action `sqrt x pow 2` (GMATCH_SIMP_TAC SQRT_POW_2);;
237 add_action `x /z <= y` (GMATCH_SIMP_TAC REAL_LE_LDIV_EQ);;
238 add_action `&0 <= x pow 2` (REWRITE_TAC[ REAL_LE_POW_2]);;
239 add_action `x < sqrt y` (GMATCH_SIMP_TAC REAL_LT_RSQRT);;
240 add_action `x /z <= y/ z` (GMATCH_SIMP_TAC REAL_LE_DIV2_EQ);;
241 add_action `sqrt(y*y)` (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);;
242 add_action `x * y <= x * z` (GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP);;
243 add_action `x < y/ z` (GMATCH_SIMP_TAC REAL_LT_RDIV_EQ);;
244 add_action `&0 < x/y` (GMATCH_SIMP_TAC REAL_LT_DIV);;
245 add_action `sqrt x * sqrt y` (GMATCH_SIMP_TAC (GSYM SQRT_MUL));;
246 add_action `x * x < y * y` (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE);;
247 add_action `x * y < x * z` (GMATCH_SIMP_TAC REAL_LT_LMUL_EQ);;
248 add_action `x <= y/z` (GMATCH_SIMP_TAC REAL_LE_RDIV_EQ);;
249 add_action `inv y <= inv x` (GMATCH_SIMP_TAC REAL_LE_INV2);;
250 add_action `&0 < inv x` (GMATCH_SIMP_TAC REAL_LT_INV);;
252 add_thm `(x:A) IN {}` NOT_IN_EMPTY;;
253 add_thm `&x < &y`( REAL_OF_NUM_LT);;
254 add_thm `&x <= &y`( REAL_OF_NUM_LE);;
255 add_thm `&0 <= inv x`(REAL_LE_INV_EQ);;
256 add_thm `&0 < inv x`(REAL_LT_INV_EQ);;
257 add_thm `abs(a*b)`(REAL_ABS_MUL);;
258 add_thm `inv (&0) = &0` REAL_INV_0;;
259 add_thm `hl [u0:real^A; u1]` Marchal_cells_3.HL_2;;
261 add_thm `~(n = 0)` (ARITH_RULE `1 < n ==> ~(n = 0)`);;
264 getl [`a:bool`;`inv (&0)`];;
272 (* auto matches pattern anywhere and does a sub1 repeatedly at the end of each proof step *)
275 let LIST_PROPS = map (fun t -> prove_by_refinement(t,[ BY(REWRITE_TAC[Bump.EL_EXPLICIT;set_of_list;LENGTH])]))
277 `!(x:A) y. EL 0 (CONS (x:A) y) = x`;
278 `!(x:A) y. EL 1 (CONS (x:A) y) = EL 0 y`;
279 `!(x:A) y. EL 2 (CONS (x:A) y) = EL 1 y`;
280 `!(x:A) y. EL 3 (CONS (x:A) y) = EL 2 y`;
281 `!(x:A) y. set_of_list (CONS x y) = x INSERT (set_of_list y)`;
282 `set_of_list ([]:(A)list) = {}`;
283 `LENGTH ([]:(A)list) = 0`;
284 `!x y. LENGTH (CONS (x:A) y) = SUC (LENGTH y)`
287 map add_simp_thm LIST_PROPS;;
291 INITIAL_SUBLIST_CONS;
294 LENGTH_TRUNCATE_SIMPLEX;
295 TRUNCATE_SIMPLEX_CONS;
297 TRUNCATE_SIMPLEX_EXPLICIT;
300 let XIN_BARV = prove_by_refinement(
301 `!V u k. u IN barV V k <=> barV V k u`,
308 add_simp_thm XIN_BARV;;
310 let LEAF_BARV = prove_by_refinement(
311 `!V ul. leaf V ul ==> barV V 2 ul`,
314 BY(MESON_TAC[Leaf_cell.leaf;IN])
318 add_simp_thm LEAF_BARV;;
320 add_simp_thm Sphere.sqrt2;;
323 (* has variable in antecedent problem *)
325 let LEAF_SQRT2 = prove_by_refinement(
326 `!V ul. leaf V ul ==> hl ul < sqrt(&2)`,
329 BY(MESON_TAC[Leaf_cell.leaf;IN;Sphere.sqrt2])
335 auto (`EL 0 (CONS (x:A) y)`,EL0_CONS);;
336 auto (`EL 1 (CONS (x:A) y)`,EL1_CONS);;
337 auto (`EL 2 (CONS (x:A) y)`,EL2_CONS);;
338 auto (`EL 3 (CONS (x:A) y)`,EL3_CONS);;
339 auto (`set_of_list (CONS (x:A) y)`,SET_OF_LIST_CONS);;
340 auto (`set_of_list []`,SET_OF_LIST_EMPTY);;
341 auto (`truncate_simplex 0 (CONS x y)`,
342 auto (`truncate_simplex 1 (CONS x y)`,
343 auto (`truncate_simplex 2 (CONS x y)`,
344 auto (`truncate_simplex 3 (CONS x y)`,
345 auto (`truncate_simplex 0 ul = [EL 0 ul]`,
347 auto (`x IN barV V k`)
348 assumption `saturated V`;;
352 add_simp_thm (arith `1 < 2`);;
353 add_simp_thm (LE_REFL);;
355 add_simp_thm Fan.th3a;;
357 let REUHADY = prove_by_refinement(
359 saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
361 sum {X | mcell_set V X /\ {u0,u1} IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2}
362 (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2`,
365 REPEAT WEAK_STRIP_TAC;
366 MATCH_MP_TAC Reuhady.REUHADY1;
367 GEXISTL_TAC [`[u0;u1;v1]`;`[u0;u1;v2]`];
369 TYPIFY `hl [u0;u1] < sqrt(&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
370 INTRO_TAC Rogers.XNHPWAB4 [`V`;`[u0;u1;v1]`;`2`];
372 DISCH_THEN (C INTRO_TAC [`1`;`2`]);
374 TYPIFY `hl [u0;u1;v1] < sqrt (&2)` ENOUGH_TO_SHOW_TAC;
376 BY(LOCAL_STEP_TAC());
377 TYPIFY `~collinear (set_of_list [u0; u1; v1]) /\ ~collinear (set_of_list [u0; u1; v2])` (C SUBGOAL_THEN ASSUME_TAC);
378 BY(ASM_MESON_TAC[Leaf_cell.GBEWYFX]);
380 ASM_SIMP_TAC[Leaf_cell.WEDGE_GE_ALMOST_DISJOINT];
381 TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
382 BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
383 TYPIFY `u0 IN V /\ u1 IN V` (C SUBGOAL_THEN (unlist ASM_REWRITE_TAC));
384 INTRO_TAC Packing3.BARV_SUBSET [`V`;`2`;`[u0;u1;v1]`];
388 ASM_SIMP_TAC[Local_lemmas.AZIM_EQ_0_GE_ALT2];
390 INTRO_TAC Leaf_cell.FCHKUGT [`V`;`u0`;`u1`;`v1`;`v2`];
392 REWRITE_TAC[Leaf_cell.cc_A0];
394 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
396 FIRST_X_ASSUM MP_TAC;
397 GMATCH_SIMP_TAC Collect_geom.IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF;
399 REWRITE_TAC[Collect_geom.aff];
400 DISCH_THEN DISJ_CASES_TAC;
401 BY(ASM_REWRITE_TAC[]);
402 FIRST_X_ASSUM (MP_TAC o (MATCH_MP AFFINE_HULL_3_IMP_COLLINEAR));
405 REPEAT WEAK_STRIP_TAC;
406 MATCH_MP_TAC Leaf_cell.EWYBJUA;
407 TYPIFY `V` EXISTS_TAC;
412 let LEAF_RANKING_LEMMA = prove_by_refinement(
413 `!V ul w0 n. 0 < n /\ packing V /\ saturated V /\
414 s_leaf V ul HAS_SIZE n /\
415 ~collinear {EL 0 ul,EL 1 ul,w0} ==>
416 (?f. IMAGE f (:num) = s_leaf V ul /\
417 (!i. f (i + n) = f i) /\
418 (!i j. i < n /\ j < n /\ i < j ==> azim (EL 0 ul) (EL 1 ul) w0 (f i) < azim (EL 0 ul) (EL 1 ul) w0 (f j)))`,
421 REPEAT WEAK_STRIP_TAC;
422 TYPIFY `(s:real^3->bool) = s_leaf V ul` TYPED_ABBREV_TAC;
423 TYPIFY `!x. x IN s ==> ~(collinear {EL 0 ul,EL 1 ul,x})` (C SUBGOAL_THEN ASSUME_TAC);
424 BY(ASM_MESON_TAC[s_leaf_collinear]);
425 INTRO_TAC STRICT_SORT_FINITE [`\v w. (azim (EL 0 ul) (EL 1 ul) w0 v <= azim (EL 0 ul) (EL 1 ul) w0 w)`;`s`;`n` ];
431 REPEAT WEAK_STRIP_TAC;
432 TYPIFY `azim (EL 0 ul) (EL 1 ul) w0 x = azim (EL 0 ul) (EL 1 ul) w0 y ==> (x = y)` ENOUGH_TO_SHOW_TAC;
433 REPEAT WEAK_STRIP_TAC;
434 FIRST_X_ASSUM MATCH_MP_TAC;
435 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
437 MATCH_MP_TAC Leaf_cell.FCHKUGT;
438 GEXISTL_TAC [`V`;`EL 0 ul`;`EL 1 ul`];
439 REWRITE_TAC[Leaf_cell.cc_A0];
440 REWRITE_TAC[Bump.EL_EXPLICIT];
441 FIRST_ASSUM (C INTRO_TAC [`x`]);
442 FIRST_X_ASSUM (C INTRO_TAC [`y`]);
444 REPEAT WEAK_STRIP_TAC;
445 FIRST_X_ASSUM_ST `azim` MP_TAC;
446 ASM_SIMP_TAC[AZIM_EQ_ALT];
447 BY(ASM_MESON_TAC[Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;s_leaf_leaf]);
448 REPEAT WEAK_STRIP_TAC;
449 TYPIFY `\i. f (SUC (i MOD n))` EXISTS_TAC;
453 REPEAT WEAK_STRIP_TAC;
454 INTRO_TAC MOD_MULT_ADD [`1`;`n`;`i`];
455 REWRITE_TAC[arith `1 * n + i = i + n`];
456 DISCH_THEN SUBST1_TAC;
458 REPEAT WEAK_STRIP_TAC;
459 ASM_SIMP_TAC[MOD_LT];
460 FIRST_X_ASSUM (C INTRO_TAC [`SUC i`;`SUC j`]);
461 REWRITE_TAC[arith `~(a <= b) <=> (b <a)`];
462 DISCH_THEN MATCH_MP_TAC;
463 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
465 REWRITE_TAC[EXTENSION;IMAGE;IN_ELIM_THM;IN_UNIV];
467 MATCH_MP_TAC (TAUT `((a==> b) /\ (b ==> a)) ==> (a = b)`);
469 REPEAT WEAK_STRIP_TAC;
470 TYPIFY `SUC (x' MOD n)` EXISTS_TAC;
471 ASM_REWRITE_TAC[IN_NUMSEG];
472 REWRITE_TAC[arith `1 <= SUC x`];
473 REWRITE_TAC[arith `SUC x <= n <=> x < n`];
474 BY(ASM_MESON_TAC[DIVISION;arith `~(n=0) <=> (0 < n)`]);
475 REPEAT WEAK_STRIP_TAC;
477 TYPIFY `PRE x'` EXISTS_TAC;
479 TYPIFY `PRE x' MOD n = PRE x'` (C SUBGOAL_THEN SUBST1_TAC);
481 FIRST_X_ASSUM_ST `IN` MP_TAC;
482 REWRITE_TAC[IN_NUMSEG];
484 FIRST_X_ASSUM_ST `IN` MP_TAC;
485 REWRITE_TAC[IN_NUMSEG];