2 People who are working on the later chapters may use results from earlier chapters. Suppose I want to use
3 GLTVHUM_concl from the file pack/pack_concl.hl before it has been proved.
5 First, create a new definition:
6 let GLTVHUM_concl = mk_eq (`GLTVHUM_concl:bool`,Pack_concl.GLTVHUM_concl);;
9 let mylemma = prove (`GLTVHUM_concl ==> RiemannHypothesis`,AMAZING_TAC);;
13 (* lemma about sup of function on finite set *)
14 let let finite_num_func_attain_max =
16 `! (S:A->bool) (f:A->num). FINITE S /\ ~ (S = {})
17 ==> (? x. x IN S /\ (! y. y IN S ==> f y <= f x))`,
23 ` FINITE (IMAGE (& o(f:A->num)) (S:A->bool)) /\ ~ (IMAGE (& o f) S = {})`
27 (ASM_SIMP_TAC[FINITE_IMAGE]);
29 (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
31 (FIRST_ASSUM(MP_TAC o (MATCH_MP SUP_FINITE)));
32 (CONV_TAC(PAT_CONV `\k. _ IN k /\ _ ==> _` (REWRITE_CONV[IMAGE])));
33 (PURE_REWRITE_TAC[IN_ELIM_THM]);
38 (FIRST_X_ASSUM(MP_TAC o SPEC ` (& o (f:A->num)) y`));
41 (SUBGOAL_THEN ` (& o (f:A->num)) y IN IMAGE (& o f) S` ASSUME_TAC);
42 (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
43 (EXISTS_TAC `y:A` THEN ASM_SIMP_TAC[]);
45 (ASM_SIMP_TAC[o_THM; REAL_OF_NUM_LE]);