HOL proof

Top-level proof [] |- `prime 2` RW_TAC [[] |- `!a b. divides a b = ?c. b = a * c`, [] |- `!p. prime p = ~(p = 1) /\ !x. divides x p ==> (x = 1) \/ (x = p)`] THEN STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC) THEN CONJ_TAC THENL [PROVE_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`], STP_TAC `divides x 2` TRIVIAL PROVE_TAC [[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`] THEN PROVE_TAC [[] |- `!a b. divides a b = ?c. b = a * c`]] RW_TAC [[] |- `!a b. divides a b = ?c. b = a * c`, [] |- `!p. prime p = ~(p = 1) /\ !x. divides x p ==> (x = 1) \/ (x = p)`] THEN STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC) THEN CONJ_TAC THENL [PROVE_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`], STP_TAC `divides x 2` TRIVIAL PROVE_TAC [[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`] THEN PROVE_TAC [[] |- `!a b. divides a b = ?c. b = a * c`]] [] |- `prime 2` RW_TAC [[] |- `!a b. divides a b = ?c. b = a * c`, [] |- `!p. prime p = ~(p = 1) /\ !x. divides x p ==> (x = 1) \/ (x = p)`] [`2 = x * c`] |- `(x = 1) \/ (x = 2)` STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC) [`2 = x * c`] |- `~(x = 0) /\ x <= 2` CONJ_TAC [`2 = x * c`] |- `~(x = 0)` PROVE_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`] [`2 = x * c`] |- `x <= 2` STP_TAC `divides x 2` TRIVIAL PROVE_TAC [[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`] [`2 = x * c`] |- `divides x 2` PROVE_TAC [[] |- `!a b. divides a b = ?c. b = a * c`] PROVE_TAC [[] |- `!a b. divides a b = ?c. b = a * c`] [`2 = x * c`] |- `divides x 2` STP_TAC `divides x 2` TRIVIAL PROVE_TAC [[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`] [`2 = x * c`] |- `x <= 2` STP_TAC `divides x 2` [`2 = x * c`] |- `divides x 2 ==> x <= 2` PROVE_TAC [[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`] [`2 = x * c`] |- `divides x 2` STP_TAC `divides x 2` [`2 = x * c`] |- `x <= 2` MP [`2 = x * c`] |- `divides x 2 ==> x <= 2` [`2 = x * c`] |- `divides x 2` PROVE_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`] [`2 = x * c`] |- `~(x = 0)` REPEAT POP_ASSUM THEN CONV_TAC [] |- `(2 = x * c) ==> ~(x = 0)` ASM_MESON_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`] REPEAT POP_ASSUM THEN CONV_TAC [`2 = x * c`] |- `~(x = 0)` REPEAT POP_ASSUM [] |- `(2 = x * c) ==> ~(x = 0)` CONJ_TAC [`2 = x * c`] |- `~(x = 0) /\ x <= 2` CONJ [`2 = x * c`] |- `~(x = 0)` [`2 = x * c`] |- `x <= 2` STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` STP_TAC `~(x = 0) /\ x <= 2` [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` ALL_TAC THEN UNDISCH_TAC `2 = x * c` [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` CONV_TAC [`2 = x * c`] |- `~(x = 0) /\ x <= 2` CONV_TAC [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` EQ_MP [] |- `T = (2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` SYM [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2) = T` [] |- `T` ALL_TAC THEN UNDISCH_TAC `2 = x * c` [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` ALL_TAC [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` UNDISCH_TAC `2 = x * c` [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` UNDISCH_TAC `2 = x * c` [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` MP [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` [`2 = x * c`] |- `2 = x * c` ALL_TAC [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` UNDISCH_TAC `2 = x * c` [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` UNDISCH_TAC `2 = x * c` [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` MP [] |- `(2 = x * c) ==> ~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` [`2 = x * c`] |- `2 = x * c` STP_TAC `~(x = 0) /\ x <= 2` [`2 = x * c`] |- `(x = 1) \/ (x = 2)` MP [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` [`2 = x * c`] |- `~(x = 0) /\ x <= 2` RW_TAC [[] |- `!a b. divides a b = ?c. b = a * c`, [] |- `!p. prime p = ~(p = 1) /\ !x. divides x p ==> (x = 1) \/ (x = p)`] [] |- `prime 2` (((((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) THEN TRY NO_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` (((((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) THEN TRY NO_TAC [] |- `prime 2` ((((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC)) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` TRY NO_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` TRY NO_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` NO_TAC ORELSE ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` NO_TAC ORELSE ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC) [`2 = x * c`] |- `~(x = 0) /\ x <= 2` STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` STP_TAC `~(x = 0) /\ x <= 2` [`2 = x * c`] |- `~(x = 0) /\ x <= 2 ==> (x = 1) \/ (x = 2)` [`2 = x * c`] |- `~(x = 0) /\ x <= 2` ((((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC)) [] |- `prime 2` (((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic]) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC)) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC)) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` TRY (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` TRY (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) ORELSE ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC) THEN REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) ORELSE ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` TRY NO_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` (((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic]) [] |- `prime 2` ((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic]) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic]) [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` TRY (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` TRY (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) ORELSE ALL_TAC [`2 = x * c`] |- `(x = 1) \/ (x = 2)` (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) ORELSE ALL_TAC [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic]) [`2 = x * c`] |- `(x = 1) \/ (x = 2)` ((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) [] |- `prime 2` (REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) ORELSE ALL_TAC [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) ORELSE ALL_TAC [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` ALL_TAC [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` (REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC [] |- `prime 2` REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC [] |- `prime 2` CONV_TAC [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` CONV_TAC [] |- `prime 2` EQ_MP [] |- `(!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)) = prime 2` [] |- `!x. (?c. 2 = x * c) ==> (x = 1) \/ (x = 2)` REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC [] |- `prime 2` REPEAT (GEN_TAC ORELSE CONJ_TAC) [] |- `prime 2` REPEAT NO_TAC [] |- `prime 2` REPEAT (GEN_TAC ORELSE CONJ_TAC) [] |- `prime 2` TRY ((GEN_TAC ORELSE CONJ_TAC) THEN REPEAT (GEN_TAC ORELSE CONJ_TAC)) [] |- `prime 2`