Tutorial/Changing_proof_style.ml

   1 let fix ts = MAP_EVERY X_GEN_TAC ts;;
   2
   3 let assume lab t =
   4   DISCH_THEN(fun th -> if concl th = t then LABEL_TAC lab th
   5                        else failwith "assume");;
   6
   7 let we're finished tac = tac;;
   8
   9 let suffices_to_prove q tac = SUBGOAL_THEN q (fun th -> MP_TAC th THEN tac);;
  10
  11 let note(lab,t) tac =
  12   SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
  13   DISCH_THEN(fun th -> LABEL_TAC lab th);;
  14
  15 let have t = note("",t);;
  16
  17 let cases (lab,t) tac =
  18   SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
  19   DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
  20
  21 let consider (x,lab,t) tac =
  22   let tm = mk_exists(x,t) in
  23   SUBGOAL_THEN tm (X_CHOOSE_THEN x (LABEL_TAC lab)) THENL [tac; ALL_TAC];;
  24
  25 let trivial = MESON_TAC[];;
  26 let algebra = CONV_TAC NUM_RING;;
  27 let arithmetic = ARITH_TAC;;
  28
  29 let by labs tac = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN tac;;
  30
  31 let using ths tac = MAP_EVERY MP_TAC ths THEN tac;;
  32
  33 let so constr arg tac = constr arg (FIRST_ASSUM MP_TAC THEN tac);;
  34
  35 let NSQRT_2 = prove
  36  (`!p q. p * p = 2 * q * q ==> q = 0`,
  37   suffices_to_prove
  38    `!p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
  39         ==> (!q. p * p = 2 * q * q ==> q = 0)`
  40    (MATCH_ACCEPT_TAC num_WF) THEN
  41   fix [`p:num`] THEN
  42   assume("A") `!m. m < p ==> !q. m * m = 2 * q * q ==> q = 0` THEN
  43   fix [`q:num`] THEN
  44   assume("B") `p * p = 2 * q * q` THEN
  45   so have `EVEN(p * p) <=> EVEN(2 * q * q)` (trivial) THEN
  46   so have `EVEN(p)` (using [ARITH; EVEN_MULT] trivial) THEN
  47   so consider (`m:num`,"C",`p = 2 * m`) (using [EVEN_EXISTS] trivial) THEN
  48   cases ("D",`q < p \/ p <= q`) (arithmetic) THENL
  49    [so have `q * q = 2 * m * m ==> m = 0` (by ["A"] trivial) THEN
  50     so we're finished (by ["B"; "C"] algebra);
  51
  52     so have `p * p <= q * q` (using [LE_MULT2] trivial) THEN
  53     so have `q * q = 0` (by ["B"] arithmetic) THEN
  54     so we're finished (algebra)]);;