development/thales/examples/workshop2010_quyen_example.hl

   1 (*
   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.
   4
   5 First, create a new definition:
   6 let GLTVHUM_concl = mk_eq (`GLTVHUM_concl:bool`,Pack_concl.GLTVHUM_concl);;
   7
   8 Then use it:
   9 let mylemma = prove (`GLTVHUM_concl ==>  RiemannHypothesis`,AMAZING_TAC);;
  10
  11 *)
  12
  13 (* lemma about sup of function on finite set *)
  14 let let finite_num_func_attain_max =
  15 prove_by_refinement(
  16 `! (S:A->bool) (f:A->num). FINITE S /\ ~ (S = {})
  17      ==> (? x. x IN S /\ (! y. y IN S ==> f y <= f x))`,
  18 [
  19   (REPEAT STRIP_TAC);
  20
  21 (* subgoal 1 *)
  22   (SUBGOAL_THEN
  23 ` FINITE (IMAGE (& o(f:A->num)) (S:A->bool)) /\ ~ (IMAGE (& o f) S = {})`
  24 ASSUME_TAC);
  25   CONJ_TAC;
  26 (* subgoal 1.1 *)
  27   (ASM_SIMP_TAC[FINITE_IMAGE]);
  28 (* subgoal 2.1 *)
  29   (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
  30
  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]);
  34   STRIP_TAC;
  35   (EXISTS_TAC `x:A`);
  36   (ASM_SIMP_TAC[]);
  37   (REPEAT STRIP_TAC);
  38   (FIRST_X_ASSUM(MP_TAC o SPEC ` (& o (f:A->num)) y`));
  39
  40 (* subgoal 2 *)
  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[]);
  44
  45     (ASM_SIMP_TAC[o_THM; REAL_OF_NUM_LE]);
  46 ]);;
  47
  48
  49