素数全体の集合が上に有界でないこと

g `~(?n. !p. prime p ==> p <= n)` ;;
e( STRIP_TAC THEN ABBREV_TAC `k = FACT n + 1` );;
e( SUBGOAL_THEN `?p. prime p /\ p divides k` MP_TAC );;
e( ASM_MESON_TAC [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME_FACTOR] );;
e( STRIP_TAC THEN FIRST_X_ASSUM (ASSUME_TAC o (UNDISCH o (SPEC `p:num`))) );;
e( ASM_MESON_TAC [DIVIDES_FACT_PRIME; COPRIME_PLUS1; coprime; prime] );;

# g `~(?n. !p. prime p ==> p <= n)` ;;
val it : goalstack = 1 subgoal (1 total)

`~(?n. !p. prime p ==> p <= n)`

# e( STRIP_TAC THEN ABBREV_TAC `k = FACT n + 1` );;
val it : goalstack = 1 subgoal (1 total)

  0 [`!p. prime p ==> p <= n`]
  1 [`FACT n + 1 = k`]

`F`

# e( SUBGOAL_THEN `?p. prime p /\ p divides k` MP_TAC );;
val it : goalstack = 2 subgoals (2 total)

  0 [`!p. prime p ==> p <= n`]
  1 [`FACT n + 1 = k`]

`(?p. prime p /\ p divides k) ==> F`

  0 [`!p. prime p ==> p <= n`]
  1 [`FACT n + 1 = k`]

`?p. prime p /\ p divides k`

# e( ASM_MESON_TAC [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME
_FACTOR] );;
0..0..0..3..8..18..solved at 24
val it : goalstack = 1 subgoal (1 total)

  0 [`!p. prime p ==> p <= n`]
  1 [`FACT n + 1 = k`]

`(?p. prime p /\ p divides k) ==> F`

# e( STRIP_TAC THEN FIRST_X_ASSUM (ASSUME_TAC o (UNDISCH o (SPEC `p:num`
))) );;
val it : goalstack = 1 subgoal (1 total)

  0 [`FACT n + 1 = k`]
  1 [`prime p`]
  2 [`p divides k`]
  3 [`p <= n`]

`F`

# e( ASM_MESON_TAC [DIVIDES_FACT_PRIME; COPRIME_PLUS1; coprime; prime] )
;;
0..0..0..2..5..18..41..78..solved at 103
val it : goalstack = No subgoals

miz3 へコンバートすると．．．

# miz3_of_hol "test.ml" "thm20130322_2";;
0..0..0..3..8..18..solved at 24
0..0..0..2..5..18..41..78..solved at 103
val it : step =
  ~(?n. !p. prime p ==> p <= n) [1]
  proof
    !n. (!p. prime p ==> p <= n) ==> F [2]
    proof
      let n be num;
      assume !p. prime p ==> p <= n [3];
      !k. FACT n + 1 = k ==> F [4]
      proof
        let k be num;
        assume FACT n + 1 = k [5];
        ?p. prime p /\ p divides k [6]
          by ASM_MESON_TAC [FACT_LE; ARITH_RULE (parse_term "1 <= f ==> ~(f + 1 = 1)"); PRIME_FACTOR],3,5;
        !p. p divides k ==> prime p ==> F [7]
        proof
          let p be num;
          assume p divides k [8];
          assume prime p [9];
          p <= n ==> F [10]
          proof
            assume p <= n [11];
          qed
            by ASM_MESON_TAC [DIVIDES_FACT_PRIME; COPRIME_PLUS1; coprime; prime],5,9,8,11;
        qed
          by FIRST_X_ASSUM (ASSUME_TAC o (UNDISCH o (SPEC (parse_term "p:num")))),3,5,9,8
          from 10;
        (?p. prime p /\ p divides k) ==> F [12] by STRIP_TAC,3,5 from 7;
      qed
        by SUBGOAL_THEN (parse_term "?p. prime p /\\ p divides k") MP_TAC,3,5
        from 6,12;
    qed by ABBREV_TAC (parse_term "k = FACT n + 1"),3 from 4;
  qed by STRIP_TAC from 1;